The current versions of ProB can make use the clingo ASP solver as an alternate way of solving constraints.
This backend translates a subset of B formulas to SAT by encoding the formulas in ASP (Answer Set Programming) first and then using clingo to translate this to SAT and solve it.

== Using B2ASP ==

B2ASP solving consists of the following phases:
* a CLP(FD) based bounds analysis to infer finite bounds for all variables,
* a translation of set theory and B to ASP programs (aka Horn clauses),
* using clingo to translate and solve ASP programs via SAT solving,
* a Prolog back-translation of ASP models to B values.

=== B2ASP (clingo) in the REPL ===

The backend can be used in the REPL of [[Using_the_Command-Line_Version_of_ProB|probcli]]:

<pre>
>>> :clingo pq = 1..2 /\ {2,4}
PREDICATE is TRUE
Solution:
pq = {2}
</pre>

You can use <tt>:clingo #file=FILE</tt> to solve a predicate from a file.
The command <tt>:clingo-double-check</tt> double checks the solution using ProB's default solver.

=== B2ASP (clingo) for PROPERTIES ===

You can also use SOLVER_FOR_PROPERTIES preference to specify clingo as backend for solving PROPERTIES (aka axioms) of B models.
For example, you can put this into your DEFINITIONS section for this:
<pre>
SET_PREF_SOLVER_FOR_PROPERTIES == "clingo";
</pre>

Here is an example using this preference to compute a dominating set of a graph:

<pre>
MACHINE IceCream_Clingo
// Dominating set example:
// place ice cream vans so that every house (node) is at most one block away from a van
DEFINITIONS
N == 24;
CUSTOM_GRAPH == rec(layout:"dot", rankdir:"TB",
nodes: {j•j∈NODES |
rec(value:j, style:"filled",
fillcolor:IF ice(j)=TRUE THEN "mistyrose" ELSE "white" END
)},
edges: rec(color:"gray", arrowhead:"odot",
arrowtail:"odot", dir:"both",
label:"edge",
edges: edge)
);
bi_edge == (edge ∪ edge⁻¹);

SET_PREF_SOLVER_FOR_PROPERTIES == "clingo";

VISB_SVG_FILE == "IceCream.svg";
VISB_SVG_UPDATES == {n • n∈NODES |
rec(`id`:n, fill: IF ice(n)=TRUE THEN "red" ELSE "LightBlue" END)}
SETS
NODES = {n1,n2,n3,n4,n5,n6,n7,n8,n9,n10,
n11,n12,n13,n14,n15,n16,n17,n18,n19,n20,n21,n22,n23,n24}
CONSTANTS edge, ice
PROPERTIES
edge∈ NODES ↔ NODES ∧
edge = { n1↦n2, n1↦n4,
n2↦n3,
n3↦n4, n3↦n5, n3↦n7,
n4↦n7,
n5↦n6, n5↦n9,
n6↦n7, n6↦n8,
n7↦n8,
n8↦n10, n8↦n13,
n9↦n10, n9↦n11, n9↦n12,
n11↦n12, n11↦n14,
n12↦n13,
n13↦n16,
n14↦n15, n14↦n17,
n15↦n16, n15↦n17, n15↦n18, n15↦n21,
n16↦n18, n16↦n19,
n17↦n19,
n18↦n19, n18↦n20, n18↦n21,
n19↦n20, n19↦n21,
n20↦n21, n20↦n22,
n21↦n22, n21↦n23, n21↦n24,
n22↦n23, n21↦n24,
n23↦n24
} ∧
ice ∈ NODES→ BOOL ∧
∀x.(x∈NODES ⇒
(ice(x)=TRUE or
TRUE ∈ ice[edge[{x}] ∪ edge⁻¹[{x}]]
)
)

∧ card({x|x∈NODES ∧ ice(x)=TRUE})≤6
/* minimal solution requires 6 vans */

OPERATIONS
v <-- NrVans = BEGIN v := card(ice⁻¹[{TRUE}]) END;
xx <-- Get(yy) = PRE yy∈NODES ∧ {CUSTOM_GRAPH} = ∅ THEN xx:= ice(yy) END;
v <-- Vans = BEGIN v:= ice⁻¹[{TRUE}] END
END
</pre>

Here is the graphical rendering of a solution using the custom graph definition above:

[[File:IceCream_Generic.png|500px|center]]

== Article ==

[https://link.springer.com/chapter/10.1007/978-3-032-15981-6_9 Michael Leuschel:
Using Prolog to Translate Set Theory and B to SAT. PADL 2025: 143-160.]

[https://zenodo.org/records/17660151 Zenodo archive of benchmarks].

B2ASP

2026-03-19T13:35:40Z

Michael Leuschel:

B2ASP

2026-03-19T13:34:03Z

Michael Leuschel:

2026-01-29T15:03:00Z

Michael Leuschel:

ProB can store the values of constants and operations in a cache file.
Compared to [[Memoization_for_Functions|memoization for functions]] and
[[Tutorial_Tuning_Model_Checking#Operation_Caching_.28Reuse.29|operation reuse during model checking]], this caching is persistent across different runs of probcli or ProB Tcl/Tk and is applicable to the constant setup and operations, not at the level of computation of values using (constant) functions.
(It thus may make sense to activate both [[Memoization_for_Functions|memoization]] and caching.)

=== Activating Caching ===

In the [[Using_the_Command-Line_Version_of_ProB|command-line version probcli]] the cache can be activated using the option
* -cache DIRECTORY
This means that cache results will be stored in that directory.
The directory may contain multiple files, namely one file per B machine.
The files contain a hash to detect whether they are still up-to-date.

The same option has to be used to activate the caching for ProB Tcl/Tk, i.e., you need to launch ProB Tcl/Tk from the command-line with the -cache option:
* prob -cache DIRECTORY

Caching is currently only available for classical B machines without refinement,
and when symmetry reduction is off (which it is by default).
(Note to developers: the conditions are checked in the Prolog predicate cache_is_applicable in the module value_persistance.pl).
The cache feature can, however, deal with composed machines (e.g., with INCLUDES, USES, SEES) and stores constant values for individual sub-machines.
Constants are cached when
* no time-out occurred during SET_UP_CONSTANTS
* all enabled solutions were computed (i.e., the MAX_INITIALISATIONS limit was not reached)
* the machine has no parameters
Operations are cached when
* no time-out occurred
* all enabled operations were computed (i.e., the MAX_OPERATIONS limit was not reached)
* the preference CACHE_OPERATIONS is true (which it is by default; it is only available as of version 1.11.0)

The cache file will also contain the values of relevant preferences, which can influence the computation of constants or operation results (e.g., MAXINT, MININT, DEFAULT_SETSIZE,...)
If the cache cannot be re-used a message will be displayed:
value caching: general computations parameters have changed, no re-use of stored operations

=== Inspecting the Cache ===

In the [[Using_the_Command-Line_Version_of_ProB|command-line version probcli]] a summary of the cache can be displayed using this option (together with the -cache option mentioned above).
* -show_cache
In verbose mode (-v flag) more details are displayed, but the additional information is probably only useful for ProB developers. You can also use -show_cache_verbose to this effect.

<pre>
probcli CrewAllocationConstants.mch -cache cache/ -show-cache

Contents of cache file cache/CrewAllocationConstants.probcst of type constants for machine CrewAllocationConstants:
( male={(tom|->TRUE),(david|->TRUE),(jeremy|->TRUE),(carol|->FALSE),(janet|->FALSE),(tracy|->FALSE)} &
speaks={(tom|->german),(david|->french),(jeremy|->german),(carol|->spanish),(janet|->french),(tracy|->spanish)} &
assign={(1|->tom),(1|->david),(1|->jeremy),(1|->carol),(1|->janet),(1|->tracy),(2|->tom),(2|->david),(2|->carol),(3|->jeremy),(3|->janet),(3|->tracy)} )
</pre>

In Tcl/Tk this information can be obtained by choosing the command "Show ProB Cache Info" in the Debug menu.

=== Example ===
Take the following B machine
<pre>
MACHINE PrimeNumbers
// A machine with a slow constant set up to check -cache option
DEFINITIONS SET_PREF_TIME_OUT == 10000
CONSTANTS n, primes, maxprime
PROPERTIES
n:NATURAL1 &
primes = {x|x:2..n & !y.(y>1 & y*y<=x => x mod y /= 0)} &
(n = 10000 or n=1000) &
maxprime = max(primes)
ASSERTIONS
(n = 10000 => card(primes) = 1229)
VARIABLES x
INVARIANT
x:2..n & x:primes
INITIALISATION x:=2
OPERATIONS
NextPrime(nxt) = SELECT x<maxprime &
nxt:primes & nxt = min(primes /\ (x+1)..n) THEN
x:=nxt
END
END
</pre>

Without caching we have this behaviour:

<pre>
$ time probcli PrimeNumbers.mch -init
% Runtime for SOLUTION for SETUP_CONSTANTS: 137 ms (walltime: 140 ms)
% Runtime for SOLUTION for SETUP_CONSTANTS: 1176 ms (walltime: 1187 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

real 0m2.549s
user 0m2.341s
sys 0m0.125s
</pre>

With cache, we obviously do not yet see a benefit the first time around:
<pre>
$ time probcli PrimeNumbers.mch -init -cache ./cache/
% Runtime for SOLUTION for SETUP_CONSTANTS: 134 ms (walltime: 136 ms)
% Runtime for SOLUTION for SETUP_CONSTANTS: 1161 ms (walltime: 1169 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

real 0m2.536s
user 0m2.311s
sys 0m0.134s
</pre>

The second time around we get a much faster performance; the values of the constants are simply restored from disk:
<pre>
$ time probcli PrimeNumbers.mch -init -cache ./cache/

real 0m1.210s
user 0m1.010s
sys 0m0.117s
</pre>

We can inspect the cache contents either using probcli or inspecting the directory:

<pre>
$ probcli PrimeNumbers.mch -init -cache ./cache/ -show_cache

Contents of cache file ./cache/PrimeNumbers.probcst of type constants for machine PrimeNumbers:
( n=1000 &
primes=#168:{2,3,...,991,997} &
maxprime=997 )
( n=10000 &
primes=#1229:{2,3,...,9967,9973} &
maxprime=9973 )

$ ls -l cache/
total 48
-rw-r--r-- 1 leuschel staff 0 15 May 16:25 PrimeNumbers.opdata
-rw-r--r-- 1 leuschel staff 14988 15 May 16:25 PrimeNumbers.probcst
-rw-r--r-- 1 leuschel staff 5831 15 May 16:26 PrimeNumbers.probops
</pre>

The cache option is worthwhile for constants and operations which are computation intensive.
For example, it is not really worthwhile for the operation NextPrime.
As of version 1.11.0 you can turn off caching operations by setting the preference CACHE_OPERATIONS to FALSE.

Note that the cache is also used for when other machines include a cached machine.
Take for example:
<pre>
MACHINE PrimeNumberSum
INCLUDES PrimeNumbers
CONSTANTS
mx
PROPERTIES
mx = n
VARIABLES
sum
INVARIANT
sum : 0..mx
INITIALISATION
sum := 1
OPERATIONS
Next(nxtP) = PRE nxtP:0..mx THEN
NextPrime(nxtP) || sum := sum + 1
END
END
</pre>

Then you see that the cache of the included machine is re-used straight away:
<pre>
$ probcli PrimeNumbersSum.mch -init -cache ./cache/ -show_cache
% Runtime for SOLUTION for SETUP_CONSTANTS: 32 ms (walltime: 33 ms)
% Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

Contents of cache file ./cache/PrimeNumberSum.probcst of type constants for machine PrimeNumberSum:
( mx=1000 &
n=1000 &
primes=#168:{2,3,...,991,997} &
maxprime=997 )
( mx=10000 &
n=10000 &
primes=#1229:{2,3,...,9967,9973} &
maxprime=9973 )

Contents of cache file ./cache/PrimeNumbers.probcst of type constants for machine PrimeNumbers:
( n=1000 &
primes=#168:{2,3,...,991,997} &
maxprime=997 )
( n=10000 &
primes=#1229:{2,3,...,9967,9973} &
maxprime=9973 )
</pre>

=== Example ===

The following commands can also be useful:
* -ccache DIR works like -cache DIR but creates the directory if it does not exist
* -cache_statistics to print statistics about cache re-use
* -clear_cache to clear the cache
* -clear_cache_for M to clear the cache for the machine M
* -show_inclusion_hierarchy to display the list of included subsidiary machines and a minimal cover

The latter command produces a list of sufficient includes to cover all machines.
By performing
probcli FILE.mch -init -cache DIR
for all machines in that list you can pre-populate the cache with all
the necessary constants.

Caching Constants and Operations

2026-01-29T14:55:52Z

Michael Leuschel: /* Inspecting the Cache */

Using the Command-Line Version of ProB

2026-01-29T14:48:43Z

Michael Leuschel: /* -cache */

[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:ProB Cli]]

The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.6 of ProB. Some features are only available in the nightly build of ProB. You can run <tt>probcli –help</tt> to find out which commands are supported by your version of ProB. For Bash users we provide [[Bash Completion|command completion]] support.

Note: the order of commands is not relevant for <tt>probcli</tt> (except within groups of commands such as <tt>-p MAXINT 127</tt>). Any argument that is not recognised by <tt>probcli</tt> is treated as a filename to be analysed.

[[file:ProBTerminalizerDemo.gif|center||600px]]

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

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

The underscore within all options can as of version 1.5.1-beta7 be replaced with dashes. Also, all commands can either be typed with single leading dashes or double leading dashes.
For example, all of the following commands have the same effect:
probcli M.mch -model_check
probcli M.mch -model-check
probcli M.mch --model_check
probcli M.mch --model-check

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options <tt>-nodead, -noinv, -nogoal, -noass</tt> to influence which kinds of errors are reported by <tt>-mc</tt>.
You can also set a target goal predicate using the <tt>-goal "PRED"</tt> command and limit the scope of the model checking using the <tt>-scope "PRED"</tt> command.

=== -model_check ===

The same as <tt>-mc</tt> but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking (-mc), TLC model checking (-mc_with_tlc), animation (-animate) and execution (-execute) 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

=== -disable_timeout ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| turn off ProB's timeout mechanism, e.g., for computing enabled operations and invariant checking; this can sometimes speed up model checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7.
|}

Example

probcli my.mch -model-check -disable-timeout

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first during model checking
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first during model checking
|}

Example

probcli my.mch -df -mc 1000

=== -mc_mode <M> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| influence how the model checker proceeds. Available as of version 1.5.1. Supersedes the <tt>-df</tt> and <tt>-bf</tt> switches.
Possible values for the mode <M> are: <ul>
<li><tt>df</tt> (depth-first traversal),</li>
<li><tt>bf</tt> (breadth-first traversal),</li>
<li><tt>mixed</tt> (mixed depth-first / breadth-first traversal with random choice; currently the default),</li>
<li><tt>random</tt> (choosing next node to process completely at random), </li>
<li><tt>hash</tt> (similar to random, but uses the Prolog hash function of a node instead of a random number generator),</li>
<li><tt>heuristic</tt> (try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause). Some explanations can be found [[Blocks_World_(Directed_Model_Checking)|in an example about directed model checking]].</li>
<li><tt>out_degree_hash</tt> (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking)
</ul>
|}

Example

probcli my.mch -model_check -mc_mode random

=== --timeout <N> ===

Deprecated, please use --global-time-out command instead.

=== --global-time-out <N> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global timeout 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>. Note that the <tt>TIME_OUT</tt> preference also influences other computations, such as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option.
|}

