Skip to content
Snippets Groups Projects
Commit 9bf9e9d9 authored by dgelessus's avatar dgelessus
Browse files

Remove Tutorials section whose content can be found on the wiki

parent 915e98c8
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 1644 deletions
src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ 915e98c8
[[tutorials]]
= Tutorials
:leveloffset: +1
src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc deleted 100644 → 0
+ 0
− 27
View file @ 915e98c8
[[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)].
src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc deleted 100644 → 0
+ 0
− 69
View file @ 915e98c8
[[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
src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc deleted 100644 → 0
+ 0
− 389
View file @ 915e98c8
[[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
....
src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc deleted 100644 → 0
+ 0
− 274
View file @ 915e98c8
[[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].
src/docs/chapter/user/YZ_Tutorials/Tutorial_ProB_Java_API.adoc deleted 100644 → 0
+ 0
− 343
View file @ 915e98c8
[[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`
src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc deleted 100644 → 0
+ 0
− 166
View file @ 915e98c8
[[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[]
src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc deleted 100644 → 0
+ 0
− 296
View file @ 915e98c8
[[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.)
src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc deleted 100644 → 0
+ 0
− 73
View file @ 915e98c8
[[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.
src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 3
View file @ 915e98c8
:leveloffset: -1
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment