Introduction
AF3 provides a deep integration of the NuSMV model checker, and of its successor nuXmv,
with the following features:
- user proximity: AF3 brings model checker closer to its users. Model checking with
AF3 is easy to understand, easy to learn, simple and efficient to use.
- easy to specify properties: AF users can work at the abstraction level of AF3 models.
- analyses results are easy to interpret. Counter-examples can be simulated in AF3 such that
the users gain an immediate feedback about the causes that brought the property violation.
Prerequisite: NuSMV/nuXmv
First ensure that nuXmv or NuSMV is installed: see External Tools for instructions.
Activation
You need to ensure that the reachability check is activated:
- Double click on the root of your project:
- And check "All states are reachable":
Be sure also that the configuration in which this check is activated is the one which is the "current objective".
This will trigger the check that all state automata of the project have 100% state coverage
and activate the automatic trigger of this check for every state automaton that you might
add later on to your project. It will also trigger a check for every state automaton as soon
as it is modified.
Example
Open the simple traffic light example and double-click on the Controller component.
Open the V&V dashboard tab below the editor and add a specification as follows:
You shall see that the check has automatically been run (and in this case provides a successful result).
In case of failure:
Double-clicking the status message will start a simulation demonstrating the coutner-example.