Example

probcli my.mch -global_timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -trace_replay <KIND> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Replay a trace file in the given format (json,prolog,B).
|}

KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
Example

probcli my.mch -trace_replay json my.prob2trace

Alternative command -det_trace_replay KIND FILE.

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -cbc_assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based checking of assertions on constants
|}
This will try and find a solution for the constants which make an assertion (on constants) false.

You can use the extra command <tt>-cbc_output_file FILE</tt> to write the result of this check to a file.
You can also use the extra command <tt>-cbc_option contradiction_check</tt> to ask ProB to check if there is a contradiction in the properties (in case the check did not find a counter-example to the assertions). The extra command <tt>-cbc_option unsat_core</tt> tells ProB to compute the unsatisfiable core in case a proof the assertions was found.
Note that the <tt>TIME_OUT</tt> preference is multiplied by 10 for this command.

There are various variations of this command:
-cbc_assertions_proof
-cbc_assertions_tautology_proof
Both commands do not allow enumeration warnings to occur.
The latter command ignores the PROPERTIES and tries to check whether the ASSERTION(s) are tautologies.
Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3).

=== -cbc_sequence <SEQ> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based searching for a sequence of operation names (separated by semicolons)
|}
This will try and find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible.

Example

probcli my.mch -cbc_sequence "op1;op2"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error and stop probcli if anything unexpected happens, e.g., if model checking finds a counter example or trace checking fails or any unexpected error happens
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

Variations
-animate_all : animate until deadlock reached
-animate_until_ltl P : animate until LTL property holds on trace
-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

=== -execute <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| execution (max Nr steps)
|}

Executes the "first" enabled operation of a machine, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-execute_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-execute_all</tt> could run forever.

In contrast to -animate, -execute will
* always choose the first enabled operation it finds and stop searching for further enabled operations in that state (-animate will compute all enabled operations up to the limit set by the <tt>MAX_OPERATIONS</tt> or <tt>MAX_INITIALISATIONS</tt> preference and then choose randomly); the order of operations in the B machine is thus important for -execute
* not store intermediate states in the state space; as such -execute is faster but after execution one only has access to the first state and the final state of execution

Example

probcli my.mch -execute 100

=== -execute_all===

See <tt>-execute <Nr></tt> above.

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -his command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command.

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -repl ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-print-loop
|}

Example

probcli my.mch -p CLPFD TRUE -repl

A list of commands can be obtained by typing <tt>:help</tt> (just help for versions 1.3.x of probcli). The interactive read-eval-print-loop can be exited using <tt>:q</tt> (just typing a return on a blank line for versions 1.3.x of probcli)..
If in addition you want see a graphical representation of the solutions found you can use the following command and open the <tt>out.dot</tt> file using dotty or GraphViz:
probcli -repl -evaldot ~/out.dot

You can also use the <tt>-eval</tt> command to evaluate specific formulas or expressions:
probcli -eval "1+2"
For convenience, these formulas can also be put into a separate file:
probcli -eval_file MyFormula.txt

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

You can also use the longer name for the command:

probcli my.mch -mc 1000 --coverage

There is also a version which prints a shorter summary (and which is much faster for large state spaces):

probcli my.mch -mc 1000 --coverage_summary

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -pref_group <PREFGROUP> <SETTING> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set to the group of preferences <PREFGROUP> to a predefined setting <SETTING>
|}

Example

probcli my.mch -pref_group model_check unlimited

Available groups and settings are:

* PREFERENCE GROUP integer : SETTINGS [int32] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set cardinality (scope in Alloy terminology) of a B deferred set. This overrides the default cardinality (which can be set using <tt>-p DEFAULT_SETSIZE <VAL></tt>).
|}

Example

probcli my.mch -card PID 5

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

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

=== -scope <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set SCOPE predicate for model checker; states which do not satisfy the SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed)
|}

Example

probcli my.mch -mc 10000000 -scope "n<18"

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -cache <DIRECTORY>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants (and in future also variables) to a file to avoid recomputation
|}

This commands saves the values of constants for the current B machine and puts those values into files in the specified directory. The command will also tell ProB to try and reuse constants saved for subsidiary machines (included using SEES for example) whenever possible.
The purpose of the command is to avoid recomputing constants as much as possible, as this can be very time consuming.
This also works for values of variables computed in the initialisation or even using operations.
However, we do not support refinements at the moment.

Note: this command can also be used when starting up the ProB Tcl/Tk version.

Note: the variation -ccache will create the directory if it does not exist.
The command -show_cache and -show_cache_verbose can be used to display the cache contents.
The command -cache_statistics provides statistics about the re-use of the cache.
The commands -clear_cache and -clear_cache_for MACHINE can be used to force clearing the caching.

=== -logxml <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities and results of probcli in XML format in <LogFile>
|}

A schema declaration file (xsd) can be found at <tt>doc/logxml_xsd.xml</tt> in the ProB [[Download#Sourcecode|Prolog sources]].
The log file contains information about the various commands performed by probcli.
It also contains version information, the parameters provided to probcli and details about the errors that occured.

Example

probcli my.mch -mc 1000 -logxml log.xml

=== -logxml_write_vars <PREFIX> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| after processing other commands (such as -execute) write values of variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command)
|}

Example

probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile> using Prolog format
|}

Example

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

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

You can use <tt>probcli -version -v</tt> to obtain more information about your version of probcli.

=== -check_java_version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check Java and B parser version information
|}

This command is available as of ProB version 1.5.1-beta5 or higher. It can be useful to check that your Java is correctly installed and that the ProB B parser can operate correctly

probcli -check_java_version
Result of checking Java version:
Java is correctly installed and version 1.7.0_55-b13 is compatible with ProB requirements (>= 1.7).
ProB B Java Parser available in version: 2016-02-25 15:27:18.55.

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -property ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| virtually add predicate to PROPERTIES
|}

Example

probcli my.mch -property "PRED"

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch --model_check -save my_saved.P

=== -refchk <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space (e.g. using -save)
|}

Example

probcli my.mch -refchk abs_saved.P

=== -ref_check <MODE> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space (e.g. using -save) with particular failure/trace/divergence model
|}

MODE is one of F, FD, T, R, RD, SF, V.
Meaning of mode: F: Failures, FD: Failure-Divergences, R: Refusals, RD: Refusals-Divergences, SF: Singleton-Failures, T: Traces, V: Revival.
Default used by -refchck command above is T (traces model).

Example

probcli my.mch -ref_check F abstract_saved.P

=== -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 <Operation(s)>|-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'''.

As of version 1.6.0, the operation arguments are also written to the XML file.
The preference <tt>INTERNAL_ARGUMENT_PREFIX</tt> can be used to provide a prefix for internal operation arguments; any argument/parameter whose name starts with that prefix is considered an internal parameter and not shown in the trace file.
Also, as of version 1.6.0, the non-deterministic initialisations are shown in the XML trace file: all variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event.

=== -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 <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch -mc 100 -spdot my_statespace.dot

=== -cbc_tests <Depth> <EndPredicate> <File> ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''. If the predicate is the empty string we assume truth. If the filename is the empty string no file is generated. See also the page on [[Test_Case_Generation]].

=== -cbc_cover <Operation> ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma. You can also use the option <pre>-cbc_cover_match PartialName</pre> to match all operations whose name contains PartialName. See also the page about [[Test_Case_Generation]].

=== -test_description <File> ===
Read the options for constraint based test case generation from '''File'''.

=== -bmc <Depth> ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Run the [[Bounded_Model_Checking|bounded model checker]] until maximum trace depth <Depth> specified. Looks for invariant violations using the constraint-based test case generation algorithm.
|}

Example

probcli my.mch -bmc 20

=== -csp-guide <File> ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)
As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
DEFINITION (which also works in ProB2-UI).

=== -rule_report <File> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Generates rule validation report for rules machines (.rmch) at the specified location <File> for the current animation state. Depending on the file extension an HTML or an XML version of the report is generated (.html/.xml).
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.rmch -execute_all -rule_report my_report.html

=== -machine_files_sha ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Computes SHA1 hash of all B files used by a B model.
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.mch -machine_files_sha

=== -check_machine_file_sha ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Compute and check SHA1 hash of a particular B file used by the main B model.
|}

probcli ./Demo/scheduler.mch -check_machine_file_sha scheduler.mch 1cab7ec89adc9f9b153af85c1ae16ba8a7a2a661

== Environment Variables ==

Set NO_COLOR environment variable to disable terminal colors.
See [https://no-color.org https://no-color.org].

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <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. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants 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
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| 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, is multiplied by a factor for other computations)
|-
| PROOF_INFO
| bool ==> Use Proof Information to restrict invariant checking to affected unproven clauses. Most useful in EventB for models exported from Rodin.
|-
| 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 (use 0 to disable expansion)
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| 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 analyzing assertions or properties
|-
| 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)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|-
| CSE
| bool ==> Perform common-sub-expression elimination
|-
| CSE_SUBST
| bool ==> Perform common-sub-expression elimination also for B substitutions
|}

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:
<pre>
probcli -init My.mch
</pre>
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:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To fully model check a specification M.mch while tryining to minimize memory consumption do:
<pre>
probcli -model_check -p COMPRESSION TRUE M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption further by not storing processed stats and using symmetry reduction (and accepting hash collisions) do:
<pre>
probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
</pre>

== 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.
{{Feedback}}

Using the Command-Line Version of ProB

2025-12-24T07:30:49Z

Michael Leuschel: /* --timeout */

[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:ProB Cli]]

The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.6 of ProB. Some features are only available in the nightly build of ProB. You can run <tt>probcli –help</tt> to find out which commands are supported by your version of ProB. For Bash users we provide [[Bash Completion|command completion]] support.

Note: the order of commands is not relevant for <tt>probcli</tt> (except within groups of commands such as <tt>-p MAXINT 127</tt>). Any argument that is not recognised by <tt>probcli</tt> is treated as a filename to be analysed.

[[file:ProBTerminalizerDemo.gif|center||600px]]

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

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

The underscore within all options can as of version 1.5.1-beta7 be replaced with dashes. Also, all commands can either be typed with single leading dashes or double leading dashes.
For example, all of the following commands have the same effect:
probcli M.mch -model_check
probcli M.mch -model-check
probcli M.mch --model_check
probcli M.mch --model-check

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options <tt>-nodead, -noinv, -nogoal, -noass</tt> to influence which kinds of errors are reported by <tt>-mc</tt>.
You can also set a target goal predicate using the <tt>-goal "PRED"</tt> command and limit the scope of the model checking using the <tt>-scope "PRED"</tt> command.

=== -model_check ===

The same as <tt>-mc</tt> but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking (-mc), TLC model checking (-mc_with_tlc), animation (-animate) and execution (-execute) 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

=== -disable_timeout ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| turn off ProB's timeout mechanism, e.g., for computing enabled operations and invariant checking; this can sometimes speed up model checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7.
|}

Example

probcli my.mch -model-check -disable-timeout

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first during model checking
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first during model checking
|}

Example

probcli my.mch -df -mc 1000

=== -mc_mode <M> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| influence how the model checker proceeds. Available as of version 1.5.1. Supersedes the <tt>-df</tt> and <tt>-bf</tt> switches.
Possible values for the mode <M> are: <ul>
<li><tt>df</tt> (depth-first traversal),</li>
<li><tt>bf</tt> (breadth-first traversal),</li>
<li><tt>mixed</tt> (mixed depth-first / breadth-first traversal with random choice; currently the default),</li>
<li><tt>random</tt> (choosing next node to process completely at random), </li>
<li><tt>hash</tt> (similar to random, but uses the Prolog hash function of a node instead of a random number generator),</li>
<li><tt>heuristic</tt> (try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause). Some explanations can be found [[Blocks_World_(Directed_Model_Checking)|in an example about directed model checking]].</li>
<li><tt>out_degree_hash</tt> (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking)
</ul>
|}

Example

probcli my.mch -model_check -mc_mode random

=== --timeout <N> ===

Deprecated, please use --global-time-out command instead.

=== --global-time-out <N> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global timeout 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>. Note that the <tt>TIME_OUT</tt> preference also influences other computations, such as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option.
|}

Example

probcli my.mch -global_timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -trace_replay <KIND> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Replay a trace file in the given format (json,prolog,B).
|}

KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
Example

probcli my.mch -trace_replay json my.prob2trace

Alternative command -det_trace_replay KIND FILE.

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -cbc_assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based checking of assertions on constants
|}
This will try and find a solution for the constants which make an assertion (on constants) false.

You can use the extra command <tt>-cbc_output_file FILE</tt> to write the result of this check to a file.
You can also use the extra command <tt>-cbc_option contradiction_check</tt> to ask ProB to check if there is a contradiction in the properties (in case the check did not find a counter-example to the assertions). The extra command <tt>-cbc_option unsat_core</tt> tells ProB to compute the unsatisfiable core in case a proof the assertions was found.
Note that the <tt>TIME_OUT</tt> preference is multiplied by 10 for this command.

There are various variations of this command:
-cbc_assertions_proof
-cbc_assertions_tautology_proof
Both commands do not allow enumeration warnings to occur.
The latter command ignores the PROPERTIES and tries to check whether the ASSERTION(s) are tautologies.
Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3).

=== -cbc_sequence <SEQ> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based searching for a sequence of operation names (separated by semicolons)
|}
This will try and find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible.

Example

probcli my.mch -cbc_sequence "op1;op2"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error and stop probcli if anything unexpected happens, e.g., if model checking finds a counter example or trace checking fails or any unexpected error happens
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

Variations
-animate_all : animate until deadlock reached
-animate_until_ltl P : animate until LTL property holds on trace
-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

=== -execute <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| execution (max Nr steps)
|}

Executes the "first" enabled operation of a machine, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-execute_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-execute_all</tt> could run forever.

In contrast to -animate, -execute will
* always choose the first enabled operation it finds and stop searching for further enabled operations in that state (-animate will compute all enabled operations up to the limit set by the <tt>MAX_OPERATIONS</tt> or <tt>MAX_INITIALISATIONS</tt> preference and then choose randomly); the order of operations in the B machine is thus important for -execute
* not store intermediate states in the state space; as such -execute is faster but after execution one only has access to the first state and the final state of execution

Example

probcli my.mch -execute 100

=== -execute_all===

See <tt>-execute <Nr></tt> above.

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -his command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command.

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -repl ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-print-loop
|}

Example

probcli my.mch -p CLPFD TRUE -repl

A list of commands can be obtained by typing <tt>:help</tt> (just help for versions 1.3.x of probcli). The interactive read-eval-print-loop can be exited using <tt>:q</tt> (just typing a return on a blank line for versions 1.3.x of probcli)..
If in addition you want see a graphical representation of the solutions found you can use the following command and open the <tt>out.dot</tt> file using dotty or GraphViz:
probcli -repl -evaldot ~/out.dot

You can also use the <tt>-eval</tt> command to evaluate specific formulas or expressions:
probcli -eval "1+2"
For convenience, these formulas can also be put into a separate file:
probcli -eval_file MyFormula.txt

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

You can also use the longer name for the command:

probcli my.mch -mc 1000 --coverage

There is also a version which prints a shorter summary (and which is much faster for large state spaces):

probcli my.mch -mc 1000 --coverage_summary

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -pref_group <PREFGROUP> <SETTING> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set to the group of preferences <PREFGROUP> to a predefined setting <SETTING>
|}

Example

probcli my.mch -pref_group model_check unlimited

Available groups and settings are:

* PREFERENCE GROUP integer : SETTINGS [int32] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set cardinality (scope in Alloy terminology) of a B deferred set. This overrides the default cardinality (which can be set using <tt>-p DEFAULT_SETSIZE <VAL></tt>).
|}

Example

probcli my.mch -card PID 5

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

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

=== -scope <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set SCOPE predicate for model checker; states which do not satisfy the SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed)
|}

Example

probcli my.mch -mc 10000000 -scope "n<18"

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -cache <DIRECTORY>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants (and in future also variables) to a file to avoid recomputation
|}

This commands saves the values of constants for the current B machine and puts those values into files in the specified directory. The command will also tell ProB to try and reuse constants saved for subsidiary machines (included using SEES for example) whenever possible.
The purpose of the command is to avoid recomputing constants as much as possible, as this can be very time consuming.
This also works for values of variables computed in the initialisation or even using operations.
However, we do not support refinements at the moment.

Note: this command can also be used when starting up the ProB Tcl/Tk version.

=== -logxml <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities and results of probcli in XML format in <LogFile>
|}

A schema declaration file (xsd) can be found at <tt>doc/logxml_xsd.xml</tt> in the ProB [[Download#Sourcecode|Prolog sources]].
The log file contains information about the various commands performed by probcli.
It also contains version information, the parameters provided to probcli and details about the errors that occured.

Example

probcli my.mch -mc 1000 -logxml log.xml

=== -logxml_write_vars <PREFIX> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| after processing other commands (such as -execute) write values of variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command)
|}

Example

probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile> using Prolog format
|}

Example

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

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

You can use <tt>probcli -version -v</tt> to obtain more information about your version of probcli.

=== -check_java_version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check Java and B parser version information
|}

This command is available as of ProB version 1.5.1-beta5 or higher. It can be useful to check that your Java is correctly installed and that the ProB B parser can operate correctly

probcli -check_java_version
Result of checking Java version:
Java is correctly installed and version 1.7.0_55-b13 is compatible with ProB requirements (>= 1.7).
ProB B Java Parser available in version: 2016-02-25 15:27:18.55.

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -property ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| virtually add predicate to PROPERTIES
|}

Example

probcli my.mch -property "PRED"

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch --model_check -save my_saved.P

=== -refchk <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space (e.g. using -save)
|}

Example

probcli my.mch -refchk abs_saved.P

=== -ref_check <MODE> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space (e.g. using -save) with particular failure/trace/divergence model
|}

MODE is one of F, FD, T, R, RD, SF, V.
Meaning of mode: F: Failures, FD: Failure-Divergences, R: Refusals, RD: Refusals-Divergences, SF: Singleton-Failures, T: Traces, V: Revival.
Default used by -refchck command above is T (traces model).

Example

probcli my.mch -ref_check F abstract_saved.P

=== -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 <Operation(s)>|-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'''.

As of version 1.6.0, the operation arguments are also written to the XML file.
The preference <tt>INTERNAL_ARGUMENT_PREFIX</tt> can be used to provide a prefix for internal operation arguments; any argument/parameter whose name starts with that prefix is considered an internal parameter and not shown in the trace file.
Also, as of version 1.6.0, the non-deterministic initialisations are shown in the XML trace file: all variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event.

=== -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 <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch -mc 100 -spdot my_statespace.dot

=== -cbc_tests <Depth> <EndPredicate> <File> ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''. If the predicate is the empty string we assume truth. If the filename is the empty string no file is generated. See also the page on [[Test_Case_Generation]].

=== -cbc_cover <Operation> ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma. You can also use the option <pre>-cbc_cover_match PartialName</pre> to match all operations whose name contains PartialName. See also the page about [[Test_Case_Generation]].

=== -test_description <File> ===
Read the options for constraint based test case generation from '''File'''.

=== -bmc <Depth> ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Run the [[Bounded_Model_Checking|bounded model checker]] until maximum trace depth <Depth> specified. Looks for invariant violations using the constraint-based test case generation algorithm.
|}

Example

probcli my.mch -bmc 20

=== -csp-guide <File> ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)
As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
DEFINITION (which also works in ProB2-UI).

=== -rule_report <File> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Generates rule validation report for rules machines (.rmch) at the specified location <File> for the current animation state. Depending on the file extension an HTML or an XML version of the report is generated (.html/.xml).
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.rmch -execute_all -rule_report my_report.html

=== -machine_files_sha ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Computes SHA1 hash of all B files used by a B model.
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.mch -machine_files_sha

=== -check_machine_file_sha ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Compute and check SHA1 hash of a particular B file used by the main B model.
|}

probcli ./Demo/scheduler.mch -check_machine_file_sha scheduler.mch 1cab7ec89adc9f9b153af85c1ae16ba8a7a2a661

== Environment Variables ==

Set NO_COLOR environment variable to disable terminal colors.
See [https://no-color.org https://no-color.org].

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <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. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants 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
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| 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, is multiplied by a factor for other computations)
|-
| PROOF_INFO
| bool ==> Use Proof Information to restrict invariant checking to affected unproven clauses. Most useful in EventB for models exported from Rodin.
|-
| 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 (use 0 to disable expansion)
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| 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 analyzing assertions or properties
|-
| 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)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|-
| CSE
| bool ==> Perform common-sub-expression elimination
|-
| CSE_SUBST
| bool ==> Perform common-sub-expression elimination also for B substitutions
|}

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:
<pre>
probcli -init My.mch
</pre>
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:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To fully model check a specification M.mch while tryining to minimize memory consumption do:
<pre>
probcli -model_check -p COMPRESSION TRUE M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption further by not storing processed stats and using symmetry reduction (and accepting hash collisions) do:
<pre>
probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
</pre>

== 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.
{{Feedback}}

Using the Command-Line Version of ProB

2025-12-24T07:28:31Z

Michael Leuschel: /* -ref_check */

[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:ProB Cli]]

The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.6 of ProB. Some features are only available in the nightly build of ProB. You can run <tt>probcli –help</tt> to find out which commands are supported by your version of ProB. For Bash users we provide [[Bash Completion|command completion]] support.

Note: the order of commands is not relevant for <tt>probcli</tt> (except within groups of commands such as <tt>-p MAXINT 127</tt>). Any argument that is not recognised by <tt>probcli</tt> is treated as a filename to be analysed.

[[file:ProBTerminalizerDemo.gif|center||600px]]

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

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

The underscore within all options can as of version 1.5.1-beta7 be replaced with dashes. Also, all commands can either be typed with single leading dashes or double leading dashes.
For example, all of the following commands have the same effect:
probcli M.mch -model_check
probcli M.mch -model-check
probcli M.mch --model_check
probcli M.mch --model-check

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options <tt>-nodead, -noinv, -nogoal, -noass</tt> to influence which kinds of errors are reported by <tt>-mc</tt>.
You can also set a target goal predicate using the <tt>-goal "PRED"</tt> command and limit the scope of the model checking using the <tt>-scope "PRED"</tt> command.

=== -model_check ===

The same as <tt>-mc</tt> but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking (-mc), TLC model checking (-mc_with_tlc), animation (-animate) and execution (-execute) 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

=== -disable_timeout ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| turn off ProB's timeout mechanism, e.g., for computing enabled operations and invariant checking; this can sometimes speed up model checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7.
|}

Example

probcli my.mch -model-check -disable-timeout

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first during model checking
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first during model checking
|}

Example

probcli my.mch -df -mc 1000

=== -mc_mode <M> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| influence how the model checker proceeds. Available as of version 1.5.1. Supersedes the <tt>-df</tt> and <tt>-bf</tt> switches.
Possible values for the mode <M> are: <ul>
<li><tt>df</tt> (depth-first traversal),</li>
<li><tt>bf</tt> (breadth-first traversal),</li>
<li><tt>mixed</tt> (mixed depth-first / breadth-first traversal with random choice; currently the default),</li>
<li><tt>random</tt> (choosing next node to process completely at random), </li>
<li><tt>hash</tt> (similar to random, but uses the Prolog hash function of a node instead of a random number generator),</li>
<li><tt>heuristic</tt> (try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause). Some explanations can be found [[Blocks_World_(Directed_Model_Checking)|in an example about directed model checking]].</li>
<li><tt>out_degree_hash</tt> (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking)
</ul>
|}

Example

probcli my.mch -model_check -mc_mode random

=== --timeout <N> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global timeout 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>. Note that the <tt>TIME_OUT</tt> preference also influences other computations, such as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -trace_replay <KIND> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Replay a trace file in the given format (json,prolog,B).
|}

KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
Example

probcli my.mch -trace_replay json my.prob2trace

