Select Git revision
mode_automaton.html
non_determinism_analysis.html 3.58 KiB
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<!--
Documentation of the Non-Determinism Analysis.
@author becker
@ConQAT.Rating GREEN Hash: DF4DAA0F959EC4C132440CD3D10FDB19
-->
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<title>Non-Determinism Check</title>
</head>
<body>
<h2><u><font color="#336699">Non-Determinism</font></u></h2>
<font color="#000000" style="font-family:Verdana, Geneva, sans-serif" size="2px">
<h3><font color="#336699">Prerequisite: NuSMV/nuXmv</font></h3>
First ensure that nuXmv or NuSMV is installed: see <a href="external_tools.html">External Tools</a> for instructions.
<h3><font color="#336699">Activation</font></h3>
You need to ensure that the non-determinism check is activated:
<ol>
<li>Double click on the root of your project:
<br>
<img src="./pictures/clickOnRoot.png" border="1" />
<br>
<br></li>
<li>And check "All state automata are deterministic":
<br>
<img src="./pictures/determinism.png" border="1" />
<br>
<br>
<li>You will probably observe the following message:
<br>
<img src="./pictures/timeConsuming.png" border="1" />
<br>
<br>
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.
</ol>
Be sure also that the configuration in which this check is activated is the one which is the "current objective".
<p>
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.
<h3><font color="#336699">Example</font></h3>
Consider the following state automaton:
<br>
<img src="./pictures/determinismStateAutomaton.png" alt="State automaton" border="1" />
<br>
<br>
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:
<br>
<img src="./pictures/determinismModelNavigator.png" border="1" />
<br>
<br>
As well as is in the editor of the containing component:
<br>
<img src="./pictures/determinismEditor.png" border="1" />
<br>
<br>
If you right-click on the error in the model navigator or in the editor, the following context menu will be shown:
<br>
<img src="./pictures/determinismContextMenu.png" border="1" />
<br>
<br>
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:
<br>
<img src="./pictures/determinismInfo.png" border="1" />
<br>
<br>
If you fix the non-determinism by, say, changing the transition "Input >= 5" to "Input > 5", then the error will automatically disappear.
<p>
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:
<br>
<img src="./pictures/determinismDashboard.png" border="1" />
<br>
<br>
Which of course shows the corresponding information in case of error:
<br>
<img src="./pictures/determinismInfoFail.png" border="1" />
<br>
<br>
Pressing the button "More..." provides the same information as the context menu above.
</font>
</body>
</html>