diff --git a/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc b/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc
deleted file mode 100644
index 0afe68c34c6249ee55fded13f2eb38b61530b951..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc
+++ /dev/null
@@ -1,4 +0,0 @@
-
-[[tutorials]]
-= Tutorials
-:leveloffset: +1
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc
deleted file mode 100644
index d61c5ada65520f5c3908c3ef9c90d5533073fdb9..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc
+++ /dev/null
@@ -1,27 +0,0 @@
-
-[[tutorial-co-simulation]]
-= Tutorial Co-Simulation
-
-You can create Co-Simulations using FMI with ProB.
-
-[[overview-tutorial-co-simulation]]
-== Overview
-
-The ProB 2.0 Java API contains some classes for cosimulating discrete
-models specified in one of the formalisms that are supported by ProB,
-and continuous models that are implemented using the
-https://www.fmi-standard.org/[functional mockup interface (FMI)]. A so
-called functional mockup unit (FMU) can, for example, be created in C
-using the FMI SDK or exported from third party tools such as Dymola. The
-framework is built on top of
-http://ptolemy.eecs.berkeley.edu/java/jfmi/[JFMI] from the Ptolemy
-Project. In fact, we only added a thin wrapper on top of the JFMI
-library. The de.prob.cosimulation.FMU class can be used to load a .fmu
-file and to control the continuous part of the simulation.
-
-This tutorial will be created soon.
-
-In the meantime you can have a look at chapter 6 of the
-http://www.advance-ict.eu[Advance] deliverable
-http://www.advance-ict.eu/sites/www.advance-ict.eu/files/AdvanceD4.2-issue2.pdf[D4.2
-(Methods and tools for simulation and testing I)].
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc
deleted file mode 100644
index d0eac527f8efc02bfaa51d056cd2a1945702e7fe..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc
+++ /dev/null
@@ -1,69 +0,0 @@
-
-[[tutorial-debugging-well-definedness-and-transition-errors]]
-= Tutorial Debugging Well-Definedness and Transition Errors
-
-We assume that you have grasped the way that ProB setups up the initial
-states of a B machine as outlined in
-<<tutorial-setup-phases,Tutorial Setup Phases>>, and have understood
-why animation is difficult as outlined in
-<<tutorial-understanding-the-complexity-of-b-animation,Tutorial
-Understanding the Complexity of B Animation>>. You may also want to have
-a look at the explanation of
-<<well-definedness-checking,well-definedness in B>>.
-
-== A simple example
-
-Let us use the following B machine as starting point:
-
-....
-MACHINE WhileLoopInvariantError
-VARIABLES xx
-INVARIANT
- xx:NATURAL
-INITIALISATION xx:=1
-OPERATIONS
-  Set(c) = PRE c:1..10 & xx<=c THEN
-    WHILE xx < c DO xx := xx+1
-    INVARIANT
-      xx <= c & xx:NATURAL &
-      xx<10 /* this is wrong */
-    VARIANT c-xx
-    END
-  END;
-  r <-- Get = BEGIN r:= xx END
-END
-....
-
-After loading and initialising the machine you see that ProB has found a
-so-called "transition error", i.e., an error that occured while
-computing enabled operations (which correspond to a transition from one
-state to the B machine to another). These errors are displayed in red in
-the State Properties pane:
-
-image::ProB_WhileAfterLoad.png[]
-
-When you click on the red transition error you get presented with more
-details about the error:
-
-image::ProB_WhileAfterErrClick.png[]
-
-Sometimes you can also have the possibility to click on a "Visualise"
-button, which in this case will give you a graphical visualisation of
-the invariant violation:
-
-image::ProB_While_INV_Violation.png[]
-
-The same technique applies for inspecting other transition errors, such
-as:
-
-* <<well-definedness-checking,well-definedness errors>> of
-expressions such as:
-** arithmetic well-definedness errors (division by 0, modulo by 0,
-modulo for negative numbers, min or max of empty set)
-** functional well-definedness errors (function applied outside of
-domain or applied to relation,...)
-** sequence well-definedness errors (first, last, tail, front of empt
-sequence,...)
-* PRE condition errors (not for outermost preconditions, which are
-treated specially)
-* ASSERT condition violations
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc
deleted file mode 100644
index d1b8448df452ae2caa2443f3a0b4ea959ae0fc4e..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc
+++ /dev/null
@@ -1,389 +0,0 @@
-
-[[tutorial-enabling-analysis]]
-= Tutorial Enabling Analysis
-
-The B-method and in particular its successor Event-B are methodologies
-for formal development and verification of systems. In Event-B, a
-machine is usually viewed as a reactive system executing continuously
-enabled (atomic) events in an interleaved fashion. Thus, parallel events
-of the system are easily modeled as an interleaving of operation
-executions. On the other hand, the introduction of abstract counters is
-required when events are supposed to be executed in some (sequential)
-order. This, however, can in some cases slow the work of understanding
-and verifying a model since identifying the sequential ordering of
-events in an Event-B model is not that obvious. Thus, using methods for
-determining the control flow can be sometimes very beneficial for
-understanding the model, as well as for techniques for automatic
-verification such as model checking.
-
-In this tutorial we present a static analysis for B and Event-B that can
-be used to reveal the control flow of a machine and to optimize model
-checking of models written in B and Event-B (see also
-https://www3.hhu.de/stups/prob/index.php/Tutorial_Various_Optimizations#Partial_Guard_Evaluation[Tutorial
-on Partial Guard Evaluation]). The results of the analysis, designated
-also as "enabling analysis", can be presented as relations by means of
-a table or by means of a graph. For simplicity, we will concentrate
-mainly on B and use the terminology of the formalism.
-
-[[enabling-relations]]
-== Enabling Relations
-
-What we want to find out is how the operations influence each other
-within a B model. In other words, for each pair (op1, op2) of operations
-we try to determine as precise as possible how op1 can affect the guard
-condition of op2 with regard to enabledness. To determine the enabling
-relations between operations we use syntactic analyses, as well as the
-constraint-based abilities of ProB.
-
-Consider the following B machine:
-
-....
-MACHINE Example
-VARIABLES x, y, z
-INVARIANT
-    x:NATURAL
-  & y:INTEGER
-  & z:INTEGER
-INITIALISATION
-  x:=6 || y:=-2 || z:=0
-OPERATIONS
-  Op1 = PRE x + y>=4  THEN x:=x+2 || y:=2 END;
-  Op2 = PRE x mod 2=1 THEN x:=x+1 || y:=2 END;
-  Op3 = PRE x mod 2=0 THEN x:=x+2 END;
-  Op4 = PRE x<0 THEN y:=y-1 END;
-  Op5 = PRE y/=2 THEN z:=3 END
-END
-....
-
-The machine has three variables x,y,z, where x ranges over the domain of
-natural numbers and y and z over the domain of all integers. For this
-machine we have 25 pairs of operations for which we want to determine
-the respective enabling relations. Additionally, we identify 5 further
-pairs that show the influence of the INITIALISATION on the guard
-conditions of all other operations. Consider, for example, the pair
-(Op2,Op1) in `Example.mch`. Clearly, Op1 is enabled in each state of
-`Example.mch` where the predicate ‘x+y>=4’ is fulfilled. Since the
-effect of Op2 assigns 2 to y and increments x by one upon condition that
-x is a positive odd number in the before-state of Op2, we can assume
-that Op1 is always enabled after the execution of Op2. In other words,
-in all after-states of Op2 the operation Op1 is guaranteed to be
-enabled. This relation between Op2 and Op1 we can illustrate as follows:
-
-image::GuaranteedRelationEn.png[]
-
-In the figure above the green boxes denote that the evaluation of the
-guard of Op1 is true, whereas the red boxes denote that the evaluation
-of the guard of Op1 is false.
-
-Another pair of interest is (Op2,Op5) in `Example.mch`. Clearly, Op5 is
-enabled only in those states in which y is not equal to 2. Obviously, in
-each after-state of Op2 y is equal to 2 and thus we can conclude that
-Op5 is impossible to be enabled after each execution of Op2. Such a
-relation between two operations we denote as "impossible" and can be
-illustrated as follows:
-
-image::ImpossibleRelationEn.png[]
-
-Both arrows in the illustration of the "impossible" relation indicate
-that whether the guard condition of Op5 is fulfilled or not in a
-before-state of Op2 operation Op5 will be disabled in the respective
-after-state of Op2. In order to recognize a tuple (op1,op2) as
-"impossible" we require that op2 is always disabled after op1 without
-further considering whether op2 is always enabled or always disabled in
-the before-states of op1.
-
-Consider, for instance, the pair (Op2, Op2) in the machine above. We can
-easily conclude that Op2 becomes disabled after it is executed and
-clearly, the second case (\false -> \false) of the impossible relation
-is not possible for (Op2, Op2). This gives rise of introducing another
-(more precise) impossible relation:
-
-image::ImpossibleDisableRelation.png[]
-
-Accordingly, we can derive another relation from "impossible" for
-which only the second case of the "impossible" relation is fulfilled:
-
-image::ImpossibleKeepRelation.png[]
-
-As an example for a pair of operations that fulfills the
-"impossible_keep" requirement you can take, for example, the pair
-(Op3,Op2) from `Example.mch`. Since Op2 and Op3 cannot be both enabled
-in a state and the execution of Op3 cannot enable Op2, then we can
-easily conclude that Op2 remains always disabled after Op3.
-
-Similarly as for "impossible", one could derive two further enabling
-relations from "guaranteed":
-
-image::GuaranteedEnableKeepRelation.png[]
-
-Another interesting class of enabling relations that could be helpful
-for better understanding and analyzing B and Event-B models is that of
-the "keep" relations. We say that an operation op1 "keeps" another
-operation op2 if op1 cannot change the status of the enabling condition
-of op2, i.e. op1 keeps op2 enabled respectively disabled. This
-relationship could be illustrated as follows:
-
-image::KeepRelation.png[]
-
-We can take (Op1,Op2) and (Op1,Op3) as examples of pairs in
-`Example.mch` that are elements of the keep relation. "keep" relations
-can sometimes be easily determined by analyzing just the syntactic
-structure of both operations, or more precisely the “read” and “write”
-sets of both operations.footnote:[For an operation op the set read(op)
-denotes the set of variables that are read by op. Accordingly, by
-write(op) we denote the set of variables that are written by op.] If,
-for example, an operation op1 does not write any variable of the machine
-that is read in the guard condition of op2, then we can infer that op1
-"keeps" op2. In that case we also say that op1 does not change op2
-syntactically. In the class of the "keep" relations are included also
-relations such as independence. Two operations op1 and op2 are called
-independent if each of them cannot disable the other operation and the
-both orders of execution and have the same effect.footnote:[See the
-https://www3.hhu.de/stups/prob/index.php/Tutorial_Various_Optimizations#Partial_Order_Reduction[Tutorial
-on Partial Order Reduction] for more information on independence between
-operations.]
-
-All three classes ("guaranteed", "impossible" and "keep") of
-enabling relations presented so far represent definite relations. That
-is, if a pair of operations (op1,op2) is confirmed to be a relation of
-one of this three classes, then we can certainly say what effect on the
-enabling condition of op2 would the execution of op1 have. However, for
-some pairs of operations we cannot certainly say what effect an
-operation would have on the enabling condition of another operation.
-This is due to the fact that the enabling status of an operation does
-not only depend on the effect of the executed operations, but also on
-the current variables’ evaluation. Take, for instance, the tuple
-(Op3,Op1) from the B machine above. Considering the action part of Op3
-and the guard condition of Op1 we can assume that Op3 can enable Op1.
-Since the guard of Op1 depends not only on the current value of x, but
-also on y, there could be transitions s -> s' of Op3 in the state space
-of the machine where Op1 is disabled in both states s and s’. Though,
-what we could definitely say is that Op3 cannot disable Op1. This
-relationship we can illustrate as follows:
-
-image::PossibleEnableRelation.png[]
-
-The opposite relation of “possible_enable” is the relation where an
-operation op2 can disable another operation op1. Formally, we say that
-op2 can disable op1 if op2 may disable op1 and op2 cannot enable op1.
-This relationship is denoted as “possible_disable” and can be
-illustrated as follows:
-
-image::PossibleDisableRelation.png[]
-
-In order to determine how operations influence each other we need to
-assure first that these are feasible. An operation "op" is said to be
-feasible if there is a state of the machine that satisfies the invariant
-of the machine and in which "op" is enabled. In the B machine above
-the operation Op4, for example, is not feasible. Obviously, Op4 is
-enabled only in states where x is a negative number and states in which
-x is a negative number are visibly not consistent with the invariant
-since "x : NATURAL". Such incompatibilities are sometimes of great
-importance for the modeler and therefore they should be revealed in the
-process of computing the enabling relations. In our case for each pair
-of operations (Op4,-) and (-,Op4) the status “infeasible” will be
-returned.
-
-We can now list all possible enabling relations for the machine
-`Example.mch` by means of a table. For each entry in the table the
-operation in the row is the operation whose effect is studied on the
-status of the guard of the operation in the column.
-
-image::EnablingResults.png[]
-
-Rather than showing the enabling information for each pair of operations
-of the machine, one can display the enabling relations by means of a
-graph. The graph contains the operations as nodes and the above enabling
-relations as edges between the nodes, with the exception that relations
-marked as impossible, independent or infeasible are not shown in the
-graph. We denote such graphs as enable graphs. The enable graph of
-`Example.mch` looks as follows.
-
-image::EnableGraph_Example.png[]
-
-From the enable graph one can recognize the control flow of the model
-and deduce some properties. For example, we can clearly see that `Op4`
-cannot occur after the execution of another operation.
-
-[[summary-of-the-enabling-relations]]
-== Summary of the Enabling Relations
-
-In the following, we summarize most of the enabling relations that we
-think can provide a useful feedback to the user. For each of the
-enabling relations we have given an appropriate example. In the examples
-below we compute the effect of executing ‘op1’ on the status of the
-guard of ‘op2’. The relation identifiers are the same as they appear as
-results in ProB.
-
-* _guaranteed_: op2 guaranteed to be executable after op1.
-
-image::GuaranteedExample.png[]
-
-* _guaranteed_enable_: op2 is guaranteed to become enabled after op1.
-
-image::GuaranteedEnableExample.png[]
-
-* _guaranteed_keep_: op2 is guaranteed to stay enabled after op1.
-
-image::GuaranteedKeepExample.png[]
-
-* _impossible_: op2 is impossible to be executed after op1.
-
-image::ImpossibleExample.png[]
-
-* _impossible_disable_: op2 is guaranteed to become disabled after op1.
-
-image::ImpossibleDisableExample.png[]
-
-* _impossible_keep_: op2 is impossible to become enabled after op1.
-
-image::ImpossibleKeepExample.png[]
-
-* _keep_: op2 always stays enabled resp. disabled after op1.
-
-image::KeepExample.png[]
-
-* _syntactic_unchanged_: op1 does not write any variable read in the
-guard of op2, i.e. write(op1) /\ read(op2) = \{}
-
-image::SyntacticUnchangedExample.png[]
-
-* _syntactic_independent_: op1 and op2 are syntactically independent,
-i.e. read(op1) /\ write(op2) = \{} & write(op1) /\ read(op2) = \{} &
-write(op1) /\ write(op2) = \{}
-
-image::SyntacticIndependentExample.png[]
-
-* _syntactically_fully_independent_: op1 and op2 are syntactically
-independent and additionally, read(op1) /\ read(op2) = \{}
-
-image::SyntacticFullyIndependentExample.png[]
-
-* _possible_enable_: op2 possible after op1, but op2 cannot be disabled
-by op1.
-
-image::PossibleEnableExample.png[]
-
-* _possible_disable_: op2 possible after op1, but op2 cannot be enabled
-by op1.
-
-image::PossibleDisableExample.png[]
-
-* _infeasible_: op1 is not feasible and thus cannot influence op2.
-
-image::InfeasibleExample.png[]
-
-[[performing-enabling-analysis-within-prob]]
-== Performing Enabling Analysis within ProB
-
-The enabling analysis has been implemented in the ProB toolset. The
-computation of the enabling relations is based on syntactic and
-constraint-based techniques. The identification of relations such as
-"syntactic_independent" and "syntactic_unchanged" requires just a
-thorough study of the syntactic structure of the operations, i.e. no
-calls to the constraint solver have to be made. However, to confirm, for
-example, that an operation is guaranteed or impossible to be executed
-after another operation the use of the ProB’s constraint solver is
-unavoidable. For instance, consider the pair (Op2,Op1) from
-`Example.mch`. As we have seen, in `Example.mch` the operation Op1 is
-guaranteed to be enabled after each execution of Op2. In ProB this could
-be computed by feeding the (before-after) predicate “ (x mod 2 = 1) &
-(x'=x+1 & y=2) & (x'+y'<4)” into the constraint solver. As a result, the
-constraint solver will not find a solution for the predicate, i.e. the
-constraint solver will not find a state "s" satisfying “x mod 2 = 1”
-from which after executing Op2 at "s" a solution state s’ will be
-found that fulfills “x+y<4”; note that “x+y<4” is the negation of the
-guard of Op1. Since there is no after-state of Op2 at which Op1 is
-disabled we can conclude that Op1 is guaranteed to be executed after
-Op2. When constraints are getting more complex the constraint solver may
-need more time for solving. Thus, the computation of the enabling
-relations may become a very time-expensive task. Therefore, a time-out
-for each constraint solver call is set. In other words, if the
-constraint solver does not find a solution in the given time by the
-user, then the respective relation will be denoted as time-outed. By
-default, in ProB the time-out for each constraint solver call is set to
-300 ms.
-
-Within `ProB Tcl/Tk` you can find the menu "Enabling Analysis" in the
-"Analysis" menu of the menu bar.
-
-image::EnablingAnalysisMenu.png[]
-
-The "Enabling Analysis" menu provides multiple commands:
-
-* "Enabling Analysis (Table)": this command performs a (fast) enabling
-analysis on the respective B model using a time-out of 300 ms for the
-constraint-solver calls. The result of the enabling analysis is shown in
-a table. The table lists all enabling relations between the operations
-of the loaded B model. These can be exported to a CSV file. The table
-for `Example.mch` at the end of the _' Enabling Relations_' section was
-constructed this way.
-* "Enabling Analysis (Precise, Table)": this command performs an
-enabling analysis using a time-out of 2800 ms for each of the
-constraint-solver calls. As for the command above, the result of the
-analysis is shown in a table that can be exported to a CSV file.
-* "Enabling Relations After...": this command computes all the
-enabling relations involving an operation chosen by the user.
-* "Enabling Analysis (Graph)": this command performs the fast enabling
-analysis but displays the results as a graph. In case the preference
-"DOT_SHOW_OP_READ_WRITES" is set for each operation the read/write
-information is displayed.
-* "Enabling Analysis (POR)...": this menu provides further commands
-for another form of enabling analysis the results of which are used for
-the partial guard evaluation optimisation in ProB.
-* "Read/Write Matrix (Table)": this command performs syntactic
-analysis on the model. The analysis determines the read and write sets
-for each operation of the machine.
-* "Dependence Analysis (Table)": this command performs a dependency
-analysis for each pair of operations. More specifically, the analysis
-determines which operations are dependent or independent to each other.
-
-With the command line version of ProB (probcli) one can perform an
-enabling analysis on a B or Event-B model by means of the
-`-enabling_analysis` option. The results of the analysis, as well as
-intermediate data and some statistics are printed out on the console:
-
-----
-$ probcli Example.mch -enabling_analysis
-CHECKING ENABLING AFTER INITIALISATION
-INITIALISATION ---> Op1  :: ok : guaranteed
-INITIALISATION ---> Op2  :: impossible
-INITIALISATION ---> Op3  :: ok : guaranteed
-INITIALISATION ---> Op4  :: impossible
-INITIALISATION ---> Op5  :: ok : guaranteed
-.....
-CHECKING ENABLING AFTER: Op5 r:[y] / w:[z]
-Op5 ---> Op1  :: Enable=syntactic_independent
-Op5 ---> Op2  :: Enable=syntactic_unchanged
-Op5 ---> Op3  :: Enable=syntactic_fully_independent
-Op5 ---> Op4  :: Enable=syntactic_unchanged
-Op5 ---> Op5  :: Enable=syntactic_unchanged
-% Finished CBC Enabling Analysis 810 ms walltime (770 ms runtime), since start: 1650 ms
-% CBC Enabling Stats:
-% Nr of events: 5
-% Nr of cbc calls: 30, Timeout results: 2
-Origin,Op1,Op2,Op3,Op4,Op5
-INITIALISATION,guaranteed,impossible,guaranteed,impossible,guaranteed
-Op1,timeout_possible_disable,keep,keep,impossible_keep,syntactic_independent
-Op2,guaranteed,impossible,guaranteed,impossible_keep,impossible
-Op3,timeout_possible,impossible_keep,guaranteed,impossible_keep,syntactic_fully_independent
-Op4,impossible_keep,syntactic_unchanged,syntactic_unchanged,syntactic_keep,impossible_keep
-Op5,syntactic_independent,syntactic_unchanged,syntactic_fully_independent,syntactic_unchanged,syntactic_unchanged
-----
-
-To perform enabling analysis from the command line and save the results
-into a CSV-file use the following commando:
-
-....
-$ probcli file.mch -enabling_analysis_csv FILE
-....
-
-where FILE is the name of the CSV-file in which the results of the
-analysis are stored.
-
-Related to this command is the feasibility analysis, which just checks
-whether a single event is in principle possible (given the invariant):
-
-....
-$ probcli file.mch -feasibility_analysis_csv FILE
-....
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc
deleted file mode 100644
index 850415e07abe926d70fe39407db73f27d69ad317..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc
+++ /dev/null
@@ -1,274 +0,0 @@
-
-[[tutorial-ltl-counter-example-view]]
-= Tutorial LTL Counter-example View
-
-In this tutorial a quick overview will be given describing the LTL
-counter-example visualization plug-in in Rodin. The functionality of the
-plug-in will be presented by means of an Event-B model on which
-different properties will be checked that are not satisfied by the
-model.
-
-[[ltl-model-checking-and-the-meaning-of-counter-examples]]
-== LTL Model Checking and the Meaning of Counter-examples
-
-Model checking is a technique for checking in an automatic way whether a
-model satisfies a property expressed in formal logic. LTL (standing for
-linear temporal logic) is a version of the temporal logic used mainly
-for encoding time-dependent properties of systems.
-
-Verifying whether a system fulfills an LTL property by means of model
-checking is realized by searching a path in the state space of the
-system that violates the property being checked. That is, if the system
-behaves in a way violating the LTL property being checked, then the
-erroneous behavior will be reported by returning a path (mostly
-infinite) representing the false behavior. Otherwise, if no
-counter-example was found, it will be considered that the system
-satisfies the LTL property.
-
-The LTL model checker of ProB provides three types of counter-examples:
-
-* Finite path leading to a deadlock state (see Figure 1):
-
-image::Deadlock_path.png[]
-
-* Infinite path (see Figure 2), the infinite path in this case is
-represented by means of a loop:
-
-image::LTLViewInfinitePath.png[]
-
-* Finite path (see Figure 3). (In this case an infinite path
-representing the respective counter-example has been shortened in order
-to attract the attention to the relevant part of the counter-example).
-
-image::LTLViewFinitePath.png[]
-
-Intuitively, the first two types of counter-examples (Figure 1 and
-Figure 2) constitute a violation of a liveness footnote:[The first type
-of a counter-example (Figure 1) can in some cases be a valid
-counter-example for safety properties. For example, if the model cannot
-perform any actions, then a path possessing only single deadlock state
-is a counter-example for each LTL formula latexmath:[$X^{n} (true)$],
-with latexmath:[$n\geq 1$].] property, whereas the path in Figure 3
-represents usually a counter-example for a safety property.
-
-== Visualization of Counter-examples in Rodin
-
-*Coloring and highlighting nodes in a counter-example*
-Each state of a path in the LTL counter-example view is marked by a
-respective color that denotes the evaluation of an LTL formula at that
-state. There are three possible statuses (colors) that a state _s_ may
-have in respect to an LTL formula _f_:
-
-*  T : the value of _f_ is true at _s_
-*  F : the value of _f_ is false at _s_
-*  U : the value of _f_ cannot be determined at _s_ (unknown value)
-
-A state will be colored in grey if the value of the respective LTL
-formula cannot be determined. This may happen in case the
-counter-example is represented by finite path. For example, evaluating
-the LTL formula ‘X \{p2=crit2}’ on a path of length two where the value
-of _p2_ is not equal to _crit2_ in both states (see Figure 4) yields the
-following coloring of the states in Rodin: footnote:[The visualization
-refers to the LTL formula ‘XX \{p2=crit2}’. However, in this example we
-are interested in the coloring of the states in regard to the LTL
-formula ‘X \{p2=crit2}’.]
-
-image::LTLViewVisualisation1.png[]
-
-Since the value of the atom ‘\{p2=crit2}’ in latexmath:[$s_{1}$] is
-equal to false the value of the LTL formula ‘X \{p2=crit2}’ in
-latexmath:[$s_{0}$] is also equal to false. Therefore, the first state
-is colored in red. On the other hand, the value of the formula ‘X
-\{p2=crit2}’ in latexmath:[$s_{1}$] is unknown as there is no successor
-state of latexmath:[$s_{1}$] in the path, as shown in Figure 4.
-Accordingly, the second state in the LTL counter-example viewer will be
-colored in grey.
-
-image::LTLViewFinitePathUnknown.png[]
-
-States in the path considered to be significant for the evaluation of
-the respective LTL formula are highlighted by bright colors.
-Accordingly, the other states will be grayed out.
-
-Consider the path in Figure 5 that can be reported as a counter-example
-for the LTL formula ‘\{p1=noncrit1} U \{p1=crit1}’. footnote:[An LTL
-formula latexmath:[$\phi U \psi$] is satisfied by a path
-latexmath:[$\pi$] if there exists a state latexmath:[$s$] in
-latexmath:[$\pi$] fulfilling latexmath:[$\psi$] and latexmath:[$\phi$]
-holds at all states of latexmath:[$\pi$] until latexmath:[$s$] is
-reached.] As a consequence, the LTL counter-example view will display
-the following visualization of the counter-example:
-
-image::LTLViewVisualisation2.png[]
-
-The path in Figure 5 violates ‘\{p1=noncrit1} U \{p1=crit1}’ since the
-goal (‘\{p1=crit1}’) of the until-formula does not hold in all states of
-the path. This is illustrated by means of the bottom colored path in the
-picture above. Both states have been colored with bright red as both are
-significant for the violation of the until-formula in regard to
-‘\{p1=crit1}’.
-
-The upper path in the picture above has been evaluated and colored in
-regard to the condition (‘\{p1=noncrit1}’) of the until-formula. The
-critical state here is the second one as ‘\{p1=noncrit1}’ does not hold
-in that state and therefore it is highlighted by bright red. On the
-other hand, the atom ‘\{p1=noncrit1}’ holds in latexmath:[$s_{0}$] and
-thus the state is colored in green. latexmath:[$s_{0}$] has been grayed
-out since the evaluation of ‘\{p1=noncrit1}’ in that state has no
-significant meaning for the violation of ‘\{p1=noncrit1} U
-\{p1=crit1}’.
-
-image::LTLViewFinitePathUntil.png[]
-
-Notice, for a given LTL formula _f_ the values (or the colors) of the
-states are set in regard to the evaluation of the sub-formula/-s of _f_
-and highlighted with respect to the semantics of _f_. In case of the
-formula ‘\{p1=noncrit1} U \{p1=crit1}’ the states are colored in regard
-to the atoms ‘\{p1=noncrit1}’ and ‘\{p1=crit1}’ and highlighted in
-regard to the semantics of the until-operator.
-
-_' Obtaining transition and state information_'
-A path reported as a counter-example of an LTL formula represents a
-possible trace of the model being analyzed. In some cases it may be
-helpful to know which transitions are executed along the path in order
-to reproduce the erroneous behavior of the model (e.g. by animating the
-trace). To see which transitions are being executed in the
-counter-example hold the mouse cursor on the respective edge. A label
-will appear with the transition name:
-
-image::LTLViewVisualisation3.png[]
-
-Another way to find out the transitions of the path is to inspect the
-current trace loaded in the history view.
-
-To view a state of a counter-example shown in the LTL counter-example
-view perform a double-click action on the respective state. After
-double-clicking a state the relevant information (variables’ evaluation,
-invariant evaluation, etc.) of the state is displayed in the state view
-and the trace leading to the double-clicked state is loaded in the
-history view.
-
-*Number of visualizations per LTL formula*
-The counter-example reported by the LTL model checker will be visualized
-in regard to all operators used in the LTL formula. For example, three
-different visualizations will be illustrated for ‘G (\{p1=wait1} => F
-\{p1=crit1})’ as shown in the picture below. footnote:[There are five
-sub-formulas for ‘G (\{p1=wait1} => F \{p1=crit1})’: ‘G (\{p1=wait1} =>
-F \{p1=crit1})’, ‘\{p1=wait1} => F \{p1=crit1}’, ‘\{p1=wait1}’, ‘F
-\{p1=crit1}’, and ‘\{p1=crit1}’. However, the number of visualizations
-corresponds not to the number of sub-formulas, but to the number of the
-operators used in the LTL formula.]:
-
-image::LTLViewVisualisation4.png[]
-
-In order to view the visualizations of the sub-formulas, one should
-click on one of the states of the source-formula.
-
-== Use Case for the LTL Counter-example Viewer
-
-Consider an Event-B model formalizing an algorithm for mutual exclusion
-with semaphores for two concurrent processes latexmath:[$P_1$] and
-latexmath:[$P_2$]. Each process has been simplified to perform three
-types of events: request (for entering in the critical section), enter
-(entering the critical section), and release (exiting the critical
-section).
-
-image::LTLViewMUTEXEvents.png[]
-
-Each process latexmath:[$P_{i}$] has three possible states that are
-denoted by the constants latexmath:[$noncrit_{i}$] (the state in which
-latexmath:[$P_{i}$] performs noncritical actions),
-latexmath:[$wait_{i}$] (the state in which latexmath:[$P_{i}$] waits to
-enter the critical section), and latexmath:[$crit_{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.
-
-There are several requirements that the mutual exclusion algorithm
-should satisfy. The most important one is the mutual exclusion property
-that says _always at most one process is in its critical section_. This
-can be simply expressed, for example, as an invariant of the respective
-Event-B model: ‘not(p1 = crit1 & p2 = crit2)’. However, there are other
-properties that can be easily expressed by means of LTL formulas and
-automatically checked on the model. For example, the requirement _each
-process will enter infinitely often its critical section_ can be
-specified by the LTL formula `GF \{p1 = crit1} & GF \{p2 = crit2}` and
-the starvation freedom property that states _each waiting process will
-eventually enter its critical section_ can be encoded in LTL by means of
-the formula `G (\{p1 = wait1} => F \{p1 = crit1}) & G (\{p2 = wait2} =>
-F \{p2=crit2}) `.
-
-The second requirement _each process will enter infinitely often its
-critical section_ can be divided in two single requirements:
-
-1.  Process 1 will enter infinitely often its critical section (‘GF
-\{p1=crit1}’)
-2.  Process 2 will enter infinitely often its critical section (‘GF
-\{p2=crit2}’)
-
-Running the LTL model checker of ProB with the LTL formula ‘GF
-\{p1=crit1}’ on the MUTEX model will provide the following path as a
-counter-example, where the equations in the set braces represent the
-current variables’ evaluation in the respective state and the labels
-above the edges the executed events in the path:
-
-image::LTLViewCEForGF1.png[]
-
-Obviously the property ‘GF \{p1=crit1}’ is violated for the path in
-Figure 6 since it constitutes an infinite path where no state exists in
-which _p1_ is equal to _crit1_. The counter-example for ‘GF \{p1=crit1}’
-will be then visualized as follows:
-
-image::LTLViewVisualisation5.png[]
-
-Each state of the counter-example is colored in red since ‘F
-\{p1=crit1}’ does not hold for all states of the path. Additionally,
-state latexmath:[$s_{0}$] has been highlighted since *all* paths
-starting in latexmath:[$s_{0}$] do not satisfy ‘F \{p1=crit1}’ (the
-semantic of the globally-operator).
-
-To see why the LTL formula ‘F \{p1=crit1}’ does not hold in each state
-of the path in Figure 6 click on one of the nodes in the visualization.
-As a result, a second box will appear visualizing the counter-example in
-regard to the LTL formula ‘F \{p1=crit1}’. In the second visualization
-all states are colored in red since ‘p1=crit1’ does not hold in all
-states. All states are highlighted as well since ‘F \{p1=crit1}’ holds
-if and only if there is a state in which _p1_ is equal to _crit1_ and
-thus all states are significant for the violation of the formula.
-
-image::LTLViewVisualisation6.png[]
-
-For the starvation freedom property (_each waiting process will
-eventually enter its critical section_) of process P1 three operators
-are needed for encoding it in LTL: ‘G (\{p1=wait1} => F \{p1=crit1})’.
-The mutual exclusion model violates the property because it permits the
-second process P2 to perform infinitely often consecutively the events
-Req2, Enter2, Rel2 and thus not allowing process P1 to get access to its
-critical section. This means that the path in Figure 6 may also be
-reported as a counter-example for ‘G (\{p1=wait1} => F \{p1=crit1})’ by
-the LTL model checker. As a consequence, the following visualization
-will be shown in the LTL counter-example view:
-
-image::LTLViewVisualisation4.png[]
-
-In this visualization the crucial state for violating the property ‘G
-(\{p1=wait1} => F \{p1=crit1})’ is latexmath:[$s_{1}$] since at this
-state ‘p1=wait1’ becomes true. Once a state is encountered where
-‘p1=wait1’ holds, it should be guaranteed that eventually ‘p1=crit1’
-will hold. This is apparently not fulfilled as in all successor states
-_p1_ will not become equal to _crit1_.
-
-== Literature Sources
-
-For more detailed information on visualizing counter-examples in the LTL
-counter-example view in Rodin refer to footnote:[Andriy Tolstoy,
-http://www.stups.uni-duesseldorf.de/mediawiki/images/1/10/Master_tolstoy.pdf[_Visualisierung
-von LTL-Gegenbeispielen_], Master Thesis.]. For a thorough introduction
-to LTL and LTL model checking consult footnote:[E. M. Clarke, Jr.,
-Grumberg, and D.A. Peled. _Model Checking_. MIT Press, Cambridge, MA,
-USA, 1999.] or footnote:[C. Baier and J.-P. Katoen. _Principles of Model
-Checking_. MIT Press, 2008.].
-
-The Event-B model used in this tutorial can be downloaded from
-http://www.stups.uni-duesseldorf.de/~dobrikov/modelchecking/MUTEX.zip[here].
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_ProB_Java_API.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_ProB_Java_API.adoc
deleted file mode 100644
index ef3480a01b148f0b55988f026f50499f30719e2f..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_ProB_Java_API.adoc
+++ /dev/null
@@ -1,343 +0,0 @@
-
-[[prob-java-api-tutorial]]
-= ProB Java API Tutorial
-
-ProB 2.0 is currently experimental. This means that the implementation
-may change during the course of development. However, we have reached
-the point in development where some of the features have reached a
-certain level of stability. Therefore, we are writing this tutorial to
-explain what those features are.
-
-[[how-to-get-started-developing-with-prob-2.0]]
-== How to get started developing with ProB 2.0
-
-The source code for ProB 2.0 is available via GitHub. Click
-https://github.com/bendisposto/prob2[here] to view the prob2 repository.
-There is also a short guide available there which will help getting
-Eclipse set up so that you can get started with the development. Our
-bugtracker is available
-http://jira.cobra.cs.uni-duesseldorf.de/browse/PROBCORE[here]. There you
-can view the features that we are currently working on and can submit
-new feature requests.
-
-[[how-to-open-the-groovy-shell]]
-== How to open the Groovy Shell
-
-The ProB Groovy shell is available in the Eclipse application. To open
-it, select
-
-`Window > Show View > Other..`
-
-Then select
-
-`ProB > Groovy Console`
-
-and hit `ok`.
-
-[[open-the-prob-api-from-sourcejar-file]]
-== Open the ProB API from Source/JAR file
-
-In order to access the console from source or from a JAR file, start the
-application with the parameters -s (short for --shell) and -local (which
-specifies that you are running the application from a local computer).
-This will start a web server at a given port (the default is 8080, but
-it increments the port number if a port is already active). The shell
-can then be accessed at the following address:
-
-localhost:PORTNR/sessions/GroovyConsoleSession
-
-[[how-to-load-a-model]]
-== How to load a model
-
-[[java-api-classical-b]]
-=== Classical B
-
-You can load a Classical B model into the groovy console using the `api`
-variable that is available. There is a method `b_load` that is available
-to load Classical B models. For example:
-
-`m = api.b_load("/home/pathToFile/example.mch")`
-
-will load example.mch into the variable `m`.
-
-[[java-api-event-b]]
-=== Event B
-
-To load an Event B model into ProB, right click on the model and select
-
-`Start Animation / Model Checking`
-
-from the context menu that drops down.
-
-You can also load Event B models into the API via the eventb_load
-command in the Api object. The eventb_load command accepts .bcm and .bcc
-files.
-
-[[how-to-animate-models]]
-== How to animate models
-
-The Trace abstraction is available to carry out animations.
-
-[[in-the-console]]
-=== In The Console
-
-There are several different ways that a new transition can be added to
-the current trace. The most important thing to remember is that each
-Trace object is completely immutable. This means that when you change a
-trace, you are actually getting a new Trace back. This means that when
-you carry out an animation step, you always have to make sure that you
-save the Trace object that is returned.
-
-The simplest way to add a transition is to specify it with the name of
-the event to be executed and predicates to specify how the parameters
-for the event are to be allocated. Specifying no predicate will assume a
-predicate of "TRUE=TRUE" for the given event.
-
-`t = t.execute("new","pp=PID1")`
-
-If executing the event in a groovy environment (console or script), the
-event will be recognized as a method on the Trace class. This means that
-you can execute the event "new" as follows:
-
-`t = t.new("pp=PID1") `
-
-If you know the id that has been allocated by the ProB kernel to a given
-transition, this can be added via the "add" method. This will search
-the outgoing transitions from the current state and attempts to find one
-with a matching id. For instance, if operation 0 is among the enabled
-operations for the current state, then
-
-`t = t.add(0)`
-
-will add operation 0 to the current trace, create a new trace, and
-return it.
-
-If you know the name and parameters combination for a specific
-transition, you can also add operations via operation name and a list of
-the parameters. For instance
-
-`t = t.addTransitionWith("new",["PID3"])`
-
-will add the transition new(PID3) to the trace.
-
-It is also possible to execute any event by executing
-
-`t = t.anyEvent()`
-
-and it is also possible to execute any event with name "name". For
-instance,
-
-`t = t.anyEvent("name")`
-
-will execute any event with the name "name".
-
-It also possible to move backwards and forwards within a trace.
-
-Move backwards:
-
-`t = t.back()`
-
-Move forwards:
-
-`t = t.forward()`
-
-[[in-the-ui]]
-=== In The UI
-
-In order to animate a loaded model in the UI, double-click on an enabled
-event in the `Events` view. Then, the resulting trace will automatically
-be loaded into the different views and it can be further animated. To
-move backwards and forwards in the trace, use the buttons in the upper
-right hand corner of the `Events` view.
-
-[[how-to-switch-from-ui-to-groovy-console]]
-== How to switch from UI to groovy console
-
-There is an easy way to switch from the UI to the groovy console and
-back. It all happens using the "animations" global variable in the
-groovy console. What is important to remember, is that in this case,
-there is no distinction between an animation and a trace.
-
-[[from-ui-to-console]]
-=== From UI to Console
-
-In the UI, switch to the `Current Animations` view. Here you can view
-the different animations that are available. If the desired animation is
-not available, double click on it in this view and it will be set as the
-current animation. Now, to move this animation from the UI to the groovy
-console, simply type
-
-`x = animations.getCurrentTrace()`
-
-into the groovy console and the current animation will be loaded into
-the variable `x`.
-
-[[from-the-console-to-the-ui]]
-=== From the Console to the UI
-
-If you have a trace saved into variable `trace_0` in the groovy console,
-you can easily add it to the UI. Simply type
-
-`animations.addNewAnimation(trace_0)`
-
-into the groovy console and the trace will automatically be added to the
-list of current animations and all of the views will be updated.
-
-[[how-to-carry-out-evaluations]]
-== How to carry out evaluations
-
-It is very simple to evaluate strings in the groovy console. There is a
-build in eval method in both the Trace and the StateSpace. In the trace,
-you just need to specify a string and the parser that is needed to parse
-the string. The two parsers currently available are `ClassicalB` and
-`EventB`.For instance,
-
-`t.evalCurrent("x:NAT" as EventB) `
-
-will parse "x:NAT" using the Event B parser and then will evaluate it
-at the current state. The following code
-
-`t.evalCurrent("x:NAT" as ClassicalB)`
-
-will parse "x:NAT" using the Classical B parser and then will evaluate
-it at the current state.
-
-The Trace class can also attempt to identify the correct parser for the
-formula in question. This means that for an EventBModel the EventB
-parser will be used, and for a ClassicalBModel, the ClassicalB parser
-will be used. In this case, calling the evalCurrent method with a String
-parameter will parse the String formula with the parser associated with
-the current formalism being animated. In this case
-
-`t.eval("x:NAT")`.
-
-will identify which model type is being animated and choose the
-appropriate parser.
-
-It is also possible to evaluate formulas on the SpaceSpace level. For
-instance, if `space_0` is a StateSpace, you can evaluate a list of
-formulas by typing
-
-`space_0.eval(space_0[5],["x:NAT" as EventB,"y:NAT" as ClassicalB])`
-
-into the console. This will parse "x:NAT" with the Event B parser and
-"y:NAT" with the Classical B parser and then will evaluate them at the
-state with id 5. The parser is not implicit in the StateSpace, so it is
-important to specify it here. In order to evaluate a formula, you need
-to specify the StateId object that is associated with the desired id. To
-extract a StateId from a StateSpace, you can use the notation
-`space[ID]` where ID is either a String or an integer representing the
-StateId that you want to view.
-
-[[how-to-convert-between-the-main-abstractions]]
-== How to convert between the main abstractions
-
-There is a connection between all of the main abstractions. You can
-easily convert between them by using the `as` operator.
-
-To convert between a Model and a StateSpace, use:
-
-`eventb = statespace_0 as EventBModel` (if you are animating an Event B
-model)
-
-or
-
-`classicalb = statespace_0 as ClassicalBModel` (if you are animating
-ClassicalB).
-
-The reverse translation is just as easy:
-
-`space = model as StateSpace`
-
-will return the StateSpace associated with model.
-
-Conversion between a Trace and a StateSpace and between a Trace and
-Model are also simple. The following conversions are valid:
-
-`space = trace as StateSpace`
-
-`trace = StateSpace as Trace`
-
-`trace = model as Trace`
-
-`model = trace as EventBModel` or `model = trace as ClassicalBModel`
-
-The only thing to mention is that every time you convert from a
-StateSpace or Model to a Trace, a new trace from the root state is
-created.
-
-[[how-to-save-a-trace]]
-== How to save a trace
-
-ProB currently supports a mechanism to save a trace in a script so that
-the same trace can be recreated. We are currently working on some
-improvements to this mechanism, so expect it to change over the next
-period of time. Currently, it is possible to save a Trace as an XML
-trace by typing
-
-`TraceConverter.save(trace_0,"/pathToFile/fileName.xml")`
-
-into the console. This will create the XML file `fileName.xml`.
-
-If you want to load this trace back into the console, there are two
-options available. You can convert the XML file to a Groovy closure that
-will then take a Model object and return a Trace with all of the
-operations specified in the XML file. This can be triggered by calling
-the method
-
-`TraceConverter.xmlToGroovy("/pathToFile/fileName.xml","/pathToFile/groovyScript.groovy")`
-
-You can then run the produced Groovy script and execute the resulting
-closure to restore your Trace
-
-`run /pathToFile/groovyScript.groovy`
-
-A script `script_NUM` will be produced. Then enter
-
-`trace = script_NUM(modelForThisTrace)`
-
-into the console, where modelForThisTrace is the model for which the
-trace should be executed.
-
-Another option is to simply restore the Trace directly from the
-TraceConverter
-
-`trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")`
-
-[[how-to-run-a-groovy-script]]
-== How to run a groovy script
-
-You can use the build in `run` command to run a groovy script. Simply
-type
-
-`run new File(pathToScript/script.groovy)`
-
-into the console.
-
-[[how-to-animate-with-only-the-statespace-abstraction]]
-== How to animate with only the StateSpace abstraction
-
-It is also possible to carry out animations without using a trace
-object.
-
-To get the root vertex from StateSpace space_0, type:
-
-`st = space_0.root`
-
-from there, you can execute a chain of events. For instance,
-
-`st = st.anyEvent("new").anyEvent().new("pp=PID1").new()`
-
-So you can execute anyEvent with the method anyEvent(filter), where
-filter can be a String name, or a List of names. You can also execute an
-event with name "name", with the method name(predicate), where
-predicate is the predicate string intended to filter the solutions for
-the event. If there are no parameters, the predicate "TRUE = TRUE"
-will automatically be added.
-
-[[how-to-use-a-different-probcli-binary-for-prob2]]
-== How to use a different probcli binary for ProB2
-
-You need to start ProB2 or the respective Java application with:
-
-`-Dprob.home=PATHTOPROBCLIFOLDER`
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc
deleted file mode 100644
index 9bc968f557233dcd818b277332cd0ddee42912c2..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc
+++ /dev/null
@@ -1,166 +0,0 @@
-
-[[tutorial-troubleshooting-the-setup]]
-= Tutorial Troubleshooting the Setup
-
-We assume that you have grasped the way that ProB setups up the initial
-states of a B machine as outlined in
-<<tutorial-setup-phases,Tutorial Setup Phases>>.
-
-In this lesson, we examine what can go wrong in these phases and how one
-can find a solution. Indeed, setting up the constants and initial values
-of a machine is often the most difficult step for an animator.
-Unfortunately, it is also the very first step an animator has to
-perform.
-
-We will also learn to use the various predicate analysis features
-provided by ProB.
-
-[[simple-inconsistency-in-the-properties]]
-== Simple Inconsistency in the PROPERTIES
-
-First, open the machine "Jukebox.mch" which can be found in the
-SchneiderBook/Jukebox_Chapter13 subdirectory of the ProB Examples
-folder. The main ProB window should look more or less as follows:
-
-image::ProB_JukeboxAfterLoad.png[]
-
-Now edit the file, and type `& limit>99` after `PROPERTIES limit:NAT1`.
-Save the machine and reload it. Hint: there is a "Save and reopen"
-command in the _File_ menu for this action.
-
-ProB should now popup the following message:
-
-image::ProB_Jukebox_UnsatProp.png[]
-
-If you click "Yes" (or Ja), you will get the following window:
-
-image::ProB_Jukebox_DebugUnsatProp.png[]
-
-What ProB does is add conjuncts from the PROPERTIES (and CONSTRAINTS
-clause) one-by-one, until it can no longer find a solution. This can
-often give you an indication of what is wrong, and the source of the
-trouble (or inconsistency).
-
-An alternate means to figure out the source of the problem is ProB's
-graphical formula viewer. For this, choose the "Analyse
-Graphically/Properties" in the _Analyse_ menu:
-
-image::ProB_Jukebox_AnalyseGraphicallyCommand.png[]
-
-This will result in the following visualization:
-
-image::ProB_Jukebox_AnalyseGraphicallyUnsatProp.png[]
-
-This viewer uses another, more sophisticated algorithm to determine a
-maximal subset of the Properties which is satisfiable. In this case, it
-has determined `limit=1` to make `limit:NAT1` true (but which obviously
-does not make `limit>99` true.
-
-In any way, the problem here is that we have set MAXINT to 3, and hence
-`NAT1={1,2,3}`. To make our PROPERTIES satisfiable again, we could add
-for example
-
-....
-DEFINITIONS
- SET_PREF_MAXINT==255
-....
-
-to the machine and re-load it. As we can see, the problem is solved and
-we can proceed with animation of the machine:
-
-image::ProB_JukeboxAfterLoad2.png[]
-
-[[a-more-involved-inconsistency]]
-== A more involved inconsistency
-
-Let us add
-
-....
-& !x.(x<limit => x<99)
-....
-
-to the PROPERTIES of the machine and then save and reopen it. We again
-get the error message that ProB cannot find CONSTANTS which satisfy the
-PROPERTIES. If click on the "Yes" button to debug the PROPERTIES we
-get the following picture:
-
-image::ProB_Jukebox_DebugUnsatProp2.png[]
-
-We can see that ProB has found the solution `limit=100` for the first
-two properties and then got stuck. Using the graphical viewer results
-the following visualization:
-
-image::ProB_Jukebox_AnalyseGraphicallyUnsatProp2.png[]
-
-Here we can see that ProB has used another partial solution, namely
-`limit=1`, which also satisfies two properties (and fails to satisfy
-`limit>99`).
-
-If the feedback provided by ProB is not sufficient to locate the
-problem, one can try to comment out parts of the PROPERTIES by hand
-until they become satisfiable. One can also move them to the ASSERTIONS
-clause, which has the advantage that we can check them later. Let us
-move the last property into an assertion:
-
-....
-PROPERTIES        limit : NAT1 & limit>99
-ASSERTIONS        !x.(x<limit => x<99)
-....
-
-Now save and reopen the machine. This time the properties are
-satisfiable. After selecting SETUP_CONSTANTS(100) and
-INITIALISATION(\{}) we obtain the following picture:
-
-image::ProB_JukeboxAfterInit3.png[]
-
-We can now analyze the ASSERTIONS. For this, choose the "Analyse
-Graphically/Assertions" in the _Analyse_ menu:
-
-image::ProB_Jukebox_AnalyseGraphicallyUnsatAssertion3.png[]
-
-The graphical viewer gives us an instance where the universally
-quantified formula is false: `x=99`, which hopefully helps us in fixing
-the problem, e.g., writing `!x.(x<limit => x<=99)`.
-
-Note, that ProB also allows us to inspect custom predicates using the
-graphical viewer (without saving and reopening a machine). For this,
-choose the "Analyse Graphically/Custom Predicate..." in the
-_Analyse_ menu and enter `!x.(x<limit => x<=99)`:
-
-image::ProB_Jukebox_AnalyseGraphicallyCustomCommand.png[]
-
-After hitting OK we obtain:
-
-image::ProB_Jukebox_AnalyseGraphicallyCustom3.png[]
-
-As we can see, this predicate is true in that particular state of the
-machine. Note, there is also the option to use "Analyse
-Predicate/Custom Predicate...". This will result in a simpler
-(non-graphical) visualization. Use this if the graphical visualization
-is too large or takes too much time to compute. The custom predicate
-analysis commands have one disadvantage: the formula has to be typed
-into a single line inside the dialog box (and parse errors are not very
-user-friendly). The alternatives are entering the formula into the
-ASSERTIONS clause as above. One can also define a special GOAL predicate
-in the DEFINITIONS:
-
-....
-DEFINITIONS       GOAL == !x.(x<limit => x<99)
-....
-
-Then one can use "Analyse Predicate/GOAL" or "Analyse
-Graphically/GOAL". The GOAL predicate can also be used to guide the
-model checker.
-
-Finally, the "Analyse" commands can also be applied to the
-precondition and guards of operations. This is useful to find out why a
-particular operation is (maybe) unexpectedly disabled or enabled. For
-this, choose the "Analyse Graphically/Operation PRE..." in the
-_Analyse_ menu and select the "select" operation:
-
-image::ProB_Jukebox_AnalyseGraphicallyOperationPRE.png[]
-
-After hitting "Select" or typing return we obtain, which shows us why
-the operation is not enabled:
-
-image::ProB_Jukebox_AnalyseGraphicallyOperationPRE3.png[]
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc
deleted file mode 100644
index b5e4ac75a936ee753efc4d13b4cc9834d8c60a71..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc
+++ /dev/null
@@ -1,296 +0,0 @@
-
-[[tutorial-understanding-probs-constraint-solver]]
-= Tutorial Understanding ProB's Constraint Solver
-
-We assume that you have grasped the way that ProB setups up the initial
-states of a B machine as outlined in
-<<tutorial-setup-phases,Tutorial Setup Phases>>, and have understood
-why animation is difficult as outlined in
-<<tutorial-understanding-the-complexity-of-b-animation,Tutorial
-Understanding the Complexity of B Animation>>.
-
-First, it is important to understand that as of version 1.3, ProB uses
-three representations for sets and relations:
-
-* a classical list representation
-* a symbolic representation (using what is called a closure)
-* a representation using AVL-trees.
-
-The third representation allows ProB to deal with larger sets and
-relations (starting at around 100,000 elements performance will start to
-slow down). However, this representation can only be used if the
-constraint solver knows exactly *all* elements of a set or relation. The
-list representation will be used if only part of the set or relation is
-known. The symbolic representation can be used to represent certain sets
-(and set comprehensions) symbolically (such as large intervals, and to
-some very limited extent also infinite sets).
-
-To give an idea about the performance related to the new AVL-based
-representation, take the substitution:
-
-....
-numbers := numbers - ran(%n.(n:cur..limit/cur|cur*n))
-....
-
-* For limit=10,000, this takes 0.2 seconds (on a 2008 laptop); with the
-list representation this operation ran out of memory after 2 minutes in
-ProB 1.2.x.
-* For limit=100,000, this takes 2.1 seconds. (An encoding of this
-problem in Kodkod took 363 seconds on the same hardware.)
-* For limit=1,000,000 this takes about 21.9 seconds.
-
-For example, if the PROPERTIES contains the following predicates
-
-* x = \{1,2}
-* y = \{1|-2, 3|->4, 4|->5}
-* a = 1 & b=2 & d = \{a|-b}
-
-then all values will be fully known and the new AVL-based representation
-will be used. However, for
-
-* card(x) = 2 & dom(x) = \{1,2}
-
-we would only have partial information about x (which the constraint
-solver will encode using the list `[1|->_, 2|->_]` where the underscore
-marks as of yet unknown bits).
-
-Basically, the ProB constraint solver works as follows:
-
-* while interpreting the predicates, it will first try to "execute"
-predicates (or sub-predicates) which result in information which can be
-stored in AVL-form
-* after having interpreted the whole predicate, it will then perform
-deterministic propagation
-* only after all deterministic propagation has been performed, will the
-constraint solver start enumerating possibilities. For this it maintains
-a priority queue of enumerations and choice points.
-
-The priority is a rough estimate of the number of possible solutions;
-predicates with the lowest estimate will be "executed" first.
-
-The following picture provides a very rough picture of this process:
-
-image::ProB_Propagation.png[]
-
-== A simple example
-
-Let us use the following B machine as starting point:
-
-....
-MACHINE Propagation
-CONSTANTS low,up,f,fi,invert
-PROPERTIES
- f:low..up --> 0..1 &
- invert: 0..1 --> 0..1 &
- fi = (f ; invert) &
- invert = {0|->1,1|->0} &
- low = 0 & up = 3 &
- f = {0 |-> 1, 1|->1, 2|->0, 3|->1}
-VARIABLES xx
-INVARIANT
- xx:low..up
-INITIALISATION xx:=low
-OPERATIONS
-  val <-- Sense = BEGIN val := f(xx) END;
-  Inc = IF xx<up THEN xx := xx+1 ELSE xx := low END
-END
-....
-
-After loading the file, we get offered one possible way to setup the
-constants:
-
-image::ProB_PropagationAfterLoad.png[]
-
-In this case, ProB performed no enumeration at all. It could immediately
-determine the values of all constants. We can inspect the behaviour of
-the constraint solver by choosing "Advanced Preferences..." in the
-_Preferences_ menu and the turning the "Provide various tracing
-information on the terminal/console" on. If we now reopen the machine,
-the following information will be printed (amongst others) on the
-console:
-
-----
-...
-% checking_properties
-
- ====> low = 0
--->> low
-     val/1: int(0)
-
- ====> up = 3
--->> up
-     val/1: int(3)
-
- ====> invert = {0 |-> 1,1 |-> 0}
--->> invert
-     val/1: AVL.size=2
-
- ====> f = {0 |-> 1,1 |-> 1,2 |-> 0,3 |-> 1}
--->> f
-     val/1: AVL.size=4
-
- ====> f : low .. up --> 0 .. 1
-
- ====> invert : 0 .. 1 --> 0 .. 1
-
- ====> fi = f ; invert
--->> fi
-     val/1: AVL.size=4
-
--->> SUCCESS; all constants valued
-
-% start_enumerating_constants
-% grounding_wait_flags_for_constants(wfx(_57893,_66619,_56937))
-% found_enumeration_of_constants(10)
-...
-----
-
-The arrow `-->>` shows us when an AVL-representation was found for a
-constant. The `====>` tells us when a predicate is interpreted. You can
-also see that all constants have been valued *before* enumeration was
-started. You can also see that ProB does *not* treat the predicates in
-the same order as you have typed them in the PROPERTIES clause: indeed,
-ProB sorts the properties (e.g., moving equalities earlier) before
-starting the interpretation. As of version 1.3.2 the PROPERTIES are also
-partitioned, to improve performance and make it easier to locate
-inconsistencies.
-
-After selecting SETUP_CONSTANTS and INITIALISATION, we obtain the
-following state, and we can ensure ourselves that the values found for f
-and fi are correct (by looking at the "State Properties" pane):
-
-image::ProB_PropagationAfterInit.png[]
-
-[[complicating-the-example]]
-== Complicating the Example
-
-To make the example more challenging, let us increase `up` to 100 and
-remove the equality for `f`. In other words, the PROPERTIES will now
-look like this:
-
-....
- f:low..up --> 0..1 &
- invert: 0..1 --> 0..1 &
- fi = (f ; invert) &
- invert = {0|->1,1|->0} &
- low = 0 & up = 100
-....
-
-Saving and reopening the machine, results in the following picture:
-
-image::ProB_PropagationAfterLoad2.png[]
-
-You can see that ProB had no problem with this machine. Still, one may
-wonder why it only proposes four solutions for the constants. Indeed,
-there should be 2^101 = 2.54e+30 different solutions (over 2 thousand
-billion billion billion solutions). In fact, as quite often there are a
-lot of solutions for the constants, ProB (luckily) does not compute all
-of them. Indeed, there is a cut-off point after which it will no longer
-search for more solutions. In this case, the orange button "max"
-appears in the "Enabled Operatoins" pane. The cut-off itself is
-controlled by a preference. You can either
-
-* change the preference "Max Number of Initialisations Computed" in
-the "Animation Preferences", or
-* add a definition `SET_PREF_MAX_INITIALISATIONS == xxx`, where xxx is
-the maximum number of initialisations or possible ways to value the
-constants that ProB should compute.
-
-There is a similar preference to control how many solutions are found
-for ways to execute an operation (`SET_PREF_MAX_OPERATIONS`). (As a side
-note: these preferences can also be set to 0. This means that you will
-have to use "Execute an Operation..." in the _Animate_ menu to add
-transitions one by one.)
-
-One may wonder what happens if there are no solutions. Will not ProB
-have to examine all of these solutions? The answer is: sometimes yes.
-Let us add the predicate `f=fi` to the PROPERTIES, which are now
-unsatisfiable. If we save and reopen the machine, we get the following
-picture:
-
-image::ProB_PropagationAfterLoadMsg3.png[]
-
-If we answer yes, the Properties will be debugged by adding conjuncts
-one-by-one. We obtain the following:
-
-image::ProB_PropagationAfterLoadDebug3.png[]
-
-This will hopefully help us pinpoint the error in our properties. More
-recent versions of ProB also have a "Minimize" button in the lower
-left corner of the above dialog, in order to compute a minimal set of
-inconsistent properties. See
-<<tutorial-troubleshooting-the-setup,Tutorial Troubleshooting the
-Setup>> for more ways to locate problems in the properties. After
-clicking "Done", we get the following; observe the orange timeout
-button in the "State Properties" pane:
-
-image::ProB_PropagationAfterLoad3.png[]
-
-Note that one can click on the orange Timeout button: this will offer us
-the option to try to find solutions without a timeout. You should use
-this option with care: it can lock up your computer for a long time. You
-should be able to stop the computation by selecting ProB's terminal
-window and hitting CONTROL-C. Hopefully, the following message will
-appear in the terminal:
-
-....
-^CProlog interruption (h for help)?
-....
-
-You can now type A followed by RETURN. This will typically raise an
-error message which you can dismiss. Afterwards, you should be able to
-continue working.
-
-Finally, one can control the time after which a timeout will trigger
-using the preference "Time out for computing enabled transitions (in
-ms)"" in the "Animation Preferences". You can also control it using a
-definition for `SET_PREF_TIME_OUT` in the DEFINITIONS clause.
-
-[[adding-universally-quantified-formulas]]
-== Adding universally quantified formulas
-
-Let us replace `f=fi` by the following property:
-
-....
-!x.(x:low..up => f(x)=x mod 2)
-....
-
-If we save and reopen, we obtain the following picture:
-
-image::ProB_PropagationAfterLoad4.png[]
-
-ProB had no trouble finding a solution here. Indeed, it expanded the
-universally quantified formula before starting enumeration of `f`. Here
-it is important to understand that a universally quantified formula
-`!x.(P=>Q)` is expanded:
-
-* either when it can fully determine all solutions to `P`; this involves
-knowing exactly all open variables appearing in `P`
-* or when `P` is of the form `x:S` for some set S (the forall will be
-expanded for the known elements of S).
-
-Take for example,
-
-....
-!x.(x:dom(f) => f(x)=x mod 2)
-....
-
-Here the first case does not apply as `f` is not yet fully known.
-Luckily, the formula is in of the second form and ProB will still be
-able to quickly find the single solution.
-
-However, if we use
-
-....
-!x.(#y.(x|->y:f) => f(x)=x mod 2)
-....
-
-then none of the cases apply, and ProB will delay checking the formula
-until it knows `f`. As there are 2^101 possibilities, this will lead to
-a timeout.
-
-Finally, in the current version of ProB (1.3) it is better to use
-`!x.(x:low..up => f(x)=x mod 2)` rather than the seemingly equivalent
-`!x.(x>=low & x<=up => f(x)=x mod 2)`. The former version is currently
-more efficient especially for large values of MAXINT and MININT. (But we
-are planning to overcome this issue.)
diff --git a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc
deleted file mode 100644
index 14e1c5ee7d1aa449c94f0fad7252384a8975fb0a..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc
+++ /dev/null
@@ -1,73 +0,0 @@
-
-[[tutorial-unit-plugin-with-rodin]]
-= Tutorial Unit Plugin With Rodin
-
-This tutorial describes, how ProB's integrated plugin for unit analysis
-can be used with Event-B machines from inside the Rodin platform. This
-includes
-
-1.  Annotating variables with their physical unit,
-2.  Infer the unit of variables without an annotation,
-3.  Detect incorrect usage of units, like addition of differently
-annotated variables.
-
-Both the plugin itself and the bridge to Rodin are a work in progress.
-Preliminary support is available in the nightly builds of ProB for Rodin
-and will be merged in the regular releases in the future.
-
-We assume that you have a general understanding of Event-B and the usage
-of ProB / Rodin.
-
-[[installing-physical-units-support-for-prob-for-rodin]]
-== Installing Physical Units Support for ProB for Rodin
-
-You can follow the <<tutorial-rodin-first-step,First Steps
-Instructions>> or the
-<<installation-instruction-for-prob-rodin-plugin,Screencast>>
-to install ProB for Rodin.
-
-In addition to the "ProB for Rodin2" plugin there is a "ProB for
-Rodin2 - Physical Units Support" plugin at out Rodin update site. You
-have to install both to enable physical units support for Rodin.
-
-[[attaching-physical-units-to-variables-and-constants]]
-== Attaching Physical Units to Variables and Constants
-
-Once both plugins are installed, ProB allows to annotate both variables
-and constants with physical units:
-
-image::ProBRodinUnitPragmas.png[]
-
-We store the user supplied unit and the units inferred by ProB as a new
-attribute in the Rodin database.
-
-Units can be supplied in two forms:
-
-* by using an alias like "m", "cm", "mps" and so on,
-* or by using an Event-B Expression in an SI unit compatible form, like
-"10^2 * m^2".
-
-[[starting-the-analysis]]
-== Starting the Analysis
-
-The supplied units can now be used by ProB to infer missing units,
-verify the supplied units and detect unit errors. To start the analysis
-use the context menu of the machine / context you want to analyse:
-
-image::ProBRodinStartUnitAnalysis.png[]
-
-Necessary machines and contexts will be translated and passed to ProB.
-Once the analysis is finished, the "inferred unit" text fields are
-filled with the resulting units.
-
-[[possible-errors]]
-== Possible Errors
-
-Inside the Rodin Errors view, several errors might occur:
-
-* An invalid unit has been supplied. Please check your input to the
-corresponding "Physical Unit" attribute.
-* Multiple units have been inferred for a variable or constant.
-
-Furthermore, we output a warning if no unit could be inferred for a
-variable or constant.
diff --git a/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc b/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc
deleted file mode 100644
index 47b3e87fa988d762de4f62225f8c99efe8f56565..0000000000000000000000000000000000000000
--- a/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc
+++ /dev/null
@@ -1,3 +0,0 @@
-
-
-:leveloffset: -1