ProB Documentation - User contributions [en]

Download

2010-03-05T09:29:37Z

Ingo Weigelt:

== Latest Release ==

Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.

{| border="1"
! Platform
! Release Date
! Download
! Dependencies
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.2-beta
|-
| Linux
| 03.03.2010 11.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux.tar.gz Tarball],
[http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/prob_1.3.2beta3_i386.deb Ubuntu / Debian package]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 03.03.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_Win.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 03.03.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_snowleopard.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 19.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_leopard_intel.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]

|-
| Mac OS X, Tiger, Intel
| 11.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_tiger_intel.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.4],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.1final
|-
| Mac OS X, Snow Leopard
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-snowleopard-1.3.1final5.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5 (for Leopard)],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Linux
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-linux-1.3.1final5.tar.gz Tarball]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-win-1.3.1final5.zip Zipfile]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, PPC Tiger
| 07.12.2009
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final3/ProB-ppctiger-1.3.1final3.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}

== Earlier Releases ==

If you are interested in earlier releases, please have a look at the [http://www.stups.uni-duesseldorf.de/ProB_Releases/ Download directory].

Download

2010-03-05T09:28:58Z

Ingo Weigelt: fixed broken links

== Latest Release ==

Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.

{| border="1"
! Platform
! Release Date
! Download
! Dependencies
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.2-beta
|-
| Linux
| 03.03.2010 11.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux.tar.gz Tarball],
[http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/prob_1.3.2beta3_i386.deb Ubuntu / Debian package]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 03.03.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_Win.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 03.03.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_snowleopard.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 19.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ ProB_leopard_intel.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]

|-
| Mac OS X, Tiger, Intel
| 11.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_tiger_intel.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.4],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.1final
|-
| Mac OS X, Snow Leopard
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-snowleopard-1.3.1final5.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5 (for Leopard)],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Linux
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-linux-1.3.1final5.tar.gz Tarball]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-win-1.3.1final5.zip Zipfile]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, PPC Tiger
| 07.12.2009
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final3/ProB-ppctiger-1.3.1final3.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}

== Earlier Releases ==

If you are interested in earlier releases, please have a look at the [http://www.stups.uni-duesseldorf.de/ProB_Releases/ Download directory].

Download

2010-03-05T09:26:23Z

Ingo Weigelt: fixed broken link

== Latest Release ==

Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.

{| border="1"
! Platform
! Release Date
! Download
! Dependencies
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.2-beta
|-
| Linux
| 03.03.2010 11.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_linux.tar.gz Tarball],
[http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/prob_1.3.2beta3_i386.deb Ubuntu / Debian package]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 03.03.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_Win.zip Zipfile (with probcli)]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, Snow Leopard, Intel
| 03.03.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_snowleopard.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Mac OS X, Leopard, Intel
| 19.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_leopard.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]

|-
| Mac OS X, Tiger, Intel
| 11.02.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.2/ProB_tigerd.tar.gz Tarball]
| [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.4],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.3.1final
|-
| Mac OS X, Snow Leopard
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-snowleopard-1.3.1final5.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5 (for Leopard)],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|-
| Linux
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-linux-1.3.1final5.tar.gz Tarball]
| Java Runtime Environment (5.0 or newer), Tcl/Tk 8.4
|-
| Windows
| 13.01.2010
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final5/ProB-win-1.3.1final5.zip Zipfile]
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk 8.4 for Windows],
[http://java.com/en/ Java Runtime Environment (5.0 or newer)]
|-
| Mac OS X, PPC Tiger
| 07.12.2009
| [http://www.stups.uni-duesseldorf.de/ProB_Releases/1.3.1final3/ProB-ppctiger-1.3.1final3.tar.gz Tarball]
| [http://www.tcl.tk/software/tcltk/8.5.html Tcl/TK 8.5],
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}

== Earlier Releases ==

If you are interested in earlier releases, please have a look at the [http://www.stups.uni-duesseldorf.de/ProB_Releases/ Download directory].

Tutorial First Model Checking

2010-01-22T11:23:22Z

Ingo Weigelt: fixed link to Tutorial First Step

[[Category:User Manual]]

We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Step]]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.

== Simple Model Checking ==

The model checker can be used to systematically execute the operations and tries to find an erroneous state (e.g., where the invariant is violated).
Select the "Model Check..." command in the "Verify" menu:
[[file:ProBWinModelCheckCommand.png|center]]
This brings up the following dialog box:
[[file:ProBWinModelCheckDialog.png|center]]
Now click the "Model Check" button. After a short while, ProB will give you the following error message:
[[file:ProBWinModelCheckCounterExampleFound.png|center]]

The lower half of the ProB window should now look as follows:

[[file:ProB_LiftAfterModelCheck.png|center||700px]]

The red "'''KO'''" button in the "State Properties" pane tells us that the model checker has moved us into a state where the invariant is violated. Indeed, the <tt>floor</tt> variable has taken up a negative value, while the invariant requires floor to be between 0 and 99.
The "History" pane tells us the sequence of operations that has led to this error.
(Note that this sequence is not necessarily the shortest sequence that leads to an error or to this error. However, by selecting "Breadth First" in the model check dialog above, one can ensure that the shortest paths are found.)

== Coverage Statistics ==

We can obtain some statistics about how many states ProB has explored by selecting the "Compute Coverage" command in the "Analyse" menu:

[[file:ProB_LiftAfterModelCheck_Coverage.png|center]]

In the NODES section we can see that ProB has explored a total of 11 nodes (i.e., states of the B machine).
None of these nodes are deadlocked, in the sense that no operations are applicable.
We can also see that for one node the invariant is violated.
Of these 11 nodes, 2 are '''open''', meaning that they have not been explored in the sense that:
* the invariant has not been evaluated
* the enabled operations have not been computed.
As such, an open node may contain an invariant violation and/or could be a deadlocking node.
A live node, is a node which is not deadlocked and not open.

We can also see, that all in all there are 17 transitions among these 11 nodes. A transition is either an operation or an initialisation (there can be one more transition, which we will examine later in the tutorial).

In the COVERED_OPERATIONS section, we can see more details about these transitions: we have one initialisation, 8 <tt>inc</tt> operations and 8 <tt>dec</tt> operations.

== View Statespace ==

We can obtain a graphical visualization of the state space explored by ProB.
For this, be sure that you have correctly [[Graphical Viewer|installed and setup the graphical viewer as desribed in the user manual]].
Now, choose the "View Statespace" command in the "Animate" menu:

[[file:ProB_LiftAfterModelCheck_Statespace.png|center]]

We can now see the 11 nodes. The two open nodes are marked in red. You can also see that there is a virtual root node (the inverted triangle at the top), representing the "state" of the machine before initialisation. The current node is depicted by the blue hexagon in the right hand corner.

Note: you can influence the colouring and shapes used by ProB, by selecting "Graphical Viewer Preferences..." in the "Preferences" menu.

[[file:ProB_GraphicalViewerPreferences_Shapes.png|center]]

You can obtain more information about the state space visualisation in the user manual: [[State Space Visualization]].