Help

Using the Command-Line Version of ProB: Difference between revisions

No edit summary
No edit summary
Line 9: Line 9:


{| cellpadding="10"
{| cellpadding="10"
| valign="top" | <<replaceme>>
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing << >>
| All values that should be replaced with some value are shown withing < >
|-
|-
| valign="top" | line breaks
| valign="top" | line breaks
Line 35: Line 35:
== Options ==
== Options ==


=== -mc <<nr>> ===
=== -mc <nr> ===


'''Description'''
'''Description'''


{| style="color:black; background-color:#FFFFDF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
{| style="color:black; background-color:#FFFFDF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <<nr>> states
| model check; checking at most <nr> states
|}
|}


Line 47: Line 47:
  probcli -mc 5
  probcli -mc 5


=== -no<<xxx>> ===
=== -no<x> ===


'''Description'''
'''Description'''


{| style="color:black; background-color:#FFFFDF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
{| style="color:black; background-color:#FFFFDF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| <<xxx>>=dead,inv,goal,ass (for model check)
| <x>=dead,inv,goal,ass (for model check)
|}
|}


Revision as of 08:35, 6 May 2011


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.

Conventions used

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.

Synopsis

Command-line Arguments for ProB Tcl/Tk

Note that the stand-alone Tcl/Tk version also supports a limited form of command-line preferences:

  • FILE (the name/path of the file to be loaded)
  • -prefs PREF_FILE (to use a specific preferences file, rather than the default ProB_Preferences.pl in your home folder)
  • -batch (to instruct ProB not to try to bring up windows, but to print information only to the terminal)
  • -selfcheck (to run the standard unit tests)
  • -t (to perform the Trace Check on the default trace file associated with the specification)
  • -tcl TCL_Command (to run a particular pre-defined Tcl command)
  • -mc (to perform model checking)
  • -c (to compute the coverage)
  • -ref (to perform the default trace refinment check)

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.

Options

-mc <nr>

Description

model check; checking at most <nr> states

Example 

probcli -mc 5

-no<x>

Description

<x>=dead,inv,goal,ass (for model check)

Example 

probcli -noinv


Some probcli examples

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
Retrieved from "https://prob.hhu.de/w/index.php?title=Using_the_Command-Line_Version_of_ProB&oldid=1009"