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

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

Example

probcli my.mch ...

-properties

Description

check PROPERTIES

Example

probcli my.mch ...

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

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 ...

-mcm_cover

Description

Operation When generating MCM test cases, Operation should be covered

Example

probcli my.mch ...

-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 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)

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