No edit summary |
No edit summary |
||
Line 48: | Line 48: | ||
Example | Example | ||
probcli -mc 5 | probcli my.mch -mc 5 | ||
=== -no<x> === | === -no<x> === | ||
Line 60: | Line 60: | ||
Example | Example | ||
probcli -noinv | probcli my.mch -noinv | ||
The command-line version of ProB offers many of the feature of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
The following conventions are used in this guide:
<replaceme> | All values that should be replaced with some value are shown withing < > |
line breaks | Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line. |
probcli [--help] <filename> [ <options> ]
Note that the stand-alone Tcl/Tk version also supports a limited form of command-line preferences:
However, the comand-line version of ProB, called probcli, provides more features. It also does not depend on Tcl/Tk and can therefore be run on systems without Tcl/Tk.
Description
model check; checking at most <nr> states |
Example
probcli my.mch -mc 5
Description
<x>=dead,inv,goal,ass (for model check) |
Example
probcli my.mch -noinv
To load a file My.mch, setup the constants and initialize it do:
probcli -init My.mch
To load a file M.mch, setup the constants, initialize and then check all assertions with Atelier-B's default values for MININT and MAXINT and an increased timeout of 5 seconds do:
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch