From 17169addf29dbe7d9ad817428b467293ac74f10f Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 4 Feb 2021 18:48:47 +0100
Subject: [PATCH] Remove Animation section whose content can be found on the
 wiki

---
 .../11_Animation/10_GeneralPresentation.adoc  |  69 -------
 .../user/11_Animation/12_Animation.adoc       | 157 ----------------
 .../13_Colours_of_enabled_operations.adoc     |  16 --
 .../Controlling_ProB_Preferences.adoc         |  61 -------
 .../11_Animation/Tutorial_Animation_Tips.adoc | 168 ------------------
 .../11_Animation/Tutorial_First_Step.adoc     | 114 ------------
 .../11_Animation/Tutorial_Setup_Phases.adoc   | 126 -------------
 ...tanding_the_Complexity_of_B_Animation.adoc | 151 ----------------
 8 files changed, 862 deletions(-)
 delete mode 100644 src/docs/chapter/user/11_Animation/10_GeneralPresentation.adoc
 delete mode 100644 src/docs/chapter/user/11_Animation/12_Animation.adoc
 delete mode 100644 src/docs/chapter/user/11_Animation/13_Colours_of_enabled_operations.adoc
 delete mode 100644 src/docs/chapter/user/11_Animation/Controlling_ProB_Preferences.adoc
 delete mode 100644 src/docs/chapter/user/11_Animation/Tutorial_Animation_Tips.adoc
 delete mode 100644 src/docs/chapter/user/11_Animation/Tutorial_First_Step.adoc
 delete mode 100644 src/docs/chapter/user/11_Animation/Tutorial_Setup_Phases.adoc
 delete mode 100644 src/docs/chapter/user/11_Animation/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc

