Skip to content
Snippets Groups Projects
Commit 17169add authored by dgelessus's avatar dgelessus
Browse files

Remove Animation section whose content can be found on the wiki

parent 6111eac6
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 862 deletions
src/docs/chapter/user/11_Animation/10_GeneralPresentation.adoc deleted 100644 → 0
+ 0
− 69
View file @ 6111eac6
[[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.*
src/docs/chapter/user/11_Animation/12_Animation.adoc deleted 100644 → 0
+ 0
− 157
View file @ 6111eac6
[[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.
src/docs/chapter/user/11_Animation/13_Colours_of_enabled_operations.adoc deleted 100644 → 0
+ 0
− 16
View file @ 6111eac6
[[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.
src/docs/chapter/user/11_Animation/Controlling_ProB_Preferences.adoc deleted 100644 → 0
+ 0
− 61
View file @ 6111eac6
[[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[]
src/docs/chapter/user/11_Animation/Tutorial_Animation_Tips.adoc deleted 100644 → 0
+ 0
− 168
View file @ 6111eac6
[[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.
src/docs/chapter/user/11_Animation/Tutorial_First_Step.adoc deleted 100644 → 0
+ 0
− 114
View file @ 6111eac6
[[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).
src/docs/chapter/user/11_Animation/Tutorial_Setup_Phases.adoc deleted 100644 → 0
+ 0
− 126
View file @ 6111eac6
[[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`.
src/docs/chapter/user/11_Animation/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc deleted 100644 → 0
+ 0
− 151
View file @ 6111eac6
[[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.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment