The Analyses Master View
Introduction
AF3 provides a deep integration of the Yices SMT
solver and of the NuSMV model checker. Based on these tools,
can be performed the following analyzes:
Installing YICES
To use the Analyses Master functionality in AF3, firstly we have to install the
Yices SMT solver. You only have to make sure that Yices is in the PATH. To check whether
AF3 can access Yices, just press the "Yices Version" button from the
"Assume Guarantee Reasoning View". If Yices is correctly installed, a dialog showing its version
is displayed (as below), otherwise an error message will be displayed.
Installing NuSMV
Also, you have to install NuSMV model checker. Like for Yices, you only have to make sure that NuSMV is
in the PATH. To check whether AF3 can access NuSMV, just press the "NuSMV Version" button from the
"Analyses Master View". If NuSMV is correctly installed, a dialog showing its version
is displayed (as below), otherwise an error message will be displayed.
Using the "Master Analyzer"
- Step 1 - Open the "Analyses Master" view by clicking on the button from the toolbar.
- Step 2 - Select a component or a component architecture and press the button :"Perform all analyses for the
selected component". (If no component/component architecture is selected, an error message will be displayed).
- Step 3 - Optional: modify the total timeout or the timeout/analysis by changing the default values.
- Step 4 - The results are displayed in the table (as below). For each analysis, are mentioned the type,
the analyzed component, the result state and the execution time. By clicking on one of this results, the analyzed system is
opened in the editor and the analyzed component is highlighted (with red).