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. |
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.
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/
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