Alternative command -det_trace_replay KIND FILE.

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -cbc_assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based checking of assertions on constants
|}
This will try and find a solution for the constants which make an assertion (on constants) false.

You can use the extra command <tt>-cbc_output_file FILE</tt> to write the result of this check to a file.
You can also use the extra command <tt>-cbc_option contradiction_check</tt> to ask ProB to check if there is a contradiction in the properties (in case the check did not find a counter-example to the assertions). The extra command <tt>-cbc_option unsat_core</tt> tells ProB to compute the unsatisfiable core in case a proof the assertions was found.
Note that the <tt>TIME_OUT</tt> preference is multiplied by 10 for this command.

There are various variations of this command:
-cbc_assertions_proof
-cbc_assertions_tautology_proof
Both commands do not allow enumeration warnings to occur.
The latter command ignores the PROPERTIES and tries to check whether the ASSERTION(s) are tautologies.
Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3).

=== -cbc_sequence <SEQ> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based searching for a sequence of operation names (separated by semicolons)
|}
This will try and find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible.

Example

probcli my.mch -cbc_sequence "op1;op2"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error and stop probcli if anything unexpected happens, e.g., if model checking finds a counter example or trace checking fails or any unexpected error happens
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

Variations
-animate_all : animate until deadlock reached
-animate_until_ltl P : animate until LTL property holds on trace
-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

=== -execute <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| execution (max Nr steps)
|}

Executes the "first" enabled operation of a machine, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-execute_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-execute_all</tt> could run forever.

In contrast to -animate, -execute will
* always choose the first enabled operation it finds and stop searching for further enabled operations in that state (-animate will compute all enabled operations up to the limit set by the <tt>MAX_OPERATIONS</tt> or <tt>MAX_INITIALISATIONS</tt> preference and then choose randomly); the order of operations in the B machine is thus important for -execute
* not store intermediate states in the state space; as such -execute is faster but after execution one only has access to the first state and the final state of execution

Example

probcli my.mch -execute 100

=== -execute_all===

See <tt>-execute <Nr></tt> above.

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -his command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command.

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -repl ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-print-loop
|}

Example

probcli my.mch -p CLPFD TRUE -repl

A list of commands can be obtained by typing <tt>:help</tt> (just help for versions 1.3.x of probcli). The interactive read-eval-print-loop can be exited using <tt>:q</tt> (just typing a return on a blank line for versions 1.3.x of probcli)..
If in addition you want see a graphical representation of the solutions found you can use the following command and open the <tt>out.dot</tt> file using dotty or GraphViz:
probcli -repl -evaldot ~/out.dot

You can also use the <tt>-eval</tt> command to evaluate specific formulas or expressions:
probcli -eval "1+2"
For convenience, these formulas can also be put into a separate file:
probcli -eval_file MyFormula.txt

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

You can also use the longer name for the command:

probcli my.mch -mc 1000 --coverage

There is also a version which prints a shorter summary (and which is much faster for large state spaces):

probcli my.mch -mc 1000 --coverage_summary

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -pref_group <PREFGROUP> <SETTING> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set to the group of preferences <PREFGROUP> to a predefined setting <SETTING>
|}

Example

probcli my.mch -pref_group model_check unlimited

Available groups and settings are:

* PREFERENCE GROUP integer : SETTINGS [int32] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set cardinality (scope in Alloy terminology) of a B deferred set. This overrides the default cardinality (which can be set using <tt>-p DEFAULT_SETSIZE <VAL></tt>).
|}

Example

probcli my.mch -card PID 5

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

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

=== -scope <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set SCOPE predicate for model checker; states which do not satisfy the SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed)
|}

Example

probcli my.mch -mc 10000000 -scope "n<18"

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -cache <DIRECTORY>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants (and in future also variables) to a file to avoid recomputation
|}

This commands saves the values of constants for the current B machine and puts those values into files in the specified directory. The command will also tell ProB to try and reuse constants saved for subsidiary machines (included using SEES for example) whenever possible.
The purpose of the command is to avoid recomputing constants as much as possible, as this can be very time consuming.
This also works for values of variables computed in the initialisation or even using operations.
However, we do not support refinements at the moment.

Note: this command can also be used when starting up the ProB Tcl/Tk version.

=== -logxml <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities and results of probcli in XML format in <LogFile>
|}

A schema declaration file (xsd) can be found at <tt>doc/logxml_xsd.xml</tt> in the ProB [[Download#Sourcecode|Prolog sources]].
The log file contains information about the various commands performed by probcli.
It also contains version information, the parameters provided to probcli and details about the errors that occured.

Example

probcli my.mch -mc 1000 -logxml log.xml

=== -logxml_write_vars <PREFIX> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| after processing other commands (such as -execute) write values of variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command)
|}

Example

probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile> using Prolog format
|}

Example

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

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

You can use <tt>probcli -version -v</tt> to obtain more information about your version of probcli.

=== -check_java_version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check Java and B parser version information
|}

This command is available as of ProB version 1.5.1-beta5 or higher. It can be useful to check that your Java is correctly installed and that the ProB B parser can operate correctly

probcli -check_java_version
Result of checking Java version:
Java is correctly installed and version 1.7.0_55-b13 is compatible with ProB requirements (>= 1.7).
ProB B Java Parser available in version: 2016-02-25 15:27:18.55.

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -property ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| virtually add predicate to PROPERTIES
|}

Example

probcli my.mch -property "PRED"

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch --model_check -save my_saved.P

=== -refchk <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space (e.g. using -save)
|}

Example

probcli my.mch -refchk abs_saved.P

=== -ref_check <MODE> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space (e.g. using -save) with particular failure/trace/divergence model
|}

MODE is one of F, FD, T, R, RD, SF, V.
Meaning of mode: F: Failures, FD: Failure-Divergences, R: Refusals, RD: Refusals-Divergences, SF: Singleton-Failures, T: Traces, V: Revival.
Default used by -refchck command above is T (traces model).

Example

probcli my.mch -ref_check F abstract_saved.P

=== -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 <Operation(s)>|-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'''.

As of version 1.6.0, the operation arguments are also written to the XML file.
The preference <tt>INTERNAL_ARGUMENT_PREFIX</tt> can be used to provide a prefix for internal operation arguments; any argument/parameter whose name starts with that prefix is considered an internal parameter and not shown in the trace file.
Also, as of version 1.6.0, the non-deterministic initialisations are shown in the XML trace file: all variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event.

=== -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 <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch -mc 100 -spdot my_statespace.dot

=== -cbc_tests <Depth> <EndPredicate> <File> ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''. If the predicate is the empty string we assume truth. If the filename is the empty string no file is generated. See also the page on [[Test_Case_Generation]].

=== -cbc_cover <Operation> ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma. You can also use the option <pre>-cbc_cover_match PartialName</pre> to match all operations whose name contains PartialName. See also the page about [[Test_Case_Generation]].

=== -test_description <File> ===
Read the options for constraint based test case generation from '''File'''.

=== -bmc <Depth> ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Run the [[Bounded_Model_Checking|bounded model checker]] until maximum trace depth <Depth> specified. Looks for invariant violations using the constraint-based test case generation algorithm.
|}

Example

probcli my.mch -bmc 20

=== -csp-guide <File> ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)
As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
DEFINITION (which also works in ProB2-UI).

=== -rule_report <File> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Generates rule validation report for rules machines (.rmch) at the specified location <File> for the current animation state. Depending on the file extension an HTML or an XML version of the report is generated (.html/.xml).
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.rmch -execute_all -rule_report my_report.html

=== -machine_files_sha ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Computes SHA1 hash of all B files used by a B model.
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.mch -machine_files_sha

=== -check_machine_file_sha ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Compute and check SHA1 hash of a particular B file used by the main B model.
|}

probcli ./Demo/scheduler.mch -check_machine_file_sha scheduler.mch 1cab7ec89adc9f9b153af85c1ae16ba8a7a2a661

== Environment Variables ==

Set NO_COLOR environment variable to disable terminal colors.
See [https://no-color.org https://no-color.org].

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <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. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants 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
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| 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, is multiplied by a factor for other computations)
|-
| PROOF_INFO
| bool ==> Use Proof Information to restrict invariant checking to affected unproven clauses. Most useful in EventB for models exported from Rodin.
|-
| 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 (use 0 to disable expansion)
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| 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 analyzing assertions or properties
|-
| 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)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|-
| CSE
| bool ==> Perform common-sub-expression elimination
|-
| CSE_SUBST
| bool ==> Perform common-sub-expression elimination also for B substitutions
|}

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:
<pre>
probcli -init My.mch
</pre>
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:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To fully model check a specification M.mch while tryining to minimize memory consumption do:
<pre>
probcli -model_check -p COMPRESSION TRUE M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption further by not storing processed stats and using symmetry reduction (and accepting hash collisions) do:
<pre>
probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
</pre>

== 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.
{{Feedback}}

Using the Command-Line Version of ProB

2025-12-24T07:24:00Z

Michael Leuschel: /* -refchk */

[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:ProB Cli]]

The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.6 of ProB. Some features are only available in the nightly build of ProB. You can run <tt>probcli –help</tt> to find out which commands are supported by your version of ProB. For Bash users we provide [[Bash Completion|command completion]] support.

Note: the order of commands is not relevant for <tt>probcli</tt> (except within groups of commands such as <tt>-p MAXINT 127</tt>). Any argument that is not recognised by <tt>probcli</tt> is treated as a filename to be analysed.

[[file:ProBTerminalizerDemo.gif|center||600px]]

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

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

The underscore within all options can as of version 1.5.1-beta7 be replaced with dashes. Also, all commands can either be typed with single leading dashes or double leading dashes.
For example, all of the following commands have the same effect:
probcli M.mch -model_check
probcli M.mch -model-check
probcli M.mch --model_check
probcli M.mch --model-check

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options <tt>-nodead, -noinv, -nogoal, -noass</tt> to influence which kinds of errors are reported by <tt>-mc</tt>.
You can also set a target goal predicate using the <tt>-goal "PRED"</tt> command and limit the scope of the model checking using the <tt>-scope "PRED"</tt> command.

=== -model_check ===

The same as <tt>-mc</tt> but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking (-mc), TLC model checking (-mc_with_tlc), animation (-animate) and execution (-execute) 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

=== -disable_timeout ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| turn off ProB's timeout mechanism, e.g., for computing enabled operations and invariant checking; this can sometimes speed up model checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7.
|}

Example

probcli my.mch -model-check -disable-timeout

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first during model checking
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first during model checking
|}

Example

probcli my.mch -df -mc 1000

=== -mc_mode <M> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| influence how the model checker proceeds. Available as of version 1.5.1. Supersedes the <tt>-df</tt> and <tt>-bf</tt> switches.
Possible values for the mode <M> are: <ul>
<li><tt>df</tt> (depth-first traversal),</li>
<li><tt>bf</tt> (breadth-first traversal),</li>
<li><tt>mixed</tt> (mixed depth-first / breadth-first traversal with random choice; currently the default),</li>
<li><tt>random</tt> (choosing next node to process completely at random), </li>
<li><tt>hash</tt> (similar to random, but uses the Prolog hash function of a node instead of a random number generator),</li>
<li><tt>heuristic</tt> (try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause). Some explanations can be found [[Blocks_World_(Directed_Model_Checking)|in an example about directed model checking]].</li>
<li><tt>out_degree_hash</tt> (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking)
</ul>
|}

Example

probcli my.mch -model_check -mc_mode random

=== --timeout <N> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global timeout 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>. Note that the <tt>TIME_OUT</tt> preference also influences other computations, such as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -trace_replay <KIND> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Replay a trace file in the given format (json,prolog,B).
|}

KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
Example

probcli my.mch -trace_replay json my.prob2trace

Alternative command -det_trace_replay KIND FILE.

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -cbc_assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based checking of assertions on constants
|}
This will try and find a solution for the constants which make an assertion (on constants) false.

You can use the extra command <tt>-cbc_output_file FILE</tt> to write the result of this check to a file.
You can also use the extra command <tt>-cbc_option contradiction_check</tt> to ask ProB to check if there is a contradiction in the properties (in case the check did not find a counter-example to the assertions). The extra command <tt>-cbc_option unsat_core</tt> tells ProB to compute the unsatisfiable core in case a proof the assertions was found.
Note that the <tt>TIME_OUT</tt> preference is multiplied by 10 for this command.

There are various variations of this command:
-cbc_assertions_proof
-cbc_assertions_tautology_proof
Both commands do not allow enumeration warnings to occur.
The latter command ignores the PROPERTIES and tries to check whether the ASSERTION(s) are tautologies.
Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3).

=== -cbc_sequence <SEQ> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based searching for a sequence of operation names (separated by semicolons)
|}
This will try and find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible.

Example

probcli my.mch -cbc_sequence "op1;op2"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error and stop probcli if anything unexpected happens, e.g., if model checking finds a counter example or trace checking fails or any unexpected error happens
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

Variations
-animate_all : animate until deadlock reached
-animate_until_ltl P : animate until LTL property holds on trace
-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

=== -execute <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| execution (max Nr steps)
|}

Executes the "first" enabled operation of a machine, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-execute_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-execute_all</tt> could run forever.

In contrast to -animate, -execute will
* always choose the first enabled operation it finds and stop searching for further enabled operations in that state (-animate will compute all enabled operations up to the limit set by the <tt>MAX_OPERATIONS</tt> or <tt>MAX_INITIALISATIONS</tt> preference and then choose randomly); the order of operations in the B machine is thus important for -execute
* not store intermediate states in the state space; as such -execute is faster but after execution one only has access to the first state and the final state of execution

Example

probcli my.mch -execute 100

=== -execute_all===

See <tt>-execute <Nr></tt> above.

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -his command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command.

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -repl ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-print-loop
|}

Example

probcli my.mch -p CLPFD TRUE -repl

A list of commands can be obtained by typing <tt>:help</tt> (just help for versions 1.3.x of probcli). The interactive read-eval-print-loop can be exited using <tt>:q</tt> (just typing a return on a blank line for versions 1.3.x of probcli)..
If in addition you want see a graphical representation of the solutions found you can use the following command and open the <tt>out.dot</tt> file using dotty or GraphViz:
probcli -repl -evaldot ~/out.dot

You can also use the <tt>-eval</tt> command to evaluate specific formulas or expressions:
probcli -eval "1+2"
For convenience, these formulas can also be put into a separate file:
probcli -eval_file MyFormula.txt

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

You can also use the longer name for the command:

probcli my.mch -mc 1000 --coverage

There is also a version which prints a shorter summary (and which is much faster for large state spaces):

probcli my.mch -mc 1000 --coverage_summary

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -pref_group <PREFGROUP> <SETTING> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set to the group of preferences <PREFGROUP> to a predefined setting <SETTING>
|}

Example

probcli my.mch -pref_group model_check unlimited

Available groups and settings are:

* PREFERENCE GROUP integer : SETTINGS [int32] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set cardinality (scope in Alloy terminology) of a B deferred set. This overrides the default cardinality (which can be set using <tt>-p DEFAULT_SETSIZE <VAL></tt>).
|}

Example

probcli my.mch -card PID 5

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

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

=== -scope <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set SCOPE predicate for model checker; states which do not satisfy the SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed)
|}

Example

probcli my.mch -mc 10000000 -scope "n<18"

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -cache <DIRECTORY>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants (and in future also variables) to a file to avoid recomputation
|}

This commands saves the values of constants for the current B machine and puts those values into files in the specified directory. The command will also tell ProB to try and reuse constants saved for subsidiary machines (included using SEES for example) whenever possible.
The purpose of the command is to avoid recomputing constants as much as possible, as this can be very time consuming.
This also works for values of variables computed in the initialisation or even using operations.
However, we do not support refinements at the moment.

Note: this command can also be used when starting up the ProB Tcl/Tk version.

=== -logxml <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities and results of probcli in XML format in <LogFile>
|}

A schema declaration file (xsd) can be found at <tt>doc/logxml_xsd.xml</tt> in the ProB [[Download#Sourcecode|Prolog sources]].
The log file contains information about the various commands performed by probcli.
It also contains version information, the parameters provided to probcli and details about the errors that occured.

Example

probcli my.mch -mc 1000 -logxml log.xml

=== -logxml_write_vars <PREFIX> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| after processing other commands (such as -execute) write values of variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command)
|}

Example

probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile> using Prolog format
|}

Example

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

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

You can use <tt>probcli -version -v</tt> to obtain more information about your version of probcli.

=== -check_java_version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check Java and B parser version information
|}

This command is available as of ProB version 1.5.1-beta5 or higher. It can be useful to check that your Java is correctly installed and that the ProB B parser can operate correctly

probcli -check_java_version
Result of checking Java version:
Java is correctly installed and version 1.7.0_55-b13 is compatible with ProB requirements (>= 1.7).
ProB B Java Parser available in version: 2016-02-25 15:27:18.55.

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -property ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| virtually add predicate to PROPERTIES
|}

Example

probcli my.mch -property "PRED"

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch --model_check -save my_saved.P

=== -refchk <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space (e.g. using -save)
|}

Example

probcli my.mch -refchk abs_saved.P

=== -ref_check <MODE> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space using provide
|}

MODE is one of F, FD, T, R, RD, V, VD.
Default used by -refchck command above is T (traces model).

Example

probcli my.mch -ref_check F abstract_saved.P

=== -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 <Operation(s)>|-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'''.

