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 ...
Description
restrict errors reported by model checking with <x>=dead,inv,goal,ass
-nodead : do not report deadlocks -noinv : do not report invariant violations -nogoal : do not stop if a state satisfying the GOAL predicate has been found -noass : do not report assertion violations |
Example
probcli my.mch -mc 1000 -nodead -nogoal
Description
proceed breadth-first |
Example
probcli my.mch -bf -mc 1000
Description
proceed depth-first |
Example
probcli my.mch -df -mc 1000
Description
Global imeout in ms for model checking and refinement checking.
This does not influence the timeout used for computing individual transitions/operations. This has to be set with the -p TIME_OUT <N>. See the description of the -p option. |
Example
probcli my.mch -timeout 10000
Description
trace check (associated .trace file must exist) |
Example
probcli my.mch -t
Description
initialise specification |
Example
probcli my.mch -init nr_of_components(1) % checking_component_properties(1,[]) % enumerating_constants_without_constraints([typedval(fd(_24428,ID),global(ID),iv)]) % grounding_wait_flags grounding_component(1) grounding_component(2) % found_enumeration_of_constants(0,2) % backtrack(found_enumeration_of_constants(0,2)) % found_enumeration_of_constants(0,1) % backtrack(found_enumeration_of_constants(0,1)) <- 0: SETUP_CONSTANTS :: root % Could not set up constants with parameters from trace file. % Will attempt any possible initialisation of constants. | 0: SETUP_CONSTANTS success -->0 - <- 1: INITIALISATION :: 0 % Could not initialise with parameters from trace file. % Will attempt any possible initialisation. ALL OPERATIONS COVERED - | 1: INITIALISATION success -->2 - - SUCCESS
Description
constraint-based invariant checking for an operation (also use <OPNAME>=all) |
Example
probcli my.mch -cbc all
Description
constraint-based deadlock checking (also use -cbc_deadlock_pred PRED) |
Description
Example
probcli my.mch -cbc_deadlock_pred "n=15"
Description
raise error if mc finds counter example or trace checking fails |
Example
probcli my.mch -t -strict
Description
expect error to occur (<ERR>=cbc,mc,ltl,...)
Tell ProB that you expect a certain error to occur. Mainly useful for regression tests (in conjunction with the -strict option). |
Example
probcli examples/B/Benchmarks/CarlaTravelAgencyErr.mch -mc 1000 -expcterr invariant_violation -strict
Description
interactive animation |
Example
probcli my.mch -i
Description
start interactive read-eval-loop |
Example
probcli my.mch -p CLPFD TRUE -eval
Description
print coverage statistics |
Example
probcli my.mch -mc 1000 -c
Description
print and check coverage statistics
Print coverage statistics and check that the given number of nodes and transitions have been computed. |
Example
probcli my.mch -mc 1000 -cc 10 25
Description
Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at Preferences |
Example
probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000
Description
set scope of B deferred set |
Example
probcli my.mch ...
Description
set GOAL predicate for model checker |
Example
probcli my.mch -mc 10000000 -goal "n=18" -strict -expcterr goal_found
Description
start socket server on given port |
Example
probcli my.mch ...
Description
start socket server on port 9000 |
Example
probcli my.mch ...
Description
start socket server on some free port |
Example
probcli my.mch ...
Description
log activities in <LogFile> |
Example
probcli my.mch -mc 1000 -l my.log
Description
log activities in /tmp/prob_cli_debug.log |
Example
probcli my.mch -mc 1000 -ll
Description
analyse <LogFile> using gnuplot |
Example
probcli my.mch ...
Description
pretty-print internal representation to <FILE> |
Example
probcli my.mch -pp my_pp.mch
Description
pretty-print internal representation to <FILE>, force printing of all type infos |
Example
probcli my.mch -ppf my_ppf.mch
Description
set ProB into verbose mode |
Example
probcli my.mch -mc 1000 -v
Description
print version information |
Example
probcli -version 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
Description
check ASSERTIONS
Note: you should probably first initialise the machine (e.g., with -init). |
Example
probcli my.mch -init -assertions
Description
check PROPERTIES
Note: you should probably first initialise the machine (e.g., with -init). If the constants have not yet been set up, probcli will debug the properties. |
Example
probcli my.mch -init -properties
Description
runtime checking of types/pre-/post-conditions |
Example
probcli my.mch ...
Description
check LTL formulas in file <FILE> |
Example
probcli my.mch ...
Description
check LTL assertions (in DEFINITIONS) |
Example
probcli my.mch ...
Description
explore at most <LIMIT> states when model-checking LTL |
Example
probcli my.mch ...
Description
save state space for later refinement check |
Example
probcli my.mch ...
Description
refinement check against previous saved state space |
Example
probcli my.mch ...
Description
generate test cases with maximum length <Depth>, explore maximally <MaxStates>, the last state satisfies <EndPredicate> and the test cases are written to <FILE> |
Example
probcli my.mch ...
Description
Operation When generating MCM test cases, Operation should be covered |
Example
probcli my.mch ...
Description
Write graph of the state space to a dot <FILE> |
Example
probcli my.mch ...
You can use these preferences within the command:
-p <PREFERENCE> <VALUE>
<PREFERENCE> | <VALUE> |
---|---|
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 computers) |
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: |
TRACE_INFO | bool ==> Provide various tracing information on the terminal/console. |
DOUBLE_EVALUATION | bool ==> Evaluate PREDICATES positively and negatively when 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) |
Example
probcli my.mch -p TIME_OUT 5000 -p CLPFD TRUE -p SYMMETRY_MODE hash -mc 1000
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