diff --git a/src/docs/chapter/user/11_Animation/10_GeneralPresentation.adoc b/src/docs/chapter/user/11_Animation/10_GeneralPresentation.adoc
deleted file mode 100644
index 3532ae5..0000000
--- a/src/docs/chapter/user/11_Animation/10_GeneralPresentation.adoc
+++ /dev/null
@@ -1,69 +0,0 @@
-
-[[general-presentation]]
-= General Presentation
-
-[[the-prob-main-window]]
-== The ProB Main Window
-
-The menu bar contains the various commands to access the features of
-ProB. It includes the traditional _File_ menu with a sub-menu "Recent
-Files" to quickly access the files previously opened in ProB. Notice
-the commands "Open\Save", "Reopen\Save" and "Reopen"; the latter
-reopens the currently opened file and re-initialises the state of the
-animation and the model checking processes completely. The _About_
-menu provides help on the tool and includes a command to check if an
-update is available on the ProB website. By default, ProB starts with a
-limited set of commands in the *Beginner mode*. The *Normal mode* gives
-access to more features and can be set in the menu _Preferences|User
-Mod_.
-
-Under the menu bar, the main window contains four panes:
-
-* In the top pane, the specification of the B machine is displayed with
-the syntax highlighted and can also be edited by typing directly in this
-pane; you can find out more about this editor and how to use external
-editors in our <<editors-for-prob,wiki page on editors>>.
-
-* At the bottom, the animation window is composed of three panes which
-display at the current point during the animation:
-
-1.  The current state of the B machine (State Properties), listing the
-current values of the machine variables;
-
-2.  The enabled operations (Enabled Operations), listing the operations
-whose preconditions and guards are true in this state (see
-<<colours-of-enabled-operations,here>> for what the different colours
-mean);
-
-3.  The history of operations leading to this state (History).
-
-[[general-presentation-preferences]]
-== Preferences
-
-The _Preferences_ menu allows the various features of ProB to be
-configured. When ProB is started for the first time, it creates a file
-prob_preferences.pl that stores those preferences.
-
-* The sub-menu "Font" changes the font size of the B specification
-displayed in the main window.
-
-The next three commands correspond to groups of preferences displayed in
-separate pop-up windows.
-
-* The command "Animation Preferences" configures important aspects
-of ProB relative to the animation and model checking of the B
-specifications. These preferences influence directly the way ProB
-interprets the B specification and are described in "Animation and
-Visualisation", amongst others.
-
-* The command "Graphical Viewer Preferences" allows the user to
-set the options of the visualization tool used by ProB and the shapes
-and colors used to display the nodes of the state space.
-
-* The command "Syntax Highlight Preferences" allows the user to
-activate the syntax highlight of the B specification in the main window
-and also to select the various colors corresponding to the syntactic
-elements of the B notation.
-
-*IMPORTANT: Changes in the animation preferences take effect only after
-reloading the machine.*
diff --git a/src/docs/chapter/user/11_Animation/12_Animation.adoc b/src/docs/chapter/user/11_Animation/12_Animation.adoc
deleted file mode 100644
index 7e58319..0000000
--- a/src/docs/chapter/user/11_Animation/12_Animation.adoc
+++ /dev/null
@@ -1,157 +0,0 @@
-
-[[animation]]
-= Animation
-
-The animation facilities of ProB allow users to gain confidence in their
-specifications. These features try to be as user-friendly as possible
-(e.g., the user does not have to guess the right values for the
-operation arguments or choice variables, and he uses the mouse to
-operate the animation).
-
-[[basic-animation]]
-== Basic Animation
-
-When the B specification is opened, the syntax and type checker analyses
-it and, if a syntax or type error is detected, it is then reported,
-highlighted in yellow in the specification. Furthermore, if the B
-specification contains features of B that are not supported by ProB or
-constraints that are not satisfiable, an appropriate message is
-displayed. When these checks are passed, the B machine is loaded, but it
-has no state yet. ProB will then display the operations that can be
-performed in the Enabled Operations pane. These operations can be of two
-types described below.
-
-[[operations-from-the-b-machine]]
-=== Operations from the B Machine
-
-These operations are the ones whose preconditions and guards are
-satisfiable in the current state. The parameter values that make true
-the precondition and guard are automatically computed by ProB, and one
-entry for the operation is displayed in the Enabled Operations pane for
-each group of parameter values. Each parameter value is displayed as a
-set between curly brackets, and the group of parameter values are
-enclosed between brackets after the operation name.
-
-The computation of the parameter values greatly facilitates the work of
-the user, as he does not have to enumerate the possible values and check
-the preconditions and guards. This computation process involves trying
-to solve the various constraints imposed on the parameter values in the
-preconditions and guards.
-
-*HINT: If no operation is enabled, the state of the B machine
-corresponds to a deadlock*
-
-[[virtual-operations]]
-=== Virtual Operations
-
-There are three particular operations that correspond to specific tasks
-performed by ProB:
-
-* _SETUP_CONSTANTS_ This virtual operation corresponds to the assignment
-of values to the constants of the B machine. These values must satisfy
-the PROPERTIES clause. ProB automatically computes the possible values
-and displays one initialise constants virtual operation for each
-possible group of of constant values. If the PROPERTIES clause is not
-satisfiable, an error message is displayed.
-
-* _INITIALISATION_ This virtual operation plays the same role as
-initialise constants but for initial values of the variables (clauses
-VARIABLES and INITIALISATION) instead of constants. If the
-INITIALISATION clause does not satisfy the constraints in the INVARIANT
-clause, an error message is displayed.
-
-Note, there are also forward and backward buttons in the Operations
-pane. These enable the user to explore interactively the behaviour of
-the B machine.
-
-[[animating-the-b-machine]]
-=== Animating the B machine
-
-If the B machine has constants, one or several initialise constants
-operations are displayed. The user selects one of these operations, then
-the corresponding values of the constants are displayed in the State
-Properties pane and the selected initialise constants operation is
-displayed in the History pane. In the State Properties pane, functions
-and relations are displayed by indicating each of their tuples on a
-different line.
-
-At that point during the animation (also reached directly if the B
-machine has no constants), ProB displays one or several initialise
-machine operations. The user selects one of these operations, and then
-the machine is in its initial state. The initial values of the variables
-are displayed in the State Properties pane and the initialise machine
-operation selected is displayed in the History. From that moment on, an
-indicator of the status of the invariant is displayed at the top of the
-State Properties pane and the backtrack operation is displayed at the
-bottom of the Enabled Operations pane. The invariant status indicator is
-invariant ok if the invariant is satisfied or invariant violated if the
-invariant is violated.
-
-From there, the user selects operations among the enabled ones. If the
-selected operation is backtrack, the last selected operation is removed
-from the top of the History pane and the previous state is displayed in
-the State Properties pane. If the operation was not backtrack, it is
-added to the History pane, the effect of the operation are computed and
-the state is updated in the State Properties pane.
-
-[[the-analyse-menu]]
-== The Analyse menu
-
-At each point during the animation process, several useful commands
-displaying various information on the B machine are available in the
-_Analyse_ menu. The Compute Coverage command opens a window that displays
-three groups of information:
-
-* *NODES* This is the number of nodes (i.e. states) explored so far;
-there are four kinds of nodes:
-1.  live: states already computed by ProB;
-2.  deadlocked: states where the B machine is deadlocked;
-3.  invariant violated: states where the invariant is violated;
-4.  open: states that are reachable from the live nodes by an enabled
-operation.
-
-* *COVERED OPERATIONS* This is the number of operations that have been
-enabled so far, including the initialise machine operations.
-
-* *UNCOVERED OPERATIONS* This is the names of the operations that have
-not been enabled so far.
-
-The Analyse Invariant command opens a window displaying the truth values
-of the various conjuncts of the invariant of the B machine, while the
-Analyse Properties command plays the same role but for the constant
-properties and the Analyse Assertions plays this role for the
-assertions.
-
-[[animation-preferences]]
-== Animation Preferences
-
-The animation process in ProB can be configured via several preferences
-set in the preference window Preferences|Animation Preferences.
-
-First, the preference Show effect of initialisation and setup constants
-in operation name toggles the display of the values of the constants and
-the initial values of the variables when the corresponding virtual
-operations are shown in the Enabled Operations pane.
-
-The preference Nr of Initialisations shown determines the number of
-maximum initialise machine operations that ProB should compute.
-Similarly, the preference Max Number of Enablings shown sets the maximum
-number of groups of parameter values computed for each operation of the
-B machine.
-
-The preference Check invariant will toggle the display of the invariant
-status indicator in the State Properties pane.
-
-[[other-animation-features]]
-== Other Animation Features
-
-Several other commands are provided by ProB in the _Animate_ menu for
-animating B specifications. The Reset command will set the state of the
-machine to the root, as if the machine has just been opened, i.e. when
-the initialise constants or initialise machine operations are displayed
-in the Enabled Operations pane. The Random Animation(10) command
-operates a sequence of 10 randomly chosen operations from the B
-specification. The variant Random Animation enables to specify the
-number of operation to operate randomly. In the _File_ menu, the command
-Save State stores the current state of the B machine, which can then be
-reloaded with the command Load Saved State.
diff --git a/src/docs/chapter/user/11_Animation/13_Colours_of_enabled_operations.adoc b/src/docs/chapter/user/11_Animation/13_Colours_of_enabled_operations.adoc
deleted file mode 100644
index aa892eb..0000000
--- a/src/docs/chapter/user/11_Animation/13_Colours_of_enabled_operations.adoc
+++ /dev/null
@@ -1,16 +0,0 @@
-
-[[colours-of-enabled-operations]]
-= Colours of enabled operations
-
-The enabled operations are shown in different colours, depending on the
-state where the operation leads to. If more than one rule of the
-following list apply, the first colour is taken:
-
-blue : The operation does not change the state (behaves like skip). +
-green : The operation leads to a new, not yet explored state. +
-red : The operation leads to a state where the invariant is violated. +
-orange : The operation leads to a deadlock state, i.e. a state where no
-operation is enabled. +
-black : Otherwise, the operation leads to a state that is different to
-the current state, has already been visited and is neither an invariant
-violating or deadlock state.
diff --git a/src/docs/chapter/user/11_Animation/Controlling_ProB_Preferences.adoc b/src/docs/chapter/user/11_Animation/Controlling_ProB_Preferences.adoc
deleted file mode 100644
index 7e3c80a..0000000
--- a/src/docs/chapter/user/11_Animation/Controlling_ProB_Preferences.adoc
+++ /dev/null
@@ -1,61 +0,0 @@
-
-[[controlling-prob-preferences]]
-= Controlling ProB Preferences
-
-ProB provides a variety of preferences to control its behaviour. A list
-of the most important preferences can be found
-<<using-the-command-line-version-of-prob,in the manual
-page for probcli>>. We also have a separate <<deferred-sets,manual
-page about setting the sizes of deferred sets>>.
-
-[[setting-preferences-in-a-b-machine]]
-== Setting Preferences in a B machine
-
-This only works for classical B models. For a preference `P` you can add
-the following definition to the `DEFINITIONS` section of the main
-machine:
-
-`SET_PREF_P == VAL`
-
-This will set the preference `P` to the value `VAL` for this model only.
-
-[[setting-preferences-from-the-command-line]]
-== Setting Preferences from the command-line
-
-You can set a preference `P` to a value `VAL` for a particular run of
-probcli by adding the command-line switch `-p P VAL`, e.g.,
-
-`probcli -p P VAL mymachine.mch -mc 9999`
-
-You can obtain a list of preferences by calling
-<<using-the-command-line-version-of-prob,probcli>> as
-follows:
-
-`probcli -help -v`
-
-You can use a preference file generated by ProB Tcl/Tk:
-
-`-prefs FILE`
-
-This will import all preferences from this file, as set by ProB Tcl/Tk.
-
-You can also set the scope for a particular <<deferred-sets,deferred
-set>> `GS` using the following command-line switch:
-
-`-card GS Val`
-
-[[setting-preferences-from-prob-tcltk]]
-== Setting Preferences from ProB Tcl/Tk
-
-ProB Tcl/Tk stores your preferences settings in a file
-`ProB_Preferences.pl`.
-
-The ProB preferences are grouped into various categories. In the
-_Preferences_ Menu you can modify the preferences for each category:
-
-image::GraphicalViewerPreferencesMenuEntry.png[]
-
-For example, if you choose the graphical viewer preferences you will get
-this dialog:
-
-image::GraphicalViewerPreferences.png[]
diff --git a/src/docs/chapter/user/11_Animation/Tutorial_Animation_Tips.adoc b/src/docs/chapter/user/11_Animation/Tutorial_Animation_Tips.adoc
deleted file mode 100644
index ae1bdb9..0000000
--- a/src/docs/chapter/user/11_Animation/Tutorial_Animation_Tips.adoc
+++ /dev/null
@@ -1,168 +0,0 @@
-
-[[tutorial-animation-tips]]
-= Tutorial Animation Tips
-
-Make sure you have the Lift.mch model from the first part of the
-tutorial: <<tutorial-first-step,Starting ProB and first animation
-steps>>.
-
-[[operation-with-many-solutions-for-the-parameters]]
-== Operation with many solutions for the parameters
-
-Add the following operation to the Lift model:
-
-....
-jump(level) = PRE level : 0..99 THEN floor := level END
-....
-
-Now reload your model and initialise the machine. Your ProB window
-should now look as follows:
-
-image::ProB_LiftWithJump.png[]
-
-As you can see, only 10 values for the level parameter of the jump
-operation are displayed in the "Enabled Operations" pane. The orange
-"max" button to the left of "Enabled Operation" tells you that not
-all possible parameter values for the operations were computed.
-
-There are several solutions to overcome this.
-
-[[increasing-max_operations]]
-=== Increasing MAX_OPERATIONS
-
-First, you could increase the "MAX_OPERATIONS" preference of ProB by
-selecting the "Animation Preferences" command in the _Preferences_
-menu:
-
-image::ProB_Lift_MAX_OPERATIONS.png[]
-
-You should then set the preference "MAX_OPERATIONS" to at least 101 and then re-load
-the B machine.
-
-image::ProB_Lift_OpPane_WithJump101.png[]
-
-[[executing-an-operation-by-predicate]]
-
-=== Increasing MAX_OPERATIONS for an individual operation
-
-As of version 1.9.0 of ProB you can also set the MAX_OPERATIONS limit individually per operation.
-For this you need to add a declaration in the DEFINITIONS section of your B machine:
-
-....
- DEFINITIONS
-   MAX_OPERATIONS_jump == 101
-....
-
-
-[[execute-operation-by-predicate]]
-=== Executing an Operation by Predicate
-
-The alternative is to provide the parameter value for `level` yourself.
-For this, select the "Execute an Operation..." command in the _Animate_
-menu:
-
-image::ProB_Lift_ExecuteOperationMenu.png[]
-
-After that, select the `jump` operation
-
-image::ProB_ExecuteOperation.png[]
-
-and you will be provided with the following dialog:
-
-image::ProB_Lift_ExecuteOperation_Dialog.png[]
-
-Type in `98` into the level field and hit the "Execute" button.
-
-image::ProB_Lift_OpPane_WithJump_Exec98.png[]
-
-Note: instead or in addition to providing concrete values, you can also
-specify a predicate that constrains the values of the parameters:
-
-image::ProB_Lift_ExecuteOperation_Dialog_Pred.png[]
-
-The above predicate, `level>96 & level mod 2 =0` would select the same
-value `98` for level. When there are multiple solutions, ProB will only
-execute the operation for the first solution found.
-
-[[using-random-enumeration]]
-=== Using Random enumeration
-
-You can also tell ProB to try and perform random enumerations. This
-feature is available in ProB 1.5.0 or newer. You add the following lines
-to your model:
-
-`DEFINITIONS` +
-`SET_PREF_RANDOMISE_ENUMERATION_ORDER == TRUE`
-
-Alternatively, you can set this preference using the "Advanced
-Preferences" pane in the _Preferences_ menu. After reloading the machine
-you should see a picture similar to the following one:
-
-image::ProB_Lift_Randomise.png[]
-
-[[using-constraint-based-validation-techniques]]
-=== Using Constraint-Based Validation Techniques
-
-[[find-sequence]]
-==== Find Sequence
-
-You can also use the constraint solver to construct sequences which are
-of interest to you. Let us add the following operation to the lift
-model:
-
-`top_reached = PRE floor=99 THEN skip END`
-
-Now suppose we want to execute this new operation as early as possible.
-We can ask the constraint solver to generate a feasible sequence of
-operations. First select the "Find Sequence..." command in the _Verify_
-menu:
-
-image::FindSequenceMenu.png[]
-
-Now type in
-
-`jump ; top_reached`
-
-in this dialog box:
-
-image::FindSequenceDialog.png[]
-
-ProB will then find a solution operation sequence for you and execute
-it:
-
-image::FindSequenceResult.png[]
-
-[[constraint-based-model-based-testing]]
-==== Constraint-Based Model-Based Testing
-
-Alternatively, you could for example use the constraint-based test-case
-generator to find for every operation the shortest trace that enables
-it.
-
-First select the "Constraint-based Testcase Generation.." command in
-the _Analyse_ menu:
-
-image::CBCMBTMenu.png[]
-
-Now click on the ok button in the dialog box (which allows you to select
-the target operations to cover in the generated test cases):
-
-image::CBCMBTDialog.png[]
-
-ProB will then find four test cases for you, one for each operation:
-
-image::CBCMBTResult.png[]
-
-You can also visualise these test cases as a tree by clicking the "View
-Tree" button:
-
-image::CBCMBTTreeResult.png[]
-
-Green entries show test cases (traces which cover an operation in the
-shortest possible way), gray entries are traces which did not contribute
-to a test case.
-
-More details are available in the
-<<tutorial-model-based-testing,Tutorial_Model-Based_Testing>> and
-<<tutorial-model-checking-proof-and-cbc,Tutorial_Model_Checking,_Proof_and_CBC>>
-sections.
diff --git a/src/docs/chapter/user/11_Animation/Tutorial_First_Step.adoc b/src/docs/chapter/user/11_Animation/Tutorial_First_Step.adoc
deleted file mode 100644
index a79c151..0000000
--- a/src/docs/chapter/user/11_Animation/Tutorial_First_Step.adoc
+++ /dev/null
@@ -1,114 +0,0 @@
-
-[[tutorial-first-step]]
-= Tutorial First Step
-
-[[installation-tutorial-first-step]]
-== Installation
-
-Start off by installing the standalone Tcl/Tk version of ProB. Follow
-the instructions in <<installation,Installation>>.
-
-[[starting-prob-tutorial-first-step]]
-== Starting ProB
-
-Start ProB by double-clicking on `ProBWin` (for Windows users), or by
-launching `StartProB.sh` from a Terminal (for Linux and Mac users).
-
-image::ProBWinContents.png[]
-
-Mac users may also be able to launch ProB by double-clicking on
-`StartProB.sh`.
-
-This should bring up a window as follows (on a Mac):
-
-image::ProBStartWindow.png[]
-
-In case this does not work, please have a look at the output of ProB in
-the terminal window (on Windows a separate window will be automatically
-started) and send us a description of what is printed in that window
-along with a detailed report (list which operating system you use, which
-version it is, which version of ProB have you downloaded, etc.).
-Normally, it should look as follows (on Windows):
-
-image::ProBStartTerminal.png[]
-
-[[loading-a-first-b-machine]]
-== Loading a first B machine
-
-Use the "Open..." command in the _File_ menu
-
-image::ProBWinOpen.png[]
-
-and then navigate to the "Examples" directory that came with your ProB installation:
-
-image::ProBWinExamplesFolder.png[]
-
-Inside the samples folder, open the "Lift.mch" machine. Your main ProB
-window should now look as follows:
-
-image::ProB_LiftAfterLoad.png[]
-
-[[first-steps-in-animation]]
-== First Steps in Animation
-
-We have now loaded a first simple B model. Let us look at the contents
-of the ProB window (ignoring the menu bar).
-
-* The upper half of the ProB window contains the source code of themodel.
-
-* The lower half contains three panes.
-
-** The "State Properties" pane contains information about the current
-state of the model. We will explain the contents of this pane in more
-detail later.
-
-** The Pane called "Enabled Operations" contains a list of operations
-that can be applied to your model. Before a B machine can be animated,
-we have to initialise it. Hence, initially the only option presented is
-"INITIALISATION(4)". The `4` indicates that the initialisation will
-set the main variable of the machine (`floor`) to the value 4. This
-information is useful in case multiple initialisations are possible (in
-order to distinguish them).
-
-** The History pane contains the list of operations you have executed to
-reach the current state of the animator. Obviously, this list is
-initially empty.
-
-Now, double click on "INITIALISATION(4)" in the "Enabled
-Operations" Pane. This has the effect of executing the initialization
-and moving the machine into its initialised state. The lower half of the
-ProB window should now look as follows (the upper half will remain
-unchanged):
-
-image::ProB_LiftAfterInit.png[]
-
-In the "Enabled Operations" pane we can see that two operations can be
-executed: `inc` and `dec`. The "History" pane shows us that we have
-executed "INITIALISATION(4)" to reach the current state. In the
-"State Properties" pane we can see that the variable `floor` now has
-value 4. The green "OK" button indicates that the invariant of the
-machine is true. By clicking on the "OK" button, we obtain more
-details about the invariant of the machine:
-
-image::ProB_LiftAfterInitInvariant.png[]
-
-Now, double click on "`dec`" in the "Enabled Operations" Pane
-thereby executing the associated operation. The lower half of the ProB
-window should now look as follows:
-
-image::ProB_LiftAfterDec.png[]
-
-As you can see, the lift is now on floor 3. You can also see in the
-"Enabled Operations" pane that the `inc` operation is colored in blue,
-while `dec` is still colored in green. The blue color indicates that
-executing this operation would lead us back to a state which we have
-already explored (namely with `floor=4`). In the "Enabled Operations"
-pane you can also see a backward and forward arrow button. These buttons
-work similar to a browser. Clicking on the back arrow will "undo" the
-last animation step and lead us back to the previous state of the
-machine:
-
-image::ProB_LiftAfterDecBack.png[]
-
-This time, the forward button is also enabled which will undo the action
-of the back button (i.e., re-apply the `dec` operation).
diff --git a/src/docs/chapter/user/11_Animation/Tutorial_Setup_Phases.adoc b/src/docs/chapter/user/11_Animation/Tutorial_Setup_Phases.adoc
deleted file mode 100644
index f14b8d9..0000000
--- a/src/docs/chapter/user/11_Animation/Tutorial_Setup_Phases.adoc
+++ /dev/null
@@ -1,126 +0,0 @@
-
-[[tutorial-setup-phases]]
-= Tutorial Setup Phases
-
-We assume that you have grasped the first steps of opening and animating
-a B machine as outlined in <<tutorial-first-step,Tutorial First
-Step>>.
-
-In this lesson, we examine more closely the various steps that ProB
-undertakes before a machine can be animated.
-
-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[]
-
-In general, before the operations of a machine can be applied, ProB
-needs to traverse three phases:
-
-* 1. Loading the machine and determining the sizes of the deferred sets,
-as well as fixing the values of MININT and MAXINT.
-* 2. Setting up the constants of the machine, such that the PROPERTIES
-and CONSTRAINTS are satisfied.
-* 3. Performing a valid initialisation of the machine.
-
-This process is illustrated in the following picture:
-
-image::ProB_AnimationPhases.png[]
-
-We now examine these phases on the Jukebox machine in more detail
-
-[[loading]]
-== 1. Loading
-
-Here ProB parses and type checks the machine.
-
-Then it will fix the values of MININT and MAXINT. There are two ways you
-can influence this:
-
-* by using "Animation Preferences..." command in the _Preferences_
-menu and modifying the corresponding preferences.
-* by including a "DEFINITIONS" section in your machine (if there is
-not yet one) and then adding a definition of the form
-`SET_PREF_MAXINT == 5` or `SET_PREF_MININT == -2147483648`.
-
-Note that these preferences determine the elements of the sets `INT`
-(implementable integers), `NAT` (implementable natural numbers) and
-`NAT1`. In addition, they are used to control the enumeration of
-variables of type `INTEGER` (mathematical integers), in case a definite
-value cannot be inferred from the machine.
-
-Afterwards, ProB will determine the cardinality of all deferred sets
-(such as `TRACK` in the Jukebox machine). There are several ways you can
-influence this:
-
-* by using "Animation Preferences..." command in the _Preferences_
-menu and modifying the preference "Size of unspecified deferred sets in
-SETS section".
-* by including a "DEFINITIONS" section in your machine (if there is
-not yet one) and then adding a definition of the form `scope_TRACK == 5`
-(where `TRACK` is the name of the deferred set you wish to influence and
-5 is its desired cardinality). This will override the default size.
-* by including a predicate of the form `card(TRACK)=5` in the
-`PROPERTIES` or `CONSTRAINTS` section of your machine.
-
-As you can see above in the "State Properties" pane, ProB has chosen
-MAXINT=3, MININT=-1 and card(TRACK)=2. If you wish to change these
-settings, perform the steps above and reload the machine. Hint: there is
-a "Reopen" command in the _File_ menu:
-
-image::ProB_JukeboxReopenCommand.png[]
-
-[[setup_constants]]
-== 2. SETUP_CONSTANTS
-
-In this phase ProB will try and find values for the constants and
-parameters of your machine, so that the `PROPERTIES` and `CONSTRAINTS`
-are true. Note that ProB will *not* (yet) modify the settings from phase
-1 for MAXINT, MININT and the size of the deferred sets.
-
-ProB will initiate this phase automatically, and as we can see above,
-ProB has found three distinct ways to setup the constant limit. Observe
-that a little orange button labeled max has appeared in the "Enabled
-Operations" pane. This means that there might actually be more than
-three ways to setup the constants. We will return to this issue later.
-
-By double clicking on "SETUP_CONSTANTS(2)" we proceed to the next
-phase:
-
-image::ProB_JukeboxAfterSETUPCONSTANTS.png[]
-
-[[initialisation]]
-== 3. INITIALISATION
-
-In this phase the values for the constants have been found, but the
-initial values of the variables still remain to be determined. For this,
-ProB will try to execute the `INITIALISATION` substitution. As we can
-see above, ProB has found just one possible way to initialise the
-variables `credit` and `playset`. Double-clicking on
-INITIALISATION(0,\{}) leads the animator into a state where all
-constants and variables are valued, and where the `INVARIANT` can be
-checked and operations can be applied:
-
-image::ProB_JukeboxAfterINITIALISATION.png[]
-
-Let us conclude by choosing the "View Statespace" command in the
-_Animate_ menu:
-
-image::ProB_Jukebox_Statespace.png[]
-
-As you can see, there is only one root node (inverted triangle): in
-order to change MAXINT, MININT or the deferred set sizes you have to
-reload the machine. There are, however, three different ways to setup
-the constants. The model checker will explore all of them. Let us choose
-the "Model Check..." command in the _Verify_ menu and then press on
-the "Model Check" button.
-
-If we now choose the "View Statespace" command in the _Animate_
-menu, we get the following picture:
-
-image::ProB_Jukebox_StatespaceFull.png[]
-
-We can see (or guess at
-least) that ProB has validated the machine and explored the statespace
-not just for `limit=2` but also for `limit=1` and `limit=3`.
diff --git a/src/docs/chapter/user/11_Animation/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc b/src/docs/chapter/user/11_Animation/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc
deleted file mode 100644
index fb4efe7..0000000
--- a/src/docs/chapter/user/11_Animation/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc
+++ /dev/null
@@ -1,151 +0,0 @@
-
-[[tutorial-understanding-the-complexity-of-b-animation]]
-= Tutorial Understanding the Complexity of B Animation
-
-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 the complexity of animation of B models in
-general, how ProB solves this problem, and what the ramification for
-users are.
-
-[[undecidability]]
-== Undecidability
-
-In general, animation of a B model is undecidable. More precisely, it is
-undecidable to find out
-
-* whether a solution to the PROPERTIES can be found,
-* whether a valid INITIALISATION exists and
-* whether any given operation can be applied.
-
-For example, the following B machine encodes Goldbach's conjecture (that
-every even number greater than 2 is a Goldbach number, i.e., it can be
-expressed as the sum of two primes):
-
-....
-MACHINE Goldbach
-DEFINITIONS
-  prime(x) == x>1 & !y.(y:NATURAL & y>1 & y<x => x mod y /= 0)
-OPERATIONS
-  GoldbachNumber(x,p1,p2) = SELECT x:NATURAL & x mod 2 = 0 & x>2 &
-         p1<x & p2<x & p1<=p2 & prime(p1) & prime(p2) & x = p1+p2 THEN
-  skip
- END;
-  NotGoldbachNumber(x) = SELECT x:NATURAL & x mod 2 = 0 & x>2 &
-      !(p1,p2).(p1<x & p2<x & p1<=p2 & prime(p1) & prime(p2) => x /= p1+p2) THEN
-  skip
- END
-END
-....
-
-If the conjecture is true, then the operation NotGoldbachNumber is
-disabled; if the conjecture is false then it is enabled.
-
-How does ProB overcome undecidability? First, it will enumerate integer
-variables only between MININT and MAXINT (unless the machine itself
-fixes the value to be outside of that range). Hence, ProB will look for
-solutions to the parameter `x` of NotGoldbachNumber only until MAXINT.
-Hence, if we set MAXINT to 16 (adding a definiton
-`SET_PREF_MAXINT == 16`) we get the following picture after executing
-the INITIALISATION:
-
-image::ProB_GoldbachAfterInit.png[]
-
-We can see that 10 can be expressed as the sum 5+5 or 3+7. At least
-until 16, Goldbach's conjecture is confirmed, as NotGoldbachNumber is
-disabled.
-
-Note, that this restriction (of enumerating only between MININT and
-MAXINT) means that ProB is in general incomplete and sometimes unsound
-when using mathematical integers. We recommend using the implementable
-integers only (INT, NAT, NAT1). In future, we plan to integrate an
-interval analysis into ProB so as to highlight predicates over
-mathematical integers which are potentially problematic.
-
-The mathematical integers are, however, not the only source of
-undecidability. Another source stems from the deferred sets. Indeed, the
-size of those sets can be unknown, and they may even be infinite. To
-overcome this issue, ProB is required to fix the cardinality of every
-deferred set to a finite number before animation (see also
-<<tutorial-setup-phases,Understanding the ProB Setup Phases>> on how
-you can control the cardinality of the deferred sets).
-
-[[complexity-of-animation]]
-== Complexity of Animation
-
-However, after addressing the undecidability issue, there is still the
-problem of complexity. The animation task can be arbitrarily complex
-even for finite sets and implementable integers. Take for example the
-following predicate, which declares `rr` to be a binary relation over
--3..3:
-
-....
- rr : (-3..3) <-> (-3..3)
-....
-
-This predicate could be part of a precondition of an operation. In order
-to find possible ways to enable the operation, the possible values for
-`rr` need to be examined. Even if ProB did enumerate 100,000 candidate
-solutions for `rr` per second, it would take over 178 years to check all
-solutions for `rr`. Indeed, there are 49 possible pairs of values
-between -3 and 3 and hence 2^49 = 562,949,953,421,312 binary relations
-over -3..3.
-
-The following table shows how the size of a deferred set S influences
-the number of subsets, partial functions, relations over S, and a total
-function over relations of S:
-
-.__Number of distinct solutions__
-[cols=",,,,",options="header",]
-|=======================================================================
-|`card(S)` |`sub:POW(S)` |`pf:S+->S` |`rl: S<->S`
-|`tclos: (S<->S) --> (S<->S)`
-|1 |2 |2 |2 |4
-
-|2 |4 |9 |16 |1.84e+19
-
-|3 |8 |64 |512 |overflow (1.40e+1387)
-
-|4 |16 |624 |65,536 |overflow (6.74e+315652)
-
-|5 |32 |7,776 |33,554,432 |overflow
-
-|6 |64 |117,649 |6.87e+10 |overflow
-
-|7 |128 |2,097,152 |5.63e+14 |overflow
-
-|8 |256 |43,046,721 |1.85e+19 |overflow
-
-|9 |512 |1,000,000,000 |2.42e+24 |overflow
-
-|n |2^n |(n+1)^n |2^n*n |(2^n*n)^(2^n*n)
-|=======================================================================
-
-tclos is actually the type of a function that does appear in some models
-(often Event-B models): namely, the transitive closure which gets a
-relation as argument and computes its transitive closure. As you can
-see, we already run into problems with a `card(S)=2`. (Note that the age
-of the universe is about 4e+17 seconds and 4e+26 nanoseconds.) For
-`card(S)=3` the number of possible solutions (512^512) can no longer be
-represented as a standard floating point number (it is roughly 1.40e1387
-and is a number with 1388 digits).
-
-In order to make a B model amenable to animation, we have three options:
-
-* use small cardinalities for the deferred sets and avoid using overly
-complicated datastructures (e.g., relations over relations or total
-functions over relations)
-
-* ensure that ProB does not have to enumerate variables with complicated
-types, by providing concrete values (e.g., in the form of an equality
-such as `rel = {1|->2, 2|->3, 3|->1}`)
-
-* hope that the constraint solver of ProB will be able to find a
-solution.
-
-In the next part of the tutorial, we will explain in more detail how the
-constraint solver of ProB works, so that you will be in a better
-position to write specifications which can be successfully animated or
-validated.
-- 
GitLab