| Line 545: | Line 545: | ||
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. | 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. | ||
=== -mcm_cover === | === -mcm_cover <Operation(s)> === | ||
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_test''' for further details. | |||
=== -spdot <FILE> === | === -spdot <FILE> === | ||
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 ...
Test cases are generated 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.
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_test 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