As of version 1.6.0, the operation arguments are also written to the XML file.
The preference <tt>INTERNAL_ARGUMENT_PREFIX</tt> can be used to provide a prefix for internal operation arguments; any argument/parameter whose name starts with that prefix is considered an internal parameter and not shown in the trace file.
Also, as of version 1.6.0, the non-deterministic initialisations are shown in the XML trace file: all variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event.

=== -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 <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch -mc 100 -spdot my_statespace.dot

=== -cbc_tests <Depth> <EndPredicate> <File> ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''. If the predicate is the empty string we assume truth. If the filename is the empty string no file is generated. See also the page on [[Test_Case_Generation]].

=== -cbc_cover <Operation> ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma. You can also use the option <pre>-cbc_cover_match PartialName</pre> to match all operations whose name contains PartialName. See also the page about [[Test_Case_Generation]].

=== -test_description <File> ===
Read the options for constraint based test case generation from '''File'''.

=== -bmc <Depth> ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Run the [[Bounded_Model_Checking|bounded model checker]] until maximum trace depth <Depth> specified. Looks for invariant violations using the constraint-based test case generation algorithm.
|}

Example

probcli my.mch -bmc 20

=== -csp-guide <File> ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)
As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
DEFINITION (which also works in ProB2-UI).

=== -rule_report <File> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Generates rule validation report for rules machines (.rmch) at the specified location <File> for the current animation state. Depending on the file extension an HTML or an XML version of the report is generated (.html/.xml).
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.rmch -execute_all -rule_report my_report.html

=== -machine_files_sha ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Computes SHA1 hash of all B files used by a B model.
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.mch -machine_files_sha

=== -check_machine_file_sha ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Compute and check SHA1 hash of a particular B file used by the main B model.
|}

probcli ./Demo/scheduler.mch -check_machine_file_sha scheduler.mch 1cab7ec89adc9f9b153af85c1ae16ba8a7a2a661

== Environment Variables ==

Set NO_COLOR environment variable to disable terminal colors.
See [https://no-color.org https://no-color.org].

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <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. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants 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
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| 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, is multiplied by a factor for other computations)
|-
| PROOF_INFO
| bool ==> Use Proof Information to restrict invariant checking to affected unproven clauses. Most useful in EventB for models exported from Rodin.
|-
| 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 (use 0 to disable expansion)
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| 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 analyzing assertions or properties
|-
| 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)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|-
| CSE
| bool ==> Perform common-sub-expression elimination
|-
| CSE_SUBST
| bool ==> Perform common-sub-expression elimination also for B substitutions
|}

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:
<pre>
probcli -init My.mch
</pre>
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:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To fully model check a specification M.mch while tryining to minimize memory consumption do:
<pre>
probcli -model_check -p COMPRESSION TRUE M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption further by not storing processed stats and using symmetry reduction (and accepting hash collisions) do:
<pre>
probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
</pre>

== 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.
{{Feedback}}

Using the Command-Line Version of ProB

2025-12-24T07:23:36Z

Michael Leuschel: /* -save */

[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:ProB Cli]]

The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.6 of ProB. Some features are only available in the nightly build of ProB. You can run <tt>probcli –help</tt> to find out which commands are supported by your version of ProB. For Bash users we provide [[Bash Completion|command completion]] support.

Note: the order of commands is not relevant for <tt>probcli</tt> (except within groups of commands such as <tt>-p MAXINT 127</tt>). Any argument that is not recognised by <tt>probcli</tt> is treated as a filename to be analysed.

[[file:ProBTerminalizerDemo.gif|center||600px]]

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

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

The underscore within all options can as of version 1.5.1-beta7 be replaced with dashes. Also, all commands can either be typed with single leading dashes or double leading dashes.
For example, all of the following commands have the same effect:
probcli M.mch -model_check
probcli M.mch -model-check
probcli M.mch --model_check
probcli M.mch --model-check

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options <tt>-nodead, -noinv, -nogoal, -noass</tt> to influence which kinds of errors are reported by <tt>-mc</tt>.
You can also set a target goal predicate using the <tt>-goal "PRED"</tt> command and limit the scope of the model checking using the <tt>-scope "PRED"</tt> command.

=== -model_check ===

The same as <tt>-mc</tt> but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking (-mc), TLC model checking (-mc_with_tlc), animation (-animate) and execution (-execute) 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

=== -disable_timeout ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| turn off ProB's timeout mechanism, e.g., for computing enabled operations and invariant checking; this can sometimes speed up model checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7.
|}

Example

probcli my.mch -model-check -disable-timeout

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first during model checking
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first during model checking
|}

Example

probcli my.mch -df -mc 1000

=== -mc_mode <M> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| influence how the model checker proceeds. Available as of version 1.5.1. Supersedes the <tt>-df</tt> and <tt>-bf</tt> switches.
Possible values for the mode <M> are: <ul>
<li><tt>df</tt> (depth-first traversal),</li>
<li><tt>bf</tt> (breadth-first traversal),</li>
<li><tt>mixed</tt> (mixed depth-first / breadth-first traversal with random choice; currently the default),</li>
<li><tt>random</tt> (choosing next node to process completely at random), </li>
<li><tt>hash</tt> (similar to random, but uses the Prolog hash function of a node instead of a random number generator),</li>
<li><tt>heuristic</tt> (try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause). Some explanations can be found [[Blocks_World_(Directed_Model_Checking)|in an example about directed model checking]].</li>
<li><tt>out_degree_hash</tt> (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking)
</ul>
|}

Example

probcli my.mch -model_check -mc_mode random

=== --timeout <N> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global timeout 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>. Note that the <tt>TIME_OUT</tt> preference also influences other computations, such as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -trace_replay <KIND> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Replay a trace file in the given format (json,prolog,B).
|}

KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
Example

probcli my.mch -trace_replay json my.prob2trace

Alternative command -det_trace_replay KIND FILE.

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -cbc_assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based checking of assertions on constants
|}
This will try and find a solution for the constants which make an assertion (on constants) false.

You can use the extra command <tt>-cbc_output_file FILE</tt> to write the result of this check to a file.
You can also use the extra command <tt>-cbc_option contradiction_check</tt> to ask ProB to check if there is a contradiction in the properties (in case the check did not find a counter-example to the assertions). The extra command <tt>-cbc_option unsat_core</tt> tells ProB to compute the unsatisfiable core in case a proof the assertions was found.
Note that the <tt>TIME_OUT</tt> preference is multiplied by 10 for this command.

There are various variations of this command:
-cbc_assertions_proof
-cbc_assertions_tautology_proof
Both commands do not allow enumeration warnings to occur.
The latter command ignores the PROPERTIES and tries to check whether the ASSERTION(s) are tautologies.
Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3).

=== -cbc_sequence <SEQ> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based searching for a sequence of operation names (separated by semicolons)
|}
This will try and find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible.

Example

probcli my.mch -cbc_sequence "op1;op2"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error and stop probcli if anything unexpected happens, e.g., if model checking finds a counter example or trace checking fails or any unexpected error happens
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

Variations
-animate_all : animate until deadlock reached
-animate_until_ltl P : animate until LTL property holds on trace
-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

=== -execute <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| execution (max Nr steps)
|}

Executes the "first" enabled operation of a machine, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-execute_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-execute_all</tt> could run forever.

In contrast to -animate, -execute will
* always choose the first enabled operation it finds and stop searching for further enabled operations in that state (-animate will compute all enabled operations up to the limit set by the <tt>MAX_OPERATIONS</tt> or <tt>MAX_INITIALISATIONS</tt> preference and then choose randomly); the order of operations in the B machine is thus important for -execute
* not store intermediate states in the state space; as such -execute is faster but after execution one only has access to the first state and the final state of execution

Example

probcli my.mch -execute 100

=== -execute_all===

See <tt>-execute <Nr></tt> above.

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -his command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command.

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -repl ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-print-loop
|}

Example

probcli my.mch -p CLPFD TRUE -repl

A list of commands can be obtained by typing <tt>:help</tt> (just help for versions 1.3.x of probcli). The interactive read-eval-print-loop can be exited using <tt>:q</tt> (just typing a return on a blank line for versions 1.3.x of probcli)..
If in addition you want see a graphical representation of the solutions found you can use the following command and open the <tt>out.dot</tt> file using dotty or GraphViz:
probcli -repl -evaldot ~/out.dot

You can also use the <tt>-eval</tt> command to evaluate specific formulas or expressions:
probcli -eval "1+2"
For convenience, these formulas can also be put into a separate file:
probcli -eval_file MyFormula.txt

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

You can also use the longer name for the command:

probcli my.mch -mc 1000 --coverage

There is also a version which prints a shorter summary (and which is much faster for large state spaces):

probcli my.mch -mc 1000 --coverage_summary

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -pref_group <PREFGROUP> <SETTING> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set to the group of preferences <PREFGROUP> to a predefined setting <SETTING>
|}

Example

probcli my.mch -pref_group model_check unlimited

Available groups and settings are:

