Using the Command-Line Version of ProB: Difference between revisions

Revision as of 15:58, 30 May 2011

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.

Conventions used

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.

Synopsis

probcli [--help]
<filename> [ <options> ]

Command-line Arguments for ProB Tcl/Tk

Note that the stand-alone Tcl/Tk version also supports a limited form of command-line preferences:

FILE (the name/path of the file to be loaded)
-prefs PREF_FILE (to use a specific preferences file, rather than the default ProB_Preferences.pl in your home folder)
-batch (to instruct ProB not to try to bring up windows, but to print information only to the terminal)
-selfcheck (to run the standard unit tests)
-t (to perform the Trace Check on the default trace file associated with the specification)
-tcl TCL_Command (to run a particular pre-defined Tcl command)
-mc (to perform model checking)
-c (to compute the coverage)
-ref (to perform the default trace refinment check)

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.

Options

-mc <nr>

Description

model check; checking at most <nr> states

Example

 probcli my.mch ...

-no<x>

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

-bf

Description

proceed breadth-first

Example

 probcli my.mch -bf -mc 1000

-df

Description

proceed depth-first

Example

 probcli my.mch -df -mc 1000

--timeout <N>

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

-t

Description

trace check (associated .trace file must exist)

Example

probcli my.mch -t

-init

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

-cbc <OPNAME>

Description

constraint-based invariant checking for an operation (also use <OPNAME>=all)

Example

probcli my.mch -cbc all

-cbc_deadlock

Description

constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)

-cbc_deadlock_pred <<PRED>>

Description

Example

probcli my.mch  -cbc_deadlock_pred "n=15"

-strict

Description

raise error if mc finds counter example or trace checking fails

Example

probcli my.mch -t -strict

-expcterr <ERR>

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

-i

Description

interactive animation

Example

probcli my.mch -i

-eval

Description

start interactive read-eval-loop

Example

probcli my.mch -p CLPFD TRUE -eval

-c

Description

print coverage statistics

Example

probcli my.mch -mc 1000 -c

-cc <Nr> <Nr>

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

-p <PREFERENCE> <VALUE>

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

-card <GS> <VAL>

Description

set scope of B deferred set

Example

probcli my.mch ...

-goal <PRED>

Description

set GOAL predicate for model checker

Example

probcli my.mch -mc 10000000 -goal "n=18"  -strict -expcterr goal_found

-s <PORT>

Description

start socket server on given port

Example

probcli my.mch ...

-ss

Description

start socket server on port 9000

Example

probcli my.mch ...

-sf

Description

start socket server on some free port

Example

probcli my.mch ...

-l <LogFile>

Description

log activities in <LogFile>

Example

probcli my.mch -mc 1000 -l my.log

-ll

Description

log activities in /tmp/prob_cli_debug.log

Example

probcli my.mch -mc 1000 -ll

-lg <LogFile>

Description

analyse <LogFile> using gnuplot

Example

probcli my.mch ...

-pp <FILE>

Description

pretty-print internal representation to <FILE>

Example

probcli my.mch -pp my_pp.mch

-ppf <FILE>

Description

pretty-print internal representation to <FILE>, force printing of all type infos

Example

probcli my.mch -ppf my_ppf.mch

-v

Description

set ProB into verbose mode

Example

probcli my.mch -mc 1000 -v

-version

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

-assertions

Description

check ASSERTIONS

Note: you should probably first initialise the machine (e.g., with -init).

Example

probcli my.mch -init -assertions

-properties

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

-rc

Description

runtime checking of types/pre-/post-conditions

Example

probcli my.mch ...

-ltlfile <FILE>

Description

check LTL formulas in file <FILE>

Example

probcli my.mch ...

-ltlassertions

Description

check LTL assertions (in DEFINITIONS)

Example

probcli my.mch ...

-ltllimit <LIMIT>

Description

explore at most <LIMIT> states when model-checking LTL

Example

probcli my.mch ...

-save <FILE>

Description

save state space for later refinement check

Example

probcli my.mch ...

-refchk <FILE>

Description

refinement check against previous saved state space

Example

probcli my.mch ...

-mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE>

Generate test cases for the given specification. Each test case consists of a sequence of operations resp. events (a so-called trace) that

start in a state after an initialisation
contain a requested operation/event
end in a state where the <EndPredicate> is fulfilled

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

it has covered all required operations/events with the current search depth
or it has reached the maximum search depth or maximum number of explored states.

The required parameters are:

Depth: The maximum length of traces that the algorithm searches for test until it stops without covering all required operations/events.
MaxStates: The maximum number of explored states until the algorithm stops without covering all required operations/events.
EndPredicate: A predicate in B syntax that the last state of a trace must fulfil. If you do not have any restrictions on that state, use a trivially true predicate like 1=1
FILE: The found test cases a written to the XML file <FILE>.

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.

-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-tests for further details.

-spdot <FILE>

Description

Write graph of the state space to a dot <FILE>

Example

probcli my.mch ...

Preferences

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

Some probcli examples

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 
</pre/