Reachability Analysis

Prerequisite: NuSMV/nuXmv

First ensure that nuXmv or NuSMV is installed: see External Tools for instructions.

Activation

You need to ensure that the reachability analysis is activated:
  1. Double click on the root of your project:


  2. And check "All states are reachable":


  3. You will probably observe the following message:


    This informs you that the reachability analysis will be now run on all the state automata in the current project and that this might therefore take some resources (if your project already contains lots of state automata). This will be however done only once since, once the check is activated, it is only re-run for the state automata which are modified.
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

Consider the following state automaton:
State automaton

State "State" is obviously non-reachable since the guard can never be satisfied: one cannot have Input >= 5 and Input < 5 at the same time. Therefore, you should see, as soon after you finished drawing this automaton (and specifying the guard accordingly) an error message on the corresponding component in the model navigator:


As well as is in the editor of the containing component:


If you right-click on the error in the model navigator or in the editor, the following context menu will be shown:


Clicking on the entry will open the state automaton editor and highlight the state which is not reachable:


If you fix the guard by, say, changing the transition to "Input >= 5" only, then the error will automatically disappear.

You can also check the status of the check at any time, whether it is successful or not, by simply clicking on the "V&V Dashboard" tab of the state automaton editor:


Pressing the button "More..." provides simulations for every state allowing to check that it is indeed reachable.