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

The command-line version of ProB offers many of the feature of the standalone Tcl/Tk Version, but via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.

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 as such also be run on systems without Tcl/Tk.

probcli Basics

Typing probcli will give you a help printout, describing most of the functions:

%./probcli

ProB Command Line Interface
  VERSION 1.3.1-final6 ($Rev: 4187 $)
  $LastChangedDate: 2010-01-15 12:47:38 +0100 (Fri, 15 Jan 2010) $
Usage: probcli FILE [OPTIONS]
  OPTIONS are: 
     -mc Nr       model check; checking at most Nr states
     -noXXX       XXX=dead,inv,goal,ass (for model check)
     -bf          proceed breadth-first
     -df          proceed depth-first
     -t           trace check (associated .trace file must exist)
     -init        initialise specification
     -cbc         constraint based checking of all operations
     -strict      raise error if mc finds counter example or trace checking fails
     -expcterr ERR expect error to occur (ERR=cbc,mc,ltl,...)
     -i           interactive animation
     -c           print coverage statistics
     -cc Nr Nr    print and check coverage statistics
     -p PREF Val  set Preference to Value
     -s Port      start socket server on given port
     -ss          start socket server on port 9000
     -sf          start socket server on some free port
     -l LogFile   log activities in LogFile
     -ll          log activities in /tmp/prob_cli_debug.log
     -lg LogFile  analyse logfile using gnuplot
     -v           verbose
     -version     print version information
     -assertions  check ASSERTIONS
     -rc          runtime checking of types/pre-/post-conditions
     -ltlfile F   check LTL formulas in file F
     -ltlassertions check LTL assertions (in DEFINITIONS)
     -save File   save state space for later refinement check
     -refchk File refinement check against previous saved state space
 FILE extensions are: 
      .mch         for B abstract machines
      .ref         for B refinement machines
      .imp         for B implementation machines
      .csp, .cspm  for CSP-M files, same format as FDR
      .eventb      for Event-B packages exported from Rodin ProB Plugin
 Preferences PREF are: 
     MAXINT : nat ==> MaxInt, used for expressions such as xx::NAT (2147483647 for 4 byte ints)
     MININT : neg ==> MinInt, used for expressions such as xx::INT (-2147483648 for 4 byte ints)
     DEFAULT_SETSIZE : nat ==> Size of unspecified deferred sets in SETS section
     MAX_INITIALISATIONS : nat1 ==> Max Number of Initialisations Computed
     MAX_OPERATIONS : nat ==> Max Number of Enablings per Operation Computed
     SHOW_EVENTB_ANY_VALUES : bool ==> Show top-level ANY variable values of Event B Events as operation parameters
     ANIMATE_SKIP_OPERATIONS : bool ==> Animate operations which are skip or PRE C THEN skip
     EXPAND_CLOSURES_FOR_STATE : bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments
     SYMBOLIC : bool ==> Lazy expansion of lambdas & set comprehensions
     RECURSIVE : bool ==> Lazy expansion of *Recursive* set Comprehensions and lambdas
     STATIC_ORDERING : bool ==> Use static ordering to enumerate constants which occur in most PROPERTIES first
     SYMMETRY_MODE : [off,flood,nauty,hash] ==> Symmetry Mode: off,flood,canon,nauty,hash
     TIME_OUT : nat1 ==> Time out for computing enabled transitions (in ms)
     USE_PO : bool ==> Restrict invariant checking to affected clauses. Also remove clauses that are proven (EventB)
     TRY_FIND_ABORT : bool ==> Try more aggressively to detect ill-defined expressions (e.g. applying function outside of domain), may slow down animator
     NUMBER_OF_ANIMATED_ABSTRACTIONS : nat ==> How many levels of refined models are animated by default
 More info at: http://www.stups.uni-duesseldorf.de/ProB/

Some probcli examples

To load a file My.mch, setup the constants and initialise it do:

probcli -init My.mch

To load a file M.mch, setup the constants and initialise and then check all assertions - all this 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