Tutorial Troubleshooting the Setup: Difference between revisions
No edit summary |
No edit summary |
||
| Line 17: | Line 17: | ||
ProB should now popup the following message: | ProB should now popup the following message: | ||
[[file:ProB_Jukebox_UnsatProp.png|center | [[file:ProB_Jukebox_UnsatProp.png|center]] | ||
If you click "Yes" (or Ja), you will get the following window: | If you click "Yes" (or Ja), you will get the following window: | ||
[[file:ProB_Jukebox_DebugUnsatProp.png|center | [[file:ProB_Jukebox_DebugUnsatProp.png|center]] | ||
What ProB does is add conjuncts from the PROPERTIES (and CONSTRAINTS clause) one-by-one, until it can no longer find a solution. This can often give you an indication of what is wrong, and where the trouble (or inconsistency) stems from. | What ProB does is add conjuncts from the PROPERTIES (and CONSTRAINTS clause) one-by-one, until it can no longer find a solution. This can often give you an indication of what is wrong, and where the trouble (or inconsistency) stems from. | ||
| Line 29: | Line 29: | ||
[[file:ProB_Jukebox_AnalyseGraphicallyCommand.png|center | [[file:ProB_Jukebox_AnalyseGraphicallyCommand.png|center]] | ||
This will result in the following visualisation: | This will result in the following visualisation: | ||
[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png|center | [[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png|center]] | ||
Revision as of 16:47, 18 January 2010
We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in Tutorial Setup Phases.
In this lesson, we examine what can go wrong in these phases and how one can find a solution. Indeed, setting up the constants and initial values of a machine is often the most difficult step for an animator. Unfortunately, it is also the very first step an animator has to perform.
First, open the machine "Jukebox.mch" which can be found in the SchneiderBook/Jukebox_Chapter13 subdirectory of the ProB Examples folder.
The main ProB window should look more or less as follows:
Now edit the file, and type & limit>99 after PROPERTIES limit:NAT1.
Save the machine and reload it. Hint: there is a "Save and reopen" command in the "File" menu for this action.
ProB should now popup the following message:
If you click "Yes" (or Ja), you will get the following window:
What ProB does is add conjuncts from the PROPERTIES (and CONSTRAINTS clause) one-by-one, until it can no longer find a solution. This can often give you an indication of what is wrong, and where the trouble (or inconsistency) stems from.
An alternate means to figure out the source of the problem is ProB's graphical formula viewer. For this, choose the "Analyse Graphically"...
This will result in the following visualisation:
