diff --git a/src/docs/chapter/user/12_BLanguage/00_section_header.adoc b/src/docs/chapter/user/12_BLanguage/00_section_header.adoc
deleted file mode 100644
index 39d27f577895ad6096f02e355fc5bcf75505c140..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[b-language]]
-= B Language
-:leveloffset: +1
diff --git a/src/docs/chapter/user/12_BLanguage/01_Current_Limitations.adoc b/src/docs/chapter/user/12_BLanguage/01_Current_Limitations.adoc
deleted file mode 100644
index 18d7d3273cea77c9c41dcaf7f6eccdc12aa0653e..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/01_Current_Limitations.adoc
+++ /dev/null
@@ -1,57 +0,0 @@
-
-[[current-limitations]]
-= Current Limitations
-
-ProB in general requires all <<deferred-sets,deferred sets>> to be
-given a finite cardinality. If no cardinality is specified, a default
-size will be used. Also, unless finite bounds can be inferred by the
-ProB constraint solver, mathematical integers will only be enumerated
-within `MININT` to `MAXINT` (and ProB will generate enumeration
-warnings in case no solution is found).
-
-Other general limitations are:
-
-* Trees and binary trees are specific to the AtelierB
-tool and are only partially supported (the `STRING` type is now supported).
-
-* Definitions (from the `DEFINITIONS` clause) with
-arguments are supported, but in contrast to AtelierB they are parsed
-independently and have to be either an expression, a predicate, or a
-substitution; definitions which are predicates or substitutions must be
-declared before first use.
-Also: the arguments of `DEFINITIONS` have to
-be expressions. Finally, when replacing DEFINITIONS the associativity is
-not changed. E.g., with `PLUS(x,y) == x+y`, the expression
-`PLUS(2,3)*10` will evaluate to 50 (and not to 32 as with Atelier-B).
-Also, ProB will generate a warning when variable capture may occur.
-
-* There are also limitations with refinements, as discussed below.
-
-* The `VALUES` clause of `IMPLEMENTATION` machines is not yet
-supported.
-
-* Parsing: ProB will require parentheses around the comma, the
-relational composition, and parallel product operators. For example, you
-cannot write `r2=rel;rel`. You need to write `r2=(rel;rel)`. This allows
-ProB to distinguish the relational composition from the sequential
-composition (or other uses of the semicolon).
-
-See the page <<using-prob-with-atelier-b,Using ProB with Atelier B>> for more details.
-
-[[multiple-machines-and-refinements]]
-== Multiple Machines and Refinements
-
-It is possible to use multiple B machines with ProB. However, ProB may
-not enforce all of the classical B visibility rules (although we try
-to). As far as the visibility rules are concerned, it is thus a good
-idea to check the machines in another B tool, such as Atelier B or the
-B-Toolkit.
-
-While refinements are supported, the preconditions of operations are not
-propagated down to refinement machines. This means that you should
-rewrite the preconditions of operations (and, if necessary, reformulate
-them in terms of the variables of the refinement machine). Also, the
-refinement checker does yet check the gluing invariant.
-
-Note however, that for Rodin Event-B models, ProB fully supports multi-level
-animation and validation.
diff --git a/src/docs/chapter/user/12_BLanguage/01_Summary_of_B_Syntax.adoc b/src/docs/chapter/user/12_BLanguage/01_Summary_of_B_Syntax.adoc
deleted file mode 100644
index a81c1190a23de6ce9e42f7f11c9238d499c17c0f..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/01_Summary_of_B_Syntax.adoc
+++ /dev/null
@@ -1,476 +0,0 @@
-
-[[summary-of-b-syntax]]
-= Summary of B Syntax
-
-[[logical-predicates]]
-== Logical predicates:
-
-....
- P & Q conjunction
- P or Q disjunction
- P => Q implication
- P <=> Q equivalence
- not P negation
- !(x).(P=>Q) universal quantification
- #(x).(P&Q) existential quantification
-....
-
-Above, `P` and `Q` stand for predicates. Inside the universal
-quantification, `P` must give a value type to the quantified variable.
-Note: you can also introduce multiple variables inside a universal or
-existential quantification, e.g., `!(x,y).(P => Q)`.
-
-[[equality]]
-== Equality:
-
-....
- E = F equality
- E /= F disequality
-....
-
-[[booleans]]
-== Booleans:
-
-....
- TRUE
- FALSE
- BOOL set of boolean values ({TRUE,FALSE})
- bool(P) convert predicate into BOOL value
-....
-
-Warning: `TRUE` and `FALSE` are values and not predicates in B and
-cannot be combined using logical connectives. To combine two boolean
-values `x` and `y` using conjunction you have to write
-`x=TRUE & y=TRUE`. To convert a predicate such as `z>0` into a boolean
-value you have to use `bool(z>0)`.
-
-[[sets]]
-== Sets:
-
-....
- {} empty set
- {E} singleton set
- {E,F} set enumeration
- {x|P} comprehension set
- POW(S) power set
- POW1(S) set of non-empty subsets
- FIN(S) set of all finite subsets
- FIN1(S) set of all non-empty finite subsets
- card(S) cardinality
- S*T cartesian product
- S\/T set union
- S/\T set intersection
- S-T set difference
- E:S element of
- E/:S not element of
- S<:T subset of
- S/<:T not subset of
- S<<:T strict subset of
- S/<<:T not strict subset of
- union(S) generalised union over sets of sets
- inter(S) generalised intersection over sets of sets
- UNION(z).(P|E) generalised union with predicate
- INTER(z).(P|E) generalised intersection with predicate
-....
-
-[[numbers]]
-== Numbers:
-
-....
- INTEGER set of integers
- NATURAL set of natural numbers
- NATURAL1 set of non-zero natural numbers
- INT set of implementable integers (MININT..MAXINT)
- NAT set of implementable natural numbers
- NAT1 set of non-zero implementable natural numbers
- n..m set of numbers from n to m
- MININT the minimum implementable integer
- MAXINT the maximum implementable integer
- m>n greater than
- m<n less than
- m>=n greater than or equal
- m<=n less than or equal
- max(S) maximum of a set of numbers
- min(S) minimum of a set of numbers
- m+n addition
- m-n difference
- m*n multiplication
- m/n division
- m**n power
- m mod n remainder of division
- PI(z).(P|E) Set product
- SIGMA(z).(P|E) Set summation
- succ(n) successor (n+1)
- pred(n) predecessor (n-1)
-....
-
-[[relations]]
-== Relations:
-
-....
- S<->T relation
- E|->F maplet
- dom(r) domain of relation
- ran(r) range of relation
- id(S) identity relation
- S<|r domain restriction
- S<<|r domain subtraction
- r|>S range restriction
- r|>>S range subtraction
- r~ inverse of relation
- r[S] relational image
- r1<+r2 relational overriding (r2 overrides r1)
- r1><r2 direct product {x,(y,z) | x,y:r1 & x,z:r2}
- (r1;r2) relational composition {x,y| x|->z:r1 & z|->y:r2}
- (r1||r2) parallel product {((x,v),(y,w)) | x,y:r1 & v,w:r2}
- prj1(S,T) projection function (usage prj1(Dom,Ran)(Pair))
- prj2(S,T) projection function (usage prj2(Dom,Ran)(Pair))
- closure1(r) transitive closure
- closure(r) reflexive & transitive closure
- (non-standard version: closure({}) = {}; see iterate(r,0) below)
- iterate(r,n) iteration of r with n>=0
- (Note: iterate(r,0) = id(s) where s = dom(r)\/ran(r))
- fnc(r) translate relation A<->B into function A+->POW(B)
- rel(r) translate relation A<->POW(B) into relation A<->B
-....
-
-[[functions]]
-== Functions:
-
-....
- S+->T partial function
- S-->T total function
- S+->>T partial surjection
- S-->>T total surjection
- S>+>T partial injection
- S>->T total injection
- S>+>>T partial bijection
- S>->>T total bijection
- %x.(P|E) lambda abstraction
- f(E) function application
- f(E1,...,En) is now supported (as well as f(E1|->E2))
-....
-
-[[sequences]]
-== Sequences:
-
-....
- <> or [] empty sequence
- [E] singleton sequence
- [E,F] constructed sequence
- seq(S) set of sequences over Sequence
- seq1(S) set of non-empty sequences over S
- iseq(S) set of injective sequences
- iseq1(S) set of non-empty injective sequences
- perm(S) set of bijective sequences (permutations)
- size(s) size of sequence
- s^t concatenation
- E->s prepend element
- s<-E append element
- rev(s) reverse of sequence
- first(s) first element
- last(s) last element
- front(s) front of sequence (all but last element)
- tail(s) tail of sequence (all but first element)
- conc(S) concatenation of sequence of sequences
- s/|\n take first n elements of sequence
- s\|/n drop first n elements from sequence
-
-....
-
-[[records]]
-== Records:
-
-....
- struct(ID:S,...,ID:S) set of records with given fields and field types
- rec(ID:E,...,ID:E) construct a record with given field names and values
- E'ID get value of field with name ID
-....
-
-[[strings]]
-== Strings:
-
-....
- "astring" a specific (single-line) string value
- '''astring''' an alternate way of writing (multi-line) strings, no need to escape "
- STRING the set of all strings
- Note: for the moment enumeration of strings is limited (if a variable
- of type STRING is not given a value by the machine, then ProB assumes
- STRING = { "STR1", "STR2" })
-....
-
-Atelier-B does not support any operations on strings, apart from
-equality and disequality. However, the ProB
-<<external-functions,external function library>> contains several
-operators on strings. ProB also allows multi-line strings. As of version
-1.7.0, ProB will support the following escape sequences within strings:
-
-....
- \n newline (ASCII character 13)
- \r carriage return (ASCII 10)
- \t tab (ASCII 9)
- \" the double quote symbol "
- \' the single quote symbol '
- \\ the backslash symbol
-....
-
-Within single-line string literals, you do not need to escape '. Within
-multi-line string literals, you do not need to escape " and you can use
-tabs and newlines. ProB assumes that all B machines and strings use the
-UTF-8 encoding.
-
-[[trees]]
-== Trees:
-
-Nodes in the tree are denoted by index sequences (branches), e.g,
-n=[1,2,1] Each node in the tree is labelled with an element from a
-domain S. A tree is a function mapping of branches to elements of the
-domain S.
-
-....
- tree(S) set of trees over domain S
- btree(S) set of binary trees over domain S
- top(t) top of a tree
- const(E,s) construct a tree from info E and sequence of subtrees s
- rank(t,n) rank of the node at end of branch n in the tree t
- father(t,n) father of the node denoted by branch n in the tree t
- son(t,n,i) the ith son of the node denoted by branch n in tree t
- sons(t) the sequence of sons of the root of the tree t
- subtree(t,n)
- arity(t,n)
- bin(E) construct a binary tree with a single node E
- bin(tl,E,tr) construct a binary tree with root info E and subtrees tl,tr
- left(t) the left (first) son of the root of the binary tree t
- right(t) the right (last) son of the root of the binary tree t
- sizet(t) the size of the tree (number of nodes)
- prefix(t) the nodes of the tree t in prefix order
- postfix(t) the nodes of the tree t in prefix order
- mirror, infix are recognised by the parser but not yet supported by ProB itself
-....
-
-[[let-and-if-then-else]]
-== LET and IF-THEN-ELSE
-
-ProB allows the following for predicates and expressions:
-
-....
- IF P THEN E1 ELSE E2 END conditional for expressions or predicates E1,E2
- LET x1,... BE x1=E1 & ... IN E END
-....
-
-Note: The expressions E1,... defining x1,... are not allowed to use x1,...
-
-[[statements-aka-substitutions]]
-== Statements (aka Substitutions):
-
-....
- skip no operation
- x := E assignment
- f(x) := E functional override
- x :: S choice from set
- x : (P) choice by predicate P (constraining x)
- x <-- OP(x) call operation and assign return value
- G||H parallel substitution**
- G;H sequential composition**
- ANY x,... WHERE P THEN G END non deterministic choice
- LET x,... BE x=E & ... IN G END
- VAR x,... IN G END generate local variables
- PRE P THEN G END
- ASSERT P THEN G END
- CHOICE G OR H END
- IF P THEN G END
- IF P THEN G ELSE H END
- IF P1 THEN G1 ELSIF P2 THEN G2 ... END
- IF P1 THEN G1 ELSIF P2 THEN G2 ... ELSE Gn END
- SELECT P THEN G WHEN ... WHEN Q THEN H END
- SELECT P THEN G WHEN ... WHEN Q THEN H ELSE I END
- CASE E OF EITHER m THEN G OR n THEN H ... END END
- CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END END
-
- WHEN P THEN G END is a synonym for SELECT P THEN G END
-
-**: cannot be used at the top-level of an operation, but needs to
- be wrapped inside a BEGIN END or another statement (to avoid
- problems with the operators ; and ||).
-....
-
-[[machine-header]]
-== Machine header:
-
-....
- MACHINE or REFINEMENT or IMPLEMENTATION
-
- Note: machine parameters can either be SETS (if identifier is all upper-case)
- or scalars (i.e., integer, boolean or SET element; if identifier is not
- all upper-case; typing must be provided be CONSTRAINTS)
- You can also use MODEL or SYSTEM as a synonym for MACHINE, as well
- as EVENTS as a synonym for OPERATIONS.
-....
-
-[[machine-sections]]
-== Machine sections:
-
-----
- CONSTRAINTS P (logical predicate)
- SETS S;T={e1,e2,...};...
- CONSTANTS x,y,...
- CONCRETE_CONSTANTS cx,cy,...
- PROPERTIES P (logical predicate)
- DEFINITIONS m(x,...) == BODY;....
- VARIABLES x,y,...
- CONCRETE_VARIABLES cv,cw,...
- INVARIANT P (logical predicate)
- ASSERTIONS P;...;P (list of logical predicates separated by ;)
- INITIALISATION
- OPERATIONS
-----
-
-[[machine-inclusion]]
-== Machine inclusion:
-
-....
- USES list of machines
- INCLUDES list of machines
- SEES list of machines
- EXTENDS list of machines
- PROMOTES list of operations
- REFINES machine
-
- CSP_CONTROLLER controller will use controller.csp to guide machine (currently disabled in 1.3)
-
- Note:
- Refinement machines should express the operation preconditions in terms
- of their own variables.
-....
-
-[[definitions]]
-== Definitions:
-
-....
- NAME1 == Expression; Definition without arguments
- NAME2(ID,...,ID) == E2; Definition with arguments
-....
-
-....
-"FILE.def"; Include definitions from file`
-....
-
-There are a few Definitions which can be used to influence the animator:
-
-....
- GOAL == P to define a custom Goal predicate for Model Checking
- (the Goal is also set by using "Advanced Find...")
- SCOPE == P to limit the search space to "interesting" nodes
- scope_SETNAME == n..n to define custom cardinality for set SETNAME
- scope_SETNAME == n equivalent to 1..n
- SET_PREF_MININT == n
- SET_PREF_MAXINT == n
- SET_PREF_MAX_INITIALISATIONS == n max. number of intialisations computed
- SET_PREF_MAX_OPERATIONS == n max. number of enablings per operation computed
- SET_PREF_SYMBOLIC == TRUE/FALSE
- ASSERT_LTL... == "LTL Formula" using X,F,G,U,R LTL operators +
- Y,O,H,S Past-LTL operators +
- atomic propositions: e(OpName), [OpName], {BPredicate}
- ANIMATION_FUNCTION == e a function (INT*INT) +-> INT or an INT
- ANIMATION_FUNCTION_DEFAULT == e a function (INT*INT) +-> INT or an INT
- instead of any INT above you can also use BOOL or any SET
- ANIMATION_IMGn == "PATH to .gif" a path to a gif file
- ANIMATION_STRn == "sometext" a string without spaces
-....
-
-[[comments-and-pragmas]]
-== Comments and Pragmas
-
-....
-B supports two styles of comments:
- /* ... */ block comments
- // ... line comments
-....
-
-----
-ProB recognises several pragma comments of the form /*@ PRAGMA VALUE */
-The whitespace between @ and PRAGMA is optional.
- /*@symbolic */ put before comprehension set or lambda to instruct ProB
- to keep it symbolic and not try to compute it explicitly
- /*@label LBL */ associates a label LBL with the following predicate
- (LBL must be identifier or a string "....")
- /*@desc DESC */ associates a description DESC with the preceding predicate
- /*@file PATH */ associates a file for machines in SEES, INCLUDES, ...
- put pragma after a seen or included machine
- /*@package NAME */ at start of machine, machine file should be in folder NAME/...
- NAME can be qualified N1.N2...Nk, in which case the machine
- file should be in N1/N2/.../Nk
- /*@import-package NAME */ adds ../NAME to search paths for SEES,...
- NAME can also be qualified N1.N2...Nk, use after package pragma
- /*@unit U */ associates a unit U with the following constant or variable in the
- CONSTANTS or VARIABLES section, possible units are, e.g.,
- "m", "s", "mps", "m * s**-2" (quotes must be used);
- see https://www3.hhu.de/stups/prob/index.php/Tutorial_Unit_Plugin
-----
-
-[[file-extensions]]
-== File Extensions
-
-....
- .mch for abstract machine files
- .ref for refinement machines
- .imp for implementation machines
- .def for DEFINITIONS files
- .rmch for Rules machines for data validation
-....
-
-[[differences-with-atelierbb4free]]
-== Differences with AtelierB/B4Free
-
-Basically, ProB tries to be compatible with Atelier B and conforms to
-the semantics of Abrial's B-Book and of
-http://www.atelierb.eu/php/documents-en.php#manuel-reference[Atelier B's
-reference manual]. Here are the main differences with Atelier B:
-
- - Tuples without parentheses are not supported; write `(a,b,c)` instead of a,b,c
- - Relational composition has to be wrapped into parentheses; write `(f;g)`
- - Parallel product also has to be wrapped into parentheses; write `(f||g)`
- - Trees are not yet fully supported
- - The VALUES clause is only partially supported
- - Definitions have to be syntactically correct and be either an expression,
- predicate or substitution;
- the arguments to definitions have to be expressions;
- definitions which are predicates or substitutions must be declared before first use
- - Definitions are local to a machine
- - For ProB the order of fields in a record is not relevant (internally the fields are
- sorted), Atelier-B reports a type error if the order of the name of the fields changes
- - Well-Definedness: for disjunctions and implications ProB uses the L-system
- of well-definedness (i.e., for `P => Q`, P should be well-defined and
- if P is true then Q should also be well-defined)
- - ProB allows WHILE loops and sequential composition in abstract machines
- - ProB now allows the IF-THEN-ELSE and LET for expressions and predicates
- (e.g., `IF x<0 THEN -x ELSE x END or LET x BE x=f(y) IN x+x END`)
- - ProB's type inference is stronger than Atelier-B's, much less typing predicates
- are required
- - ProB accepts operations with parameters but without pre-conditions
- - ProB allows identifiers consisting of a single character
- - ProB allows multi-line strings and supports UTF-8 characters in strings,
- and ProB allows string literals written using three apostrophes (`'''string'''`)
- - ProB allows a she-bang line in machine files starting with `#!` +
-(If you discover more differences, please let us know!)
-
-See also: <<using_prob_with_atelier,Using ProB with AtelierB>>
-
-Also note that there are various differences between BToolkit and
-AtelierB/ProB:
-
- - AtelierB/ProB do not allow true as predicate;
- e.g., PRE true THEN ... END is not allowed (use BEGIN ... END instead)
- - AtelierB/ProB do not allow a machine parameter to be used in the PROPERTIES
- - AtelierB/ProB require a scalar machine parameter to be typed in the
- CONSTRAINTS clause
- - In AtelierB/ProB the BOOL type is pre-defined and cannot be redefined
-
-[[other-notes]]
-== Other notes
-ProB is best at treating universally quantified formulas of the form `!x.(x:SET => RHS)`,
-or `!(x,y).(x|->y:SET =>RHS)`, `!(x,y,z).(x|->y|->z:SET =>RHS)`, ...;+
-otherwise the treatment of `!(x1,...,xn).(LHS => RHS)` may delay until all values treated by LHS are known. +
-Similarly, expressions of the form `SIGMA(x).(x:SET|Expr)` and `PI(x).(x:SET|Expr)` lead to better constraint propagation. +
-The construction S:FIN(S) is recognised by ProB as equivalent to the Event-B finite(S) operator. +
-ProB assumes that machines and STRING values are encoded using UTF-8.
diff --git a/src/docs/chapter/user/12_BLanguage/02_Types.adoc b/src/docs/chapter/user/12_BLanguage/02_Types.adoc
deleted file mode 100644
index f400fc64a9ec0427d5a2a34f210ecba2df106ad2..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/02_Types.adoc
+++ /dev/null
@@ -1,103 +0,0 @@
-
-[[types]]
-= Types
-
-ProB requires all constants and variables to be typed. As of version
-1.3, ProB uses a new unification-based type inference and checking
-algorithm. As such, you should be able to use most Atelier B models
-without problem. On the other hand, certain models that ProB accepts
-will have to be rewritten to be type checked by Atelier B (e.g., by
-adding additional typing predicates). Also note that, in contrast to
-Atelier B, ProB will type check macro DEFINITIONS.
-
-[[what-is-a-basic-type-in-b]]
-== What is a basic type in B
-
-* BOOL
-* INTEGER
-* Any name of a set introduced in a SETS clause or introduced as a
-parameter of the machine
-* POW (τ) (power set) for τ being a type
-* τ1 * τ2 (Cartesian product) for τ1 and τ2 being two types
-
-[[what-needs-to-be-typed]]
-== What needs to be typed
-
-Generally speaking, any constant or variable. More precisely:
-
-* Constants declared in the CONSTANTS clause must be typed in the
-PROPERTIES clause;
-* Variables declared in the VARIABLES clause must be typed in the
-INVARIANT;
-* Arguments of an operation must be typed in the precondition PRE or a
-top-level SELECT statement of the operation;
-* Variables in universal or existential quantifications;
-* Variables of set comprehensions must be typed in a conjunct of the
-body of the set comprehension. For example, `\{xx | xx:NAT & xx>0 & xx<5}`
-is fine, but `\{xx | xx>0 & xx<5}` is not;
-* Variables of lambda abstractions must be typed in the predicate part
-of the abstraction. For example, `%yy.(yy:NAT|yy-1)` properly types the
-variable `yy`;
-* Variables introduced in ANY statements must be typed in the WHERE part
-of the statement.
-
-ProB will warn you if a variable has not been given a type.
-
-*HINT: The Analyse|Show Typing command reveals the typing that ProB has
-inferred for your constants and global variables.*
-
-[[restriction-on-the-domains-of-the-variables]]
-== Restriction on the Domains of the Variables
-
-Animating and verifying a B specification is in principle undecidable.
-ProB overcomes this by requiring that the domain of the variables is
-finite (i.e., with finitely many values) or integer. This ensures that
-the state space has finite size. Typing of the B specification ensures
-this restriction.
-
-In the B specification, a set is either defined explicitely, thus being
-a finite domain, or its definition is deferred. In the later case, the
-user can indicate the size of the set mySET (without defining its
-elements) by creating a macro in the DEFINITIONS clause with the name
-`scope_mySET` and an integer value (e.g. `scope_mySET==2`) or a value
-specified as a range (e.g. `scope_mySET == 1..12`). The macros with the
-prefix `scope_` will be used by ProB and do not modify the B
-specification. If the size of the set is unspecified, ProB considers the
-set to have a default size. The value for the default size is defined in
-the Preferences|Animation Preferences... preference window by the
-preference Size of unspecified sets in SETS section.
-
-The B method enables to specify the size of a set with the card operator
-in the PROPERTIES clause; this form of constraint is now supported by
-ProB, provided it is of a simple form `card(S)=Nr`, where `S` is a deferred
-set and `Nr` a natural number.
-
-[[enumeration-in-prob]]
-== Enumeration in ProB
-
-The typing information is used by ProB to enumerate the possible values
-of a constant or a variable whenever a specification does not narrow
-down that value to a single value.
-
-For example, if you write `xx:NAT & xx=1` ProB does not have to resort to
-enumeration as the `xx=1` constraint imposes a single possible value for
-`xx`. However, if you write `xx:NAT & xx<3` ProB will enumerate the possible
-values of `xx` in order to find those that satisfy the constraints imposed
-by the machine (here 0,1,2).
-
-ProB will use the constraints to try to cut down the enumeration space,
-and will resort to enumeration usually only as a last resort. So
-something like `xx:NAT & xx<10 & x>2 & x=5` will not result in
-enumeration.
-
-The enumeration range for integers is controlled by two preferences in
-the Preferences|Animation Preferences... preference window: `!MinInt`,
-used for expressions such as `xx::INT`, and `!MaxInt`, used for expressions
-such as `xx::NAT` preferences. Nevertheless, writing `xx: NAT & xx = 55`
-puts the value `55` in `xx` no matter what `!MaxInt` is set to, as no
-enumeration is required.
-
-Note that these preferences also apply to the mathematical integers
-(INTEGER) and natural numbers (NATURAL). In case a mathematical integer
-or natural number is enumerated (using `!MinInt` and `!MaxInt`) a warning is
-printed on the console.
diff --git a/src/docs/chapter/user/12_BLanguage/03_Deferred_Sets.adoc b/src/docs/chapter/user/12_BLanguage/03_Deferred_Sets.adoc
deleted file mode 100644
index cff2e164f59ecc9e01b700e3ac7942bfe663dace..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/03_Deferred_Sets.adoc
+++ /dev/null
@@ -1,69 +0,0 @@
-
-[[deferred-sets]]
-= Deferred Sets
-
-A deferred set in B is declared in the SETS Section and is not
-explicitly enumerated. In the example below, AA is a deferred set and BB
-is an enumerated set.
-
-....
-MACHINE M0
-SETS AA; BB={bb,cc,dd}
-END
-....
-
-ProB in general requires all deferred sets to be given a finite
-cardinality before starting animation or model checking. If no
-cardinality is specified, a default size will be used (which is
-controlled by the `DEFAULT_SETSIZE`
-<<controlling-prob-preferences,preference>>).
-
-In general (for both probcli and ProB Tcl/Tk) you can set the
-cardinality of a set AA either by
-
-* making it an enumerated set, i.e., adding `AA = {v1,v2,…}` to the SETS
-clause
-* adding a predicate `card(AA) = constant` to the PROPERTIES clause
-* Note: various other predicates in the PROPERTIES clause will also
-influence the size used for AA by ProB, for example:
-
-`- card(AA) > 1` +
-`- aa:AA & bb:AA & aa/=bb` +
-`- AA = {aa,bb} & aa/=bb` +
-`- …`
-
-* you can add a DEFINITION `scope_AA == constant` to instruct ProB to
-set the cardinality of AA to the constant.
-
-[[using-refinement-for-animation-preferences]]
-== Using Refinement for Animation Preferences
-
-Note: instead of adding AA = \{aa,bb} to the SETS clause you can also
-add `AA = {aa,bb} & aa/=bb` to the PROPERTIES clause. This can also be
-done in a refinement. A good idea is then to generate a refinement for
-animation with ProB (which may contain other important settings for
-animation):
-
-....
-REFINEMENT M0_ProB REFINES M0
-CONSTANTS aa,bb
-PROPERTIES
-AA = {aa,bb} & aa/=bb
-END
-....
-
-[[setting-deferred-set-cardinalities-within-probcli]]
-== Setting Deferred Set Cardinalities within probcli
-
-From the command-line, using probcli you can use the command-line
-switch:
-
-`-card <GS> <VAL>`
-
-Example:
-
-`probcli my.mch -card PID 5`
-
-See
-<<using-the-command-line-version-of-prob,manual
-page for probcli>>.
diff --git a/src/docs/chapter/user/12_BLanguage/10_External_Functions.adoc b/src/docs/chapter/user/12_BLanguage/10_External_Functions.adoc
deleted file mode 100644
index 6190fff8af0e19807c58617f1a33d7d88d4832f8..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/10_External_Functions.adoc
+++ /dev/null
@@ -1,116 +0,0 @@
-
-[[external-functions]]
-= External Functions
-
-As of version 1.3.5-beta7 ProB can make use of externally defined
-functions. These functions must currently be written in Prolog (in
-principle C, Java, Tcl or even other languages can be used via the
-SICStus Prolog external function interfaces). These functions can be
-used to write expressions, predicates, or substitutions. The general
-mechanism that is used is to mark certain DEFINITIONS as external, in
-which case ProB will make use of external Prolog code rather than using
-the right-hand-side of the DEFINITION whenever it is used. However,
-these DEFINITIONS can often (unless they are polymorphic) be wrapped
-into B (constant) functions. If you just want to use the standard
-external functions already defined by ProB, then you don't have to
-understand this mechanism in detail (or at all).
-
-[[standard-libraries-provided-by-prob]]
-== Standard Libraries provided by ProB
-
-In a first instance we have predefined a series of external functions
-and grouped them in various library machines and definition files:
-
-* `LibraryMath.mch`: defining sin, cos, tan, sinx, cosx, tanx, logx,
-gcd, msb, random as well as access to all other Prolog built-in
-arithmetic functions.
-* `LibraryStrings.mch`: functions manipulating B STRING objects by
-providing `length`, `append`, `split` and conversion functions `chars`,
-`codes`.
-* `LibraryFiles.mch`: various functions to obtain information about
-files and directories in the underlying file system.
-* `LibraryIO.def`: providing functions to write information to screen or
-file. Note: these external functions are polymorphic and as such cannot
-be defined as B constants: you have to use the DEFINITIONS provided in
-`LibraryIO.def`.
-* `CHOOSE.def`: providing the
-http://planetmath.org/encyclopedia/HilbertsEpsilonOperator.html[Hilbert
-choice operator] for choosing a designated element from each set. Again,
-this function is polymorphic and thus cannot be defined as a B function.
-This function is useful for defining
-<<recursively-defined-functions,recursive functions>> over sets (see
-also <<tla,TLA>>). Note that it in ProB it is undefined for the empty
-set.
-* `LibraryMeta.def`: providing access to meta-information about the
-loaded model (`PROJECT_INFO`), about the state space (`HISTORY`,
-`STATE_TRANS`, ...) and about ProB itself (GET_PREF, `PROB_INFO_STR`,
-`PROB_INFO_INT`,..).
-
-As of version 1.6.1 there is also a `READ_XML` external function to read
-in XML files and convert them to a B data structure with strings and
-records.
-
-Since version 1.5 the standard library is shipped with ProB and
-references to machines and DEFINITION-files in the standard library are
-resolved automatically when referenced (see <<probpath,PROBPATH>> for
-information about how to customize the lookup path).
-
-To use a library machine you can use the `SEES` mechanism:
-
-`SEES LibraryMath`
-
-In general you can do the following with an external function, such as
-`sin`, wrapped into a constant:
-
-* apply the function: `sin(x)`
-* compute the image of the function: `sin[1..100]`
-* compose the function with a finite relation on the left:
-`([1..100] ; sin)`
-* compute the domain of the function: `dom(sin)`
-
-To use a library definition file, you need to include the file in the
-DEFINITIONS clause:
-
--------------
-DEFINITIONS
- "LibraryIO.def"
--------------
-
-[[overview-of-the-external-function-definition-mechanism]]
-== Overview of the External Function DEFINITION Mechanism
-
-Currently, external functions are linked to classical B machines using B
-DEFINITIONS as follows:
-
-* one definition, which defines the function as it is seen by tools
-other than ProB (e.g., Atelier-B). Suppose we want to declare an
-external cosinus function named `COS`, then this definition could be
-`COS(x) == cos(x)`.
-* one definition declaring the type of the function. For `COS` this
-would be `EXTERNAL_FUNCTION_COS == INTEGER --> INTEGER`.
-* Prolog code which gets called by ProB in place of the right-hand-side
-of the first definition
-
-Usually, it is also a good idea to encapsulate the external function
-inside a CONSTANT which is defined as a lambda abstraction with as body
-simply the call to the first DEFINITION. For `COS` this would be
-`cos = %x.(x:NATURAL|COS(x))`. Observe that for Atelier-B this is a
-tautology. For ProB, the use of such a constant allows one to have a
-real B function representing the external function, for which we can
-compute the domain, range, etc.
-
-For the typing of an external function `NAME` with type `TYPE` there are
-three possibilities, depending on whether the function is a function, a
-predicate or a substitution:
-
-* `EXTERNAL_FUNCTION_NAME == TYPE`
-* `EXTERNAL_PREDICATE_NAME == TYPE`
-* `EXTERNAL_SUBSTITUTION_NAME == TYPE`
-
-In case the external function is polymorphic, the `DEFINITION` can take
-extra arguments: each argument is treated like a type variable. For
-example, the following is used in `CHOOSE.def` to declare the
-http://planetmath.org/encyclopedia/HilbertsEpsilonOperator.html[Hilbert
-choice operator]:
-
-* `EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)`
diff --git a/src/docs/chapter/user/12_BLanguage/11_Recursively_Defined_Functions.adoc b/src/docs/chapter/user/12_BLanguage/11_Recursively_Defined_Functions.adoc
deleted file mode 100644
index 5acacdb992275cc28e922cf2d15c5145988a2041..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/11_Recursively_Defined_Functions.adoc
+++ /dev/null
@@ -1,199 +0,0 @@
-
-[[recursively-defined-functions]]
-= Recursively Defined Functions
-
-[[symbolic-functions-and-relations]]
-== Symbolic Functions and Relations
-
-Take the following function:
-
----------
-CONSTANTS parity
-PROPERTIES
-parity : (NATURAL --> {0,1}) &
-parity(0) = 0 &
-!x.(x:NATURAL => parity(x+1) = 1 - parity(x))
----------
-
-Here, ProB will complain that it cannot find a solution for parity. The
-reason is that parity is a function over an infinite domain, but ProB
-tries to represent the function as a finite set of maplets.
-
-There are basically four solutions to this problem:
-
-* Write a finite function:
-
----------
-parity : (NAT --> {0,1}) &
-parity(0) = 0 &
-!x.(x:NAT & x<MAXINT => parity(x+1) = 1 - parity(x))
----------
-
-* Rewrite your function so that in the forall you do not refer to values
-of parity greater than x:
-
----------
-parity : (NATURAL --> {0,1}) &
-parity(0) = 0 &
-!x.(x:NATURAL1 => parity(x) = 1 - parity(x-1))
----------
-
-* Write your function constructively using a single recursive equation
-using set comprehensions, lambda abstractions, finite sets and set
-union. This requires ProB 1.3.5-beta7 or higher and you need to declare
-`parity` as `ABSTRACT_CONSTANT`. Here is a possible equation:
-
----------
-parity : INTEGER <-> INTEGER &
-parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
----------
-
-Note, you have to remove the check `parity : (NATURAL --> {0,1})`, as
-this will currently cause expansion of the recursive function. We
-describe this new scheme in more detail below.
-
-* Another solution is try and write your function constructively and
-non-recursively, ideally using a lambda abstraction:
-
----------
-parity : (NATURAL --> INTEGER) &
-parity = %x.(x:NATURAL|x mod 2)
----------
-
-* Here ProB detects that parity is an infinite function and will keep it
-symbolic (if possible). With such an infinite function you can:
-** apply the function, e.g., `parity(10001)` is the value `1`
-** compute the image of the function, e.g., `parity[10..20]` is `{0,1}`
-** check if a tuple is a member of the function, e.g., `20|->0 : parity`
-** check if a tuple is not a member of the function, e.g.,
-`21|->0 /: parity`
-** check if a finite set of tuples is a subset of the function, e.g.,
-`{20|->0, 120|->0, 121|->1, 1001|->1} <: parity`
-** check if a finite set of tuples is not a subset of the function,
-e.g., `{20|->0, 120|->0, 121|->1, 1001|->2} /<: parity`
-** compose the function with a finite relation, e.g.,
-`(id(1..10) ; parity)` gives the value `[1,0,1,0,1,0,1,0,1,0]`
-** sometimes compute the domain of the function, here, `dom(parity)` is
-determined to be `NATURAL`. But this only works for simple infinite
-functions.
-** sometimes check that you have a total function, e.g.,
-`parity: NATURAL --> INTEGER` can be checked by ProB. However, if you
-change the range (say from `INTEGER` to `0..1`), then ProB will try to
-expand the function.
-** In version 1.3.7 we are adding more and more operators that can be
-treated symbolically. Thus you can now also compose two symbolic
-functions using relational composition `;` or take the transitive
-closure (`closure1`) symbolically.
-
-You can experiment with those by using the <<eval-console,Eval
-console>> of ProB, experimenting for example with the following complete
-machine. Note, you should use ProB 1.3.5-beta2 or higher. (You can also
-type expressions and predicates such as
-`parity = %x.(x:NATURAL|x mod 2) & parity[1..10] = res` directly into
-the online version of the <<eval-console,Eval console>>).
-
----------
-MACHINE InfiniteParityFunction
-CONSTANTS parity
-PROPERTIES
-parity : NATURAL --> INTEGER &
-parity = %x.(x:NATURAL|x mod 2)
-VARIABLES c
-INVARIANT
-c: NATURAL
-INITIALISATION c:=0
-OPERATIONS
-inc = BEGIN c:=c+1 END;
-r <-- Parity = BEGIN r:= parity(c) END;
-r <-- ParityImage = BEGIN r:= parity[0..c] END;
-r <-- ParityHistory = BEGIN r:= (%i.(i:1..c+1|i-1) ; parity) END
-END`
----------
-
-You may also want to look at the tutorial page on
-<<tutorial-modeling-infinite-datatypes,modeling infinite datatypes>>.
-
-[[when-does-prob-treat-a-set-comprehension-or-lambda-abstraction-symbolically]]
-=== When does ProB treat a set comprehension or lambda abstraction symbolically ?
-
-Currently there are four cases when ProB tries to keep a function such
-as `f = %x.(PRED|E)` symbolically rather than computing an explicit
-representation:
-
-* the domain of the function is obviously infinite; this is the case for
-predicates such as `x:NATURAL`; in version 1.3.7-beta5 or later this has
-been considerably improved. Now ProB also keeps those lambda
-abstractions or set comprehensions symbolic where the constraint solver
-cannot reduce the domain of the parameters to a finite domain. As such,
-e.g., `{x,y,z| x*x + y*y = z*z}` or `{x,y,z| z:seq(NATURAL) & x^y=z}`
-are now automatically kept symbolic.
-* `f` is declared to be an `ABSTRACT_CONSTANT` and the equation is part
-of the `PROPERTIES` with `f` on the left.
-* the preference `SYMBOLIC` is set to true (e.g., using a `DEFINITION`
-`SET_PREF_SYMBOLIC == TRUE`)
-* a pragma is used to mark the lambda abstraction as symbolic as
-follows: `f = /*@ symbolic */ %x.(PRED|E)`; this requires ProB version
-1.3.5-beta10 or higher. In Event-B, pragmas are represented as Rodin
-database attributes and one should use the
-<<tutorial-symbolic-constants,symbolic constants plugin>>.
-
-[[recursive-function-definitions-in-prob]]
-== Recursive Function Definitions in ProB
-
-As of version 1.3.5-beta7 ProB now accepts recursively defined
-functions. For this:
-
-* the function has to be declared an `ABSTRACT_CONSTANT`.
-* the function has to be defined using a single recursive equation with
-the name of the function on the left of the equation
-* the right-hand side of the equation can make use of lambda
-abstractions, set comprehensions, set union and other finite sets
-
-Here is a full example:
----------
-MACHINE Parity
-ABSTRACT_CONSTANTS parity
-PROPERTIES
-parity : INTEGER <-> INTEGER &
-parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
-END
----------
-As of version 1.6.1 you can also use IF-THEN-ELSE and LET constructs in
-the body of a recursive function. The above example can for example now
-be written as:
-
----------
-MACHINE ParityIFTE
-ABSTRACT_CONSTANTS parity
-PROPERTIES
-parity : INTEGER <-> INTEGER &
-parity = %x.(x:NATURAL|IF x=0 THEN 0 ELSE 1-parity(x-1)END)
-SEND
----------
-
-[[operations-applicable-for-recursive-functions]]
-=== Operations applicable for recursive functions
-
-With such a recursive function you can:
-
-* apply the function to a given argument, e.g., `parity(100)` will give
-you 0;
-* compute the image of the function, e.g., `parity[1..10]` gives
-`{0,1}`.
-* composing it with another function, notably finite sequences:
-`([1,2] ; parity)` corresponds to the "map" construct of functional
-programming and results in the output `[1,0]`.
-
-Also, you have to be careful to avoid accidentally expanding these
-functions. For example, trying to check `parity : INTEGER <-> INTEGER`
-or `parity : INTEGER +-> INTEGER` will cause older version of ProB to
-try and expand the function. ProB 1.6.1 can actually check
-`parity:NATURAL --> INTEGER`, but it cannot check
-`parity:NATURAL --> 0..1`.
-
-There are the following further restrictions:
-
-* ProB does not support mutual recursion yet.
-* The function is not allowed to depend on other constants, unless those
-other constants can be valued in a deterministic way (i.e., ProB finds
-only one possible solution for them).
diff --git a/src/docs/chapter/user/12_BLanguage/13_Memoization.adoc b/src/docs/chapter/user/12_BLanguage/13_Memoization.adoc
deleted file mode 100644
index 1ce31b9b2d0bc93e475eaf33867b43f929ae90fa..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/13_Memoization.adoc
+++ /dev/null
@@ -1,48 +0,0 @@
-
-[[function-memoization]]
-= Memoization for Functions
-
-
-
-As of version 1.9.0-beta9 ProB allows you to annotate functions in the ABSTRACT_CONSTANTS section for memoization.
-[https://en.wikipedia.org/wiki/Memoization Memoization] is a technique for storing results of function applications and reusing the result if possible to avoid re-computing the function for the same arguments again.
-
-To enable memoization you either need to
-* annotate the function in the ABSTRACT_CONSTANTS section with the pragma `/*@desc memo */`
-* set the preference `MEMOIZE_FUNCTIONS` to true. In this case ProB will try to memoize all functions in the ABSTRACT_CONSTANTS section, unless they are obviously small and finite and can thus be precomputed completely.
-
-Take the following example:
-
----------
- MACHINE MemoizationTests
- ABSTRACT_CONSTANTS
- fib /*@desc memo */,
- fact /*@desc memo */
- PROPERTIES
- fib = %x.(x:NATURAL |
- (IF x=0 or x=1 THEN 1
- ELSE fib(x-1)+fib(x-2)
- END))
- &
- fact = %x.(x:NATURAL|(IF x=0 THEN 1 ELSE x*fact(x-1) END))
- ASSERTIONS
- fib(30)=1346269;
- fib[28..30] = {514229,832040,1346269};
- END
----------
-
-Memoization means that the recursive Fibonacci function now runs in linear time rather than in exponential time.
-Generally, memoization is useful for functions which are complex to compute but which are called repeatedly with the same arguments.
-
-As can be seen above, memoization is active for
-* function calls such as fib(30) (which in turn calls fib(29) and fib(28) which are also memoized)
-* computation of relational image such as fib[28..30], which internally results in three function calls to fib
-
-The following points are relevant:
-* Memoization is currently only possible for functions declared in the ABSTRACT_CONSTANTS section
-* Memoization means that all results of function calls are stored. The memoization table is reset when another B machine is loaded or the same B machine is re-loaded.
-* Memoized functions are automatically marked as symbolic. If your function is finite and relatively small, it may be better to put the function into the CONCRETE_CONSTANTS section so that it gets computed in its entirety once.
-* Memoization of a function f is currently <b>not</b> active for computations such as dom(f), ran(f) or x|->y:f.
-
-
-With the command-line version probcli you can use the `-profile` command to obtain some statistics about memoization.
\ No newline at end of file
diff --git a/src/docs/chapter/user/12_BLanguage/20_Tips_B_Idioms.adoc b/src/docs/chapter/user/12_BLanguage/20_Tips_B_Idioms.adoc
deleted file mode 100644
index 20138fe7fd57426d3f41a51399ef552a5313432d..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/20_Tips_B_Idioms.adoc
+++ /dev/null
@@ -1,242 +0,0 @@
-
-[[tips-b-idioms]]
-= Tips: B Idioms
-
-Also have a look at <<tips-writing-models-for-prob,Tips:_Writing_Models_for_ProB>>.
-
-[[let]]
-== Let
-
-Classical B only has a LET substitution, no let construct for predicates
-or expressions. Event-B has no let construct whatsoever.
-
-[[probs-extended-syntax]]
-=== ProB's Extended Syntax
-
-Since version *1.6.1-beta* (28th of April 2016), ProB supports the use
-of the `LET` substitution syntax in expressions and predicates.
-
-[[examples-let]]
-==== Examples:
-
-----
->>> LET a BE a = 10 IN a + 10 END
-Expression Value = 20
-----
-
-----
->>> LET a BE a=10 IN a END + 10
-Expression Value = 20
-----
-
-----
->>> LET a BE a=10 IN a END = 10
-Predicate is TRUE
-----
-
-----
->>> LET a BE a = 10 IN a < 10 END
-Predicate is FALSE
-----
-
-----
->>> LET a BE a=10 IN a /= 10 END or 1=1
-Predicate is TRUE
-----
-
-----
->>> LET a, b BE a = 10 & b = 1 IN a + b END
-Expression Value = 11
-----
-
-[[let-for-predicates]]
-=== Let for predicates
-
-For predicates this encodes a let predicate:
-
-`#x.(x=E & P)`
-
-corresponds to something like
-
-`let x=E in P`
-
-Within set comprehensions one can use the following construct:
-
-`dom({x,y|y=E & P})`
-
-corresponds to something like
-
-`{x|let y=E in P}`
-
-One can also use the ran operator or introduce multiple lets in one go:
-
-`dom(dom({x,y,z|y=E1 & z=E2 &P}))`
-
-or
-
-`ran({y,z,x|y=E1 & z=E2 &P})`
-
-both encode
-
-`{x|let y=E1 & z=E2 in P}`
-
-[[let-for-expressions]]
-=== Let for expressions
-
-In case F is a set expression, then the following construct can be used
-to encode a let statement:
-
-`UNION(x).(x=E|F)`
-
-corresponds to something like
-
-`let x=E in F`
-
-The following construct has exactly the same effect:
-
-`INTER(x).(x=E|F)`
-
-[[if-then-else]]
-== If-Then-Else
-
-Classical B only has an IF-THEN-ELSE substitution (aka statement), no
-such construct for predicates or expressions.
-
-[[nightly-builds]]
-=== Nightly Builds
-
-Since version *1.6.1-beta* (28th of April 2016), ProB supports the use
-of the `LET` substitution syntax in expressions and predicates.
-
-[[examples-if-then-else]]
-==== Examples:
-
-----
->>> IF 1 = 1 THEN 3 ELSE 4 END
-Expression Value = 3
-----
-
-----
->>> IF 1 = 1 THEN 3 ELSE 4 END + 5
-Expression Value = 8
-----
-
-----
->>> IF 1=1 THEN TRUE = FALSE ELSE TRUE=TRUE END
-Predicate is FALSE
-----
-
-----
->>> IF 1=1 THEN TRUE = FALSE ELSE TRUE=TRUE END or 1=1
-Predicate is TRUE
-----
-[[expressions]]
-=== Expressions
-
-The following construct
-
-`%((x).(x=0 & PRED|C1)\/%(x).(x=0 & not(PRED)|C2)) (0)`
-
-encodes an if-then-else for expressions:
-
-`IF PRED THEN C1 ELSE C2 END`
-
-The former lambda-construct is recognised by ProB and replaced
-internally by an if-then-else construct. The latter syntax is actually
-now recognised as well by ProB 1.6 (version 1.6.0 still requires
-parentheses around the IF-THEN-ELSE; version 1.6.1 no longer requires
-them).
-
-[[finite]]
-== finite
-
-In classical B there is no counterpart to the Event-B `finite` operator.
-However, the following construct has the same effect as `finite(x)` (and
-is recognised by ProB):
-
-`x : FIN(x)`
-
-[[all-different]]
-== all-different
-
-One can encode the fact that n objects x1,...,xn are pair-wise different
-using the following construct (recognised by ProB):
-
-`card({x1,...,xn})=n`
-
-[[map]]
-== map
-
-Given a function f and a sequence `sqce` one can map the function over
-all elements of `sqce` using the relational composition operator `;`:
-
-`(sqce ; f)`
-
-For example, `([1,2,3] ; succ)` gives us the sequence `[2,3,4]`.
-
-[[recursion-using-closure1]]
-== Recursion using closure1
-
-Even though B has no built-in support for recursion, one can use the
-transitive closure operator `closure1` to compute certain recursive
-functions. For this we need to encode the recursion as a step function
-of the form:
-
-`%(in,acc).(P|(inr,accr))`
-
-where P is a predicate which in case we have not yet reached a base case
-for the input value `in`. The computation result has to be stored in an
-accumulator: `acc` is the accumulator before the recursion step, `accr`
-after. `inr` is the new input value for the recursive call. In case the
-base case is reached for `in`, the predicate P should be false and the
-value of the recursive call should be the value of the accumulator.
-
-The value of the recursive function can thus be obtained by calling:
-
-`closure1(step)[{(in,ia)}](b)`
-
-where `in` is the input value, `b` is the base case and `ia` is the
-initial (empty) accumulator.
-
-For example, to sort a set of integers into a ascending sequence, we
-would define the step function as follows:
-
-`step = %(s,o).(s/={} | (s\{min(s)},o<-min(s)))`
-
-A particular call would be:
-
-`closure1(step)[{({4,5,2},[])}]({})`
-
-resulting in the sequence `[2,4,5]`.
-
-Observe that, even though `closure1(step)` is an infinite relation, ProB
-can compute the relational image of `closure1(step)` for a particular
-set such as `{({4,5,2},[])}` (provided the recursion terminates).
-
-[[recursion-using-abstract_constants]]
-== Recursion using ABSTRACT:_CONSTANTS
-
-Recursive functions can be declared using the `ABSTRACT_CONSTANTS`
-section in B machines. Functions declared as `ABSTRACT_CONSTANTS` are
-treated symbolically by ProB and not evaluated eagerly.
-
-For example, to sort a set of integers into a ascending sequence, as
-above, we would define a recursive function as follows:
-
-----
-ABSTRACT_CONSTANTS
-Recursive_Sort
-PROPERTIES
-Recursive_Sort : POW(INTEGER) <-> POW(INTEGER*INTEGER)
-& Recursive_Sort =
-%in.(in : POW(INTEGER) & in = {} | [])
-\/ %in.(in : POW(INTEGER) & in /= {}
-| min(in) -> Recursive_Sort(in\{min(in)}))
-----
-By defining `Recursive_Sort` as an abstract constant we indicate that
-ProB should handle the function symbolically, i.e. ProB will not try to
-enumerate all elements of the function. The recursive function itself is
-composed of two single functions: a function defining the base case and
-a function defining the recursive case. Note, that the intersection of
-the domains of these function is empty, and hence, the union is still a
-function.
diff --git a/src/docs/chapter/user/12_BLanguage/21_Tips_Writing_Models_for_ProB.adoc b/src/docs/chapter/user/12_BLanguage/21_Tips_Writing_Models_for_ProB.adoc
deleted file mode 100644
index 6fb548d84b644f583618dfae5b316a48b1510e21..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/21_Tips_Writing_Models_for_ProB.adoc
+++ /dev/null
@@ -1,122 +0,0 @@
-
-[[tips-writing-models-for-prob]]
-= Tips: Writing Models for ProB
-
-The most common issue is that ProB needs to find values for the
-constants which satisfy the properties (aka axioms in Event-B). You
-should read the tutorial pages on this (in particular
-<<tutorial-setup-phases,Understanding the ProB Setup Phases>> and
-<<tutorial-troubleshooting-the-setup,Tutorial Troubleshooting the
-Setup>>)
-
-* Try to use ProB as early as possible in the modeling process; this
-will make it easier to identify the cause of problems (and also will
-hopefully give you valuable feedback on your model as well).
-
-* Try to put complicated properties into ASSERTIONS rather than
-PROPERTIES. Something like `!s.(s<:S => P)` will have to check `P` for
-all subsets of `S` (i.e., checking is exponential in the size of `S`)
-
-* You may wish to give explicit values to certain constants. For
-example, in Event-B, this can be done by refining a context.
-
-* Try to set the symbolic preference of ProB to true (use
-`-p SYMBOLIC TRUE` for probcli or set the Animation preference "Lazy
-expansion ... (SYMBOLIC)" to true) if you have large or infinite
-functions (see discussion about closure below). In symbolic mode, ProB
-will keep lambda expressions and set comprehensions symbolic as much as
-possible. In classical B, any `ABSTRACT_CONSTANT` will also at first be
-kept symbolic. However, there are only limited things you can do with a
-"symbolic" function without forcing an expansion: taking the value of
-a function is fine, computing the image over a set is also possible as
-is taking the union with another symbolic function.
-
-[[effective-constraint-solving-with-prob]]
-== Effective Constraint Solving with ProB
-
-[[existential-quantifiers]]
-=== Existential Quantifiers
-
-Existential quantifiers can pose subtle problems when solving constraint
-problems.
-
-For an existential quantifier `#x.P` ProB will often wait until all
-variables in P apart from x are known to evaluate the quantifier.
-Indeed, if all variables apart from x are known, ProB can stop when it
-finds one solution for x. Take for example:
-
-`#x.(x:0..1000 & x=p) & p:101..104`
-
-Here, ProB will wait until p is known (e.g., 101) before enumerating
-possible values for x. However, it could be that the predicate P is
-required to instantiate the outside variable, as in this example:
-
-`#x.(x:100..101 & x=p) & p:NATURAL`
-
-Here, the existential quantifier is required to narrow down the possible
-values of p. Thus, before enumerating an unbounded variable, ProB will
-start enumerating the existential variable x. Note, however, that the
-priority with which it will be enumerated is much lower than if it was a
-regular variable! Hence:
-
-* Tip: Beware of putting important domain variables into existential
-quantifiers.
-
-One exception to the above treatment are existential quantifiers of the
-form `#x.(x=E & P)`. They are recognised by ProB as LET-PREDICATES. This
-is a good use of the existential quantifier. This quantifier will never
-"block".
-
-* Tip: use existential quantifiers as LET-PREDICATES `#x.(x=E & P)` to
-avoid repeated computations
-(<<common-subexpression-elimination,common-subexpression
-elimination>>) and to make your predicates more readable.
-
-[[universal-quantifiers]]
-== Universal Quantifiers
-
-The situation is very similar to the existential quantifier. In the
-worst case ProB may delay evaluating a universal quantifier `!x.(P=>Q)`
-until all variables in `P` are known so as to be able to determine all
-values of `x` for which `Q` has to be checked.
-
-There are a few optimisations:
-
-* If ProB can determine that the domain of `x` is finite and small, then
-the universal quantifier will be expanded into a conjunction. E.g.,
-`!x.(x:1..3 & x<y => P(x))` will be expanded into
-`(1<y => P(1)) & (2<y => P(2)) & (3<y => P(3))` even if `y` is not yet known.
-Setting the preference `SMT` to true will increase the threshold for
-which this expansion occurs.
-
-* If the quantifier is of the form `!x.(x:S => P)`, then P will be
-gradually checked for every new value that is added to `S`; ProB does
-not wait for `S` to be completely known before checking the quantifier.
-
-Tip: sometimes one can force expansion of a quantifier by using two
-implications. E.g., suppose we know that the domain of `s` is a subset
-of `1..10`, then we can rewrite `!x.(s(x)=5 => P(x))` into
-`!x.(x:1..10 => (s(x)=5 => P(x)))`. This will ensure that the quantifier
-is checked.
-
-[[transitive-closure-in-event-b]]
-== Transitive Closure in Event-B
-
-Classical B contains the transitive closure operator `closure1`. It is
-not available by default in Event-B, and axiomatisations of it may be
-very difficult to treat by ProB. Indeed, if you define the transitive
-closure in Event-B as a function `tclos` from relations to relations,
-ProB will try to find a value for `tclos`. The search space for this
-function is `(2\^n*n)^(2^n*n)`, where `n` is the size of the base set
-(see <<tutorial-understanding-the-complexity-of-b-animation,Tutorial
-Understanding the Complexity of B Animation>>). For n=3 this is already
-way too big too handle (the search space has 1.40e+1387 relations).
-
-Hence, in Event-B, you should use a theory of the transitive closure
-which contains a special mapping file which instructs ProB to use the
-classical B operator. See <<event-b-theories,the page on supporting
-Event-B theories>> along with the links to theories that can be used
-efficiently with ProB.
-
-* Tip: within set comprehensions use the form `dom({x,y|P})` rather than
-`{x|#y.P}`. This is generally more efficient.
diff --git a/src/docs/chapter/user/12_BLanguage/22_Debugging.adoc b/src/docs/chapter/user/12_BLanguage/22_Debugging.adoc
deleted file mode 100644
index 396400720f54bd2bbb3aaedfd137374a26233ba2..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/22_Debugging.adoc
+++ /dev/null
@@ -1,185 +0,0 @@
-
-[[debugging-prob]]
-= Debugging Models with ProB
-
-There are various ways in which you can debug your model.
-We focus here on debugging performance issues
-
-== Debugging with LibraryIO
-
-The [[External Functions|standard library]] "LibraryIO.def" contains various external functions and predicates with which you can instrument your formal model.
-
-To use the library in your model you need to include the following
-
-....
-DEFINITIONS
- "LibraryIO.def"
-....
-
-With the external predicate <tt>printf</tt> you can view values of variables and identifiers. The printf predicate is always true and will print its arguments when all of them have been fully computed.
-The printf predicate uses the format from SICStus Prolog for the format string.
-The most important are <tt>~w</tt> for printing an argument and <tt>~n</tt>
-for a newline. There must be exactly as many <tt>~w</tt> in the format string as there
-are aguments.
-Below is a small example, to inspect in which order ProB enumerates values.
-The example is typed in the REPL of [[Using_the_Command-Line_Version_of_ProB|probcli]]
-(started using the command <tt>probcli -repl File.mch</tt> where <tt>File.mch</tt> includes the definitions section above):
-
-....
->>> {x,y | x:1..5 & y:1..2 & x+y=6 & printf("x=~w~n",[x]) & printf("y=~w~n",[y])}
-y=1
-x=5
-y=2
-x=4
-Expression Value =
-{(4|->2),(5|->1)}
-....
-
-As you can see, ProB has enumerated y before x, as its domain was smaller.
-
-You can use the external function <tt>observe</tt> to inspect a list of
-identifiers:
-
-....
->>> {x,y | x:1..5 & y:1..2 & x+y=6 & observe((x,y))}
- observing x
- observing y
- y = 1 (walltime: 562188 ms)
-. x = 5 (walltime: 562188 ms)
-..* Value complete: x |-> y = (5|->1) (walltime: 562188 ms)
-------
- y = 2 (walltime: 562188 ms)
-. x = 4 (walltime: 562188 ms)
-..* Value complete: x |-> y = (4|->2) (walltime: 562188 ms)
-------
-Expression Value =
-{(4|->2),(5|->1)}
-....
-
-With the external function <tt>TIME</tt> you can get the current time in seconds:
-....
->>> TIME("sec")
-Expression Value =
-11
->>> TIME("now")
-Expression Value =
-1581432376
->>> TIME("now")
-Expression Value =
-1581432377
-....
-
-With the external function <tt>DELTA_WALLTIME</tt> you can get the time in milliseconds since the last call to <tt>DELTA_WALLTIME</tt>.
-
-== Performance Messages
-
-By setting the preference <tt>PERFORMANCE_INFO</tt> to <tt>TRUE</tt> ProB will print various performance messages.
-For example it may print messages when the evaluation of comprehension sets has exceeded a threshold. This threshold (in ms) can be influenced by setting the preference
-<tt>PERFORMANCE_INFO_LIMIT</tt>.
-
-== Debugging Constants Setup
-
-By setting the preference <tt>TRACE_INFO</tt> to <tt>TRUE</tt> ProB will print additional messages when evaluating certain predicates, in particular the <tt>PROPERTIES</tt> clause of a B machine.
-With this feature you can observe how constants get bound to values and can sometimes spot expensive predicates and large values.
-Some additional information about debugging the PROPERTIES can be found in the [[Tutorial Troubleshooting the Setup]].
-
-Let us take the following machine
-....
-MACHINE Debug
-CONSTANTS a,b,c
-PROPERTIES
- a = card(b) &
- b = %x.(x:1..c|x*x) &
- c : 1000..1001 & c < 1001
-VARIABLES x
-INVARIANT x:NATURAL
-INITIALISATION x:=2
-OPERATIONS
- Sqr = SELECT x:dom(b) THEN x := b(x) END;
- Finished = SELECT x /: dom(b) THEN skip END
-END
-....
-
-Here is how we can debug the constants setup:
-
-....
-$ probcli Debug.mch -p TRACE_INFO TRUE -init
-% unused_constants(2,[a,c])
-nr_of_components(1)
-
- ====> (1) c < 1001
-
- ====> (1) a = card(b)
-
- ====> (1) b = %x.(x : 1 .. c|x * x)
-
- ====> (1) c : 1000 .. 1001
-finished_processing_component_predicates
-grounding_wait_flags
- :?: a int(?:0..sup)
- :?: b VARIABLE: _31319 : GRVAL-CHECK
- :?: c int(?:inf..1000)
---1-->> a
- int(1000)
---1-->> b
- AVL.size=1000
---1-->> c
- int(1000)
-% Runtime for SOLUTION for SETUP_CONSTANTS: 107 ms (walltime: 110 ms)
-% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
-
- =INIT=> x := 2
- [=OK= 0 ms]
-....
-
-== Debugging Animation or Execution
-
-By using the <tt>-animate_stats</tt> flag, you can see execution times for operations that are executed either using the <tt>-execute</tt> or <tt>-animate</tt> commands.
-In verbose mode (<tt>-v</tt> flag) you also see the memory consumption.
-
-....
-$ probcli Debug.mch -execute_all -animate_stats
-% unused_constants(2,[a,c])
-% Runtime for SOLUTION for SETUP_CONSTANTS: 79 ms (walltime: 80 ms)
-1 : SETUP_CONSTANTS
- 91 ms walltime (89 ms runtime), since start: 1107 ms
-2 : INITIALISATION
- 5 ms walltime (4 ms runtime), since start: 1112 ms
-3 : Sqr
- 10 ms walltime (10 ms runtime), since start: 1123 ms
-4 : Sqr
- 0 ms walltime (0 ms runtime), since start: 1123 ms
-5 : Sqr
- 1 ms walltime (0 ms runtime), since start: 1124 ms
-6 : Sqr
- 0 ms walltime (0 ms runtime), since start: 1124 ms
-7 : Finished
- 3 ms walltime (4 ms runtime), since start: 1127 ms
-Infinite loop reached after 8 steps (looping on Finished).
-% Runtime for -execute: 116 ms (with gc: 116 ms, walltime: 119 ms); time since start: 1132 ms
-....
-
-== Profiling ==
-
-You can obtain some profiling information using the <tt>-prob_profile</tt> command.
-This command unfortunately requires that ProB was compiled using special flags (<tt>-Dprob_profile=true</tt> and <tt>-Dprob_src_profile=true</tt>).
-
-....
-$ probcli ../prob_examples/public_examples/B/Tutorial/Debug.mch -execute_all -prob_profile
-...
---------------------------
-ProB profile info after 5685 ms walltime (5248 ms runtime)
-----Source Location Profiler Information----
-----Tracks number of times B statements (aka substitutions) are hit
- 1 hits at 9:15 -- 9:19 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch
- 1 hits at 12:37 -- 12:41 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch
- 4 hits at 11:29 -- 11:38 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch
-----
----- ProB Runtime Profiler ----
----- Tracks time spent in B operations and invariant evaluation
- $setup_constants : 78 ms (80 ms walltime & 80 ms max. walltime; #calls 1)
- Sqr : 9 ms (9 ms walltime & 9 ms max. walltime; #calls 1)
- $initialise_machine : 5 ms (5 ms walltime & 5 ms max. walltime; #calls 1)
- Finished : 3 ms (4 ms walltime & 4 ms max. walltime; #calls 1)
- Total Walltime: 98 ms for #calls 4
-....
diff --git a/src/docs/chapter/user/12_BLanguage/Tutorial_Modeling_Infinite_Datatypes.adoc b/src/docs/chapter/user/12_BLanguage/Tutorial_Modeling_Infinite_Datatypes.adoc
deleted file mode 100644
index bac81b125574beb2d7416361365845f11a396fc1..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/Tutorial_Modeling_Infinite_Datatypes.adoc
+++ /dev/null
@@ -1,73 +0,0 @@
-
-[[tutorial-modeling-infinite-datatypes]]
-= Tutorial Modeling Infinite Datatypes
-
-This tutorial describes how to model (and how not to model)
-infinite datatypes so that they can be animated with ProB. (You may also
-want to look at the manual page on
-<<recursively-defined-functions,recursive functions>>.) We illustrate
-this by modeling a Stack datatype.
-
-Unfortunately, the following B machine does not work with ProB:
-
-----
-MACHINE StackAxioms1
-SETS Stack
-CONSTANTS pop, push,empty
-PROPERTIES
-empty:Stack &
-pop : Stack \ {empty} --> Stack &
-!s,x . (s : Stack & x : NAT => pop(push(s |-> x)) = s)
-& push: Stack*NAT --> Stack \ {empty}
-END
-----
-
-The problem with the above model is that the `PROPERTIES` can only be
-satisfied if `Stack` is infinite. However, ProB does not presently
-support infinite deferred sets. We need to do a more constructive
-definition and use the infinite set ProB knows about: `INTEGER`. This is
-done in the following machine, which is included in the
-`examples/Tutorial` directory of the
-https://www3.hhu.de/stups/prob/index.php/Download[ProB
-distribution].
-
-----
-MACHINE StackConstructive
-/* A machine that shows how to model a stack of type RANGE so that it can
-be animated and validated with ProB */
-/* We could have used the sequence operations instead;
-our intention was also to show how you can model this in Event-B */
-DEFINITIONS Stack == (INTEGER <-> RANGE)
-SETS RANGE
-CONSTANTS empty, push, pop, tops
-PROPERTIES
-empty : Stack & empty = {} &
-push : (RANGE * Stack) <-> Stack &
-push = %(x,s).(x:RANGE & s:Stack | s \/ {card(s)+1|->x}) &
-pop: Stack <-> Stack &
-pop = %s.(s:Stack| {card(s)} <<| s) &
-tops: Stack <-> RANGE &
-tops = %s.(s:Stack| s(card(s)))
-ASSERTIONS
-/* the assertions cannot be checked by ProB, they will trigger
-the expansion of the infinite functions above */
-tops: Stack \ {empty} --> RANGE;
-push: (RANGE*Stack) --> Stack \ {empty};
-pop: Stack \ {empty} --> Stack
-VARIABLES cur
-INVARIANT
-cur: Stack
-& cur : seq(RANGE) /* a slightly stronger invariant */
-INITIALISATION cur := empty
-OPERATIONS
-Push(yy) = PRE yy:RANGE THEN cur:= push(yy,cur) END;
-Pop = PRE cur /= empty THEN cur := pop(cur) END;
-t <-- Top = PRE cur /= empty THEN t := tops(cur) END
-END
-----
-
-As the screenshot illustrates, this model can now be animated with ProB.
-Observe how the functions push, pop and tops are kept symbolic in the
-State View.
-
-image::StackConstructiveProB.png[]
diff --git a/src/docs/chapter/user/12_BLanguage/WD/00_section_header.adoc b/src/docs/chapter/user/12_BLanguage/WD/00_section_header.adoc
deleted file mode 100644
index 92a1941243d9f0d7ca0b3d39e584c0274c5c91f7..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/WD/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[well-definedness]]
-= Well Definedness
-:leveloffset: +1
diff --git a/src/docs/chapter/user/12_BLanguage/WD/01_Well-Definedness_Checking.adoc b/src/docs/chapter/user/12_BLanguage/WD/01_Well-Definedness_Checking.adoc
deleted file mode 100644
index 86900536b03f7f18c677b8dc349d36f2e258a593..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/WD/01_Well-Definedness_Checking.adoc
+++ /dev/null
@@ -1,43 +0,0 @@
-
-[[well-definedness-checking]]
-= Well-Definedness Checking
-
-Well-definedness errors can occur in B in the following circumstances:
-
-* a division by 0: `r=100/0`
-* modulo by 0, modulo involving negative numbers: `r=100 mod -2`
-* exponentiation using a negative exponent: `2**(-2)`
-* application of a function outside of its domain: `f={1|->2} & r=f(3)`
-* application of a relation which is not a function:
-`f={1|->2,1|->3} & r=f(1)`
-* application of the card operator to infinite sets: `card(NATURAL)`
-* application of the min or max operator to empty sets:
-`x={} & r=max(x)`
-* application of the inter operator to empty sets: `x={} & r=inter(x)`
-* wrong application of sequence operators
-** taking the first, front, last, tail of an empty sequence:
-`x=<> & r=first(x)`
-** using negative indexes for prefix or suffix sequence: `x = s /|\ -1`
-** using too large indexes for suffix sequence: `x= s \|/ (size(s)+1)`
-* ...
-
-To ensure that your models only contain well-defined formulas, Rodin
-creates well-definedness proof obligations for Event-B and Atelier-B can
-create them for classical B. ProB will check for well-definedness during
-constraint solving, animation and model checking. However, by default
-this check is not very extensive. You can force ProB to look more
-aggressively for well-definedness issues in your formulas by setting the
-following preference to true:
-
-* `TRY_FIND_ABORT`
-
-However, even with this, the search is not guaranteed to be exhaustive.
-Also, ProB's constraint solving does not necessarily solve formulas from
-left to right. Hence, the following formulas will be considered
-well-defined (and on can argue that they are) by ProB:
-
-* `r=1/x & x/=0`
-
-Technically speaking, for disjunctions and implications ProB uses the
-L-system of well-definedness (i.e., for P => Q, P should be well-defined
-and if P is true then Q should also be well-defined).
diff --git a/src/docs/chapter/user/12_BLanguage/WD/ZZ_section_footer.adoc b/src/docs/chapter/user/12_BLanguage/WD/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/WD/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1
diff --git a/src/docs/chapter/user/12_BLanguage/ZZ_section_footer.adoc b/src/docs/chapter/user/12_BLanguage/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/12_BLanguage/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1