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"