* PREFERENCE GROUP integer : SETTINGS [int32] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set cardinality (scope in Alloy terminology) of a B deferred set. This overrides the default cardinality (which can be set using <tt>-p DEFAULT_SETSIZE <VAL></tt>).
|}

Example

probcli my.mch -card PID 5

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

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

=== -scope <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set SCOPE predicate for model checker; states which do not satisfy the SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed)
|}

Example

probcli my.mch -mc 10000000 -scope "n<18"

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -cache <DIRECTORY>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants (and in future also variables) to a file to avoid recomputation
|}

This commands saves the values of constants for the current B machine and puts those values into files in the specified directory. The command will also tell ProB to try and reuse constants saved for subsidiary machines (included using SEES for example) whenever possible.
The purpose of the command is to avoid recomputing constants as much as possible, as this can be very time consuming.
This also works for values of variables computed in the initialisation or even using operations.
However, we do not support refinements at the moment.

Note: this command can also be used when starting up the ProB Tcl/Tk version.

=== -logxml <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities and results of probcli in XML format in <LogFile>
|}

A schema declaration file (xsd) can be found at <tt>doc/logxml_xsd.xml</tt> in the ProB [[Download#Sourcecode|Prolog sources]].
The log file contains information about the various commands performed by probcli.
It also contains version information, the parameters provided to probcli and details about the errors that occured.

Example

probcli my.mch -mc 1000 -logxml log.xml

=== -logxml_write_vars <PREFIX> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| after processing other commands (such as -execute) write values of variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command)
|}

Example

probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile> using Prolog format
|}

Example

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

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

You can use <tt>probcli -version -v</tt> to obtain more information about your version of probcli.

=== -check_java_version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check Java and B parser version information
|}

This command is available as of ProB version 1.5.1-beta5 or higher. It can be useful to check that your Java is correctly installed and that the ProB B parser can operate correctly

probcli -check_java_version
Result of checking Java version:
Java is correctly installed and version 1.7.0_55-b13 is compatible with ProB requirements (>= 1.7).
ProB B Java Parser available in version: 2016-02-25 15:27:18.55.

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -property ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| virtually add predicate to PROPERTIES
|}

Example

probcli my.mch -property "PRED"

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch --model_check -save my_saved.P

=== -refchk <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space
|}

Example

probcli my.mch -refchk abs_saved.P

=== -ref_check <MODE> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space using provide
|}

MODE is one of F, FD, T, R, RD, V, VD.
Default used by -refchck command above is T (traces model).

Example

probcli my.mch -ref_check F abstract_saved.P

=== -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 <Operation(s)>|-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'''.

As of version 1.6.0, the operation arguments are also written to the XML file.
The preference <tt>INTERNAL_ARGUMENT_PREFIX</tt> can be used to provide a prefix for internal operation arguments; any argument/parameter whose name starts with that prefix is considered an internal parameter and not shown in the trace file.
Also, as of version 1.6.0, the non-deterministic initialisations are shown in the XML trace file: all variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event.

=== -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 <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch -mc 100 -spdot my_statespace.dot

=== -cbc_tests <Depth> <EndPredicate> <File> ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''. If the predicate is the empty string we assume truth. If the filename is the empty string no file is generated. See also the page on [[Test_Case_Generation]].

=== -cbc_cover <Operation> ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma. You can also use the option <pre>-cbc_cover_match PartialName</pre> to match all operations whose name contains PartialName. See also the page about [[Test_Case_Generation]].

=== -test_description <File> ===
Read the options for constraint based test case generation from '''File'''.

=== -bmc <Depth> ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Run the [[Bounded_Model_Checking|bounded model checker]] until maximum trace depth <Depth> specified. Looks for invariant violations using the constraint-based test case generation algorithm.
|}

Example

probcli my.mch -bmc 20

=== -csp-guide <File> ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)
As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
DEFINITION (which also works in ProB2-UI).

=== -rule_report <File> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Generates rule validation report for rules machines (.rmch) at the specified location <File> for the current animation state. Depending on the file extension an HTML or an XML version of the report is generated (.html/.xml).
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.rmch -execute_all -rule_report my_report.html

=== -machine_files_sha ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Computes SHA1 hash of all B files used by a B model.
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.mch -machine_files_sha

=== -check_machine_file_sha ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Compute and check SHA1 hash of a particular B file used by the main B model.
|}

probcli ./Demo/scheduler.mch -check_machine_file_sha scheduler.mch 1cab7ec89adc9f9b153af85c1ae16ba8a7a2a661

== Environment Variables ==

Set NO_COLOR environment variable to disable terminal colors.
See [https://no-color.org https://no-color.org].

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <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. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants 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
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| 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, is multiplied by a factor for other computations)
|-
| PROOF_INFO
| bool ==> Use Proof Information to restrict invariant checking to affected unproven clauses. Most useful in EventB for models exported from Rodin.
|-
| 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 (use 0 to disable expansion)
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| 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 analyzing assertions or properties
|-
| 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)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|-
| CSE
| bool ==> Perform common-sub-expression elimination
|-
| CSE_SUBST
| bool ==> Perform common-sub-expression elimination also for B substitutions
|}

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:
<pre>
probcli -init My.mch
</pre>
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:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To fully model check a specification M.mch while tryining to minimize memory consumption do:
<pre>
probcli -model_check -p COMPRESSION TRUE M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption further by not storing processed stats and using symmetry reduction (and accepting hash collisions) do:
<pre>
probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
</pre>

== 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.
{{Feedback}}

Using the Command-Line Version of ProB

2025-12-24T07:22:31Z

Michael Leuschel: /* -refchk */

[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:ProB Cli]]

The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.6 of ProB. Some features are only available in the nightly build of ProB. You can run <tt>probcli –help</tt> to find out which commands are supported by your version of ProB. For Bash users we provide [[Bash Completion|command completion]] support.

Note: the order of commands is not relevant for <tt>probcli</tt> (except within groups of commands such as <tt>-p MAXINT 127</tt>). Any argument that is not recognised by <tt>probcli</tt> is treated as a filename to be analysed.

[[file:ProBTerminalizerDemo.gif|center||600px]]

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

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

The underscore within all options can as of version 1.5.1-beta7 be replaced with dashes. Also, all commands can either be typed with single leading dashes or double leading dashes.
For example, all of the following commands have the same effect:
probcli M.mch -model_check
probcli M.mch -model-check
probcli M.mch --model_check
probcli M.mch --model-check

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options <tt>-nodead, -noinv, -nogoal, -noass</tt> to influence which kinds of errors are reported by <tt>-mc</tt>.
You can also set a target goal predicate using the <tt>-goal "PRED"</tt> command and limit the scope of the model checking using the <tt>-scope "PRED"</tt> command.

=== -model_check ===

The same as <tt>-mc</tt> but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking (-mc), TLC model checking (-mc_with_tlc), animation (-animate) and execution (-execute) 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

=== -disable_timeout ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| turn off ProB's timeout mechanism, e.g., for computing enabled operations and invariant checking; this can sometimes speed up model checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7.
|}

Example

probcli my.mch -model-check -disable-timeout

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first during model checking
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first during model checking
|}

Example

probcli my.mch -df -mc 1000

=== -mc_mode <M> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| influence how the model checker proceeds. Available as of version 1.5.1. Supersedes the <tt>-df</tt> and <tt>-bf</tt> switches.
Possible values for the mode <M> are: <ul>
<li><tt>df</tt> (depth-first traversal),</li>
<li><tt>bf</tt> (breadth-first traversal),</li>
<li><tt>mixed</tt> (mixed depth-first / breadth-first traversal with random choice; currently the default),</li>
<li><tt>random</tt> (choosing next node to process completely at random), </li>
<li><tt>hash</tt> (similar to random, but uses the Prolog hash function of a node instead of a random number generator),</li>
<li><tt>heuristic</tt> (try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause). Some explanations can be found [[Blocks_World_(Directed_Model_Checking)|in an example about directed model checking]].</li>
<li><tt>out_degree_hash</tt> (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking)
</ul>
|}

Example

probcli my.mch -model_check -mc_mode random

=== --timeout <N> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global timeout 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>. Note that the <tt>TIME_OUT</tt> preference also influences other computations, such as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -trace_replay <KIND> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Replay a trace file in the given format (json,prolog,B).
|}

KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
Example

probcli my.mch -trace_replay json my.prob2trace

Alternative command -det_trace_replay KIND FILE.

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -cbc_assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based checking of assertions on constants
|}
This will try and find a solution for the constants which make an assertion (on constants) false.

You can use the extra command <tt>-cbc_output_file FILE</tt> to write the result of this check to a file.
You can also use the extra command <tt>-cbc_option contradiction_check</tt> to ask ProB to check if there is a contradiction in the properties (in case the check did not find a counter-example to the assertions). The extra command <tt>-cbc_option unsat_core</tt> tells ProB to compute the unsatisfiable core in case a proof the assertions was found.
Note that the <tt>TIME_OUT</tt> preference is multiplied by 10 for this command.

There are various variations of this command:
-cbc_assertions_proof
-cbc_assertions_tautology_proof
Both commands do not allow enumeration warnings to occur.
The latter command ignores the PROPERTIES and tries to check whether the ASSERTION(s) are tautologies.
Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3).

=== -cbc_sequence <SEQ> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based searching for a sequence of operation names (separated by semicolons)
|}
This will try and find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible.

Example

probcli my.mch -cbc_sequence "op1;op2"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error and stop probcli if anything unexpected happens, e.g., if model checking finds a counter example or trace checking fails or any unexpected error happens
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

Variations
-animate_all : animate until deadlock reached
-animate_until_ltl P : animate until LTL property holds on trace
-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

=== -execute <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| execution (max Nr steps)
|}

Executes the "first" enabled operation of a machine, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-execute_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-execute_all</tt> could run forever.

In contrast to -animate, -execute will
* always choose the first enabled operation it finds and stop searching for further enabled operations in that state (-animate will compute all enabled operations up to the limit set by the <tt>MAX_OPERATIONS</tt> or <tt>MAX_INITIALISATIONS</tt> preference and then choose randomly); the order of operations in the B machine is thus important for -execute
* not store intermediate states in the state space; as such -execute is faster but after execution one only has access to the first state and the final state of execution

Example

probcli my.mch -execute 100

=== -execute_all===

See <tt>-execute <Nr></tt> above.

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -his command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command.

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -repl ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-print-loop
|}

Example

probcli my.mch -p CLPFD TRUE -repl

A list of commands can be obtained by typing <tt>:help</tt> (just help for versions 1.3.x of probcli). The interactive read-eval-print-loop can be exited using <tt>:q</tt> (just typing a return on a blank line for versions 1.3.x of probcli)..
If in addition you want see a graphical representation of the solutions found you can use the following command and open the <tt>out.dot</tt> file using dotty or GraphViz:
probcli -repl -evaldot ~/out.dot

You can also use the <tt>-eval</tt> command to evaluate specific formulas or expressions:
probcli -eval "1+2"
For convenience, these formulas can also be put into a separate file:
probcli -eval_file MyFormula.txt

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

You can also use the longer name for the command:

probcli my.mch -mc 1000 --coverage

There is also a version which prints a shorter summary (and which is much faster for large state spaces):

probcli my.mch -mc 1000 --coverage_summary

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -pref_group <PREFGROUP> <SETTING> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set to the group of preferences <PREFGROUP> to a predefined setting <SETTING>
|}

Example

probcli my.mch -pref_group model_check unlimited

Available groups and settings are:

* PREFERENCE GROUP integer : SETTINGS [int32] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set cardinality (scope in Alloy terminology) of a B deferred set. This overrides the default cardinality (which can be set using <tt>-p DEFAULT_SETSIZE <VAL></tt>).
|}

Example

probcli my.mch -card PID 5

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

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

=== -scope <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set SCOPE predicate for model checker; states which do not satisfy the SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed)
|}

Example

probcli my.mch -mc 10000000 -scope "n<18"

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -cache <DIRECTORY>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants (and in future also variables) to a file to avoid recomputation
|}

This commands saves the values of constants for the current B machine and puts those values into files in the specified directory. The command will also tell ProB to try and reuse constants saved for subsidiary machines (included using SEES for example) whenever possible.
The purpose of the command is to avoid recomputing constants as much as possible, as this can be very time consuming.
This also works for values of variables computed in the initialisation or even using operations.
However, we do not support refinements at the moment.

Note: this command can also be used when starting up the ProB Tcl/Tk version.

=== -logxml <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities and results of probcli in XML format in <LogFile>
|}

A schema declaration file (xsd) can be found at <tt>doc/logxml_xsd.xml</tt> in the ProB [[Download#Sourcecode|Prolog sources]].
The log file contains information about the various commands performed by probcli.
It also contains version information, the parameters provided to probcli and details about the errors that occured.

Example

probcli my.mch -mc 1000 -logxml log.xml

=== -logxml_write_vars <PREFIX> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| after processing other commands (such as -execute) write values of variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command)
|}

Example

probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile> using Prolog format
|}

Example

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

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

You can use <tt>probcli -version -v</tt> to obtain more information about your version of probcli.

=== -check_java_version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check Java and B parser version information
|}

This command is available as of ProB version 1.5.1-beta5 or higher. It can be useful to check that your Java is correctly installed and that the ProB B parser can operate correctly

probcli -check_java_version
Result of checking Java version:
Java is correctly installed and version 1.7.0_55-b13 is compatible with ProB requirements (>= 1.7).
ProB B Java Parser available in version: 2016-02-25 15:27:18.55.

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -property ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| virtually add predicate to PROPERTIES
|}

Example

probcli my.mch -property "PRED"

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch ...

=== -refchk <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space
|}

Example

probcli my.mch -refchk abs_saved.P

=== -ref_check <MODE> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| refinement check against previous saved state space using provide
|}

MODE is one of F, FD, T, R, RD, V, VD.
Default used by -refchck command above is T (traces model).

Example

probcli my.mch -ref_check F abstract_saved.P

=== -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 <Operation(s)>|-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'''.

