diff --git a/src/docs/chapter/user/20_Validation/00_section_header.adoc b/src/docs/chapter/user/20_Validation/00_section_header.adoc
deleted file mode 100644
index af7d604be139e5e4c3c7097a4553f2ebb61bef07..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[validation]]
-= Validation
-:leveloffset: +1
diff --git a/src/docs/chapter/user/20_Validation/01_MC/Tutorial_Complete_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/01_MC/Tutorial_Complete_Model_Checking.adoc
deleted file mode 100644
index 5095a17d1847a17e906099cf611e2767ea4024b3..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/01_MC/Tutorial_Complete_Model_Checking.adoc
+++ /dev/null
@@ -1,186 +0,0 @@
-
-[[tutorial-complete-model-checking]]
-= Tutorial Complete Model Checking
-
-We assume that you have completed
-<<tutorial-first-model-checking,Tutorial First Model Checking>>.
-There we saw how to find invariant violations using the model checker.
-
-In this part we use the following B Machine:
-
-....
-DEFINITIONS
-MACHINE SimpleCounterForMC
-DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5
-VARIABLES count
-INVARIANT
- count: 1..MAX
-INITIALISATION count := 1
-OPERATIONS
-  Increase(y) = PRE y: 1..(MAX-count) THEN
-     count := count+y
-  END;
-  Reset = BEGIN count :: 1..MAX END
-END
-....
-
-To load this machine into ProB you can select "New..." from the
-_File_ menu, choose a file name (e.g., "SimpleCounterForMC.mch") and
-then paste the text above into the ProB source pane and choose "Save
-and Reopen" from the _File_ menu.
-
-Note that the `DEFINITION SET_PREF_MAX_OPERATIONS==5` means that ProB
-will compute at most 5 possible ways to execute any given operation
-(i.e., Increase and Reset in this case). We return to this issue below.
-
-[[successful-model-checking]]
-== Successful Model Checking
-
-Now select the "Model Check..." command in the _Verify_ menu which
-brings up the model checking dialog box:
-
-image::ProBWinModelCheckDialog.png[]
-
-Now click the "Model Check" button. After a short while, ProB will give you the following message:
-
-image::ProBModelCheckNoCounterExampleFound.png[]
-
-This message means that ProB has examine all possible states of your B
-model and has found no invariant violation and no deadlock. (In this
-case there are 4 states and one root node.)
-
-Does this mean that the B machine is guaranteed to be correct? Does this
-mean that the AtelierB provers will be able to prove the B machine
-correct? In this case yes, but in general, we have to be very careful
-about interpreting a completed model check. Below we examine several
-issues that have to be considered.
-
-[[computing-all-transitions]]
-== Computing All Transitions
-
-Let us now adapt the above B machine by changing the DEFINITION of MAX
-to 6. Now repeat the model checking exercise above. This time ProB will
-produce the following message:
-
-image::ProBModelCheckNoCounterExampleFoundTrans.png[]
-
-Again no invariant violations or deadlocks were found, but this time
-ProB warns us that not all transitions were computed. Indeed, the
-`SET_PREF_MAX_OPERATIONS` definition tells ProB to compute at most 5
-ways to execute an operation. In this case, there are 6 ways to execute
-the "Reset" operation. As such, ProB may have missed certain states
-and thus may have missed an invariant violation.
-
-Indeed, when you double click on the "INITIALISATION(1)" entry in the
-"EnabledOperations" pane, you will see the following:
-
-image::ProBSimpleCounterForMC_Max.png[]
-
-The orange "max" button tells us that not all operations were
-computed.
-
-In this case, there was no error, but assume we change the definition of
-the Reset operation to:
-
-....
-  Reset = BEGIN count :: 1..MAX+1 END
-....
-
-and repeat the model checking. We will get the exact same result as
-above, but this time the machine is actually incorrect. The only way to
-solve ensure that ProB checks the entire state space is to increase the
-"MAX_OPERATIONS" preference to a suitably large value, e.g.,
-`SET_PREF_MAX_OPERATIONS==8` in this case. Now model checking will find
-a counter example:
-
-image::ProBSimpleCounterForMC_InvViol.png[]
-
-[[tutorial-deferred-sets]]
-== Deferred Sets
-
-Let us now use the following simple machine:
-
-....
-MACHINE SimpleCountDefSet
-SETS ID
-VARIABLES s
-INVARIANT s <: ID & card(s)<10
-INITIALISATION s := {}
-OPERATIONS
-  Add(x) = PRE x:ID & x/:s THEN s := s\/{x} END;
-  Remove(x) = PRE x:s THEN s:= s - {x} END
-END
-....
-
-Here model checking with ProB will give you the following message:
-
-image::ProBModelCheckNoCounterExampleFound_Unbounded.png[]
-
-Unfortunately this does not guarantee that your machine is correct.
-Indeed, ProB has checked your machine only for one specific cardinality
-of the deferred set ID (probably 2 or 3). Indeed, if you look at the
-ProB window after loading the above machine you will see:
-
-image::ProBSimpleCountDefSet_BeforeInit.png[]
-
-In the "State Properties" pane you can see that the cardinality of ID was set to 3.
-There are various ways you can influence the cardinality chosen by ProB.
-One is by adding a DEFINITION of the form:
-
-....
-DEFINITIONS  scope_ID == 10
-....
-
-If you add this definition, ProB will now find an invariant violation:
-
-image::ProBSimpleCountDefSet_InvViol.png[]
-
-However, if you remove the above DEFINITION and add the following
-instead:
-
-....
-PROPERTIES card(ID) = 5
-....
-
-ProB will give you the message we have already seen:
-
-image::ProBModelCheckNoCounterExampleFound.png[]
-
-Indeed, you have now explicitly declare ID to be of size 5, and ProB has checked all
-states for that instantiation of ID. Another solution is to replace the
-deferred set ID by an enumerated set (this will, however, reduce the
-potential for symmetry reduction):
-
-....
-SETS ID={id1,id2,id3,id4,id5}
-....
-
-[[infinite-types]]
-== Infinite Types
-
-It could be that your B machine makes use of the mathematical integers
-(`INTEGER`) or infinite subsets thereof (`NATURAL`, `NATURAL1`). Note
-that some derived types (such as seq(.)) are defined in terms of
-INTEGER. In this case there could be no way to explore all states of
-your system. For example, the following operation:
-
-....
- Choose = BEGIN x :: NATURAL END
-....
-
-can be executed in infinitely many ways. ProB will in this case only
-find values between 0 and `MAXINT` for x. As such, a complete model
-checking does not indicate that your machine's state space has been
-fully explored. Note: ProB prints a warning on the console when an
-infinite type (like `NATURAL`) was "expanded" into a finite subset of
-it. This information is not yet fed back to the graphical user interface
-(but we are working on it).
-
-[[model-checking-and-proof]]
-== Model Checking and Proof
-
-Finally, even if ProB was able to successfully check the entire state
-space of your model, this does not imply that you can prove your machine
-correct with AtelierB (or Rodin). We dedicate another tutorial page to
-this: <<tutorial-model-checking-proof_and_cbc,Model Checking, Proof
-and CBC>>.
diff --git a/src/docs/chapter/user/20_Validation/01_MC/Tutorial_First_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/01_MC/Tutorial_First_Model_Checking.adoc
deleted file mode 100644
index 8018e4be893dfd26c614b460147e22b69df864c7..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/01_MC/Tutorial_First_Model_Checking.adoc
+++ /dev/null
@@ -1,97 +0,0 @@
-
-[[tutorial-first-model-checking]]
-= Tutorial First Model Checking
-
-We assume that you have loaded the "Lift.mch" B machine from the ProB
-Examples folder as outlined in <<tutorial-first-step,Tutorial First
-Step>>. There we have also seen how to execute operations on a B machine
-by double clicking on the items in the "Enabled Operations" pane.
-
-[[simple-model-checking]]
-== Simple Model Checking
-
-The model checker can be used to systematically execute the operations
-and tries to find an erroneous state (e.g., where the invariant is
-violated). Select the "Model Check..." command in the _Verify_ menu:
-
-image::ProBWinModelCheckCommand.png[]
-
-This brings up the following dialog box:
-
-image::ProBWinModelCheckDialog.png[]
-
-Now click the "Model Check" button. After a short while, ProB will give you the
-following error message:
-
-image::ProBWinModelCheckCounterExampleFound.png[]
-
-The lower half of the ProB window should now look as follows:
-
-image::ProB_LiftAfterModelCheck.png[]
-
-The red "**KO**" button in the "State Properties" pane tells us that
-the model checker has moved us into a state where the invariant is
-violated. Indeed, the `floor` variable has taken up a negative value,
-while the invariant requires floor to be between 0 and 99. The
-"History" pane tells us the sequence of operations that has led to
-this error. (Note that this sequence is not necessarily the shortest
-sequence that leads to an error or to this error. However, by selecting
-"Breadth First" in the model check dialog above, one can ensure that
-the shortest paths are found.)
-
-[[coverage-statistics]]
-== Coverage Statistics
-
-We can obtain some statistics about how many states ProB has explored by
-selecting the "Compute Coverage" command in the _Analyse_ menu:
-
-image::ProB_LiftAfterModelCheck_Coverage.png[]
-
-In the NODES section we can see that ProB has explored a total of 11
-nodes (i.e., states of the B machine). None of these nodes are
-deadlocked, in the sense that no operations are applicable. We can also
-see that for one node the invariant is violated. Of these 11 nodes, 2
-are *open*, meaning that they have not been explored in the sense that:
-
-* the invariant has not been evaluated
-* the enabled operations have not been computed.
-
-As such, an open node may contain an invariant violation and/or could be
-a deadlocking node. A live node is a node which is not deadlocked and
-not open.
-
-We can also see that there are in total 17 transitions among these 11
-nodes. A transition is either an operation or an initialization (there
-can be one more transition, which we will examine later in the
-tutorial).
-
-In the COVERED_OPERATIONS section, we can see more details about these
-transitions: we have one initialization, 8 `inc` operations and 8 `dec`
-operations.
-
-[[view-statespace]]
-== View Statespace
-
-We can obtain a graphical visualization of the state space explored by
-ProB. For this, be sure that you have correctly
-<<graphical-viewer,installed and setup the graphical viewer as
-desribed in the user manual>>. Now, choose the "View Statespace"
-command in the _Animate_ menu:
-
-image::ProB_LiftAfterModelCheck_Statespace.png[]
-
-We can now see the 11 nodes. The two open nodes are marked in red. You
-can also see that there is a virtual root node (the inverted triangle at
-the top), representing the "state" of the machine before
-initialization. The current node is depicted by the blue hexagon in the
-right hand corner.
-
-Note: you can influence the coloring and shapes used by ProB, by
-selecting "Graphical Viewer Preferences..." in the _Preferences_
-menu.
-
-image::ProB_GraphicalViewerPreferences_Shapes.png[]
-
-You can obtain more information about the state space visualization in
-the user manual: <<state-space-visualization,State Space
-Visualization>>.
diff --git a/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc b/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc
deleted file mode 100644
index 0e592524558bbd8a95cac0853b99603960eed970..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc
+++ /dev/null
@@ -1,19 +0,0 @@
-
-[[constraint-based-checking]]
-= Constraint Based Checking
-:leveloffset: +1
-
-ProB also offers an alternative checking method, inspired by the Alloy
-footnote:[D. Jackson: Alloy: A lightweight object modeling notation. ACM
-Transactions Software Engineering and Methodology (TOSEM),
-11(2):256–290, 2002.] analyser. In this mode of operation, ProB does not
-explore the reachable states starting from the initial state(s), but
-checks whether applying a single operation can result in a property
-violation (invariant and assertion) independently of the particular
-initialization of the B machine. This is done by symbolic constraint
-solving, and we call this approach constraint based checking (another
-sensible name would be model finding).
-
-More details and examples can be found in the
-<<tutorial-model-checking-proof-and-cbc,tutorial page on model
-checking, proof and CBC>>.
diff --git a/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc
deleted file mode 100644
index 6be1e666d89fc61f042e7de5aa9622b09038c3fe..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc
+++ /dev/null
@@ -1,55 +0,0 @@
-
-[[difference-between-constraint-based-checking-and-model-checking]]
-= Difference between Constraint Based Checking and Model Checking
-
-<<consistency-checking,Model checking>> tries to find a sequence of
-operations that, starting from an initial state, leads to a state which
-violates a property. Constraint based checking tries to find a state of
-the machine that satisfies the property but where we can apply a single
-operation to reach a state that violates this property. If the
-constraint based checker finds a counter-example, this indicates that
-the B specification may contain a problem. The sequence of operations
-discovered by the constraint based checker leads from a valid state to a
-property violation, meaning that the B machine may have to be corrected.
-The valid state is not necessarily reachable from a valid initial state.
-This situation further indicates that it will be impossible to prove the
-machine using the B proof rules. In other words, the constraint-based
-checker verifies that the invariant is inductive.
-
-A comparison between all <<prob-validation-methods,ProB validation
-methods can be found on a separate manual section>>.
-
-[[commands-of-the-constraint-based-checker]]
-= Commands of the Constraint Based Checker
-
-These commands are only accessible in the "Normal" mode of ProB (see
-<<the-prob-main-window,the general
-presentation>>) and are in the sub-menu "Verify|Constraint Based
-Checking". The command "Constraint Search for Invariant Violations"
-will execute the constraint based checking described above to check for
-invariant violations. The process stops as soon as a counterexample has
-been found and then displays the counter-example in the animation panes.
-The command "Constraint Search for Invariant Violations..." enables
-the user to specify which particular operation leading from the valid
-state to the invariant violation of the B specification should be
-considered during the constraint based checking.
-
-The "Constraint Search for Assertion Violations" command executes the
-constraint based checking looking for assertion violations, while the
-command "Constraint Search for Abort Conditions" executes it looking
-for abort conditions.
-
-Within the <<using-the-command-line-version-of-prob,command-line
-version of ProB>>, there are also several commands available:
-
-* <<using-the-command-line-version-of-prob,cbc >>
-to check whether an operation preserves the invariant
-* <<using-the-command-line-version-of-prob,cbc_deadlock>>
-to check whether the invariant implies that no deadlock is possible
-* <<using-the-command-line-version-of-prob,cbc_assertions>>
-to check whether the static assertions (on constants) are implied by the
-axioms/properties.
-
-The following command is related to the above:
-
-* <<using-the-command-line-version-of-prob,cbc_sequence>> to find a sequence of operations using the constraint solver
diff --git a/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc
deleted file mode 100644
index 9527e1692774191134a5b107a311637664269730..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc
+++ /dev/null
@@ -1,85 +0,0 @@
-
-[[bounded-model-checking]]
-= Bounded Model Checking
-
-As of version 1.5, ProB provides support for constraint-based bounded
-model checking (BMC). As opposed to
-<<constraint-based-checking,constraint-based checking>>, BMC finds
-counterexamples which are reachable from the INITIALISATION. As opposed
-to <<consistency-checking,ordinary model checking>>, it does not
-compute all possible solutions for parameters and constants, but
-constructs these on demand. This can be useful when the out-degree of
-the state-space is very high, i.e., when there are many possible
-solutions for the constants, the initialisation and/or the individual
-operations and their parameters.
-
-Take the following example:
-
-....
-MACHINE VerySimpleCounterWrong
-CONSTANTS lim
-PROPERTIES lim = 2**25
-VARIABLES ct
-INVARIANT
- ct:INTEGER & ct < lim
-INITIALISATION ct::0..(lim-1)
-OPERATIONS
-  Inc(i) = PRE i:1..1000 & ct + i <= lim THEN ct := ct+i END;
-  Reset = PRE ct = lim THEN ct := 0 END
-END
-....
-
-The ProB model checker will here run for a very long time before
-uncovering the error that occurs when `ct` is set to lim. If you run the
-<<tlc,TLC backend>> you will get the error message:
-`"Too many possible next states for the last state in the trace."`
-
-However, for the bounded model checker this is less of a problem; it
-will use the constraint solver to try and find suitable values of the
-constants, initial variable values and parameters to generate an
-invariant violation. The bounded model checker actually uses the same
-algorithm than the <<test-case-generation,constraint-based test-case
-generator>>, but uses the negation of the invariant as target. You can
-use the command-line version of ProB, with the
-<<using-the-command-line-version-of-prob,`-bmc DEPTH`>>
-command as follows:
-
-....
-$ probcli VerySimpleCounterWrong -bmc 10
-constraint based test case generation, maximum search depth: 10
-constraint based test case generation, target state predicate: #not_invariant
-constraint based test case generation, output file:
-constraint based test case generation, performing bounded model checking
-bounded_model_checking
-
-CBC test search: starting length 1
-*1.!#
-CBC test search: covered event Inc
-Found counter example
-executing_stored_test_case(1,[Inc],[(2,Inc(int(1)),1,2)])
-finding_trace_from_to(root)
-
-
-BMC counterexample found, Length=1
-
-CBC Algorithm finished (1)
-Timeouts: total: 0
-Checked paths (Depth:Paths): 1:1, total: 1
-Found paths: 1:1, total: 1
-Found test cases: 1:1, total: 1
-Runtime (wall): 120 ms
-! An error occurred !
-! source(invariant_violation)
-! Invariant violation found by bmc
-! *** error occurred ***
-! invariant_violation
-....
-
-You can also use the bounded model checker from ProB Tcl/Tk. The command
-is situated inside the Experimental sub-menu of the _Analyse_ menu (to see
-the command, you may have to change the preference entry to
-`preference(user_is_an_expert_with_accessto_source_distribution,true).`
-in the `ProB_Preferences.pl` file) Running the command on the above
-example will generate the following counter-example:
-
-image::BMC_Counter_Wrong.png[]
diff --git a/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc
deleted file mode 100644
index a6f2a333cc6133a44d59c15afec5d189ce341ff4..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc
+++ /dev/null
@@ -1,92 +0,0 @@
-
-[[symbolic-model-checking]]
-= Symbolic Model Checking
-
-[[overview-symbolic-model-checking]]
-== Overview
-
-The current nightly builds of ProB support different symbolic model
-checking algorithms:
-
-* Bounded Model Checking (BMC),
-* k-Induction, and
-* different Variants of the IC3 algorithm.
-
-As opposed to <<constraint-based-checking,constraint-based
-checking>>, these algorithms find counterexamples which are reachable
-from the INITIALISATION. As opposed to
-<<consistency-checking,ordinary model checking>>, they do not build
-up the state space explicitly, e.g., they do not compute all possible
-solutions for parameters and constants. This can be useful when the
-out-degree of the state-space is very high, i.e., when there are many
-possible solutions for the constants, the initialisation and/or the
-individual operations and their parameters.
-
-In addition to the algorithms explained here, BMC*, a bounded model
-checking algorithm based on a different technique is available in Prob.
-See <<bounded-model-checking,its wiki page>> for details.
-
-[[usage]]
-== Usage
-
-Take the following example:
-
-....
-MACHINE VerySimpleCounterWrong
-CONSTANTS lim
-PROPERTIES lim = 2**25
-VARIABLES ct
-INVARIANT
- ct:INTEGER & ct < lim
-INITIALISATION ct::0..(lim-1)
-OPERATIONS
-  Inc(i) = PRE i:1..1000 & ct + i <= lim THEN ct := ct+i END;
-  Reset = PRE ct = lim THEN ct := 0 END
-END
-....
-
-The ProB model checker will here run for a very long time before
-uncovering the error that occurs when `ct` is set to lim. If you run the
-<<tlc,TLC backend>> you will get the error message:
-`"Too many possible next states for the last state in the trace."`
-
-However, for the symbolic model checking techniques this is less of a
-problem. You can use them via command-line version of ProB as follows:
-
-....
-$ probcli VerySimpleCounterWrong.mch -symbolic_model_check bmc
-K = 0
-solve/2: result of prob: contradiction_found
-K = 1
-solve/2: result of prob: contradiction_found
-K = 2
-solve/2: result of prob: contradiction_found
-K = 3
-solve/2: result of prob: contradiction_found
-K = 4
-solve/2: result of prob: solution
-successor_found(0)
- --> INITIALISATION(0)
-successor_found(1)
- --> Inc
-successor_found(2)
- --> Inc
-successor_found(3)
- --> Inc
-successor_found(4)
- --> Inc
-! *** error occurred ***
-! invariant_violation
-....
-
-Instead of "bmc" you can use "kinduction" and "ic3" as command
-line arguments in order to use the other algorithms.
-
-The algorithms are also available from within ProB Tcl/Tk. They can be
-found inside the "Symbolic Model Checking" sub-menu of the _Analyse_ menu.
-
-[[more-details]]
-== More details
-
-A paper describing the symbolic model checking algorithms and how they
-are applied to B and Event-B machines has been submitted to ABZ 2016.
diff --git a/src/docs/chapter/user/20_Validation/CBC/Tutorial_Model_Checking_Proof_and_CBC.adoc b/src/docs/chapter/user/20_Validation/CBC/Tutorial_Model_Checking_Proof_and_CBC.adoc
deleted file mode 100644
index e35c2314a35c37a4e0bd618bf1952b700565a1f9..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/CBC/Tutorial_Model_Checking_Proof_and_CBC.adoc
+++ /dev/null
@@ -1,142 +0,0 @@
-
-[[tutorial-model-checking-proof-and-cbc]]
-= Tutorial Model Checking, Proof and CBC
-
-We assume that you have completed
-<<tutorial-complete-model-checking,Tutorial Complete Model
-Checking>>.
-
-Let us examine the following B machine:
-
-....
-MACHINE DoubleCounter
-VARIABLES counter
-INVARIANT
- counter:NATURAL & counter<=128
-INITIALISATION counter:=8
-OPERATIONS
-  Double = PRE counter<100 THEN counter := 2*counter END;
-  Halve = BEGIN counter := counter/2 END
-END
-....
-
-Now click the "Model Check" button. After a short while, ProB will
-give you the following message:
-
-image::ProBModelCheckNoCounterExampleFound.png[]
-
-Is this model correct? As you will see, this depends on your point of
-view.
-
-[[state-space]]
-== State Space
-
-If you look purely at the state space of the machine (choose the View
-State Space command in the Animate menu) you get the following picture:
-
-image::DoubleCounterStatespace.png[]
-
-Indeed, all reachable states are correct, in the sense that the
-invariant `counter:NATURAL & counter\<=128` holds for all of those
-states.
-
-However, you will not be able to prove the system correct using AtelierB
-or Rodin.
-
-[[constraint-based-checking-cbc-for-the-invariant]]
-== Constraint Based Checking (CBC) for the Invariant
-
-In addition to model checking, ProB also offers constraint-based
-checking (CBC), which is particularly useful when used in conjunction
-with proof. This will give us the clue as to why the above machine
-cannot be proven correct, and why it can also be viewed as incorrect.
-
-Before proceeding, please ensure that you have either set the CLPFD
-preference to `TRUE` or have set the MAXINT preference to at least `130`.
-This can be set by going to the "Animation Preferences" command in the
-Preferences menu or by adding for example the following to your file and
-then reloading it:
-
-....
-DEFINITIONS SET_PREF_CLPFD == TRUE
-....
-
-Let us choose the "Check Invariant Preservation for Operation" command
-inside the "Constraint Based Checking" submenu:
-
-image::DoubleCounterCBCCommand.png[]
-
-(You This will report an invariant violation and transport you to the
-following state:
-
-image::CBCDoubleCounter2.png[]
-
-As you can see, the Counter has the value 130, which clearly violates
-the invariant `counter\<=128`. However, no value in the state space above
-had this value for Counter. So how did we reach this error state? By
-pressing the left arrow in the "EnabledOperations" pane you will see
-the previous state that ProB has computed:
-
-image::CBCDoubleCounter1.png[]
-
-Now, while this state does not appear in the state space above either.
-However, this time this state does satisfy the invariant. Thus, if we
-ignore the initialization and just look at the INVARIANT
-`counter:NATURAL & counter\<=128` as describing all possible states, then
-the machine is indeed erroneous: the operation Double lead us outside of
-the safe states. The operation Halve on the other hand is correct: for
-every possible state satisfying the INVARIANT the resulting successor
-state will also satisfy the INVARIANT.
-
-If you look purely at the state space of the machine (choose the View
-State Space command in the Animate menu) you get the following picture:
-
-image::DoubleCounterStatespace2.png[]
-
-As you can see the constraint-based checker has transported us into the
-state with `counter=65`, which is not reachable from the initial state of
-the system. However, as we have said, it does satisfy the invariant and
-as such the machine cannot be proven using the B provers.
-
-If one tries to use for example Click'n Prove to prove this machine,
-there is one proof obligation for the Double operation which cannot be
-discharged:
-
-image::ClicknProveDoubleCounter.png[]
-
-Indeed, we have to prove that `2*counter` is less or equal to `128`, given
-that counter is less or equal to `99` and less or equal to `128`. This is
-not possible; above ProB has found `counter=65` as a counterexample. More
-generally, the proof obligation in classical B for an operation with
-precondition `P` and body `S` is:
-
-`I & P \=> [S] I`
-
-In other words, for any state which satisfies the invariant I and the
-precondition `P`, the operation must preserve the invariant; not just for
-the states reachable from the initialization. In particular, the
-operation must preserve the invariant for the state with `counter=65`,
-which it does not.
-
-[[how-to-correct-problems-found]]
-== How to correct problems found
-
-Below is a small guide on how to correct invariant violations found by
-constraint-based checking and model checking.
-
-.__Solving Invariant Violation Problems__
-[cols=",,",options="header",]
-|=======================================================================
-|Potential Solution |CBC |Model Check
-|Strengthen Invariant |if start state wrong |NA
-
-|Weaken Invariant |if destination state ok |If destination state ok
-
-|Guard Strengthening |if transition should not be allowed |if path not
-legal
-
-|Guard Weakening |NA |NA
-
-|Adapt Substitution |if destination state wrong |if destination (or
-intermediate) state wrong
-|=======================================================================
diff --git a/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1
diff --git a/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc b/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc
deleted file mode 100644
index 11b94be55c4d250789587bc890f5aac8202945ab..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[model-checking]]
-= Model Checking
-:leveloffset: +1
diff --git a/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc
deleted file mode 100644
index 24133576057fae5a59aa7cc493c7d96d020b1aef..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc
+++ /dev/null
@@ -1,244 +0,0 @@
-
-[[consistency-checking]]
-= Model Checking Consistency
-
-[[checking-consistency-via-model-checking]]
-== Checking Consistency via Model Checking
-
-By manually animating a B machine, it is possible to discover problems
-with the specification, such as invariant violations or deadlocks. The
-ProB model checker can do this exploration systematically and
-automatically. It will alert you as soon as a problem has been found,
-and will then present the shortest trace (within currently explored
-states) that leads from an initial state to the error.
-
-The model checker will also detect when all states have been explored
-and can thus also be used to formally guarantee the absence of errors.
-This will obviously only happen if the state space is finite, but the
-model checker can also be applied to B machines with infinite state
-spaces and will then explore the state space until it finds an error or
-runs out of memory.
-
-[[basics]]
-=== Basics
-
-During the initial draft of a specification, it is often useful to
-utilize the model checker to determine if there are any invariant
-violations or deadlocks. A model checker automatically explores the
-(finite or infinite) state space of a B machines. Recall that the
-INVARIANT specifies the types of variables and also may include
-relationships that must be true in all situations. In other words, it
-specifies the properties of a B machine that are immutable and must be
-permanently established.
-
-Since a graph of the visited states and the transformations (operations)
-between them is retained, it is therefore possible to produce traces
-(sequence of operations) of invariant violations when they are detected.
-Such a trace is called a “counter-example” and is useful in determining
-where and in what circumstances a specification contains errors.
-
-Notice that if the model checker does not find any invariant violations
-or deadlocks when a traversal of the exhaustive state space has been
-performed, this does not imply that the specification is a correct
-specification. This should be understood as the fact that, given the
-initialisation stated and the model checker preferences set at the time
-of the check, no errors were found. The main difference is that the ProB
-animation preferences (such as the number of initialisations, times that
-an operation may be enabled, and the size of unspecified sets) may be
-set too low for the exhaustive state space to be covered by the model
-checking.
-
-As a final caveat, it is not possible to check a machine with an
-infinite state space. Anecdotal evidence does suggest however, that the
-model checker does find errors quite quickly. On that basis, it remains
-a useful tool even for specifications whose state space is infinite.
-
-[[using-the-model-checker]]
-=== Using the Model Checker
-
-To model check a B machine loaded in ProB, launch the command from
-"Verify| Model Check".
-
-image::Temporal_Model_Checker_settings.png[]
-
-By default the model checking is done by exploring the state space in a
-mixed depth-first/breadth-first manner, unless the setting "pure
-Depth" or "pure Breadth First" is selected in the _Search Strategy_
-pop-up menu. As of version 1.5.1, additional options for directed model
-checking are available. For example, one can have truly random
-exploration or provide a custom heuristic function to guide the model
-checker. These features are illustrated using the
-<<blocks-world-directed-model-checking,the blocks world example>>.
-
-The two checkboxes "Find Deadlocks" and "Find Invariant Violations"
-control whether the model checker will report an error when a newly
-encountered state is deadlocked or respectively violates the invariant.
-
-Similarly, if the model contains assertions (theorems for Event-B
-models), then the "Find B ASSERTION Violations" checkbox is enabled.
-You can then control whether the model checker cheeks the assertions
-(and stops upon encountering a false assertion). Also, if the B Machine
-contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes
-enabled. You can then control whether the model checker cheeks the GOAL
-predicate (and stops when the predicate is true for a new state). More
-details about assertions and goals can be found below.
-
-The model checker is started by clicking on the "Model Check" button.
-When the model checker computes and searches the state space, a line
-prefixed with Searching... at the bottom of the pop-up window will
-update in real-time the number of nodes that have been computed, until a
-node violating one of the properties verified has been found or the
-entire state space has been checked. The user can interrupt the model
-checking at any time by pressing the "Cancel" button.
-
-[[incremental-model-checking]]
-==== Incremental Model Checking
-
-It is important to understand that the computation of and search in the
-state space is an incremental process. The model checking can be done by
-running the model checker several times; if the number of nodes
-specified in the entry "max nr. of nodes to check" is less that the
-size of the state space that remains to be checked. If the model
-checking is done in several steps, the end of the model checking step is
-indicated by the line No error so far, ... nodes visited at the bottom
-of the pop-up window, unless a violation of the properties
-(deadlockfreeness, invariant) are found. Between each model checking
-step, the user can execute the various commands of ProB, notably those
-of the _Analyse_ menu to display information on the state space (see
-<<animation,The Analyse Menu>>) and the
-visualization features (see <<state-space-visualization,State Space
-Visualization>>).
-
-By default, each model checking step starts from the open nodes of the
-last computed state space. This means that a change in the settings of
-the model checker between two steps does not affect the non-open nodes
-(those already computed), unless there is an alternative path to an
-already computed node. This behavior can be changed by toggling on the
-"Inspect Existing Nodes" setting. This forces ProB to reevaluate the
-properties set to be verified on the state space previously computed.
-Keep in mind that unless the "Inspect Existing Nodes" setting is on,
-the change of the model checking settings may not affect the state space
-already computed.
-
-[[results-of-the-model-checking]]
-==== Results of the Model Checking
-
-When the state space has been computed by ProB, the pop-up window is
-replaced by a dialog window stating "No error state found". All new
-nodes visited. If ProB finds a node where one of the property that was
-checked is not verified, it displays a similar pop-up window but with
-the text Error state was found for new node: invariant violation or
-Error state was found for new node: deadlock. Then, ProB displays in the
-animation panes the state of the B machine corresponding to the property
-violation. From there, the user can examine the state in the "State
-Properties" pane, the enabled operations (including the backtrack
-virtual operation to go back to the valid state that lead to the
-property violation) in the "Enabled Operations" pane, and the trace
-(sequence of operations) leading to the invalid state in the "History"
-pane.
-
-[[preferences-of-the-model-checking]]
-==== Preferences of the Model Checking
-
-The preferences "Nr of Initialisations shown" and "Max Number of
-Enablings shown" (described in
-<<animation,Animation Preferences>>) affect the
-model checking in exactly the same way as they do for the animation.
-These preferences are particularly important for the model checking, as
-setting the number of initialisations or the number times than an
-operation may be enabled too low will lead to computing and searching a
-state space that is too small. On the other hand, the user may have to
-set these preferences to a lower value if the exhaustive state space is
-too big to be covered by ProB.
-
-Once the state space of the B specification has been computed by ProB,
-the commands from the _Analyse_ menu (see
-<<animation,The Analyse menu>>) and the
-visualization features (see <<state-space-visualization,State Space
-Visualization>>) are then very useful to examine the state space. The
-features used to visualize a reduced state space are particularly useful
-as examining a huge state space may not yield to interesting
-observations due to excessive cluttering footnote:[M. Leuschel and
-E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S.
-King, M. Henson, and S. Schneider, editors, ZB 2005: Formal
-Specification and Development in Z and B, LNCS 3455. Springer-Verlag,
-2005
-https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf].
-
-[[machines-with-invariant-violations-and-deadlocks]]
-=== Machines with Invariant Violations and Deadlocks
-
-When the two properties (invariant and deadlock-freeness) are checked
-and a state violates both, only the invariant violation is reported. In
-that situation, the deadlock can be observed either from the Enabled
-Operations (as only the backtrack virtual operation is enabled), or from
-the state space graph (as the current node has no successors).
-
-During the model checking of a specification which contains both of
-these errors, it is often useful to be able to focus exclusively upon
-the detection of one type of error. For example, since an invariant
-violation is only reported the first time it is encountered, subsequent
-invocations of the model checker may yield deadlocks whose cause is the
-invariant violation. This is done by toggling off the corresponding
-settings of the temporal model checker pop-up window.
-
-*HINT: Turning off invariant violation and deadlock detection will
-simply compute the entire state space until the user presses the Cancel
-button or until the specified number of nodes is reached.*
-
-[[two-phase-verification]]
-==== Two Phase Verification
-
-If the state space of the specification can be exhaustively searched,
-check for deadlocks and invariant violations in two phases. To do this,
-set "Inspect Existing Nodes" to off and turn either "Check for
-Deadlocks" or "Check for Invariant Violations" on and the other off.
-Perform the temporal model check until all the deadlocks (resp.
-invariant violations) are detected or shown to be absent. To recheck the
-whole state space, either turn on the option "Inspect Existing Nodes"
-or purge the state space already computed by reopening the machine. Now
-deselect the previous property checked, and select the alternative
-property for checking. Now perform a temporal model check again to
-search for a violation of the second property.
-
-HINT: At any time during animation and model checking, the user can
-reopen the the B specification to purge the state space.
-
-[[interleaved-deadlock-and-invariant-violation-checking]]
-==== Interleaved deadlock and invariant violation checking
-
-If you wish to determine if an already encountered invariant violation
-is also a deadlocked node, turn the option "Inspect Existing Nodes"
-on, turn "Detect Invariant Violations" off, and ensure that "Detect
-Deadlocks" is on. Performing a temporal model check now will traverse
-the state space including the previously found node that violates the
-invariant.
-
-WARNING: Enabling "Inspect Existing Nodes" will continually report
-the first error it encounters until that error is corrected.
-
-[[specifying-goals-and-assertions]]
-== Specifying Goals and Assertions
-
-The ASSERTIONS clause of a B machine enables the user to define
-predicates that are supposed to be deducible from the INVARIANT or
-PROPERTIES clauses. If the B specification opened in ProB contains an
-ASSERTIONS clause, the model checking pop-up window enables to check if
-the assertion can be violated. If enabled and a state corresponding to
-the violation of the assertion is found, a message "Error state was
-found for new node: assertion violation" is displayed, and then ProB
-displays this state in the animation panes
-
-A feature that is similar to the assertions is the notion of a goal. A
-goal is a macro in the DEFINITIONS section whose name is GOAL and whose
-content is a predicate. If the B specification defines such a macro, the
-model checking pop-up window enables to check if a state satisfies this
-goal. If enabled and a state corresponding to the goal is found, a
-message "State satisfying GOAL predicate was found" is displayed, and
-then ProB displays this state in the animation panes.
-
-It is also possible to find a state of the B machine that satisfies such
-a goal without defining it explicitly in the B specification. The
-"Verify|Advanced Find..." command enables the user to type a predicate
-directly in a text field. ProB then searches for a state of the state
-space currently computed that satisfies this goal.
diff --git a/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc
deleted file mode 100644
index 3a98ff34494b23dac004708f07225a90c8acddea..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc
+++ /dev/null
@@ -1,97 +0,0 @@
-
-[[distributed-model-checking]]
-= Distributed Model Checking
-
-Distributed Model Checking allows to check invariants and
-deadlock-freedom (and assertions) with additional computational power.
-The distributed version of ProB is named _distb_. In the following, we
-will document how to run it.
-
-== Overview
-
-_distb_ consists of three components.
-
-* A master which coordinates the model checking process. Per distributed
-model checking, it must run exactly once.
-* A proxy which coordinates workers on its machine. It should run (at
-least, but usually) once per participating machine.
-* A worker which does the actual work. A good number of workers usually
-is close to the amount of available (physical) CPU cores of a
-participating machine.
-
-[[setting-up-shared-memory]]
-== Setting up shared memory
-
-It might be necessary to increase the limits of how much shared memory
-may be allocated, both per segment and overall. This is, to our
-knowledge, required for Mac OS X and older versions of Ubuntu. You can
-view the limits by running:
-
-`sysctl -a | grep shm`
-
-Per default, recent versions of Ubuntu set the following values:
-
-----
-kernel.shmall = 18446744073692774399
-kernel.shmmax = 18446744073692774399
-kernel.shmmni = 4096
-----
-
-On Mac OS X, the keys might be different and you can set them by
-executing:
-
-----
-sudo sysctl -w kern.sysv.shmmax=18446744073692774399
-sudo sysctl -w kern.sysv.shmseg=4096
-sudo sysctl -w kern.sysv.shmall=18446744073692774399
-----
-
-== Running _distb_
-
-Run once per machine:
-
-`/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER`
-
-Note that on Linux systems you might need to set the LD_LIBRARY_PATH
-variable to find the ZeroMQ libraries beforehand (for all components):
-
-`export LD_LIBRARY_PATH=/path/to/prob/lib`
-
-Run once per model checking:
-
-`/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL`
-
-Run as many workers as you want:
-
-`/path/to/prob/probcli -zmq_worker <unique identifier> &`
-
-== Additional Preferences
-
-You can fine-tune the following parameters by adding `-p NAME VALUE` to
-the corresponding call (e.g.: `./probcli -zmq_worker worker1 -p port 5010
--p max_states_in_memory 100`) :
-
-[cols=",,,",options="header",]
-|=======================================================================
-|Parameter |Default |Description |Applicable for...
-|port |5000 |TCP ports should be used starting at... |master, worker
-
-|ip |localhost |IP of the master component |master
-
-|max_states |0 |How many states should be checked at most (0 means all)
-|master
-
-|tmpdir |/tmp/ |Directory for temporary files |master, worker
-
-|logdir |./distb-logs |Directory for log output (must exist) |master,
-worker
-
-|proxynumber |0 |Which proxy should the component connect to (if
-multiple run on the same machine) |worker
-
-|max_states_in_memory |1000 |How many states may be kept in memory
-before written into a database |worker
-
-|hash_cycle |25 |Minimum amount of milliseconds that has to pass between
-hash code updates from the master |master
-|=======================================================================
diff --git a/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc b/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc
deleted file mode 100644
index a17d0cca82c0287acffbef8d62e5e86a1347cd31..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc
+++ /dev/null
@@ -1,50 +0,0 @@
-
-[[distributed-model-checking-experimental-evaluation]]
-= Distributed Model Checking : Experimental evaluation
-
-We used three different setups to evaluate the distributed version of ProB.
-
-* A standalone multi core computer
-* Amazon EC2 Instances
-* The HILBERT cluster
-
-== Multicore Computer
-
-We used a hexacore 3.33GHz Mac Pro with 16GB of RAM. On this computer we
-benchmarked all models regardless whether we expected them to be
-scalable or not. We varied the number of used cores from 1 up to 12
-hyperthreads. Each experiment was repeated at least 5 times.
-
-== Amazon EC2 Instances
-
-We used c3.8xlarge instances, each of which has 32 virtual CPUs and is
-equipped with 64 GB of RAM. We used the Mac Pro to get an impression if
-and how well the B models scale. From the experiments, we chose those
-models that seemed to scale well and ran the benchmarks on the Amazon EC
-computer with a higher number of workers. Models that did not scale on
-the Mac Pro were not considered as they would not scale on more
-processors. We used 2 or 4 instances connected with 10 GBit ethernet
-connection. Each experiment was repeated at least 5 times.
-
-== HILBERT
-
-We used the high performance cluster at the university of Düsseldorf
-(HILBERT) for a single model. The model could not be cheked using a
-single core because it would have taken too long. Based on a partial
-execution, it would take about 17 days on a single core on the Mac Pro.
-The model was checked with different numbers of cores on the HILBERT
-cluster. We varied between 44 and 140 cores. On the cluster we only
-executed the experiments once but all experiments on the other platforms
-indicated that the variation between experiments could be ignored. Also
-the execution times of all 6 experiments seem to be consistent.
-
-== Models
-
-We cannot make all models public, because they we provided by industrial
-partners from various research projects. The models that could be make
-available can be downloaded https://www3.hhu.de/stups/models/parb/[here].
-
-== Results
-
-The results of the experiments are shown in Jens Bendisposto's
-dissertation. The dissertation is available https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=34472[here].
diff --git a/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc b/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc
deleted file mode 100644
index a65002b4f162f4fee4058f0ccb2e7392311397b1..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc
+++ /dev/null
@@ -1,95 +0,0 @@
-
-[[parb]]
-= ParB
-
-This page explains how to run the distributed model checking prototype.
-
-Note that the implementation does not work with Windows, only Linux
-andMac OS are supported.
-
-It is required to set the limits for shared memory on some systems, this
-can be done using sysctl. Here is a little script that sets the limits.
-It takes the size of shared memory as parameter (usually the size of
-your memory in GB). You need to run the script with root rights.
-
-----
-#!/bin/bash
-if [ $# -gt 0 ]; then
-  echo "Setting SHM sizes:"
-  sysctl -w kern.sysv.shmmax=`perl -e "print 1073741824*$1"`
-  sysctl -w kern.sysv.shmseg=4096
-  sysctl -w kern.sysv.shmall=`perl -e "print 262144*$1"`
-  echo "Here are the current values:"
-  sysctl -a | grep shm
-else
-  echo "You need to provide the size of shared memort (in full GB)"
-fi
-----
-
-After setting up shared memory, you can use the `parB.sh` script that
-comes with the ProB distribution (see <<download,Download>>).
-
-Usage
-
-`./parB <Nr. of workers> <logfile> <file>`
-
-Example usage:
-
-`$ ./parB.sh 2 ~/parB.log scheduler.mch`
-
-[[running-in-the-cloudcluster]]
-== Running in the Cloud/Cluster
-
-The script can only be used for computation on a single physical
-computer. If you want to use multiple computers, the setup is a bit more
-complex:
-
-* On each physical computer you need to start exactly one copy of
-`lib/hasher`.
-
-`lib/hasher <MASTER_IP> <MASTER_PORT> 1`
-
-* Multiple Copies of `probcli` configured as workers:
-
-`probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0`
-
-* A single instance of `probcli` configured as the master:
-
-`probcli -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>`
-
-The minimal queue length is used to determine if a worker is allowed to
-share its queue. The experiments have shown, that a number between 10
-and 100 is fine. parB will stop after (at least) the maximal number of
-states have been explored, a value of -1 will explore all states (beware
-of this, if the state space is infinite!).
-
-As a rule of thumb use one real core for each of the processes. On
-hyperthreads the model checking still becomes faster, but the speedup is
-only 1/4 for each additional hyperthread.
-
-We plan to develop a control interface that allows configuring the
-logical network in a more convenient way and running the model checker
-from within ProB.
-
-[[options-for-parb]]
-== Options
-
-You can use preferences in parB.sh (and the master) :
-
-----
-./parB <Nr. of workers> <logfile> <file> <additional probcli options>
-./probcli <additional probcli options> -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE> <additional probcli options>
-----
-
-If you use -strict, parB will stop as soon as a violation is found,
-otherwise parB will explore the full state space (up to the maximal
-number of states)
-
-[[cleaning-up]]
-== Cleaning up
-
-If something goes wrong it may be necessary to clean up your shared
-memory. You can find out if there are still memory blocks occupied using
-`ipcs`. Removal can be done using:
-
-`ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'``
diff --git a/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc
deleted file mode 100644
index b9383a43dde227a957974a7882542ca8a81ee55c..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc
+++ /dev/null
@@ -1,535 +0,0 @@
-
-[[ltl-model-checking]]
-= LTL Model Checking
-
-ProB provides
-support for LTL (linear temporal logic) model checking. For an
-introduction to LTL see the
-http://en.wikipedia.org/wiki/Linear_temporal_logic[Wikipedia Article].
-
-To use this feature, select "Check LTL/CTL Assertions" in the
-_Verify_ menu. The feature can also be accessed by the key combination
-"Ctrl+L" under Windows and Linux, and by the key combination "Cmd+L"
-under MacOS. The following window appears:
-
-image::Ltlviewer.png[]
-
-All LTL formulas that are given in the "DEFINTIONS" section of a B
-machine are displayed in the list box of the LTL/CTL Assertions Viewer.
-For CSP-M specifications all LTL formulas given in the LTL pragmas of
-the loaded CSP-M file will be shown in the viewer. (For more detailed
-information of how LTL/CTL assertions can be stored into B and CSP-M
-models see Section *Storing LTL Assertions into a Model*).
-
-A new LTL formula can be entered in the entry below the list box. (We
-explain the supported syntax below). The typed formula can then be
-either added to the list box by clicking the "Add" button or directly
-checked by clicking the "Check" button. Before doing that assure
-whether you are in the proper frame ("Add LTL Formula") of the bottom
-part of the LTL viewer.
-
-The LTL model checker can be started for an LTL formula by performing a
-double-click on the respective formula or typing "Enter" after
-selecting the respective formula. Each LTL formula in the list box has
-on the left hand side a symbol that indicates what is the status of the
-respective formula. An LTL formula can have one of the following
-statuses (status symbols may differ under different operating systems):
-
-* ? – The formula has not been checked yet.
-* ✔ – The formula is true for all valid paths.
-* ✘ – A counterexample for the formula has been found, i.e. there is a
-path that violates the formula. In case the formula has been just
-checked on the model the animator is navigated to the last state of the
-counterexample. The full path can then be seen in the history. The
-counterexample can be also obtained by the dotty-viewer after a second
-double-click on the formula in the assertions’ viewer.
-* ⌚ – The formula is currently checked.
-* ! – The formula check has been aborted by an unexpected error
-occurrence.
-* ∞ – The formula check is incomplete, i.e. no counterexample was found
-so far, but the absence of a path that does not satisfy the formula can
-not be guaranteed because the state space was not fully explored. A new
-check can be started by a double-click.
-
-All formulas can be checked by "Assertions -> Check All Assertions" in
-the menu bar. All formulas will be then checked from top to bottom in
-the list box.
-
-Additionally, the viewer provides a context menu for the list box
-elements. The context menu can be popped-up by a right-mouse-click on a
-formula from the list box, and it performs a set of actions available to
-be performed on the currently selected formula (see Figure below).
-
-image::Ltlviewercontext.png[]
-
-The old LTL and CTL dialogs can be accessed from "OldLtlViewers" in
-the menu bar.
-
-[[ltl-preferences]]
-== LTL Preferences
-
-There is a set of options coming with the LTL model checker. In this
-section we give a brief overview of the preferences. The LTL preferences
-can be viewed by selecting "LTL Preferences" in the _Preferences_
-menu of the LTL/CTL Assertions Viewer.
-
-*Exploring new states* +
-The LTL model checker searches in the already explored search space of
-the model. If a state is encountered that has not been explored before,
-the state will be explored (i.e. all transitions to successor states are
-computed). The number of how often this can happen is limited by the
-field "Max no. of new states". Depending on the LTL formula, a
-partially explored state space can be sufficient to find a
-counterexample or to assure the absence of a counterexample. If there's
-still the possibility of a counterexample in the remaining unexplored
-state space, the user will get a message.
-
-*Optimizing the process of LTL model checking* +
-The process of model checking can be optimized for B and Event-B models
-by using partial order reduction. The idea of partial order reduction is
-to execute only a subset of all enabled actions in each state. Thus,
-only a part of the original state space is checked for the checked
-property. The reduction of the state space depends on the number of
-concurrent and independent actions in the model, as well as on the
-property being checked.
-
-*With Safety Check* +
-This checks whether a formula is a safety property or not. If it is,
-this property is treated in an optimised way. In some cases, this means
-that not the entire state space has to be computed. For this
-optimisation to work, ProB needs the LTL2BA translator. You can download
-and put it into ProB's lib folder, by choosing
-
-`Download and Install LTL2BA Tool...`
-
-from the _Help_ menu.
-
-*Search Options* +
-The model checker searches for a counterexample (i.e. a path that does
-not satisfy the current formula). Where the checked paths through the
-model's search space start depend on the following options in the "LTL
-Preferences"’ menu:
-
-1.  _Start search in initialization_ +
-All paths that start in a state of the initialization of the machine are
-checked.
-2.  _Start search in current state_ +
-All paths that start in the current state are checked.
-3.  _Start in initialization, but check formula in current state_ +
-All paths that start in a state of the initialization of the machine are
-checked, but the formula is mapped to the current state. For example,
-this option can be used to check properties like "Is this state only
-reachable directly after executing operation `xy`?": The formula would
-be `Y[xy]`. This is equivalent to "G (current => f)" with f as the
-entered formula and using the option "Start search in initialization".
-
-Note: Whereas `Y true` is always false when checked with option 1 or 2,
-it is usually true (but not in all cases) for option 3.
-
-[[supported-syntax]]
-=== Supported Syntax
-
-ProB supports LTL^[e]^, an extended version of LTL. In contrast to the
-standard LTL, LTL^[e]^ provides also support for propositions on
-transitions, not only on states. In practice, writing propositions on
-transitions is allowed by using the constructs `e(...)` and `[...]`.
-(see below). The LTL model checker of ProB supports Past-LTL^[e]^ as
-well.
-
-* Atomic propositions can be one of the following:
-** Predicates can be written in curly braces: `\{...}`. E.g.
-`\{card(someset) > 1}`
-** To check if an operation is enabled in a state use `e(Op)`, where
-`Op` is the name of the operation.
-** To start a search from the current state of the animation use
-`current` (see the section *LTL Preferences* for more information).
-** To check if a state has no outgoing transition leading to a different
-state use `sink`. This can be useful for finding "pseudo"-deadlocks,
-i.e. states where only query-operations are enabled that do not change
-the state. Note that `sink` holds for deadlock states as well.
-** For checking if a state is a deadlock state the atomic proposition `deadlock` can be used.
-** To check if a set of operations is disabled in a state use
-`deadlock(Op1,Op2,...,Opk)`, where Op1,Op2,...,Opk with k>0 are
-operations of the model. It is also possible to check if specific
-representations of an operation with arguments are disabled in a state
-using pattern-matching, e.g.: `deadlock(Op(1),Op(3))`.
-** By means of `deterministic(Op1,Op2,...,Opk)`, where Op1,Op2,...,Opk
-with k>0 are operations of the model, one can check if maximum one of
-the operations Op1,Op2,...,Opk is enabled in a state.
-** To check if exactly one operation from a set of operations
-Op1,Op2,...,Opk is enabled in a state use `controller(Op1,Op2,…,Opk)`.
-
-* Transition propositions: +
-If the next executed operation in the path is `Op`, the expression
-`[Op]` can be used. Also patter-matching for the arguments of the
-operation is supported. E.g. `[Op(3,4*v)]` checks if the next operation
-is `Op` and that the first argument is 3 and the third argument is `4*v`
-where `v` is a variable of the machine. +
-Arbitrary B expressions can be used as patterns. Constants and variables
-of the machine can be used. Variables have the values of the state where
-the operations starts.
-
-* Logical operators
-** `true` and `false`
-** `not`: negation
-** `&`, `or` and `=>`: conjunction, disjunction and implication
-
-* Temporal operators (future)
-** `G f`: globally
-** `F f`: finally
-** `X f`: next
-** `f U g`: until
-** `f W g`: weak until
-** `f R g`: release
-
-* Temporal operators (past)
-** `H f`: history (dual to G)
-** `O f`: once (dual to F)
-** `Y f`: yesterday (dual to X)
-** `f S g`: since (dual to until)
-** `f T g`: trigger (dual to release)
-
-* Fairness operators
-** `WF(Op)` or `wf(Op)`: weak fairness, where `Op` is an operation
-** `SF(Op)` or `sf(Op)`: strong fairness, where `Op` is an operation
-** `WEF`: weak fairness for all possible operations
-** `SEF`: strong fairness for all possible operations
-
-[[setting-fairness-constraints]]
-== Setting Fairness Constraints
-
-Fairness is a notion where the search for counterexamples is restricted
-to paths that do not ignore infinitely the execution of a set of enabled
-operations imposed by the user as "fair" constraints. One possibility
-to set fairness constraints in ProB is to encode them in the LTL^[e]^
-formula intended to be checked. For example, for a given LTL^[e]^
-formula "f" a set of weak fairness conditions \{a1,…,an} can be given
-as follows:
-
-`(FG e(a1) => GF [a1]) & … & (FG e(an) => GF [an]) => f.`
-
-In a similar way, strong fairness constraints can be imposed expressed
-by means of an LTL^[e]^ formula:
-
-`(GF e(a1) => GF [a1]) & … & (GF e(an) => GF [an]) => f.`
-
-Checking fairness in this way is very often considered to be inefficient
-as usually the number of atoms (the possible valuations of the property)
-of the LTL property is exponential in the size of the
-formula.footnote:[O. Lichtenstein and A. Pnueli: _Checking that Finite
-State Concurrent Programs Satisfy Their Linear Specification_. POPL '85,
-Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of
-Programming Languages, ACM, 1985] For this reason, the search algorithm
-of the LTL model checker has been extended in order to allow fairness to
-be checked efficiently. In addition, new operators have been added to
-the ProB’s LTL parser for setting fairness constraints to an LTL^[e]^
-property. The new operators are _WF(-)_ and _SF(-)_ and both accept as
-argument an operation. The fairness constraints must be given by means
-of implication: "fair => f", where "f" is the property to be checked
-and "fair" the fairness constraints.
-
-In particular, "fair" can have one of the forms: "wfair", "sfair",
-"wfair & sfair", and "sfair & wfair", where "wfair" and "sfair"
-represent the imposed weak and strong fairness constraints,
-respectively.
-
-Basically, "wfair" and "sfair" are expressed by means of logical
-formulas having the following syntax:
-
-* Weak fair conditions ("wfair"):
-** `WF(a)`, where `a` is an operation
-** `&` and `or`: conjunction and disjunction
-
-* Strong fair conditions ("sfair"):
-** `SF(a)`, where `a` is an operation
-** `&` and `or`: conjunction and disjunction
-
-For instance, if we want to check an LTL property "f" on paths that
-are weak fair in regard to the operations "a" and "b" and
-additionally strong fair in regard to "c" or "d", then this can be
-given as follows:
-
-`(WF(a) & WF(b)) & (SF(c) or SF(d)) => f`
-
-Note that the operators _WF(-)_ and _SF(-)_ cannot appear on the right
-side of the fairness implication. Basically, _WF(-)_ and _SF(-)_ can be
-described by the following equivalences:
-
-`WF(a) ≡ (FG e(a) => GF [a]) and SF(a) ≡ (GF e(a) => GF [a]), where a is an operation.`
-
-For setting fairness constraints on all possible operations of the model
-being checked use the operators "WEF" and "SEF". For instance, if
-"f" is a liveness property and we want to restrict the search only to
-strongly fair paths, then we can impose the fairness constraints by
-means of the formula "SEF => f".
-
-The grammar for imposing fairness constraints by means of the fairness
-implication ("fair => f") looks as follows:
-
-----
-fair ::= WEF | SEF | wfair | sfair | wfair & sfair | sfair & wfair
-wfair ::= wf(a) | ( wfair ) | wfair & wfair | wfair or wfair
-sfair ::= sf(a) | ( sfair ) | sfair & sfair | sfair or sfair
-----
-
-where "a" is a transition proposition.
-
-[[storing-ltl-assertions-in-the-model]]
-== Storing LTL Assertions in the Model
-
-*Storing LTL formulas in B machines* +
-LTL formulas can be stored in the DEFINITIONS section of a B machine.
-The name of the definition must start with ASSERT_LTL and a string
-must be specified. In case there is more than one LTL assertion given in
-the DEFINITIONS section, the particular LTL assertions must be
-separated by semicolon. For example:
-
-----
-DEFINITIONS
-ASSERT_LTL  == "G (e(SetCruiseSpeed) => e(CruiseBecomesNotAllowed))";
-ASSERT_LTL1 == "G (e(CruiseBecomesNotAllowed) => e(SetCruiseSpeed))";
-ASSERT_LTL2 == "G (e(CruiseBecomesNotAllowed) => (ObstacleDisappears))"
-----
-
-*Storing LTL formulas in CSP-M specifications* +
-LTL formulas can be stored within pragmas in CSP-M specifications. A
-pragma in which a single LTL formula is stored is given by "{-#
-assert_ltl "f" "c" #-}", where "assert_ltl" indicates the type of
-the information stored in the pragma (there are currently two types:
-assert_ltl and assert_ctl), and is followed by the LTL formula `f` and a
-comment `c` (the comment is optional). Both, the LTL formula and the
-comment, must be enclosed in double quotes. It is also possible to give
-several LTL formulas in a single pragma within which the corresponding
-LTL assertions are separated by semicolon. For example:
-
-----
-{-# assert_ltl "SF(enter.1) & WF(req.1) => GF([enter.1])";
-    assert_ltl "SF(enter.2) & WF(req.2) => GF([enter.2])";
-    assert_ltl "GF [enter.1] & GF [enter.2]" "Should fail."#-}
-----
-
-Note that a semicolon must not follow the last assertion in a pragma.
-
-For CSP-M specifications, it is also possible to assert LTL-formulae to
-particular processes in the model. This is possible by means of
-`assert` declarations, which have been recently included to the CSP-M
-grammar of the ProB CSP-M parser:
-
-`assert P |= LTL: "ltl-formula"`
-
-where `P` is an arbitrary process and `ltl-formula` an LTL formula.
-
-
-[[ltl-formulas-in-a-separate-file]]
-== LTL Formulas in a Separate File
-
-With the command line version of ProB it is possible to check several
-LTL^[e]^ formulae with one call. The command has the following syntax:
-
-`probcli -ltlfile FILE ...`
-
-The file FILE contains one or more sections where each section has the
-form:
-
-`[Name]  Formula`
-
-The formula itself can spread several lines. Additional comments can be
-added with a leading #. If a counter-example is found, the trace of the
-counter-example is saved into the file ltlce_Name.trace, where "Name"
-is the name of the formula in the LTL file.
-
-One also can check a single LTL^[e]^ formula _F_ using the option
-'-ltlformula' as follows:
-
-`probcli -ltlformula "F"...`
-
-[[ltl-formulae-in-a-separate-file]]
-== LTL Formulae in a Separate File
-
-With the command line version of ProB it is possible to check several
-LTL^[e]^ formulae with one call. The command has the following syntax:
-
-`probcli -ltlfile FILE ...`
-
-The file FILE contains one or more sections where each section has the
-form:
-
-`[Name]  Formula`
-
-The formula itself can spread in several lines. Additional comments can
-be added with a leading #. If a counter-example is found, the trace of
-the counter-example is saved into the file ltlce_Name.trace, where
-"Name" is the name of the formula in the LTL file.
-
-One also can check a single LTL^[e]^ formula _F_ using the option
-'-ltlformula' as follows:
-
-`probcli -ltlformula "F"...`
-
-[[ltl-model-checker-output]]
-== LTL Model Checker Output
-
-The output provided by the LTL model checker can sometimes reveal some
-interesting statistical facts about the model and the property being
-checked on the model. The LTL model checker of ProB uses the tableau
-approach for checking an LTL^[e]^ formula on a formal model. To check
-whether a model _M_ satisfies a given formula _f_, the algorithm
-generates a search graph, called also tableau graph, composed from the
-tableau of the formula and the state space of the model. If there is a
-path in the search graph that is a model for _f_, then the formula is
-satisfiable. The nodes of the search graph are called _atoms_.
-
-Basically, using the tableau approach we prove that _M_ satisfies _f_ by
-negating the given formula and searching for a path fulfilling _¬f_. If
-such a path is found, then we infer that _M_ violates _f_. Otherwise, if
-no path is found that satisfies _¬f_, we conclude that _M |= f_. The LTL
-model checking algorithm of ProB is based on searching for strongly
-connected components (SCCs) with certain properties to determine whether
-_M_ satisfies _f_. Finding such an SCC that can be reached from an
-initial state of _M_ is a witness for a counter-example for _f_.
-Sometimes, we use fairness to ignore such SCCs that do not fulfill the
-imposed fairness constraints in order to not impede proving a property
-by returning of non-fair paths as counter-examples.
-
-The LTL model checker algorithm of ProB is implemented in C using a
-callback mechanism for evaluating the atomic propositions and the
-outgoing transitions in SICStus Prolog. (For each state of the model a
-callback will be performed.) Additionally, the search for SCCs is based
-on the Tarjan's algorithm. In the terminal all messages coming from the
-LTL model checker are preceded either by "LTL (current statistics): " or
-"LTL model checking:". The output from the LTL model checker can give
-helpful insights about the model and the model checking process.
-
-Consider the CSP specifications "dphil_ltl8.csp" representing a model
-of the dining philosophers problem for eight philosophers which resolves
-the starvation problem by always forcing the first philosopher to pick
-up first the right fork instead of the left one. In other words,
-"dphil_ltl8.csp" has no deadlock states. Checking the LTL formula "GF
-[eat.0]" from the command line will produce the following output:
-
-----
-$ probcli -ltlformula "GF [eat.0]" dphil_ltl8.csp
-....
-LTL model checking formula
-% parsing_ltl_formula
-% initialising_ltlc
-starting_model_checking
-
-LTL (current statistics): 13280 atoms, 10070 transitions generated, and  2631 callbacks needed.
-
-LTL model checking: found counter-example (lasso-form): intro length = 1126, path in SCC of length = 5
-LTL model checking: memory usage approx. 1924 KiB, 14104 atoms and 10724 transitions generated
-LTL model checking: total time 22492ms, 2803 callbacks needed 22465ms, netto 26ms.
-! An error occurred !
-! source(ltl)
-! Model Check Counter-Example found for:
-! GF [eat.0]
-
-Formula FALSE.
-
-Runtime: 22220 ms
-! *** error occurred ***
-! ltl
-----
-
-As one can clearly see from the output, the LTL model checker fails to
-prove "GF [eat.0]" on the model since it has found a counter-example
-for the formula. Note that the ProB LTL model checker explores the
-search graph and the state space dynamically. The above data is to be
-understand as follows:
-
-* 14104 atoms - the LTL model checker needed to explore 14104 atoms to
-find a counter-example for the formula.
-* 2803 callbacks needed - to explore the search graph the model checker
-makes callbacks in order to explore the state space of the model being
-checked (the exploration runs dynamically) and compute the successor
-states in the tableau graph. In this case the model checker has needed
-to explore 2803 states till it finds a counter-example for the formula
-* memory usage approx. 1924 KiB - the memory needed to explore the
-tableau graph
-* found counter-example (lasso-form) - means that the counter-example
-being found is path beginning in an initial state of the model and
-reaching a state that closes a cycle:
-** intro length = 1126: the length of the sub-path from an initial state
-to the entry point of the cycle
-** path in SCC of length = 5: the cycle is comprised of five states
-* total time 22492ms - the LTL model checker needed about 23 seconds to
-find the counter-example. Here a distinction between the time needed to
-explore the state space of the model (2803 callbacks needed 22465ms) and
-the time spent for generating the tableau graph + the time for
-identifying the self-fulfilling SCC (netto 26ms)
-* LTL (current statistics) - an intermediate data information is given
-each 20 seconds spent from the last current data information.
-
-In the example above one can prove the LTL^[e]^ formula "GF [eat.0]"
-on "dphil_ltl6.csp" using fairness. One can impose, for example, strong
-fairness conditions on all transitions of the model and thus verify that
-"GF [eat.0]" is satisfied under strong fairness. The call looks as
-follows:
-
-----
-$ probcli -ltlformula "SEF => GF [eat.0]" dphil_ltl8.csp
-...
-LTL model checking formula
-% parsing_ltl_formula
-% initialising_ltlc
-starting_model_checking
-LTL (current statistics): 13016 atoms, 9834 transitions generated, and  2578 callbacks needed.
-LTL (fairness): 0 strongly connected components were rejected, 0 callbacks needed.
-
-LTL (current statistics): 27540 atoms, 44422 transitions generated, and  5123 callbacks needed.
-LTL (fairness): 284 strongly connected components were rejected, 843 callbacks needed.
-.....
-LTL (current statistics): 85980 atoms, 267821 transitions generated, and  19733 callbacks needed.
-LTL (fairness): 454 strongly connected components were rejected, 1924 callbacks needed.
-
-LTL (current statistics): 95648 atoms, 364288 transitions generated, and  22150 callbacks needed.
-LTL (fairness): 773 strongly connected components were rejected, 3085 callbacks needed.
-
-LTL model checking: memory usage approx. 13829 KiB, 96500 atoms and 381625 transitions generated
-LTL model checking: total time 190887ms, 22363 callbacks needed 186690ms, netto 467ms.
-LTL model checking (fairness): 800 strongly connected components were rejected.
-LTL model checking (fairness): total fairness checking time 3729ms, 3246 callbacks needed 3452ms, netto 277ms.
-LTL Formula TRUE.
-No counter example found for SEF => GF [eat.0].
-Runtime: 188370 ms
-----
-
-In the above check no fair counter-example could be found for the
-formula "GF [eat.0]". For this check the search graph comprises 96500
-atoms and 381625 transitions, far more than the previous formula check
-(without fairness assumptions). Since no fair counter-example was found
-we can infer that the whole state space of the model was explored.
-Further, since we know from above that 22363 callbacks were needed to
-explore the search graph, we can infer that the state space of the model
-has in total 22363 states.
-
-In the output above there is also some information about the fairness
-checking being performed for the model checker run. Form the fairness
-statistics we can see that the model checker has refuted 800 SCCs in
-total, i.e. there were 800 SCCs in the search graph that could serve as
-a counter-example for "GF [eat.0]" in case no fairness constraints
-were imposed.
-
-[[other-relevant-tutorials-about-ltl-model-checking]]
-== Other Relevant Tutorials about LTL Model Checking
-
-A brief tutorial on visualizing LTL counter-examples in the Rodin tool
-can be found <<tutorial-ltl-counter-example-view,here>>.
-
-A tutorial of a simple case study, where setting fairness constraints to
-some of the LTL properties is required, can be found
-<<mutual-exclusion-fairness,here>>.
-
-== Summary of CTL Syntax supported by ProB
-ProB also provides limited support for CTL model checking.
-Here is a brief summary of the syntax:
-
-
-----
-   use {...} for B predicates,
-   ExUy,EXx,AXx,EFx,AGx are supported CTL syntax,
-   use e(op) to check if an operation op is enabled,
-   use EX[Op]x to check what is the next operation, e.g. EX[reset]{db={}}
-----
-
diff --git a/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc b/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc
deleted file mode 100644
index aa655b15b329bfbb15195cda815340af4cf603af..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc
+++ /dev/null
@@ -1,130 +0,0 @@
-
-[[symmetry-reduction]]
-= Symmetry Reduction
-
-ProB can make use of symmetries induced
-by the use of deferred sets in B (and given sets in Z).
-
-== Static Symmetry Reduction
-
-ProB will perform a limited form of symmetry reduction for constants
-which are elements of deferred sets. Take the following example:
-
-----
-MACHINE m SETS D
-CONSTANTS a,b,c,d
-PROPERTIES a:D & b:D & a/=b & c:D & d:D & card(D)=6
-END
-----
-
-Elements of a deferred set D of cardinality n are given a number between
-1 and n (the pretty printer of ProB renders those elements as D1,...,Dn
-respectively). Thus, in the example above we could have 1080 solutions
-(6*6*6*6 = 1296 solutions, if we ignore the constraint `a/=b`). Luckily,
-symmetry reduction will reduce this to 10 possibilities.
-
-In a first phase ProB will detect, for every deferred set D, a maximal
-set ds of type D which are disjoint. In the example above, such a set ds
-is `{a,b}`. These elements will be fixed, in the sense that they will
-get the numbers 1..k, where k is the size of ds. Thus, a will denote D1,
-b will denote D2. ProB's pretty printer will actually use a instead of
-D1, and b instead of D2 (and a and b will actually disappear from the
-list of constants visible in the state properties view). This reduces
-the number of possibilities already to 36.
-
-As of version 1.5, ProB will also further restrict the possible numbers
-of the remaining constants. It is an adapted technique described in
-Section 6 of the article "New Techniques that Improve MACE-style Finite
-Model Finding"
-(http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf[PDF]).
-Basically, the technique ensures that c will not use the index 4 and
-that d will use the index 4 only if the index 3 was used by c. Thus only
-the 10 following possibilities are generated by ProB:
-
-----
- a   b   c   d
-----------------
- a   b   a   a
- a   b   a   b
- a   b   D3  D4
- a   b   a   D3
- a   b   b   a
- a   b   b   b
- a   b   b   D3
- a   b   D3  a
- a   b   D3  b
- a   b   D3  D3
-----
-
-As of version 1.8, ProB will furthermore detect partition constraints
-for the deferred sets. This symmetry reduction is applied to the free,
-unconstrained deferred set elements. For the example above, these would
-be all elements with index 5 or higher (D5, D6, ...). For the example
-above, if we have a constraint
-
-`D = A \/ B & A /\ B = {}`
-
-the free deferred set elements D5,D6,... will be allocated in order to A
-and B. In other words, we can have D5 in A and D6 in B, but not D6 in A
-and D5 in B.
-
-In the machine below all deferred set elements are free:
-
-----
-MACHINE m SETS D
-CONSTANTS A,B
-PROPERTIES D = A \/ B & A /\ B = {} & card(D)=6 & card(A) = 3
-END
-----
-
-Hence, here ProB 1.8 will only generate one possible setup of the
-constants:
-
-----
-A = {D1,D2,D3}
-B = {D4,D5,D6}
-----
-
-== Symmetry Reduction during Model Checking
-
-In addition to the above, you can also turn of stronger symmetry
-reduction for model checking.
-
-Warning: turning on symmetry reduction will also influence the way that
-animation works. In other words, when executing an operation, the
-animator may transfer you to an equivalent symmetric state (rather than
-to the one you may have expected).
-
-In the "Symmetry" menu of the "Preferences" menu you can choose the
-following:
-
-* "off": symmetry reduction is turned off.
-* "flood": This performs permutation flooding, whereby all
-permutations of a newly added state are automatically added (and marked
-as already treated). This does not reduce the number of states of the
-state space, but it may still considerably reduce the number of
-transitions and the number of states which need to be checked (for
-invariant violations and for computing outgoing transitions). More
-details: footnote:[Michael Leuschel, Michael Butler, Corinna Spermann
-and Edd Turner: Symmetry Reduction for B by Permutation Flooding,
-Proceedings of the 7th International B Conference (B2007),2007,pp.
-79-93,LNCS 4355,Springer,
-https://www3.hhu.de/stups/downloads/pdf/LeBuSpTu07_209.pdf]
-* "nauty": This approach translates a B state into a graph and uses
-the nauty package in order to compute a canonical form of this graph. If
-two states have the same canonical form, they are considered equivalent
-and only one of them is explored footnote:[Corinna Spermann and Michael
-Leuschel: ProB gets Nauty: Effective Symmetry Reduction for B and Z
-Models, Proceedings Symposium TASE 2008,June,2008,pp. 15-22,IEEE].
-Warning: nauty sometimes can take a long time to compute the canonical
-form for complicated states (and in this case it will not respond to
-ProB's standard time-out mechanism).
-* "hash": This approach computes a symbolic hash value for every
-state, having the important property that two symmetric states have the
-same hash value. Note that this is an "approximate" method, as two
-non-symmetric states may also be mapped to the same hash
-valuefootnote:[Michael Leuschel and Thierry Massart: ProB gets Nauty:
-Efficient Approximate Verification of B via Symmetry Markers,
-Proceedings International Symmetry Conference,Januar,2007,Verlag,
-https://www3.hhu.de/stups/downloads/pdf/LeMa07_212.pdf].
-This is typically the most efficient method.
diff --git a/src/docs/chapter/user/20_Validation/MC/40_LTSmin b/src/docs/chapter/user/20_Validation/MC/40_LTSmin
deleted file mode 100644
index 8cebdad97341fbffa9268aa947566f334ac2b764..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/40_LTSmin
+++ /dev/null
@@ -1,13 +0,0 @@
-
-[[lts-min-extension]]
-= LTSmin Extension
-
-In order to set up LTSmin, do the following:
-
-* Download the latest LTSmin release: https://github.com/utwente-fmt/ltsmin/releases and extract it
-* (Linux only) start ProB via `LD_LIBRARY_PATH=lib/ ./prob` if you have not installed ZeroMQ and CZMQ
-* In ProB, go to Preferences > All Preferences (alphabetical)...
-* Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive
-* Start Model Checking via Verify > External Tools > Model Checking with LTSmin
-
-Note that the LTSmin extension is not available for Windows.
diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc
deleted file mode 100644
index fdd8745d443a50e4e8272be3e7a2c986e4795aec..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc
+++ /dev/null
@@ -1,201 +0,0 @@
-
-[[tutorial-directed-model-checking]]
-= Tutorial Directed Model Checking
-
-We assume that you have completed
-<<tutorial-first-model-checking,Tutorial First Model Checking>> and
-<<tutorial-complete-model-checking,Complete model checking>>.
-
-Here we will look a bit closer at the search strategy options of the
-ProB model checker. You can set the mode using the `-mc_mode`
-command-line switch of
-<<using-the-command-line-version-of-prob,probcli>>. In the Tcl/Tk
-version you can select the strategy in the model checking dialog box
-(which you obtain via the"Model Check..." command in the _Verify_ menu):
-
-image::ProBWinModelCheckDialog.png[]
-
-The following values are possible in all versions of ProB:
-
-* Mixed DF/BF (`mixed` for `mc_mode`) : mixed depth-first /
-breadth-first traversal with random choice; currently the default),
-* Breadth First (`bf` for `mc_mode`): breadth-first traversal,
-* Depth First (`df`) depth-first traversal,
-
-As of version 1.5.1, the following options are also available:
-
-* Heuristic Function / Random (`heuristic` for `mc_mode`) : try and use
-`HEURISTIC_FUNCTION` provided by user in `DEFINITIONS` clause; states
-with the smallest value for the heuristic function are treated first by
-the model checker. Some explanations can be found
-<<blocks-world-directed-model-checking,in an example about
-directed model checking>>.
-* Random (`random`) : choosing next node to process completely at
-random,
-* Hash-Random (`hash`) :similar to random, but uses the Prolog hash
-function of a node instead of a random number generator,
-* Out-Degree for Deadlock Checking (`out_degree_hash`): prioritise nodes
-with fewer outgoing transitions; mainly useful for deadlock checking.
-
-Note that for exhaustive model checking, where you have to look at the
-entire state space and no error state is found, the search strategy has
-little nor no influence: it does not really matter in which order we
-process the states, when we have to examine all of them anyway. In this
-case, the depth-first search is probably the most adequate choice: its
-memory requirement is smaller. However, when you expect an error (or
-goal state) to be found and when the state space is very large (or even
-infinite), then the search strategy can make a big difference: the
-difference between finding an error state very quickly, or only after a
-very long time or possibly never at all.
-
-To illustrate the effect of the search strategy we use the following
-simple example:
-
-....
-MACHINE phonebook7
-SETS
-  Name; Code = {c1,c2,c3,c4}
-VARIABLES db, active, activec
-DEFINITIONS
-  scope_Name == 1..4
-INVARIANT
-  db : Name +-> Code & active:POW(Name) & activec:POW(Code) &
-  dom(db) = active & ran(db) = activec
-ASSERTIONS
-  card(active) >= card(activec)
-INITIALISATION
-  db := {} || active := {} || activec := {}
-OPERATIONS
-dd <-- getdom = dd:= dom(db);
-cc <-- lookup(nn) =
-  PRE
-      nn : Name & nn : active
-  THEN
-      cc := db(nn)
-  END;
-add(nn,cc) =
-  PRE
-      nn:Name & cc:Code  & nn /: active
-  THEN
-      db := db \/ {nn |-> cc} || active := active \/ {nn} || activec := activec \/ {cc}
-  END;
-delete(nn,cc) =
-  PRE
-      nn:Name & cc:Code & nn: active & cc: activec & db(nn) = cc
-  THEN
-      db := db - {nn |-> cc} || active := active - {nn} || activec := db[(active - {nn})]
-  END
-END
-....
-
-We will illustrate the state space that ProB generates using the various
-search strategies when limiting the search to 10 nodes. For this we use
-the command-line version as follows (as there we can provide exactly how
-many states should be explored):
-
-`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode`
-
-However, you can also obtain a similar effect with the Tcl/Tk version by
-starting the model checker and then quickly pressing the Cancel button
-and then inspecting the state space (Statespace command in the _Visualize_ menu; see
-<<tutorial-first-model-checking,Tutorial_First_Model_Checking>>).
-Below we show the output of the above command for the various choices of
-.
-
-[[breadth-first]]
-== Breadth-First
-
-`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode bf`
-
-image::ProB_Phonebook7_spdot_bf.png[]
-
-This mode has the advantage of finding shortest counter examples first.
-We also have a guarantee that, provided a counter example exists, a
-counter example will sooner or later be found. However, the memory
-requirements can be very large and it can take very long to find long
-counter examples.
-
-[[depth-first]]
-== Depth-First
-
-`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode df`
-
-image::ProB_Phonebook7_spdot_df.png[]
-
-The depth-first traversal has the advantage of lower memory requirements
-(concerning storing the unprocessed nodes) and can find very deep
-counter examples. While it is typically the best choice for exhaustive
-model checking, it can be a poor choice for models with errors. Indeed,
-if the state space is infinite, then depth-first may progress infinitely
-in one direction, and never find existing counter examples. Also, when
-depth-first search finds a counter example, it is typically very long
-and possibly hard to understand for the user. The next search strategy,
-tries to combine the advantages of breadth-first and depth-first search.
-
-[[mixed-dfbf]]
-== Mixed DF/BF
-
-The mixed search strategy, tries to combine the advantages of
-breadth-first and depth-first search. It is the default setting for
-ProB. It has the advantage of ensuring the exploration of some branches
-in depth, to find errors which require long counter examples (e.g.,
-starvation, resource exhaustion kind of bugs). But it also ensures that
-we examine the specification more systematically in breadth, and is thus
-also good at finding counter examples which require exhaustively to test
-all operations (e.g., many errors simply require a particular faulty B
-operation to be executed).
-
-`$ probcli phonebook7.mch -p MAX_OPERATIONS 200 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode mixed`
-
-The result will vary from one run of ProB to another:
-
-image::ProB_Phonebook7_spdot_mixed1.png[]
-
-image::ProB_Phonebook7_spdot_mixed2.png[]
-
-It is interesting to compare this result with the random search
-strategy, which we show next.
-
-[[random]]
-== Random
-
-`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode random`
-
-Here are two sample results:
-
-image::ProB_Phonebook7_spdot_random1.png[]
-
-image::ProB_Phonebook7_spdot_random2.png[]
-
-Compared to the `mixed` option one can notice that the mixed option has
-more of a tendency to explore certain branches in depth.
-
-[[hash]]
-== Hash
-
-`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode hash`
-
-image::ProB_Phonebook7_spdot_hash.png[]
-
-The difference with the `random` option is that this will always return
-the same result, as the hash value of the states do not change from one
-run of ProB to another.
-
-[[out-degree]]
-== Out-Degree
-
-`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode dlk`
-
-image::ProB_Phonebook7_spdot_dlk.png[]
-
-One can notice that ProB here has a tendency to go into depth, as the
-number of enabled operations decreases: if we add a name to the
-phonebook, four enabled operations disappear and only two appear (lookup
-and delete). Note: here it is important to set the `MAX_OPERATIONS` high
-enough, otherwise the resulting state space could be different.
-
-[[more-examples]]
-== More examples
-
-A further illustration of directed model checking can be found in our
-<<blocks-world-directed-model-checking,"Blocks World" example>>.
diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc b/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc
deleted file mode 100644
index 1ea9e104267c8fd9cb720552daee206998f7d282..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc
+++ /dev/null
@@ -1,536 +0,0 @@
-
-[[tutorial-various-optimizations]]
-= Tutorial Various Optimizations
-
-The ordinary model checker of ProB enables the user to verify
-automatically whether a B model contains any errors such as deadlocks
-and invariant violations. The search for errors is performed by a graph
-traversal algorithm exploring the state space until an error state has
-been found or all states of the model have been explored. The runtime of
-the model checker is mostly determined by the number of states of the
-model being analyzed and thus model checking is generally limited by the
-size of the state space of the model. The problem is also known as the
-state space explosion problem.
-
-To combat the state space explosion problem two advantageous techniques,
-partial guard evaluation and partial order reduction, for the ordinary
-model checker of ProB have been implemented for model checking
-practically B and Event-B models with huge state spaces. This tutorial
-describes how one can apply model checking using the optimizations and
-additionally gives hints when it is recommendable to use these
-optimizations.
-
-[[partial-order-reduction]]
-== Partial Order Reduction
-
-Partial order reduction (POR) is a method proposed for combating the
-state space explosion problem by means of state space reduction. The
-technique takes advantage of the commutativity of concurrently executed
-actions. The reduction relies on selecting a subset of all enabled
-actions in each reachable state of the state space aiming in this way to
-reduce the number of possible orderings of actions. Basically, the idea
-is to check only a fragment of the original state space that is
-sufficient for checking the given property.
-
-Take, for example, the following B machine:
-
-....
-MACHINE Example
-VARIABLES x,y,z
-INVARIANT
- x:INT & y:INT & z:INT
-INITIALISATION x,y,z:=0,0,0
-OPERATIONS
-  IncX = PRE x=0 THEN x:= x+1 END;
-  IncY = PRE y=0 THEN y:= y+1 END;
-  IncZ = PRE z=0 THEN z:= z+1 END
-END
-....
-
-The machine has a deadlock state. The deadlock state will be reached by
-executing each of the operations IncX, IncY, and IncZ. The order of
-executing the operations is irrelevant with respect to reaching the
-deadlock state. This can be seen, for example, by observing the full
-state space of the machine:
-
-image::Full_state_space_por.png[]
-
-Since the order in which the operations are executed is not relevant for
-discovering the deadlock state it is sufficient to examine only one of
-the six possible paths that start in the initial state and reach the
-deadlock. Thus, for the machine it is enough to analyze only one
-arbitrary order of the events in order to detect the deadlock:
-
-image::Partial_state_space_por.png[]
-
-Using this observation the ordinary model checker of ProB has been
-extended to check a model formalized in B or Event-B using partial order
-reduction. More information about the implementation of POR in ProB and
-the theoretical background of POR can be read
-https://www3.hhu.de/stups/downloads/pdf/DobrikovLeuschelPORtechreport.pdf[here].
-Our implementation of POR uses the ample set theory footnote:[E.M.
-Clarke, O. Grumberg, M. Minea, and D. Peled: _State Space Reduction
-using Partial Order Reduction_. STTT '98, 3, pages 279-287].
-
-For enabling the POR optimization for the model checker in Tcl/Tk
-interface of ProB a new check box “Partial Order Reduction” has been
-added to the “Model Checker” menu. Note that the option shows up only
-when the user mode is set to “Normal” (see Preferences → User Mode in
-the menu bar). The POR optimization can be enabled for model checking B
-and Event-B models with the command line version of ProB by setting the
-'por' preference to the value 'ample_sets'. For example, the machine
-_Example_ can be checked for deadlock and invariant violations using the
-POR optimization with the command line version of ProB as follows:
-
-....
-$ probcli Example.mch -mc 10000 -p por ample_sets
-********* DETERMINE ACTION DEPENDENCIES AND ENABLE GRAPH *************
-********** FINISHED ANALYSIS *************
-Analysis Checking Time: 10 ms.
-
-ALL OPERATIONS COVERED
-
-found_error(deadlock,3)
-finding_trace_from_to(root)
-
-Model Checking Time: 40 ms (100 ms walltime)
-States analysed: 3
-Transitions fired: 4
-*** COUNTER EXAMPLE FOUND ***
-
-deadlock
-*** TRACE:
- 1: INITIALISATION(0,0,0):
- 2: IncZ:
- 3: IncX:
- 4: IncY:
-! *** error occurred ***
-! deadlock
-....
-
-As a result the deadlock has been discovered by exploring in total 3
-states using the Mixed DF/BF search strategy. Model checking the machine
-without using POR will possibly explore more states until it finds out
-the deadlock state (recall that the full state space of Example.mch
-consists of 8 states). Note that the POR algorithm can be applied to all
-exploration strategies (DF, BF, and Mixed DF/BF) of the ordinary model
-checker of ProB.
-
-The reduction of the state space takes effect by choosing a subset of
-the set of all enabled transitions in the currently explored state. The
-set of all enabled transitions in some state `s` is usually denoted by
-`enabled(s)` and the subset of the transitions chosen to be executed in
-`s` is denoted by `ample(s)`. The set `ample(s)` we call an ample set
-for state `s`. Each ample set should satisfy certain conditions (the
-ample set requirements) in order to guarantee that the reduction of the
-state space is sound in regard to the property being checked on the
-model. In fact, there are four conditions that each ample set should
-satisfy:
-
-* (A 1) `ample(s) = {} \<\=> enabled(s) = {}`
-* (A 2) Along every finite execution in the original state space
-starting in `s`, an event dependent on `ample(s)` cannot appear before
-some event from `ample(s)` is executed
-* (A 3) If `ample(s)` is a proper set of `enabled(s)`, then each
-transition in `ample(s)` is a stutter transition.
-* (A 4) For any cycle `C` in the reduced state space, if a state in `C`
-has an enabled event `e`, then there exists a state `s` in `C` such that
-`e` is an element of `ample(s)`.
-
-To guarantee that all deadlocks in the full state space are also
-preserved in the reduced state space it is sufficient when all computed
-ample sets satisfy just the first two conditions . This suggests that in
-some cases, when we check for deadlock freedom only, the reduction of
-the state space may be more effective if each ample set satisfies only
-the first two ample set requirements. That is, model checking with POR
-usually tends to yield more state space reduction when checking a model
-for deadlock freedom only than checking it for invariant violations or
-simultaneously for deadlock freedom and invariant violations. (The
-reduction algorithm of ProB has been adapted to this fact.) For this
-reason, keep in mind to disable the “Invariant Violations” option if it
-is intended to check a B or Event-B model just for deadlocks using the
-POR optimization as the potential for more significant reduction of the
-state space is higher.
-
-The reduction algorithm makes use of the independence of transitions.
-Two transitions `Op1` and `Op2` are called independent if for each state
-s where both are enabled we have the following situation:
-
-image::Independence.png[]
-
-Let us assume that the transitions `Op1` and `Op2` in the Figure above
-constitute the executions of two deterministic operations of a B
-machine. Then we can say that the operations `Op1` and `Op2` are
-independent, when they cannot disable one other and additionally both
-possible orders of execution of the operations
-latexmath:[$\langle Op1,Op2\rangle$] and
-latexmath:[$\langle Op2,Op1\rangle$] starting in some state
-latexmath:[$s$] reach the same state latexmath:[$s_3$]. If two
-transitions are not independent, then both are denoted as dependent.
-
-To find out whether two operations are independent one can analyze the
-syntactical structure of both operations. If each of the operations
-modifies variables of the machine not read by the other one and if both
-operations modify different variables, then these operations are
-considered to be independent. Besides performing only a syntactical
-analysis, we use also the constraint-based facilities of ProB to
-determine more exact relations between the operations. The reason for
-those extra analyzes lies in the high potential for significant
-reduction of the state space when the degree of independence of the
-checked B model is high.
-
-Thus, if we have a great amount of independent operations for some B
-machine, then we have a great potential for significant state space
-reduction. The results of the analyses for determining the independence
-of operations for a particular B machine, which are used by the
-reduction algorithm for computing the ample sets, can be viewed in the
-menu bar of the Tcl/Tk interface of ProB: “Verify → Enabling Analysis →
-Dependence Analysis (Table)”. For example, the dependency table for the
-model 'Example.mch' looks as follows:
-
-image::Dependency_table.png[]
-
-The results in the dependency table for a pair of operations `Op1` and
-`Op2` have the following meanings:
-
-*  syntactic_independent : `Op1` and `Op2` are syntactically
-independent; both events write different variables and no one of the
-events can write a variable which is read by the other one
-*  independent : one of the events or both events write variables read
-only in the guard of the other one, though the events cannot disable
-each other
-*  dependent : the events are not independent
-*  race_dependent : `Op1` and `Op2` have write variables in common
-*  - : the dependency relation is symmetric, see `(Op2,Op1)` result
-*  = : `Op1` and `Op2` represent the same event
-
-To sum up, in order to take an advantage of POR the model being checked
-should have many independent operations that are concurrently executed.
-In other words, the magnitude of reduction depends on the coupling
-between the operations in the B model. Thus, it is recommended to use
-the reduced search when the analyzed model has comparatively many
-independent operations that are concurrently executed in order to gain
-from the improvement by the reduction technique. For example, if a B
-model has no pair of independent operations or all independent
-operations are not executed concurrently, i.e. two independent
-operations are never simultaneously enabled, then no reductions of the
-state space will be performed using the reduced search algorithm.
-
-The reduction algorithm has been evaluated on various B and Event-B
-models. The evaluation can be obtained
-https://www3.hhu.de/stups/downloads/[here].
-
-[[partial-guard-evaluation]]
-== Partial Guard Evaluation
-
-When checking for consistency a B model the ProB model checker traverses
-the state space of the model beginning in some of the initial states and
-checks for errors each state, which it encounters. The ProB model
-checker explores the state space of the B machine by applying all
-operations of the machine to the current state. As a result, the
-successor states of the state are determined. The exploration of the
-state space continues until all possible states are explored or an error
-state is found.
-
-When a state, say `s`, is processed the following steps are consequently
-performed:
-
-1.  Checking `s` for errors like invariant violation, assertion
-violation, and deadlock;
-2.  Applying the machine's operations to `s`.
-
-The second step is carried out in case no error was discovered
-previously (in step 1). When step 2. is performed in some state `s` all
-operations of the checked B model are tested for being enabled in `s`
-and the substitutions of each enabled operation are performed at `s`.
-
-The effort of checking a state amounts thus to checking the state for
-errors (testing for invariant violation, assertion violations etc.) plus
-the computation of the successors. There is some redundancy in testing
-all operations' guards in each state, as usually there are operations
-that are disabled in the states being explored. Especially, when the
-model checker has to check exhaustively B models with large state spaces
-the effort of testing the guard of each operation in every state may be
-huge. Thus, an optimization may be considered by means of decreasing the
-state space exploration complexity by trying to reduce the overall
-number of guard tests via skipping the guard evaluations of operations
-known to be disabled in some states.
-
-One can determine a set of disabled operations in a state `s` by
-considering, for example, the incoming transitions of `s`. During the
-observation of the incoming transitions we examine how the operations
-represented by the incoming transitions may influence other operations.
-If, for example, operation ‘A’ surely disables operation ‘B’ we can
-assume that ‘B’ is disabled at each state having ‘A’ as incoming
-transition. This and other such relations can be used to optimize the
-ProB model checker for exhaustively checking B models. This type of
-relations we will also call _enabling relations_.
-
-Enabling relations between operations reveal how operations of a given B
-model could influence each other with regard to enabledness. In other
-words, we are interested in the effect of executing one operation `Op1`
-on the status of the guard of another operation `Op2` for each pair of
-operations `(Op1,Op2)` of the underlying B model. The effect of an
-operation `Op1` can affect the guard of another operation `Op2` in
-various ways:
-
-* `Op1` enables `Op2`, or
-* `Op1` disables `Op2`, or
-* `Op1` keeps `Op2` enabled respectively disabled;
-
-This enabling relation of two operations we can illustrate, for example,
-as follows:
-
-image::RelationFigureExplanation.png[]
-
-where the green boxes denote that the evaluation of the guard of `Op2`
-is true, whereas the red boxes indicate that the evaluation of the guard
-of `Op2` is false.
-
-The model checker optimization, partial guard evaluation, makes use of
-such a kind of relations. The enabling relations are determined by means
-of syntactic and constraint-based analyses. In particular, we
-concentrate on three kinds of enabling relations:
-
-* `Op2` is *always* enabled after the execution of `Op1`
-
-image::GuaranteedRelation.png[]
-
-* `Op2` is *impossible* to be enabled after the execution of `Op1`
-
-image::ImpossibleRelation.png[]
-
-* `Op1` *keeps* `Op2` enabled respectively disabled
-
-image::KeepRelation.png[]
-
-
-Consider the B machine below modelling an algorithm for mutual exclusion
-with a semaphore (in the machine below this is variable `y`) for two
-concurrent processes latexmath:[$P_1$] and latexmath:[$P_2$]. Each
-process has been simplified to perform three types of actions: _request_
-(for entering in the critical section), _enter_ (entering the critical
-section), and _release_ (exiting the critical section).
-
-....
-MACHINE MutualExclusion
-SETS
-  STATE={non_critical,waiting,critical}
-VARIABLES
-  p1,p2,y
-INVARIANT
-    y : 0 .. 1 & not(p1 = critical & p2 = critical)
-INITIALISATION
- p1, p2, y := non_critical, non_critical, 1
-OPERATIONS
-  Req1 = PRE p1 = non_critical THEN p1 := waiting END;
-  Enter1 = PRE p1 = waiting & y = 1 THEN p1 := critical || y := 0 END;
-  Rel1 = PRE p1 = critical THEN p1 := non_critical || y := 1 END;
-  Req2 = PRE p2 = non_critical THEN p2 := waiting END;
-  Enter2 = PRE p2 = waiting & y = 1 THEN p2 := critical || y := 0 END;
-  Rel2 = PRE p2 = critical THEN p2 := non_critical || y := 1 END
-END
-....
-
-Every of the both processes latexmath:[$P_{i}$] has three possible
-states that we will denote as follows: latexmath:[$n_{i}$] (the state in
-which latexmath:[$P_{i}$] performs noncritical actions),
-latexmath:[$w_{i}$] (the state in which latexmath:[$P_{i}$] waits to
-enter the critical section), and latexmath:[$c_{i}$] (representing the
-state in which latexmath:[$P_{i}$] is in the critical section). Both
-processes share the binary semaphore y, where y=1 indicates that the
-semaphore is free and y=0 that the semaphore is currently processed by
-one of the processes.
-
-In the B machine the operations `Req1`, `Enter1` and `Rel1` represent
-the actions _request_, _enter_ and _release_ of latexmath:[$P_1$],
-respectively. Analogously, the operations `Req2`, `Enter2` and `Rel2`
-represent the actions _request_, _enter_ and _release_ of
-latexmath:[$P_2$], respectively. The requirement _always at most one
-process is in its critical section_ guaranteeing the mutual exclusion
-property is stated in the invariant of the machine by means of the
-predicate `not(p1 = crit1 & p2 = crit2)`.
-
-To verify that the B machine satisfy the mutual exclusion property and
-has no deadlock state one can use the ProB model checker. This will
-explicitly generate all possible states of the machine and check whether
-there is any state that is a deadlock state or that violates the
-invariant. As a result, 8 states will be generated and checked, the
-machine is consistent with respect to the invariant and has no deadlock
-state. By the exhaustive search for error states the model checker will
-test by exploring the state space each guard of the machine’s operations
-for being enabled in the currently processed state. That is, while
-exploring the state space of the machine 48 guard tests (8 states
-latexmath:[$\times$] 6 operations) will be performed in order to unfold
-the entire state space of the MutualExclusion machine.
-
-image::StateSpacePGE.png[]
-
-The state space of the `MutualExclusion` machine is visualised in Figure
-1. The symbols latexmath:[$n_i$], latexmath:[$w_i$] and
-latexmath:[$c_i$] in Figure 1 denote the bindings
-latexmath:[$p_i = non_critical$], latexmath:[$p_i = waiting$] and
-latexmath:[$p_i = critical$] (where _i=1,2_), respectively. Observing,
-for example, the operation `Req1` in `MutualExclusion.mch` one can
-easily deduce that the operations `Req1` and `Rel1` will be disabled in
-the after-state of each `Req1` transition. This can be simply inferred
-by seeing that assigning the variable _p1_ the constant _waiting_ leads
-to a state in which both predicates _p1=non_critical_ and _p1=critical_
-evaluate to false. That is, `Req1` and `Rel1` are *impossible* to be
-enabled after executing `Req1`. Further, since `Req1` writes only the
-variable _p1_ we can conclude that the guards of the operations `Req2`,
-`Enter2` and `Rel2` cannot be affected after executing `Req1`, i.e.
-`Req1` *keeps* the enabling status of `Req2`, `Enter2` and `Rel2`
-unchanged. These relations can be determined in ProB by means of
-syntactic and constraint-based analyses.
-
-The enabling relations between the operations of `MutualExclusion.mch`
-used for the Partial Guard Evaluation optimisation are summerised in the
-table below. The enabling relations _guaranteed_ and _enable_ indicate
-the cases when the guard of an operation is *guaranteed* enabled after
-the execution another operation and when an operation *can be enabled*
-after the execution of another operation but the enabledness is not
-always guaranteed, respectively.
-
-[cols=",,,,,,",]
-|=======================================================================
-|Origin |Req1 |Enter1 |Rel1 |Req2 |Enter2 |Rel2
-
-|Req1 | [red]#impossible# |enable | [red]#impossible# | [yellow]#keep# | [yellow]#keep# | [yellow]#keep#
-
-|Enter1 | [red]#impossible# | [red]#impossible# | [green]#guaranteed# | [yellow]#keep# | [red]#impossible# |
-[yellow]#keep#
-
-|Rel1 | [green]#guaranteed# | [red]#impossible# | [red]#impossible# | [yellow]#keep# |enable | [yellow]#keep#
-
-|Req2 | [yellow]#keep# | [yellow]#keep# | [yellow]#keep# | [red]#impossible# |enable | [red]#impossible#
-
-|Enter2 | [yellow]#keep# | [red]#impossible# | [yellow]#keep# | [red]#impossible# | [red]#impossible# |
-[green]#guaranteed#
-
-|Rel2 | [yellow]#keep# |enable | [yellow]#keep# | [green]#guaranteed# | [red]#impossible# | [red]#impossible#
-|=======================================================================
-
-Let us now consider state latexmath:[$s_2$] in Figure 1 that we assume
-to be yet not explored by the model checker. latexmath:[$s_2$] is an
-after-state of `Req1`. Using the enabling relations that we have
-established we can infer that `Req1` and `Rel1` are disabled at
-latexmath:[$s_2$] since both are impossible to be enabled in each
-after-state of `Req1`. Further, we can omit the tests of the guards of
-`Enter2` and `Rel2` since both operations are disabled in
-latexmath:[$s_1$] and we already have shown that `Req1` cannot change
-the status of the guard of both operations. As a result, we can skip the
-test for enabledness for `Req1`, `Rel1`, `Enter2` and `Rel2` in
-latexmath:[$s_2$]. The test of the guard of `Req2` can also be omitted
-since `Req2` is enabled in latexmath:[$s_1$] and thus also enabled in
-latexmath:[$s_2$] as `Req1` keeps `Req2` enabled. Summarizing these
-results, it is thus necessary to test only the guard of `Enter1` in
-latexmath:[$s_2$] as we could determine the status of the guards of the
-residual operations via the enabling relations that we considered
-previously.
-
-Partial guard evaluation (PGE) makes use of the enabling relations.
-Above we described how guard tests can be saved up aiming to optimise
-the exploration of the state space and thus to provide smaller model
-checking times for B models, as well as for Event-B models. The
-optimisation can be enabled using the preference ('-p') option in case
-the command line of the ProB tool is used for model checking:
-
-....
-$ probcli -mc 1000000 MutualExclusion.mch -p use_pge true
-********** START PGE ANALYSIS *************
-********** PGE ANALYSIS FINISHED **********
-Analysis Checking Time: 40 ms.
-
-ALL OPERATIONS COVERED
-
-% All open nodes visited
-Model Checking Time: 10 ms (50 ms walltime)
-States analysed: 8
-Transitions fired: 15
-No Counter Example found. ALL nodes visited.
-....
-
-For our example, `MutualExclusion.mch`, the PGE analysis needed 40ms to
-determine the enabling relations of the machine and saved up overall 34
-guard evaluations while exploring the state space of the model. ProB
-uses by default a mixed breath-first/depth-first search for the
-exploration of the state space.
-
-The number of skipped guard tests may depend on the exploration strategy
-when the model checker is started with the partial guard evaluation
-method. To clarify this consider again the B machine formilising the
-mutual exclusion algorithm with semaphore for two processes. Assume
-first that the state space is explored in a depth-first manner and that
-the currently explored state is latexmath:[$s_7$] in Figure 2.
-Additionally, latexmath:[$s_1$], latexmath:[$s_2$] and latexmath:[$s_4$]
-are the states that were explored before reaching latexmath:[$s_7$].
-Before exploring state latexmath:[$s_7$] the PGE algorithm analyses
-which operations can be determined as disabled in latexmath:[$s_7$]
-using the results from the enabling analysis and observing the currently
-present incoming transitions of latexmath:[$s_7$]. From Figure 2 we can
-see that the only incoming transition of the explored state space till
-that moment is `Req2`. Since it is impossible for the operations `Req2`
-and `Rel2` to be enabled after the execution of `Req2` we can infer that
-both are disabled at state latexmath:[$s_7$]. Further, as `Req1` and
-`Enter1` are disabled at latexmath:[$s_5$] we can also assume that both
-operations are also disabled at latexmath:[$s_7$], for `Req2` cannot
-change the enabling status of `Req1` and `Enter1`. On the other hand,
-`Rel1` can be considered as enabled at latexmath:[$s_7$] because of its
-enabledness in latexmath:[$s_5$]. In the end, we could determine that
-the operations `Req1`, `Enter1`, `Req2` and `Rel2` are disabled at
-latexmath:[$s_7$] and we could infer that `Rel1` is enabled at
-latexmath:[$s_7$] without testing their guards for enabledness. The only
-operation that we need to test for enabledness in latexmath:[$s_7$] is
-`Enter2`.
-
-image::StateSpaceDepthFirst.png[]
-
-Let us now consider the explored state space in Figure 3. Using
-breadth-first search will explore all states above latexmath:[$s_7$] and
-latexmath:[$s_8$] until latexmath:[$s_7$] is reached. When
-latexmath:[$s_7$] is explored the operation `Enter1` will also be
-considered in the course of analysing which operations are disabled and
-enabled at latexmath:[$s_7$] as in the figure below state
-latexmath:[$s_5$] was already explored and `Enter1` is an incoming
-transition of latexmath:[$s_7$]. Using the results from the table above,
-we can infer that `Enter2` is disabled at latexmath:[$s_7$] since it is
-impossible for `Enter2`to be enabled after the execution of `Enter1`
-(see the Enabling Analysis table above). If we use the results inferred
-by analysing the enabling relation in regard to `Req2`, then we can
-conclude that all operations are disabled in latexmath:[$s_7$] except
-for `Rel1`. Thus, in this case we saved up one guard test more in
-comparison to the depth-first search example.
-
-image::StateSpaceBreadthFirst.png[]
-
-Model checking with partial guard evaluation usually tends to decrease
-more significantly the number of guards being tested using breadth-first
-search in comparison to the other two exploration strategies. This is
-due to the fact that in breadth-first search we explore all states from
-the current level before we begin with the exploration of the next level
-states. In this way, when the current state is explored the possibility
-that more incoming transitions are computed than other search strategies
-is higher.
-
-In the table below we list some benchmarks for evaluating the PGE
-optimisation. The test cases with '+PGE' use partial guard evaluation as
-an optimisation for model checking the models. In the *Skipped/Total
-Guard Tests* column the number of omitted guard tests and the total
-number of guards are given.
-
-image::PGEEvaluationTable.png[]
-
-In all test cases except for 'All Enabled' and 'Cruise Control' model
-checking with PGE has provided better performance results than model
-checking without PGE. The results show that partial guard evaluation can
-improve model checking up to factor 2. The larger the state space the
-higher is the possibility for better performance in model checking B
-models. For example, for 'CAN BUS' the optimisation could speed up model
-checking to factor 2, whereas for the 'Crusie Control' model no
-improvement could be detected although a significant number of guard
-evaluations could be saved up.
-
-These and various other benchmarks used for evaluating partial guard
-evaluation (PGE) can be viewed
-https://www3.hhu.de/stups/downloads/[here].
diff --git a/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1
diff --git a/src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc b/src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc
deleted file mode 100644
index f0a097e16777060d064c6b77b0e0881d0379f19d..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc
+++ /dev/null
@@ -1,39 +0,0 @@
-
-[[prob-validation-methods]]
-= ProB Validation Methods
-
-ProB offers various validation techniques:
-
-* <<consistency-checking,Consistency Checking (Finding Invariant
-Violations using the Model Checker)>>
-* <<constraint-based-checking,Constraint Based Checking>>
-* <<refinement-checking,Refinement Checking>>
-* <<ltl-model-checking,LTL Model Checking>>
-* <<bounded-model-checking,Bounded Model Checking>>
-
-Here we want to describe the advantages and disadvantages of the various
-methods.
-
-.__Comparing ProB Validation Techniques__
-[cols=",,,,",options="header",]
-|=======================================================================
-|Question |Model Checking |LTL Model Checking |CBC Checking |Bounded
-Model Checking
-|Can find Invariant Violations ? |yes |yes (`G{INV}`) |yes |yes
-
-|Only reachable counter-examples from initial state? |yes |yes |no |yes
-
-|Search Technique for counter-examples? |mixed df/bf, df, bf
-|depth-first (df) |length 1 |breadth-first (bf)
-
-|Can deal with large branching factor? |no |no |yes |yes
-
-|Can find deep counter-examples? |yes |yes |n/a (length 1) |no
-
-|Can find deadlocks ? |yes |yes (`G not(deadlock)`) |yes |not yet
-
-|Can find assertion violations ? |yes |(`G{ASS}`) |static |no
-
-|Can confirm absence of errors ? |finite statespace |finite statespace
-|invariant strong enough |bound on trace length
-|=======================================================================
diff --git a/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc b/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc
deleted file mode 100644
index 8ad9ad95b577e4e63a5417e746c517fc9cc9aa11..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc
+++ /dev/null
@@ -1,32 +0,0 @@
-
-[[refinement-checking]]
-= Refinement Checking
-
-ProB can be used for refinement checking
-of B, Z and CSP specifications. Below we first discuss refinement
-checking for B machines. There is a tutorial on checking CSP assertions
-in ProB which can be viewed
-http://stups.hhu.de/ProB/w/Checking_CSP_Assertions[here].
-
-[[what-kind-of-refinement-is-checked]]
-== What kind of refinement is checked?
-
-ProB checks trace refinement. In other words, it checks whether every
-trace (consisting of executed operations with their parameter values and
-return values) of a refinement machine can also be performed by the
-abstract specification.
-
-Hence, ProB does *not* check the gluing invariant. Also, PRE-conditions
-are treated as SELECT and PRE-conditions of the abstract machine are
-*not* always propagated down to the refinement machine. Hence,
-refinement checking has to be used with care for classical B machines,
-but it is well suited for EventB-style machines.
-
-[[how-does-it-work-refinement-checking]]
-== How does it work?
-
-1.  Open the abstract specification, explore its state space (e.g.,using
-an exhaustive temporal model check).
-2.  Use the command "Save state for later refinement check" in the _Verify_ menu.
-3.  Open the refinement machine.
-4.  You can now use the "Refinement Check..." command in the _Verify_ menu.
diff --git a/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc
deleted file mode 100644
index 909c09e0cbf5ccf1b361d16ff5dcdd73c14f6a69..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-
-:leveloffset: -1