No edit summary |
|||
Line 129: | Line 129: | ||
== Options == | == Options == | ||
=== -mc <<Nr>> === | |||
'''Description''' | |||
{| style="color:black; background-color:#FFFFDF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%" | |||
| model check; checking at most <<Nr>> states | |||
|} | |||
'''Example''' | |||
probcli -mc 5 | |||
== Some probcli examples == | == Some probcli examples == |
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/
Description
model check; checking at most <<Nr>> states |
Example
probcli -mc 5
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