As of version 1.6.0, the operation arguments are also written to the XML file.
The preference <tt>INTERNAL_ARGUMENT_PREFIX</tt> can be used to provide a prefix for internal operation arguments; any argument/parameter whose name starts with that prefix is considered an internal parameter and not shown in the trace file.
Also, as of version 1.6.0, the non-deterministic initialisations are shown in the XML trace file: all variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event.

=== -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 <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch -mc 100 -spdot my_statespace.dot

=== -cbc_tests <Depth> <EndPredicate> <File> ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''. If the predicate is the empty string we assume truth. If the filename is the empty string no file is generated. See also the page on [[Test_Case_Generation]].

=== -cbc_cover <Operation> ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma. You can also use the option <pre>-cbc_cover_match PartialName</pre> to match all operations whose name contains PartialName. See also the page about [[Test_Case_Generation]].

=== -test_description <File> ===
Read the options for constraint based test case generation from '''File'''.

=== -bmc <Depth> ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Run the [[Bounded_Model_Checking|bounded model checker]] until maximum trace depth <Depth> specified. Looks for invariant violations using the constraint-based test case generation algorithm.
|}

Example

probcli my.mch -bmc 20

=== -csp-guide <File> ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)
As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
DEFINITION (which also works in ProB2-UI).

=== -rule_report <File> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Generates rule validation report for rules machines (.rmch) at the specified location <File> for the current animation state. Depending on the file extension an HTML or an XML version of the report is generated (.html/.xml).
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.rmch -execute_all -rule_report my_report.html

=== -machine_files_sha ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Computes SHA1 hash of all B files used by a B model.
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.mch -machine_files_sha

=== -check_machine_file_sha ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Compute and check SHA1 hash of a particular B file used by the main B model.
|}

probcli ./Demo/scheduler.mch -check_machine_file_sha scheduler.mch 1cab7ec89adc9f9b153af85c1ae16ba8a7a2a661

== Environment Variables ==

Set NO_COLOR environment variable to disable terminal colors.
See [https://no-color.org https://no-color.org].

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <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. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants 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
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| 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, is multiplied by a factor for other computations)
|-
| PROOF_INFO
| bool ==> Use Proof Information to restrict invariant checking to affected unproven clauses. Most useful in EventB for models exported from Rodin.
|-
| 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 (use 0 to disable expansion)
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| 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 analyzing assertions or properties
|-
| 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)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|-
| CSE
| bool ==> Perform common-sub-expression elimination
|-
| CSE_SUBST
| bool ==> Perform common-sub-expression elimination also for B substitutions
|}

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:
<pre>
probcli -init My.mch
</pre>
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:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To fully model check a specification M.mch while tryining to minimize memory consumption do:
<pre>
probcli -model_check -p COMPRESSION TRUE M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption further by not storing processed stats and using symmetry reduction (and accepting hash collisions) do:
<pre>
probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
</pre>

== 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.
{{Feedback}}

Using the Command-Line Version of ProB

2025-12-23T15:56:55Z

Michael Leuschel: /* -animate */

[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:ProB Cli]]

The command-line version of ProB, called probcli, offers many of the features of the standalone Tcl/Tk Version via the command-line. As such, you can run ProB from your shell scripts or in your Makefiles.
These pages refer to version 1.6 of ProB. Some features are only available in the nightly build of ProB. You can run <tt>probcli –help</tt> to find out which commands are supported by your version of ProB. For Bash users we provide [[Bash Completion|command completion]] support.

Note: the order of commands is not relevant for <tt>probcli</tt> (except within groups of commands such as <tt>-p MAXINT 127</tt>). Any argument that is not recognised by <tt>probcli</tt> is treated as a filename to be analysed.

[[file:ProBTerminalizerDemo.gif|center||600px]]

== Conventions used ==

The following conventions are used in this guide:

{| cellpadding="10"
| valign="top" | <replaceme>
| All values that should be replaced with some value are shown withing < >
|-
| valign="top" | line breaks
| Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
|}

== Synopsis ==

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

The underscore within all options can as of version 1.5.1-beta7 be replaced with dashes. Also, all commands can either be typed with single leading dashes or double leading dashes.
For example, all of the following commands have the same effect:
probcli M.mch -model_check
probcli M.mch -model-check
probcli M.mch --model_check
probcli M.mch --model-check

== Options ==

=== -mc <nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| model check; checking at most <nr> states
|}

Example

probcli my.mch -mc 100

Note: with a value of nr=1 ProB will only inspect the "virtual" root node (and compute its outgoing transitions).
Also see the related options <tt>-nodead, -noinv, -nogoal, -noass</tt> to influence which kinds of errors are reported by <tt>-mc</tt>.
You can also set a target goal predicate using the <tt>-goal "PRED"</tt> command and limit the scope of the model checking using the <tt>-scope "PRED"</tt> command.

=== -model_check ===

The same as <tt>-mc</tt> but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.

=== -no<x> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| restrict errors reported by model checking (-mc), TLC model checking (-mc_with_tlc), animation (-animate) and execution (-execute) 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

=== -disable_timeout ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| turn off ProB's timeout mechanism, e.g., for computing enabled operations and invariant checking; this can sometimes speed up model checking (-mc or -model_check) and animation (-animate). Available as of version 1.5.1-beta7.
|}

Example

probcli my.mch -model-check -disable-timeout

=== -bf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed breadth-first during model checking
|}

Example

probcli my.mch -bf -mc 1000

=== -df ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| proceed depth-first during model checking
|}

Example

probcli my.mch -df -mc 1000

=== -mc_mode <M> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| influence how the model checker proceeds. Available as of version 1.5.1. Supersedes the <tt>-df</tt> and <tt>-bf</tt> switches.
Possible values for the mode <M> are: <ul>
<li><tt>df</tt> (depth-first traversal),</li>
<li><tt>bf</tt> (breadth-first traversal),</li>
<li><tt>mixed</tt> (mixed depth-first / breadth-first traversal with random choice; currently the default),</li>
<li><tt>random</tt> (choosing next node to process completely at random), </li>
<li><tt>hash</tt> (similar to random, but uses the Prolog hash function of a node instead of a random number generator),</li>
<li><tt>heuristic</tt> (try and use <tt>HEURISTIC_FUNCTION</tt> provided by user in <tt>DEFINITIONS</tt> clause). Some explanations can be found [[Blocks_World_(Directed_Model_Checking)|in an example about directed model checking]].</li>
<li><tt>out_degree_hash</tt> (prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking)
</ul>
|}

Example

probcli my.mch -model_check -mc_mode random

=== --timeout <N> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Global timeout 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>. Note that the <tt>TIME_OUT</tt> preference also influences other computations, such as invariant checking or static assertion checking, where it is multiplied by a factor. See the description of the -p option.
|}

Example

probcli my.mch -timeout 10000

=== -t ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| trace check (associated .trace file must exist)
|}

Example

probcli my.mch -t

=== -trace_replay <KIND> <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Replay a trace file in the given format (json,prolog,B).
|}

KIND is either json, prolog, B. The old ProB format is prolog. The trace files generated by ProB2-UI are json (with .prob2trace extension). The B format consists of a sequence of B operation calls.
Example

probcli my.mch -trace_replay json my.prob2trace

Alternative command -det_trace_replay KIND FILE.

=== -init ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| constraint-based invariant checking for an operation (also use <OPNAME>=all)
|}

Example

probcli my.mch -cbc all

=== -cbc_deadlock ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Perform constraint-based deadlock checking (also use -cbc_deadlock_pred PRED)
|}

This will try to find a state which satisfies the invariant and properties and where no operation/event is enabled.
Note: if ProB finds a counter example then the machine cannot be proven to be deadlock free. However, the particular state may not be reachable from the initial state(s). If you want to find a reachable deadlock you have to use the model checker.

=== -cbc_deadlock_pred <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based deadlock finding given a predicate
|}

This is like -cbc_deadlock but you provide an additional predicate. ProB will only find deadlocks which also make this predicate true.

Example

probcli my.mch -cbc_deadlock_pred "n=15"

=== -cbc_assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based checking of assertions on constants
|}
This will try and find a solution for the constants which make an assertion (on constants) false.

You can use the extra command <tt>-cbc_output_file FILE</tt> to write the result of this check to a file.
You can also use the extra command <tt>-cbc_option contradiction_check</tt> to ask ProB to check if there is a contradiction in the properties (in case the check did not find a counter-example to the assertions). The extra command <tt>-cbc_option unsat_core</tt> tells ProB to compute the unsatisfiable core in case a proof the assertions was found.
Note that the <tt>TIME_OUT</tt> preference is multiplied by 10 for this command.

There are various variations of this command:
-cbc_assertions_proof
-cbc_assertions_tautology_proof
Both commands do not allow enumeration warnings to occur.
The latter command ignores the PROPERTIES and tries to check whether the ASSERTION(s) are tautologies.
Both commands can be useful to use ProB as a Prover/Disprover (as is done in Atelier-B 4.3).

=== -cbc_sequence <SEQ> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Constraint-based searching for a sequence of operation names (separated by semicolons)
|}
This will try and find a solution for the constants, initial variable values and parameters which make execution of the given sequence of operations possible.

Example

probcli my.mch -cbc_sequence "op1;op2"

=== -strict ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| raise error and stop probcli if anything unexpected happens, e.g., if model checking finds a counter example or trace checking fails or any unexpected error happens
|}

Example

probcli my.mch -t -strict

=== -expcterr <ERR> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -animate <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| random animation (max Nr steps)
|}

Animates the machine randomly, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-animate_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-animate_all</tt> could run forever.

Example

probcli my.mch -animate 100

Variations
-animate_all : animate until deadlock reached
-animate_until_ltl P : animate until LTL property holds on trace
-animate_until_ltl_state_property P : animate until current state satisifes LTL state property

=== -execute <Nr>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| execution (max Nr steps)
|}

Executes the "first" enabled operation of a machine, maximally Nr of steps. It will stop if a deadlock is reached and report an error. You can also use the command <tt>-execute_all</tt>, which will only stop at a deadlock (and not report an error). Be careful: <tt>-execute_all</tt> could run forever.

In contrast to -animate, -execute will
* always choose the first enabled operation it finds and stop searching for further enabled operations in that state (-animate will compute all enabled operations up to the limit set by the <tt>MAX_OPERATIONS</tt> or <tt>MAX_INITIALISATIONS</tt> preference and then choose randomly); the order of operations in the B machine is thus important for -execute
* not store intermediate states in the state space; as such -execute is faster but after execution one only has access to the first state and the final state of execution

Example

probcli my.mch -execute 100

=== -execute_all===

See <tt>-execute <Nr></tt> above.

=== -det_check ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if every step of the animation is deterministic (i.e., only one operation is possible, and it can only be executed in one possible way as far as parameters and result is concerned).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -animate 100 -det_check

=== -det_constants ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check if animation steps are deterministic
|}

Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way to set up the constants is possible).
Currently this option has only an effect for the -animate <Nr> and the -init commands.

Example

probcli my.mch -init -det_constants
=== -his <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save animation history to a file
|}

Save the animation (or model checking) history to a text file. Operations are separated by semicolons.
The output can be adapted using the -his_option command. With -his_option show_states the -his command will also write out all states to the file (in the form of comments before and after operations). With -his_option show_init only the initial state is written out.
The -his command is executed after the -init, -animate, -t or -mc commands.
See also the -sptxt command to only write the current values of variables and constants to a file.

Example

probcli -animate 5 -his history.txt supersimple.mch

Additionally we can have the initialised variables and constants:

probcli -animate 5 -his history.txt -his_option show_init supersimple.mch

And we can have in addition the values of the variables in between (and at the end):

probcli -animate 5 -his history.txt -his_option show_states supersimple.mch

With -his_option trace_file as only option, probcli will write the history in Prolog format, which can later be used by the -t command.

=== -i ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| interactive animation
|}

After performing the other commands, ProB stays in interactive mode and allows the user to manually animate the loaded specification.

Example

probcli my.mch -i

=== -repl ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start interactive read-eval-print-loop
|}

Example

probcli my.mch -p CLPFD TRUE -repl

A list of commands can be obtained by typing <tt>:help</tt> (just help for versions 1.3.x of probcli). The interactive read-eval-print-loop can be exited using <tt>:q</tt> (just typing a return on a blank line for versions 1.3.x of probcli)..
If in addition you want see a graphical representation of the solutions found you can use the following command and open the <tt>out.dot</tt> file using dotty or GraphViz:
probcli -repl -evaldot ~/out.dot

