Line 691: | Line 691: | ||
<pre> | <pre> | ||
probcli -p IGNORE_HASH_COLLISIONS FALSE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -mc 999999 M.mch | probcli -p IGNORE_HASH_COLLISIONS FALSE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -mc 999999 M.mch | ||
</pre | </pre> |
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 ...
Generate test cases for the given specification. Each test case consists of a sequence of operations resp. events (a so-called trace) that
The user can specify what requested operations/events are with the option -mcm_cover.
ProB uses a "breadth-first" approach to search for test cases. When all requested operations/events are covered by test cases within maximum length M, the algorithm will explore the complete state space with that maximum distance M from the initialisation. It outputs all found traces that satisfy the requirements above.
The algorithm stops if either
The required parameters are:
Example
probcli my.mch -mcm_tests 10 2000 "EndStateVar=TRUE" testcases.xml -mcm_cover op1,op2
generates test cases for the operations op1 and op2 of the specification my.mch. The maximum length of traces is 10, at most 2000 states are explored. Each test case ends in a state where the predicate EndStateVar=TRUE holds. The found test cases are written to a file testcases.xml.
Specify an operation or event that should be covered when generating test cases with the -mcm_test option. Multiple operations/events can be specified by seperating them by comma or by using -mcm_cover several times.
See -mcm-tests for further details.
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
To model check a specification M.mch while trying to minimize memory consumption (and accepting hash collisions) do:
probcli -p IGNORE_HASH_COLLISIONS FALSE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -mc 999999 M.mch