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 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:

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.

probcli Basics

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

%./probcli

ProB Command Line Interface
  VERSION 1.3.3-final3 ($Rev: 7316 $)
  $LastChangedDate: 2011-03-09 17:14:00 +0100 (Mi, 09 Mrz 2011) $
  Prolog: SICStus 4.1.3 (x86-win32-nt-4): Wed Sep 22 21:41:09 WEDT 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
     --timeout N  Timeout in ms for model checking and refinement checking
     -t           trace check (associated .trace file must exist)
     -init        initialise specification
     -cbc OPNAME  constraint-based invariant checking for an operation (also use OPNAME=all)
     -cbc_deadlock constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
     -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
     -eval        start interactive read-eval-loop
     -c           print coverage statistics
     -cc Nr Nr    print and check coverage statistics
     -statistics  print memory and other statistics at the end
     -p PREF Val  set Preference to Value
     -card GS Val set scope of B deferred set
     -goal "PRED" set GOAL predicate for model checker
     -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
     -pp FILE     pretty-print internal representation to file
     -ppf FILE    pretty-print internal representation to file, force printing of all type infos
     -v           verbose
     -version     print version information
     -assertions  check ASSERTIONS
     -properties  check PROPERTIES
     -rc          runtime checking of types/pre-/post-conditions
     -ltlfile F   check LTL formulas in file F
     -ltlassertions check LTL assertions (in DEFINITIONS)
     -ltllimit L  explore at most L states when model-checking LTL
     -save File   save state space for later refinement check
     -refchk File refinement check against previous saved state space
     -mcm_tests Depth MaxStates EndPredicate File generate test cases with maximum length Depth, explore maximally MaxStates, the last state satisfies EndPredicate and the test cases are written to File
     -mcm_cover Operation When generating MCM test cases, Operation should be covered
     -spdot File  Write graph of the state space to a dot file.
 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 : nat ==> Max Number of Initialisations Computed
     MAX_OPERATIONS : nat ==> Max Number of Enablings per Operation Computed
     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 and set comprehensions
     CLPFD : bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit machines)
     SMT : bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates)
     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
     ALLOW_INCOMPLETE_SETUP_CONSTANTS : bool ==> Allow ProB to proceed even if only part of the CONSTANTS have been found.
     PARTITION_PROPERTIES : bool ==> Partition predicates (PROPERTIES) into components
     USE_RECORD_CONSTRUCTION : bool ==> Records: Check if axioms/properties describe a record pattern
     OPERATION_REUSE : bool ==> Try and reuse previously computed operation effects in B/Event-B
     SHOW_EVENTB_ANY_VALUES : bool ==> Show top-level ANY variable values of B Operations without parameters as parameters
     RANDOMISE_OPERATION_ORDER : bool ==> Randomise order of operations when computing successor states
     EXPAND_FORALL_UPTO : nat ==> When analysing predicates: max. domain size for expansion of forall:
     ABSTRACT_DOMAIN_MODULE : string ==> Module name with abstract domain and operations
     USE_WIDENING : bool ==> Use widening for abstract interpretation
     SOFT_WIDENING : bool ==> Use soft widening for every transition
     HOW_MANY_STATES_FOR_WIDEN : nat1 ==> Extrapolation threshold (Number of loop iterations until widening will be used)
     WARN_WHEN_EXPANDING_INFINITE_CLOSURES : int ==> Warn when expanding infinite closures if MAXINT larger than:
     WARN_IF_DEFINITION_HIDES_VARIABLE : bool ==> Warn if a DEFINITION hides a variable with the same name
     TRACE_INFO : bool ==> Provide various tracing information on the terminal/console.
     DOUBLE_EVALUATION : bool ==> Evaluate PREDICATES positively and negativelywhen analysing:
     RECURSIVE : bool ==> Lazy expansion of *Recursive* set Comprehensions and lambdas
     IGNORE_HASH_COLLISIONS : bool ==> Ignore Hash Collisions (if true not all states may be computed, visited states are not memorised !)
     FORGET_STATE_SPACE : bool ==> Do not remember state space (mainly useful in conjunction with Ignore Hash Collisions)
 More info at: http://www.stups.uni-duesseldorf.de/ProB/

Options

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