Model checking with Auto FOCUS 3

Introduction

New in 2.9.0! AF3 now supports nuXmv!

AF3 provides a deep integration of the NuSMV model checker, and of its successor nuXmv, with the following features: Note: Integration of NuSMV/nuXmv is undergoing a lot of refactorings in order to support more features; planned for AF3 2.10!

Installing NuSMV or nuXmv

To use the model checking functionality of AF3, you need to install the NuSMV model checker or its successor nuXmv. You only have to make sure that either of these software is in the PATH. To check whether AF3 can access the model checker, just press the "NuSMV/nuXmv Version" button from the "Semantic Inspector View". If correctly installed, a dialog showing the version will be displayed (as below), otherwise an error message will be displayed.


NuSMV version

Using the "Semantic Inspector"