You can also use the <tt>-eval</tt> command to evaluate specific formulas or expressions:
probcli -eval "1+2"
For convenience, these formulas can also be put into a separate file:
probcli -eval_file MyFormula.txt

=== -c ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print coverage statistics
|}

Example

probcli my.mch -mc 1000 -c

You can also use the longer name for the command:

probcli my.mch -mc 1000 --coverage

There is also a version which prints a shorter summary (and which is much faster for large state spaces):

probcli my.mch -mc 1000 --coverage_summary

=== -cc <Nr> <Nr> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set <PREFERENCE> to <VALUE>. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

You can also use --pref instead of -p.
Example

probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000

=== -pref_group <PREFGROUP> <SETTING> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set to the group of preferences <PREFGROUP> to a predefined setting <SETTING>
|}

Example

probcli my.mch -pref_group model_check unlimited

Available groups and settings are:

* PREFERENCE GROUP integer : SETTINGS [int32] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs

=== -prefs <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Set preferences from preference file <FILE>. The file should be created by the Tcl/Tk version of ProB; this version automatically creates a file called ProB_Preferences.pl. For more information about preferences please have a look at [[Using_the_Command-Line_Version_of_ProB#Preferences | Preferences]]
|}

Example

probcli my.mch -prefs ProB_Preferences.pl

=== -card <GS> <VAL> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set cardinality (scope in Alloy terminology) of a B deferred set. This overrides the default cardinality (which can be set using <tt>-p DEFAULT_SETSIZE <VAL></tt>).
|}

Example

probcli my.mch -card PID 5

=== -goal <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set GOAL predicate for model checker
|}

Example

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

=== -scope <PRED> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set SCOPE predicate for model checker; states which do not satisfy the SCOPE predicate will be ignored (invariant will not be checked and no outgoing transitions will be computed)
|}

Example

probcli my.mch -mc 10000000 -scope "n<18"

=== -s <PORT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on given port
|}

Example

probcli my.mch ...

=== -ss ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on port 9000
|}

Example

probcli my.mch ...

=== -sf ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| start socket server on some free port
|}

Example

probcli my.mch ...

=== -sptxt <FILE>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants and variables to a file
|}

Save the values of constants and variables to a text file in classical B syntax.
The -sptxt command is executed after the -init, -animate, -t or -mc commands.
The values are fully written out (some sets, e.g., infinite sets may be written out symbolically).

See also the -his command.

Example

probcli -animate 5 -sptxt state.txt supersimple.mch

This will write the values of all variables and constants to the file state.txt after animating the machine 5 steps.

=== -cache <DIRECTORY>===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save constants (and in future also variables) to a file to avoid recomputation
|}

This commands saves the values of constants for the current B machine and puts those values into files in the specified directory. The command will also tell ProB to try and reuse constants saved for subsidiary machines (included using SEES for example) whenever possible.
The purpose of the command is to avoid recomputing constants as much as possible, as this can be very time consuming.
This also works for values of variables computed in the initialisation or even using operations.
However, we do not support refinements at the moment.

Note: this command can also be used when starting up the ProB Tcl/Tk version.

=== -logxml <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities and results of probcli in XML format in <LogFile>
|}

A schema declaration file (xsd) can be found at <tt>doc/logxml_xsd.xml</tt> in the ProB [[Download#Sourcecode|Prolog sources]].
The log file contains information about the various commands performed by probcli.
It also contains version information, the parameters provided to probcli and details about the errors that occured.

Example

probcli my.mch -mc 1000 -logxml log.xml

=== -logxml_write_vars <PREFIX> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| after processing other commands (such as -execute) write values of variables having prefix PREFIX in their name into the XML log file (if XML logging has been activated using the -logxml command)
|}

Example

probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out

=== -l <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in <LogFile> using Prolog format
|}

Example

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

=== -ll ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| log activities in /tmp/prob_cli_debug.log
|}

Example

probcli my.mch -mc 1000 -ll

=== -lg <LogFile> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| analyse <LogFile> using gnuplot
|}

Example

probcli my.mch ...

=== -pp <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>
|}

Example

probcli my.mch -pp my_pp.mch

=== -ppf <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| pretty-print internal representation to <FILE>, force printing of all type infos
|}

Example

probcli my.mch -ppf my_ppf.mch

=== -v ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| set ProB into verbose mode
|}

Example

probcli my.mch -mc 1000 -v

=== -version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| print version information
|}

There is also an alternate command called -svers which just prints the version number of ProB.
Example

probcli -version
ProB Command Line Interface
VERSION 1.3.4-rc1 (9556:9570M)
$LastChangedDate: 2011-11-16 18:36:18 +0100 (Wed, 16 Nov 2011) $
Prolog: SICStus 4.2.0 (x86_64-darwin-10.6.0): Mon Mar 7 20:03:36 CET 2011
Application Path: /Users/leuschel/svn_root/NewProB

probcli -svers
VERSION 1.3.4-rc1 (9556:9570M)

You can use <tt>probcli -version -v</tt> to obtain more information about your version of probcli.

=== -check_java_version ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check Java and B parser version information
|}

This command is available as of ProB version 1.5.1-beta5 or higher. It can be useful to check that your Java is correctly installed and that the ProB B parser can operate correctly

probcli -check_java_version
Result of checking Java version:
Java is correctly installed and version 1.7.0_55-b13 is compatible with ProB requirements (>= 1.7).
ProB B Java Parser available in version: 2016-02-25 15:27:18.55.

=== -assertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check ASSERTIONS of your machine

If you provide the -t switch, the ASSERTIONS will be checked after executing your trace. Otherwise, they will be checked in an initial state.
ProB will automatically initialize the machine if you have not provide the -init or -t switch.

You can also use -main_assertions to check only the ASSERTIONS found in the main file.

If your ASSERTIONS are all static (i.e., make no reference to variables), then ProB will remove all CONSTANTS and PROPERTIES from your machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such as -mc or -animate which may require the computation of the variables.
|}

Example

probcli my.mch -init -assertions

=== -property ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| virtually add predicate to PROPERTIES
|}

Example

probcli my.mch -property "PRED"

=== -properties ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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

=== -dot_output <PATH> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| define path for generation of dot files for false properties or assertions
|}

This option is applicable to -properties and -assertions. It will result in individual dot files being generated for every false or unknown property or assertion. Assertions are numbered A0,A1,... and properties P0,P1,... You can also force to generate dot files for all properties (i.e., also the true ones) using the -dot_all command-line flag.

Example

probcli my.mch -init -properties -dot_output somewhere/

This will generate files somewhere/my_P0_false.dot, somewhere/my_P1_false.dot, ...

=== -rc ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| runtime checking of types/pre-/post-conditions
|}

Example

probcli my.mch ...

=== -ltlfile <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL formulas in file <FILE>
|}

Example

probcli my.mch ...

=== -ltlassertions ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| check LTL assertions (in DEFINITIONS)
|}

Example

probcli my.mch ...

=== -ltllimit <LIMIT> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| explore at most <LIMIT> states when model-checking LTL
|}

Example

probcli my.mch ...

=== -save <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| save state space for later refinement check
|}

Example

probcli my.mch ...

=== -refchk <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| 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 <Operation(s)>|-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'''.

As of version 1.6.0, the operation arguments are also written to the XML file.
The preference <tt>INTERNAL_ARGUMENT_PREFIX</tt> can be used to provide a prefix for internal operation arguments; any argument/parameter whose name starts with that prefix is considered an internal parameter and not shown in the trace file.
Also, as of version 1.6.0, the non-deterministic initialisations are shown in the XML trace file: all variables and constants where more than one possible initialisation exists are written into the trace file, as argument of an INITIALISATION event.

=== -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 <Depth> <MaxStates> <EndPredicate> <FILE>|-mcm-tests]] for further details.

=== -spdot <FILE> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Write graph of the state space to a dot <FILE>
|}

Example

probcli my.mch -mc 100 -spdot my_statespace.dot

=== -cbc_tests <Depth> <EndPredicate> <File> ===
Generate test cases by constraint solving with maximum
length '''Depth''', the last state satisfies '''EndPredicate'''
and the test cases are written to '''File'''. If the predicate is the empty string we assume truth. If the filename is the empty string no file is generated. See also the page on [[Test_Case_Generation]].

=== -cbc_cover <Operation> ===
When generating CB test cases, '''Operation''' should be covered.
The option can be given multiple times to specify several operations.
Alternatively, multiple operations can be separated by a comma. You can also use the option <pre>-cbc_cover_match PartialName</pre> to match all operations whose name contains PartialName. See also the page about [[Test_Case_Generation]].

=== -test_description <File> ===
Read the options for constraint based test case generation from '''File'''.

=== -bmc <Depth> ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Run the [[Bounded_Model_Checking|bounded model checker]] until maximum trace depth <Depth> specified. Looks for invariant violations using the constraint-based test case generation algorithm.
|}

Example

probcli my.mch -bmc 20

=== -csp-guide <File> ===
Use the CSP File '''File''' to guide the B Machine ("CSP||B").
(This feature is included since version 1.3.5-beta7.)
As of version 1.15.1 you can also specify a <tt>CSP_GUIDE_FILE</tt>
DEFINITION (which also works in ProB2-UI).

=== -rule_report <File> ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Generates rule validation report for rules machines (.rmch) at the specified location <File> for the current animation state. Depending on the file extension an HTML or an XML version of the report is generated (.html/.xml).
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.rmch -execute_all -rule_report my_report.html

=== -machine_files_sha ===

Description

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Computes SHA1 hash of all B files used by a B model.
|}

Useful in combination with <tt>-execute</tt> or <tt>-execute_all</tt>.

Example

probcli myrules.mch -machine_files_sha

=== -check_machine_file_sha ===

{| style="color:black; background-color:#FFFFEF; border:1px solid lightgray;" cellpadding="10" cellspacing="0" width="100%"
| Compute and check SHA1 hash of a particular B file used by the main B model.
|}

probcli ./Demo/scheduler.mch -check_machine_file_sha scheduler.mch 1cab7ec89adc9f9b153af85c1ae16ba8a7a2a661

== Environment Variables ==

Set NO_COLOR environment variable to disable terminal colors.
See [https://no-color.org https://no-color.org].

== Preferences ==

You can use these preferences within the command:

-p <PREFERENCE> <VALUE>

{| cellpadding="5" cellspacing="1" width="100%" border="1"
!style="background-color:lightgrey;" | <PREFERENCE>
!style="background-color:lightgrey;" | <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. Will be used if a set s is neither enumerated, has no no card(s)=nr predicate in the PROPERTIES and has no scope_s == Nr DEFINITION.
|-
| MAX_INITIALISATIONS
| nat ==> Max Number of Initialisations and ways to setup constants 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
|-
| COMPRESSION
| bool ==> Use more aggressive COMPRESSION when storing states
|-
| EXPAND_CLOSURES_FOR_STATE
| bool ==> Convert lazy form back into explicit form for Variables, Constants, Operation Arguments. ProB will sometimes try to keep certain sets symbolic. If this preference is TRUE then ProB will try to expand those sets for variables and constants after an operation has been executed.
|-
| SYMBOLIC
| bool ==> Lazy expansion of lambdas and set comprehensions. By default ProB will keep certain sets symbolic (e.g., sets it knows are infinite). When this preference is set to TRUE then all set comprehensions and lambda abstractions will at first be kept symbolic and only expanded into explicit form if needed.
|-
| CLPFD
| bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit computers). Setting this preference to TRUE should substantially improve ProB's ability to solve complicated predicates involving integers. However, it may cause CLP(FD) overflows in certain circumstances.
|-
| SMT
| bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates). With this predicate set to TRUE ProB will be better at solving certain constraint solving tasks. It should be enabled when doing constraint-based invariant or deadlock checking. ProB Tcl/Tk will turn this preference on automatically for those checks.
|-
| 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, is multiplied by a factor for other computations)
|-
| PROOF_INFO
| bool ==> Use Proof Information to restrict invariant checking to affected unproven clauses. Most useful in EventB for models exported from Rodin.
|-
| 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 (use 0 to disable expansion)
|-
| MAX_DISPLAY_SET
| int ==> Max size for pretty-printing sets (-1 means no limit)
|-
| CSP_STRIP_SOURCE_LOC
| bool ==> Strip source location for CSP; will speed up model checking
|-
| 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 analyzing assertions or properties
|-
| 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)
|-
| NEGATED_INVARIANT_CHECKING
| bool ==> Perform double evaluation (positive and negative) when checking invariants
|-
| CSE
| bool ==> Perform common-sub-expression elimination
|-
| CSE_SUBST
| bool ==> Perform common-sub-expression elimination also for B substitutions
|}

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:
<pre>
probcli -init My.mch
</pre>
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:
<pre>
probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
</pre>

To fully model check a specification M.mch while tryining to minimize memory consumption do:
<pre>
probcli -model_check -p COMPRESSION TRUE M.mch
</pre>

To model check a specification M.mch while trying to minimize memory consumption further by not storing processed stats and using symmetry reduction (and accepting hash collisions) do:
<pre>
probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
</pre>

== 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.
{{Feedback}}