No edit summary |
|||
Line 520: | Line 520: | ||
== Preferences == | == Preferences == | ||
{| | {| cellpadding="5" cellspacing="1" width="100%" border="1" | ||
| <PREF> | Typ | !style="background-color:lightgrey;" | <PREF> | ||
!style="background-color:lightgrey;" | Typ | |||
|- | |- | ||
| MAXINT | nat ==> MaxInt | | 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: | |||
|- | |||
| 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) | |||
|} | |} | ||
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
<x>=dead,inv,goal,ass (for model check) |
Example
probcli my.mch ...
Description
proceed breadth-first |
Example
probcli my.mch ...
Description
proceed depth-first |
Example
probcli my.mch ...
Description
Timeout in ms for model checking and refinement checking |
Example
probcli my.mch ...
Description
trace check (associated .trace file must exist) |
Example
probcli my.mch ...
Description
initialise specification |
Example
probcli my.mch -init
Description
constraint-based invariant checking for an operation (also use <OPNAME>=all) |
Example
probcli my.mch ...
Description
constraint-based deadlock checking (also use -cbc_deadlock_pred PRED) |
Description
Example
probcli my.mch ...
Description
raise error if mc finds counter example or trace checking fails |
Example
probcli my.mch ...
Description
expect error to occur (<ERR>=cbc,mc,ltl,...) |
Example
probcli my.mch ...
Description
interactive animation |
Example
probcli my.mch ...
Description
start interactive read-eval-loop |
Example
probcli my.mch ...
Description
print coverage statistics |
Example
probcli my.mch ...
Description
print and check coverage statistics |
Example
probcli my.mch ...
Description
set Preference to Value |
Example
probcli my.mch ...
Description
set scope of B deferred set |
Example
probcli my.mch ...
Description
set GOAL predicate for model checker |
Example
probcli my.mch ...
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 ...
Description
log activities in /tmp/prob_cli_debug.log |
Example
probcli my.mch ...
Description
analyse <LogFile> using gnuplot |
Example
probcli my.mch ...
Description
pretty-print internal representation to <FILE> |
Example
probcli my.mch ...
Description
pretty-print internal representation to <FILE>, force printing of all type infos |
Example
probcli my.mch ...
Description
verbose |
Example
probcli my.mch ...
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 |
Example
probcli my.mch ...
Description
check PROPERTIES |
Example
probcli my.mch ...
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 ...
<PREF> | Typ |
---|---|
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: |
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) |
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