Non-Determinism

Prerequisite: NuSMV/nuXmv

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

Activation

You need to ensure that the non-determinism check is activated:
  1. Double click on the root of your project:


  2. And check "All state automata are deterministic":


  3. You will probably observe the following message:


    This informs you that the determinism 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 are deterministic 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

It is obviously non-deterministic since when the Input is equal to 5, both transitions can be taken. Therefore, you should see, as soon after you finished drawing this automaton (and specifying the guards 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, highlight the transitions which are overlapping, and provide information about the case(s) which is yielding the overlap:


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

You can also check the status of the check at any time by simply clicking on the "V&V Dashboard" tab of the state automaton editor:


Which of course shows the corresponding information in case of error:


Pressing the button "More..." provides the same information as the context menu above.