diff --git a/src/docs/chapter/user/25_CommandLine/00_section_header.adoc b/src/docs/chapter/user/25_CommandLine/00_section_header.adoc
deleted file mode 100644
index 9b893ce6ba1ff986751228010873c18af76bf392..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/25_CommandLine/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[command-line]]
-= Command Line
-:leveloffset: +1
diff --git a/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc b/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc
deleted file mode 100644
index 7a9e48344cac975b0423d803c6514a52822550db..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc
+++ /dev/null
@@ -1,11 +0,0 @@
-
-[[prob-cli]]
-= ProB CLI
-
-The ProB Cli (command-line interface) offers many of the ProB features
-via command-line. As such, you can run ProB from your shell scripts or
-in your Makefiles. probcli contains a REPL (Read-Eval-Print-Loop) and
-you can also https://github.com/bivab/prob.vim[integrate probcli into an
-editor such as vim]. probcli can also communicate with other tools or
-graphical user interfaces via sockets (this is used by
-<<prob-for-rodin,ProB for Rodin>>).
diff --git a/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc b/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc
deleted file mode 100644
index e550cd84307e1ce20e7c165a56aea3cfcb0737d2..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc
+++ /dev/null
@@ -1,1541 +0,0 @@
-
-[[using-the-command-line-version-of-prob]]
-= Using the Command-Line Version of ProB
-
-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 `probcli –help` 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 `probcli` (except within
-groups of commands such as `-p MAXINT 127`). Any argument that is not
-recognised by `probcli` is treated as a filename to be analysed.
-
-[[conventions-used]]
-== Conventions used
-
-The following conventions are used in this guide:
-
-[cols=",",]
-|=======================================================================
-|<replaceme> |All values that should be replaced with some value are shown withing < >
-|line breaks |Command synopsis for command may be broken up on several lines. When typing commands enter all option on the same line.
-|=======================================================================
-
-[[synopsis]]
-== Synopsis
-
-....
-|probcli [--help]
-|<filename> [ <options> ]
-....
-
-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-for-command-line]]
-== Options
-
-[[mc]]
-=== -mc
-
-==== Description
-
-[cols="",]
-|====================================
-|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 `-nodead, -noinv, -nogoal, -noass` to influence which kinds of
-errors are reported by `-mc`. You can also set a target goal predicate
-using the `-goal "PRED"` command and limit the scope of the model
-checking using the `-scope "PRED"` command.
-
-[[model_check]]
-=== -model_check
-
-The same as `-mc` but without a limit on the number of nodes checked.
-ProB will run until the entire state space is explored.
-
-[[no]]
-=== -no <x>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -disable_timeout
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -bf
-
-==== Description
-
-[cols="",]
-|===========================================
-|proceed breadth-first during model checking
-|===========================================
-
-==== Example
-
-....
-probcli my.mch -bf -mc 1000
-....
-
-[[df]]
-=== -df
-
-==== Description
-
-[cols="",]
-|=========================================
-|proceed depth-first during model checking
-|=========================================
-
-==== Example
-
-....
-probcli my.mch -df -mc 1000
-....
-
-[[mc_mode]]
-=== -mc_mode <M>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|influence how the model checker proceeds. Available as of version 1.5.1.
-Supersedes the `-df` and `-bf` switches.
-|=======================================================================
-
-Possible values for the mode <M> are:
-
-* `df` (depth-first traversal),
-* `bf` (breadth-first traversal),
-* `mixed` (mixed depth-first / breadth-first traversal with random
-choice; currently the default),
-* `random` (choosing next node to process completely at random),
-* `hash` (similar to random, but uses the Prolog hash function of a node
-instead of a random number generator),
-* `heuristic` (try and use `HEURISTIC_FUNCTION` provided by user in
-`DEFINITIONS` clause). Some explanations can be found
-<<blocks-world-directed-model-checking,in an example about
-directed model checking>>.
-* `out_degree_hash` (prioritise nodes with fewer outgoing transitions;
-mainly useful for deadlock checking)
-
-==== Example
-
-....
-probcli my.mch -model_check -mc_mode random
-....
-
-[[timeout]]
-=== --timeout <N>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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 `TIME_OUT` 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]]
-=== -t
-
-==== Description
-
-[cols="",]
-|===============================================
-|trace check (associated .trace file must exist)
-|===============================================
-
-==== Example
-
-....
-probcli my.mch -t
-....
-
-[[init]]
-=== -init
-
-==== Description
-
-[cols="",]
-|========================
-|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]]
-=== -cbc <OPNAME>
-
-==== Description
-
-[cols="",]
-|====================================================================
-|constraint-based invariant checking for an operation (also use <OPNAME>=all)
-|====================================================================
-
-==== Example
-
-....
-probcli my.mch -cbc all
-....
-
-[[cbc_deadlock]]
-=== -cbc_deadlock
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -cbc_deadlock_pred <PRED>
-
-==== Description
-
-[cols="",]
-|===================================================
-|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]]
-=== -cbc_assertions
-
-==== Description
-
-[cols="",]
-|====================================================
-|constraint-based checking of assertions on constants
-|====================================================
-
-This will try to find a solution for the constants which make an
-assertion (on constants) false.
-
-You can use the extra command `-cbc_output_file FILE` to write the
-result of this check to a file. You can also use the extra command
-`-cbc_option contradiction_check` 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
-`-cbc_option unsat_core` tells ProB to compute the unsatisfiable core in
-case a proof the assertions was found. Note that the `TIME_OUT`
-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]]
-=== -cbc_sequence <SEQ>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|constraint-based searching for a sequence of operation names (separated by semicolons)
-|=======================================================================
-
-This will try to 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]]
-=== -strict
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -expcterr <ERR>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|expect error to occur (=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]]
-=== -animate <Nr>
-
-==== Description
-
-[cols="",]
-|===============================
-|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
-`-animate_all`, which will only stop at a deadlock (and not report an
-error). Be careful: `-animate_all` could run forever.
-
-==== Example
-
-....
-probcli my.mch -animate 100
-....
-
-[[execute]]
-=== -execute <Nr>
-
-==== Description
-
-[cols="",]
-|========================
-|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 `-execute_all`, which will only stop at a
-deadlock (and not report an error). Be careful: `-execute_all` 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 `MAX_OPERATIONS` or
-`MAX_INITIALISATIONS` 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
-....
-
-[[det_check]]
-=== -det_check
-
-==== Description
-
-[cols="",]
-|==========================================
-|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 and the -init commands.
-
-==== Example
-
-....
-probcli my.mch -animate 100 -det_check
-....
-
-[[det_constants]]
-=== -det_constants
-
-==== Description
-
-[cols="",]
-|==========================================
-|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 and the -init commands.
-
-==== Example
-
-....
-probcli my.mch -init -det_constants
-....
-
-[[his]]
-=== -his <FILE>
-
-==== Description
-
-[cols="",]
-|================================
-|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]]
-=== -i
-
-==== Description
-
-[cols="",]
-|=====================
-|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]]
-=== -repl
-
-==== Description
-
-[cols="",]
-|======================================
-|start interactive read-eval-print-loop
-|======================================
-
-==== Example
-
-....
-probcli my.mch -p CLPFD TRUE -repl
-....
-
-A list of commands can be obtained by typing `:help` (just help for
-versions 1.3.x of probcli). The interactive read-eval-print-loop can be
-exited using `:q` (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 `out.dot` file using dotty or GraphViz:
-
-....
-probcli -repl -evaldot ~/out.dot
-....
-
-You can also use the `-eval` 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]]
-=== -c
-
-==== Description
-
-[cols="",]
-|=========================
-|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]]
-=== -cc <Nr> <Nr>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -p <PREFERENCE> <VALUE>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|set <PREFERENCE> to <VALUE> For more information about preferences please have a look at
-<<using-the-command-line-version-of-prob,Preferences>>
-|=======================================================================
-
-You can also use --pref instead of -p.
-
-==== Example
-
-....
-probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000
-....
-
-[[prefs]]
-
-=== -pref_group <PREFGROUP> <SETTING>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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
-
-[cols="",]
-|=======================================================================
-|Set preferences from preference 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>>
-|=======================================================================
-
-==== Example
-
-....
-probcli my.mch -prefs ProB_Preferences.pl
-....
-
-[[card]]
-=== -card <GS> <VAL>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|set cardinality (scope in Alloy terminology) of a B deferred set. This
-overrides the default cardinality (which can be set using
-`-p DEFAULT_SETSIZE`).
-|=======================================================================
-
-==== Example
-
-....
-probcli my.mch -card PID 5
-....
-
-[[goal]]
-=== -goal <PRED>
-
-==== Description
-
-[cols="",]
-|====================================
-|set GOAL predicate for model checker
-|====================================
-
-==== Example
-
-....
-probcli my.mch -mc 10000000 -goal "n=18"-strict -expcterr goal_found
-....
-
-[[scope]]
-=== -scope <PRED>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -s <PORT>
-
-==== Description
-
-[cols="",]
-|=================================
-|start socket server on given port
-|=================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[ss]]
-=== -ss
-
-==== Description
-
-[cols="",]
-|================================
-|start socket server on port 9000
-|================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[sf]]
-=== -sf
-
-==== Description
-
-[cols="",]
-|=====================================
-|start socket server on some free port
-|=====================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[sptxt]]
-=== -sptxt <FILE>
-
-==== Description
-
-[cols="",]
-|======================================
-|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]]
-=== -cache <DIRECTORY>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -logxml <LogFile>
-
-==== Description
-
-[cols="",]
-|======================================================
-|log activities and results of probcli in XML format in <LogFile>
-|======================================================
-
-==== Example
-
-....
-probcli my.mch -mc 1000 -logxml log.xml
-....
-
-[[logxml_write_vars]]
-=== -logxml_write_vars <PREFIX>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -l <LogFile>
-
-==== Description
-
-[cols="",]
-|=====================================
-|log activities <LogFile> in using Prolog format
-|=====================================
-
-==== Example
-
-....
-probcli my.mch -mc 1000 -l my.log
-....
-
-[[ll]]
-=== -ll
-
-==== Description
-
-[cols="",]
-|=========================================
-|log activities in /tmp/prob_cli_debug.log
-|=========================================
-
-==== Example
-
-....
-probcli my.mch -mc 1000 -ll
-....
-
-[[lg]]
-=== -lg <LogFile>
-
-==== Description
-
-[cols="",]
-|=====================
-|analyse <LogFile> using gnuplot
-|=====================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[pp]]
-=== -pp <FILE>
-
-==== Description
-
-[cols="",]
-|=======================================
-|pretty-print internal representation to <FILE>
-|=======================================
-
-==== Example
-
-....
-probcli my.mch -pp my_pp.mch
-....
-
-[[ppf]]
-=== -ppf <FILE>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|pretty-print internal representation to <FILE>, force printing of all type
-infos
-|=======================================================================
-
-==== Example
-
-....
-probcli my.mch -ppf my_ppf.mch
-....
-
-[[v]]
-=== -v
-
-==== Description
-
-[cols="",]
-|==========================
-|set ProB into verbose mode
-|==========================
-
-==== Example
-
-....
-probcli my.mch -mc 1000 -v
-....
-
-[[version]]
-=== -version
-
-==== Description
-
-[cols="",]
-|=========================
-|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 `probcli -version -v` to obtain more information about your
-version of probcli.
-
-[[check_java_version]]
-=== -check_java_version
-
-==== Description
-
-[cols="",]
-|===========================================
-|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]]
-=== -assertions
-
-==== Description
-
-[cols="",]
-|===================================
-|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
-....
-
-[[properties]]
-=== -properties
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -dot_output <PATH>
-
-==== Description
-
-[cols="",]
-|=======================================================================
-|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]]
-=== -rc
-
-==== Description
-
-[cols="",]
-|==============================================
-|runtime checking of types/pre-/post-conditions
-|==============================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[ltlfile]]
-=== -ltlfile <FILE>
-
-==== Description
-
-[cols="",]
-|==========================
-|check LTL formulas in file <FILE>
-|==========================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[ltlassertions]]
-=== -ltlassertions
-
-==== Description
-
-[cols="",]
-|=====================================
-|check LTL assertions (in DEFINITIONS)
-|=====================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[ltllimit]]
-=== -ltllimit <LIMIT>
-
-==== Description
-
-[cols="",]
-|==============================================
-|explore at most <LIMIT> states when model-checking LTL
-|==============================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[save]]
-=== -save <FILE>
-
-==== Description
-
-[cols="",]
-|===========================================
-|save state space for later refinement check
-|===========================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[refchk]]
-=== -refchk <FILE>
-
-==== Description
-
-[cols="",]
-|===================================================
-|refinement check against previous saved state space
-|===================================================
-
-==== Example
-
-....
-probcli my.mch ...
-....
-
-[[mcm_tests]]
-=== -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,-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 it either
-
-* has covered all required operations/events with the current search
-depth
-* or 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 .
-
-==== 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 `INTERNAL_ARGUMENT_PREFIX` 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]]
-=== -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, -mcm-tests>> for further details.
-
-[[spdot]]
-=== -spdot <FILE>
-
-==== Description
-
-[cols="",]
-|=======================================
-|Write graph of the state space to a dot <FILE>
-|=======================================
-
-==== Example
-
-....
-probcli my.mch -mc 100 -spdot my_statespace.dot
-....
-
-[[cbc_tests]]
-=== -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,Test_Case_Generation>>.
-
-[[cbc_cover]]
-=== -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
-
-....
--cbc_cover_match PartialName
-....
-
-to match all operations whose name contains PartialName. See also the
-page about <<test-case-generation,Test_Case_Generation>>.
-
-[[test_description]]
-=== -test_description <File>
-
-Read the options for constraint based test case generation from *File*.
-
-[[bmc]]
-=== -bmc <Depth>
-
-[cols="",]
-|=======================================================================
-|Run the <<bounded-model-checking,bounded model checker>> until
-maximum trace depth specified. Looks for invariant violations using the
-constraint-based test case generation algorithm.
-|=======================================================================
-
-==== Example
-
-....
-probcli my.mch -bmc 20
-....
-
-[[csp-guide]]
-=== -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.)
-
-[[environment-variables-for-command-line]]
-== Environment Variables
-
-Set NO_COLOR environment variable to disable terminal colors.
-See also https://no-color.org[https://no-color.org].
-
-
-[[preferences-for-command-line]]
-== Preferences
-
-You can use these preferences within the command:
-
-`-p`
-
-[cols=",",options="header",]
-|=======================================================================
-|<PREFERENCE> | <VALUE>
-|MAXINT |nat =\=> MaxInt, used for expressions such as xx::NAT
-(2147483647 for 4 byte ints)
-
-|MININT |neg =\=> MinInt, used for expressions such as xx::INT
-(-2147483648 for 4 byte ints)
-
-|DEFAULT_SETSIZE |nat =\=> Size of unspecified deferred sets in SETS
-section. 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]]
-== Some probcli examples
-
-To load a file My.mch, setup the constants and initialize it do:
-
-....
-probcli -init My.mch
-....
-
-To load a file M.mch, setup the constants, initialize and then check all
-assertions with Atelier-B's default values for MININT and MAXINT and an
-increased timeout of 5 seconds do:
-
-....
-probcli -init -assertions -p MAXINT 2147483647 -p MININT -2147483647 -p TIME_OUT 5000 M.mch
-....
-
-To fully model check a specification M.mch while tryining to minimize
-memory consumption do:
-
-....
-probcli -model_check -p COMPRESSION TRUE M.mch
-....
-
-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:
-
-....
-probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE -p SYMMETRY_MODE hash -model_check M.mch
-....
-
-[[command-line-arguments-for-prob-tcltk]]
-== 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.
diff --git a/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc b/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1