|
|
| Line 15: |
Line 15: |
| | Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line. | | | Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line. |
| |} | | |} |
| | |
| | == Synopsis == |
|
| |
|
| == Command-line Arguments for ProB Tcl/Tk == | | == Command-line Arguments for ProB Tcl/Tk == |
| Line 30: |
Line 32: |
|
| |
|
| 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. | | 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. |
|
| |
| == probcli Basics ==
| |
|
| |
| Typing <tt>probcli</tt> will give you a help printout, describing most of the functions:
| |
|
| |
| <pre>
| |
| %./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/
| |
| </pre>
| |
|
| |
|
| == Options == | | == Options == |