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

Remove Validation section whose content can be found on the wiki

parent 53de0a44
Branches
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 2589 deletions
src/docs/chapter/user/20_Validation/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ 53de0a44
[[validation]]
= Validation
:leveloffset: +1
src/docs/chapter/user/20_Validation/01_MC/Tutorial_Complete_Model_Checking.adoc deleted 100644 → 0
+ 0
− 186
View file @ 53de0a44
[[tutorial-complete-model-checking]]
= Tutorial Complete Model Checking
We assume that you have completed
<<tutorial-first-model-checking,Tutorial First Model Checking>>.
There we saw how to find invariant violations using the model checker.
In this part we use the following B Machine:
....
DEFINITIONS
MACHINE SimpleCounterForMC
DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5
VARIABLES count
INVARIANT
count: 1..MAX
INITIALISATION count := 1
OPERATIONS
Increase(y) = PRE y: 1..(MAX-count) THEN
count := count+y
END;
Reset = BEGIN count :: 1..MAX END
END
....
To load this machine into ProB you can select "New..." from the
_File_ menu, choose a file name (e.g., "SimpleCounterForMC.mch") and
then paste the text above into the ProB source pane and choose "Save
and Reopen" from the _File_ menu.
Note that the `DEFINITION SET_PREF_MAX_OPERATIONS==5` means that ProB
will compute at most 5 possible ways to execute any given operation
(i.e., Increase and Reset in this case). We return to this issue below.
[[successful-model-checking]]
== Successful Model Checking
Now select the "Model Check..." command in the _Verify_ menu which
brings up the model checking dialog box:
image::ProBWinModelCheckDialog.png[]
Now click the "Model Check" button. After a short while, ProB will give you the following message:
image::ProBModelCheckNoCounterExampleFound.png[]
This message means that ProB has examine all possible states of your B
model and has found no invariant violation and no deadlock. (In this
case there are 4 states and one root node.)
Does this mean that the B machine is guaranteed to be correct? Does this
mean that the AtelierB provers will be able to prove the B machine
correct? In this case yes, but in general, we have to be very careful
about interpreting a completed model check. Below we examine several
issues that have to be considered.
[[computing-all-transitions]]
== Computing All Transitions
Let us now adapt the above B machine by changing the DEFINITION of MAX
to 6. Now repeat the model checking exercise above. This time ProB will
produce the following message:
image::ProBModelCheckNoCounterExampleFoundTrans.png[]
Again no invariant violations or deadlocks were found, but this time
ProB warns us that not all transitions were computed. Indeed, the
`SET_PREF_MAX_OPERATIONS` definition tells ProB to compute at most 5
ways to execute an operation. In this case, there are 6 ways to execute
the "Reset" operation. As such, ProB may have missed certain states
and thus may have missed an invariant violation.
Indeed, when you double click on the "INITIALISATION(1)" entry in the
"EnabledOperations" pane, you will see the following:
image::ProBSimpleCounterForMC_Max.png[]
The orange "max" button tells us that not all operations were
computed.
In this case, there was no error, but assume we change the definition of
the Reset operation to:
....
Reset = BEGIN count :: 1..MAX+1 END
....
and repeat the model checking. We will get the exact same result as
above, but this time the machine is actually incorrect. The only way to
solve ensure that ProB checks the entire state space is to increase the
"MAX_OPERATIONS" preference to a suitably large value, e.g.,
`SET_PREF_MAX_OPERATIONS==8` in this case. Now model checking will find
a counter example:
image::ProBSimpleCounterForMC_InvViol.png[]
[[tutorial-deferred-sets]]
== Deferred Sets
Let us now use the following simple machine:
....
MACHINE SimpleCountDefSet
SETS ID
VARIABLES s
INVARIANT s <: ID & card(s)<10
INITIALISATION s := {}
OPERATIONS
Add(x) = PRE x:ID & x/:s THEN s := s\/{x} END;
Remove(x) = PRE x:s THEN s:= s - {x} END
END
....
Here model checking with ProB will give you the following message:
image::ProBModelCheckNoCounterExampleFound_Unbounded.png[]
Unfortunately this does not guarantee that your machine is correct.
Indeed, ProB has checked your machine only for one specific cardinality
of the deferred set ID (probably 2 or 3). Indeed, if you look at the
ProB window after loading the above machine you will see:
image::ProBSimpleCountDefSet_BeforeInit.png[]
In the "State Properties" pane you can see that the cardinality of ID was set to 3.
There are various ways you can influence the cardinality chosen by ProB.
One is by adding a DEFINITION of the form:
....
DEFINITIONS scope_ID == 10
....
If you add this definition, ProB will now find an invariant violation:
image::ProBSimpleCountDefSet_InvViol.png[]
However, if you remove the above DEFINITION and add the following
instead:
....
PROPERTIES card(ID) = 5
....
ProB will give you the message we have already seen:
image::ProBModelCheckNoCounterExampleFound.png[]
Indeed, you have now explicitly declare ID to be of size 5, and ProB has checked all
states for that instantiation of ID. Another solution is to replace the
deferred set ID by an enumerated set (this will, however, reduce the
potential for symmetry reduction):
....
SETS ID={id1,id2,id3,id4,id5}
....
[[infinite-types]]
== Infinite Types
It could be that your B machine makes use of the mathematical integers
(`INTEGER`) or infinite subsets thereof (`NATURAL`, `NATURAL1`). Note
that some derived types (such as seq(.)) are defined in terms of
INTEGER. In this case there could be no way to explore all states of
your system. For example, the following operation:
....
Choose = BEGIN x :: NATURAL END
....
can be executed in infinitely many ways. ProB will in this case only
find values between 0 and `MAXINT` for x. As such, a complete model
checking does not indicate that your machine's state space has been
fully explored. Note: ProB prints a warning on the console when an
infinite type (like `NATURAL`) was "expanded" into a finite subset of
it. This information is not yet fed back to the graphical user interface
(but we are working on it).
[[model-checking-and-proof]]
== Model Checking and Proof
Finally, even if ProB was able to successfully check the entire state
space of your model, this does not imply that you can prove your machine
correct with AtelierB (or Rodin). We dedicate another tutorial page to
this: <<tutorial-model-checking-proof_and_cbc,Model Checking, Proof
and CBC>>.
src/docs/chapter/user/20_Validation/01_MC/Tutorial_First_Model_Checking.adoc deleted 100644 → 0
+ 0
− 97
View file @ 53de0a44
[[tutorial-first-model-checking]]
= Tutorial First Model Checking
We assume that you have loaded the "Lift.mch" B machine from the ProB
Examples folder as outlined in <<tutorial-first-step,Tutorial First
Step>>. There we have also seen how to execute operations on a B machine
by double clicking on the items in the "Enabled Operations" pane.
[[simple-model-checking]]
== Simple Model Checking
The model checker can be used to systematically execute the operations
and tries to find an erroneous state (e.g., where the invariant is
violated). Select the "Model Check..." command in the _Verify_ menu:
image::ProBWinModelCheckCommand.png[]
This brings up the following dialog box:
image::ProBWinModelCheckDialog.png[]
Now click the "Model Check" button. After a short while, ProB will give you the
following error message:
image::ProBWinModelCheckCounterExampleFound.png[]
The lower half of the ProB window should now look as follows:
image::ProB_LiftAfterModelCheck.png[]
The red "**KO**" button in the "State Properties" pane tells us that
the model checker has moved us into a state where the invariant is
violated. Indeed, the `floor` variable has taken up a negative value,
while the invariant requires floor to be between 0 and 99. The
"History" pane tells us the sequence of operations that has led to
this error. (Note that this sequence is not necessarily the shortest
sequence that leads to an error or to this error. However, by selecting
"Breadth First" in the model check dialog above, one can ensure that
the shortest paths are found.)
[[coverage-statistics]]
== Coverage Statistics
We can obtain some statistics about how many states ProB has explored by
selecting the "Compute Coverage" command in the _Analyse_ menu:
image::ProB_LiftAfterModelCheck_Coverage.png[]
In the NODES section we can see that ProB has explored a total of 11
nodes (i.e., states of the B machine). None of these nodes are
deadlocked, in the sense that no operations are applicable. We can also
see that for one node the invariant is violated. Of these 11 nodes, 2
are *open*, meaning that they have not been explored in the sense that:
* the invariant has not been evaluated
* the enabled operations have not been computed.
As such, an open node may contain an invariant violation and/or could be
a deadlocking node. A live node is a node which is not deadlocked and
not open.
We can also see that there are in total 17 transitions among these 11
nodes. A transition is either an operation or an initialization (there
can be one more transition, which we will examine later in the
tutorial).
In the COVERED_OPERATIONS section, we can see more details about these
transitions: we have one initialization, 8 `inc` operations and 8 `dec`
operations.
[[view-statespace]]
== View Statespace
We can obtain a graphical visualization of the state space explored by
ProB. For this, be sure that you have correctly
<<graphical-viewer,installed and setup the graphical viewer as
desribed in the user manual>>. Now, choose the "View Statespace"
command in the _Animate_ menu:
image::ProB_LiftAfterModelCheck_Statespace.png[]
We can now see the 11 nodes. The two open nodes are marked in red. You
can also see that there is a virtual root node (the inverted triangle at
the top), representing the "state" of the machine before
initialization. The current node is depicted by the blue hexagon in the
right hand corner.
Note: you can influence the coloring and shapes used by ProB, by
selecting "Graphical Viewer Preferences..." in the _Preferences_
menu.
image::ProB_GraphicalViewerPreferences_Shapes.png[]
You can obtain more information about the state space visualization in
the user manual: <<state-space-visualization,State Space
Visualization>>.
src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc deleted 100644 → 0
+ 0
− 19
View file @ 53de0a44
[[constraint-based-checking]]
= Constraint Based Checking
:leveloffset: +1
ProB also offers an alternative checking method, inspired by the Alloy
footnote:[D. Jackson: Alloy: A lightweight object modeling notation. ACM
Transactions Software Engineering and Methodology (TOSEM),
11(2):256–290, 2002.] analyser. In this mode of operation, ProB does not
explore the reachable states starting from the initial state(s), but
checks whether applying a single operation can result in a property
violation (invariant and assertion) independently of the particular
initialization of the B machine. This is done by symbolic constraint
solving, and we call this approach constraint based checking (another
sensible name would be model finding).
More details and examples can be found in the
<<tutorial-model-checking-proof-and-cbc,tutorial page on model
checking, proof and CBC>>.
src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc deleted 100644 → 0
+ 0
− 55
View file @ 53de0a44
[[difference-between-constraint-based-checking-and-model-checking]]
= Difference between Constraint Based Checking and Model Checking
<<consistency-checking,Model checking>> tries to find a sequence of
operations that, starting from an initial state, leads to a state which
violates a property. Constraint based checking tries to find a state of
the machine that satisfies the property but where we can apply a single
operation to reach a state that violates this property. If the
constraint based checker finds a counter-example, this indicates that
the B specification may contain a problem. The sequence of operations
discovered by the constraint based checker leads from a valid state to a
property violation, meaning that the B machine may have to be corrected.
The valid state is not necessarily reachable from a valid initial state.
This situation further indicates that it will be impossible to prove the
machine using the B proof rules. In other words, the constraint-based
checker verifies that the invariant is inductive.
A comparison between all <<prob-validation-methods,ProB validation
methods can be found on a separate manual section>>.
[[commands-of-the-constraint-based-checker]]
= Commands of the Constraint Based Checker
These commands are only accessible in the "Normal" mode of ProB (see
<<the-prob-main-window,the general
presentation>>) and are in the sub-menu "Verify|Constraint Based
Checking". The command "Constraint Search for Invariant Violations"
will execute the constraint based checking described above to check for
invariant violations. The process stops as soon as a counterexample has
been found and then displays the counter-example in the animation panes.
The command "Constraint Search for Invariant Violations..." enables
the user to specify which particular operation leading from the valid
state to the invariant violation of the B specification should be
considered during the constraint based checking.
The "Constraint Search for Assertion Violations" command executes the
constraint based checking looking for assertion violations, while the
command "Constraint Search for Abort Conditions" executes it looking
for abort conditions.
Within the <<using-the-command-line-version-of-prob,command-line
version of ProB>>, there are also several commands available:
* <<using-the-command-line-version-of-prob,cbc >>
to check whether an operation preserves the invariant
* <<using-the-command-line-version-of-prob,cbc_deadlock>>
to check whether the invariant implies that no deadlock is possible
* <<using-the-command-line-version-of-prob,cbc_assertions>>
to check whether the static assertions (on constants) are implied by the
axioms/properties.
The following command is related to the above:
* <<using-the-command-line-version-of-prob,cbc_sequence>> to find a sequence of operations using the constraint solver
src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc deleted 100644 → 0
+ 0
− 85
View file @ 53de0a44
[[bounded-model-checking]]
= Bounded Model Checking
As of version 1.5, ProB provides support for constraint-based bounded
model checking (BMC). As opposed to
<<constraint-based-checking,constraint-based checking>>, BMC finds
counterexamples which are reachable from the INITIALISATION. As opposed
to <<consistency-checking,ordinary model checking>>, it does not
compute all possible solutions for parameters and constants, but
constructs these on demand. This can be useful when the out-degree of
the state-space is very high, i.e., when there are many possible
solutions for the constants, the initialisation and/or the individual
operations and their parameters.
Take the following example:
....
MACHINE VerySimpleCounterWrong
CONSTANTS lim
PROPERTIES lim = 2**25
VARIABLES ct
INVARIANT
ct:INTEGER & ct < lim
INITIALISATION ct::0..(lim-1)
OPERATIONS
Inc(i) = PRE i:1..1000 & ct + i <= lim THEN ct := ct+i END;
Reset = PRE ct = lim THEN ct := 0 END
END
....
The ProB model checker will here run for a very long time before
uncovering the error that occurs when `ct` is set to lim. If you run the
<<tlc,TLC backend>> you will get the error message:
`"Too many possible next states for the last state in the trace."`
However, for the bounded model checker this is less of a problem; it
will use the constraint solver to try and find suitable values of the
constants, initial variable values and parameters to generate an
invariant violation. The bounded model checker actually uses the same
algorithm than the <<test-case-generation,constraint-based test-case
generator>>, but uses the negation of the invariant as target. You can
use the command-line version of ProB, with the
<<using-the-command-line-version-of-prob,`-bmc DEPTH`>>
command as follows:
....
$ probcli VerySimpleCounterWrong -bmc 10
constraint based test case generation, maximum search depth: 10
constraint based test case generation, target state predicate: #not_invariant
constraint based test case generation, output file:
constraint based test case generation, performing bounded model checking
bounded_model_checking
CBC test search: starting length 1
*1.!#
CBC test search: covered event Inc
Found counter example
executing_stored_test_case(1,[Inc],[(2,Inc(int(1)),1,2)])
finding_trace_from_to(root)
BMC counterexample found, Length=1
CBC Algorithm finished (1)
Timeouts: total: 0
Checked paths (Depth:Paths): 1:1, total: 1
Found paths: 1:1, total: 1
Found test cases: 1:1, total: 1
Runtime (wall): 120 ms
! An error occurred !
! source(invariant_violation)
! Invariant violation found by bmc
! *** error occurred ***
! invariant_violation
....
You can also use the bounded model checker from ProB Tcl/Tk. The command
is situated inside the Experimental sub-menu of the _Analyse_ menu (to see
the command, you may have to change the preference entry to
`preference(user_is_an_expert_with_accessto_source_distribution,true).`
in the `ProB_Preferences.pl` file) Running the command on the above
example will generate the following counter-example:
image::BMC_Counter_Wrong.png[]
src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc deleted 100644 → 0
+ 0
− 92
View file @ 53de0a44
[[symbolic-model-checking]]
= Symbolic Model Checking
[[overview-symbolic-model-checking]]
== Overview
The current nightly builds of ProB support different symbolic model
checking algorithms:
* Bounded Model Checking (BMC),
* k-Induction, and
* different Variants of the IC3 algorithm.
As opposed to <<constraint-based-checking,constraint-based
checking>>, these algorithms find counterexamples which are reachable
from the INITIALISATION. As opposed to
<<consistency-checking,ordinary model checking>>, they do not build
up the state space explicitly, e.g., they do not compute all possible
solutions for parameters and constants. This can be useful when the
out-degree of the state-space is very high, i.e., when there are many
possible solutions for the constants, the initialisation and/or the
individual operations and their parameters.
In addition to the algorithms explained here, BMC*, a bounded model
checking algorithm based on a different technique is available in Prob.
See <<bounded-model-checking,its wiki page>> for details.
[[usage]]
== Usage
Take the following example:
....
MACHINE VerySimpleCounterWrong
CONSTANTS lim
PROPERTIES lim = 2**25
VARIABLES ct
INVARIANT
ct:INTEGER & ct < lim
INITIALISATION ct::0..(lim-1)
OPERATIONS
Inc(i) = PRE i:1..1000 & ct + i <= lim THEN ct := ct+i END;
Reset = PRE ct = lim THEN ct := 0 END
END
....
The ProB model checker will here run for a very long time before
uncovering the error that occurs when `ct` is set to lim. If you run the
<<tlc,TLC backend>> you will get the error message:
`"Too many possible next states for the last state in the trace."`
However, for the symbolic model checking techniques this is less of a
problem. You can use them via command-line version of ProB as follows:
....
$ probcli VerySimpleCounterWrong.mch -symbolic_model_check bmc
K = 0
solve/2: result of prob: contradiction_found
K = 1
solve/2: result of prob: contradiction_found
K = 2
solve/2: result of prob: contradiction_found
K = 3
solve/2: result of prob: contradiction_found
K = 4
solve/2: result of prob: solution
successor_found(0)
--> INITIALISATION(0)
successor_found(1)
--> Inc
successor_found(2)
--> Inc
successor_found(3)
--> Inc
successor_found(4)
--> Inc
! *** error occurred ***
! invariant_violation
....
Instead of "bmc" you can use "kinduction" and "ic3" as command
line arguments in order to use the other algorithms.
The algorithms are also available from within ProB Tcl/Tk. They can be
found inside the "Symbolic Model Checking" sub-menu of the _Analyse_ menu.
[[more-details]]
== More details
A paper describing the symbolic model checking algorithms and how they
are applied to B and Event-B machines has been submitted to ABZ 2016.
src/docs/chapter/user/20_Validation/CBC/Tutorial_Model_Checking_Proof_and_CBC.adoc deleted 100644 → 0
+ 0
− 142
View file @ 53de0a44
[[tutorial-model-checking-proof-and-cbc]]
= Tutorial Model Checking, Proof and CBC
We assume that you have completed
<<tutorial-complete-model-checking,Tutorial Complete Model
Checking>>.
Let us examine the following B machine:
....
MACHINE DoubleCounter
VARIABLES counter
INVARIANT
counter:NATURAL & counter<=128
INITIALISATION counter:=8
OPERATIONS
Double = PRE counter<100 THEN counter := 2*counter END;
Halve = BEGIN counter := counter/2 END
END
....
Now click the "Model Check" button. After a short while, ProB will
give you the following message:
image::ProBModelCheckNoCounterExampleFound.png[]
Is this model correct? As you will see, this depends on your point of
view.
[[state-space]]
== State Space
If you look purely at the state space of the machine (choose the View
State Space command in the Animate menu) you get the following picture:
image::DoubleCounterStatespace.png[]
Indeed, all reachable states are correct, in the sense that the
invariant `counter:NATURAL & counter\<=128` holds for all of those
states.
However, you will not be able to prove the system correct using AtelierB
or Rodin.
[[constraint-based-checking-cbc-for-the-invariant]]
== Constraint Based Checking (CBC) for the Invariant
In addition to model checking, ProB also offers constraint-based
checking (CBC), which is particularly useful when used in conjunction
with proof. This will give us the clue as to why the above machine
cannot be proven correct, and why it can also be viewed as incorrect.
Before proceeding, please ensure that you have either set the CLPFD
preference to `TRUE` or have set the MAXINT preference to at least `130`.
This can be set by going to the "Animation Preferences" command in the
Preferences menu or by adding for example the following to your file and
then reloading it:
....
DEFINITIONS SET_PREF_CLPFD == TRUE
....
Let us choose the "Check Invariant Preservation for Operation" command
inside the "Constraint Based Checking" submenu:
image::DoubleCounterCBCCommand.png[]
(You This will report an invariant violation and transport you to the
following state:
image::CBCDoubleCounter2.png[]
As you can see, the Counter has the value 130, which clearly violates
the invariant `counter\<=128`. However, no value in the state space above
had this value for Counter. So how did we reach this error state? By
pressing the left arrow in the "EnabledOperations" pane you will see
the previous state that ProB has computed:
image::CBCDoubleCounter1.png[]
Now, while this state does not appear in the state space above either.
However, this time this state does satisfy the invariant. Thus, if we
ignore the initialization and just look at the INVARIANT
`counter:NATURAL & counter\<=128` as describing all possible states, then
the machine is indeed erroneous: the operation Double lead us outside of
the safe states. The operation Halve on the other hand is correct: for
every possible state satisfying the INVARIANT the resulting successor
state will also satisfy the INVARIANT.
If you look purely at the state space of the machine (choose the View
State Space command in the Animate menu) you get the following picture:
image::DoubleCounterStatespace2.png[]
As you can see the constraint-based checker has transported us into the
state with `counter=65`, which is not reachable from the initial state of
the system. However, as we have said, it does satisfy the invariant and
as such the machine cannot be proven using the B provers.
If one tries to use for example Click'n Prove to prove this machine,
there is one proof obligation for the Double operation which cannot be
discharged:
image::ClicknProveDoubleCounter.png[]
Indeed, we have to prove that `2*counter` is less or equal to `128`, given
that counter is less or equal to `99` and less or equal to `128`. This is
not possible; above ProB has found `counter=65` as a counterexample. More
generally, the proof obligation in classical B for an operation with
precondition `P` and body `S` is:
`I & P \=> [S] I`
In other words, for any state which satisfies the invariant I and the
precondition `P`, the operation must preserve the invariant; not just for
the states reachable from the initialization. In particular, the
operation must preserve the invariant for the state with `counter=65`,
which it does not.
[[how-to-correct-problems-found]]
== How to correct problems found
Below is a small guide on how to correct invariant violations found by
constraint-based checking and model checking.
.__Solving Invariant Violation Problems__
[cols=",,",options="header",]
|=======================================================================
|Potential Solution |CBC |Model Check
|Strengthen Invariant |if start state wrong |NA
|Weaken Invariant |if destination state ok |If destination state ok
|Guard Strengthening |if transition should not be allowed |if path not
legal
|Guard Weakening |NA |NA
|Adapt Substitution |if destination state wrong |if destination (or
intermediate) state wrong
|=======================================================================
src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ 53de0a44
:leveloffset: -1
src/docs/chapter/user/20_Validation/MC/00_section_header.adoc deleted 100644 → 0
+ 0
− 4
View file @ 53de0a44
[[model-checking]]
= Model Checking
:leveloffset: +1
src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc deleted 100644 → 0
+ 0
− 244
View file @ 53de0a44
[[consistency-checking]]
= Model Checking Consistency
[[checking-consistency-via-model-checking]]
== Checking Consistency via Model Checking
By manually animating a B machine, it is possible to discover problems
with the specification, such as invariant violations or deadlocks. The
ProB model checker can do this exploration systematically and
automatically. It will alert you as soon as a problem has been found,
and will then present the shortest trace (within currently explored
states) that leads from an initial state to the error.
The model checker will also detect when all states have been explored
and can thus also be used to formally guarantee the absence of errors.
This will obviously only happen if the state space is finite, but the
model checker can also be applied to B machines with infinite state
spaces and will then explore the state space until it finds an error or
runs out of memory.
[[basics]]
=== Basics
During the initial draft of a specification, it is often useful to
utilize the model checker to determine if there are any invariant
violations or deadlocks. A model checker automatically explores the
(finite or infinite) state space of a B machines. Recall that the
INVARIANT specifies the types of variables and also may include
relationships that must be true in all situations. In other words, it
specifies the properties of a B machine that are immutable and must be
permanently established.
Since a graph of the visited states and the transformations (operations)
between them is retained, it is therefore possible to produce traces
(sequence of operations) of invariant violations when they are detected.
Such a trace is called a “counter-example” and is useful in determining
where and in what circumstances a specification contains errors.
Notice that if the model checker does not find any invariant violations
or deadlocks when a traversal of the exhaustive state space has been
performed, this does not imply that the specification is a correct
specification. This should be understood as the fact that, given the
initialisation stated and the model checker preferences set at the time
of the check, no errors were found. The main difference is that the ProB
animation preferences (such as the number of initialisations, times that
an operation may be enabled, and the size of unspecified sets) may be
set too low for the exhaustive state space to be covered by the model
checking.
As a final caveat, it is not possible to check a machine with an
infinite state space. Anecdotal evidence does suggest however, that the
model checker does find errors quite quickly. On that basis, it remains
a useful tool even for specifications whose state space is infinite.
[[using-the-model-checker]]
=== Using the Model Checker
To model check a B machine loaded in ProB, launch the command from
"Verify| Model Check".
image::Temporal_Model_Checker_settings.png[]
By default the model checking is done by exploring the state space in a
mixed depth-first/breadth-first manner, unless the setting "pure
Depth" or "pure Breadth First" is selected in the _Search Strategy_
pop-up menu. As of version 1.5.1, additional options for directed model
checking are available. For example, one can have truly random
exploration or provide a custom heuristic function to guide the model
checker. These features are illustrated using the
<<blocks-world-directed-model-checking,the blocks world example>>.
The two checkboxes "Find Deadlocks" and "Find Invariant Violations"
control whether the model checker will report an error when a newly
encountered state is deadlocked or respectively violates the invariant.
Similarly, if the model contains assertions (theorems for Event-B
models), then the "Find B ASSERTION Violations" checkbox is enabled.
You can then control whether the model checker cheeks the assertions
(and stops upon encountering a false assertion). Also, if the B Machine
contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes
enabled. You can then control whether the model checker cheeks the GOAL
predicate (and stops when the predicate is true for a new state). More
details about assertions and goals can be found below.
The model checker is started by clicking on the "Model Check" button.
When the model checker computes and searches the state space, a line
prefixed with Searching... at the bottom of the pop-up window will
update in real-time the number of nodes that have been computed, until a
node violating one of the properties verified has been found or the
entire state space has been checked. The user can interrupt the model
checking at any time by pressing the "Cancel" button.
[[incremental-model-checking]]
==== Incremental Model Checking
It is important to understand that the computation of and search in the
state space is an incremental process. The model checking can be done by
running the model checker several times; if the number of nodes
specified in the entry "max nr. of nodes to check" is less that the
size of the state space that remains to be checked. If the model
checking is done in several steps, the end of the model checking step is
indicated by the line No error so far, ... nodes visited at the bottom
of the pop-up window, unless a violation of the properties
(deadlockfreeness, invariant) are found. Between each model checking
step, the user can execute the various commands of ProB, notably those
of the _Analyse_ menu to display information on the state space (see
<<animation,The Analyse Menu>>) and the
visualization features (see <<state-space-visualization,State Space
Visualization>>).
By default, each model checking step starts from the open nodes of the
last computed state space. This means that a change in the settings of
the model checker between two steps does not affect the non-open nodes
(those already computed), unless there is an alternative path to an
already computed node. This behavior can be changed by toggling on the
"Inspect Existing Nodes" setting. This forces ProB to reevaluate the
properties set to be verified on the state space previously computed.
Keep in mind that unless the "Inspect Existing Nodes" setting is on,
the change of the model checking settings may not affect the state space
already computed.
[[results-of-the-model-checking]]
==== Results of the Model Checking
When the state space has been computed by ProB, the pop-up window is
replaced by a dialog window stating "No error state found". All new
nodes visited. If ProB finds a node where one of the property that was
checked is not verified, it displays a similar pop-up window but with
the text Error state was found for new node: invariant violation or
Error state was found for new node: deadlock. Then, ProB displays in the
animation panes the state of the B machine corresponding to the property
violation. From there, the user can examine the state in the "State
Properties" pane, the enabled operations (including the backtrack
virtual operation to go back to the valid state that lead to the
property violation) in the "Enabled Operations" pane, and the trace
(sequence of operations) leading to the invalid state in the "History"
pane.
[[preferences-of-the-model-checking]]
==== Preferences of the Model Checking
The preferences "Nr of Initialisations shown" and "Max Number of
Enablings shown" (described in
<<animation,Animation Preferences>>) affect the
model checking in exactly the same way as they do for the animation.
These preferences are particularly important for the model checking, as
setting the number of initialisations or the number times than an
operation may be enabled too low will lead to computing and searching a
state space that is too small. On the other hand, the user may have to
set these preferences to a lower value if the exhaustive state space is
too big to be covered by ProB.
Once the state space of the B specification has been computed by ProB,
the commands from the _Analyse_ menu (see
<<animation,The Analyse menu>>) and the
visualization features (see <<state-space-visualization,State Space
Visualization>>) are then very useful to examine the state space. The
features used to visualize a reduced state space are particularly useful
as examining a huge state space may not yield to interesting
observations due to excessive cluttering footnote:[M. Leuschel and
E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S.
King, M. Henson, and S. Schneider, editors, ZB 2005: Formal
Specification and Development in Z and B, LNCS 3455. Springer-Verlag,
2005
https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf].
[[machines-with-invariant-violations-and-deadlocks]]
=== Machines with Invariant Violations and Deadlocks
When the two properties (invariant and deadlock-freeness) are checked
and a state violates both, only the invariant violation is reported. In
that situation, the deadlock can be observed either from the Enabled
Operations (as only the backtrack virtual operation is enabled), or from
the state space graph (as the current node has no successors).
During the model checking of a specification which contains both of
these errors, it is often useful to be able to focus exclusively upon
the detection of one type of error. For example, since an invariant
violation is only reported the first time it is encountered, subsequent
invocations of the model checker may yield deadlocks whose cause is the
invariant violation. This is done by toggling off the corresponding
settings of the temporal model checker pop-up window.
*HINT: Turning off invariant violation and deadlock detection will
simply compute the entire state space until the user presses the Cancel
button or until the specified number of nodes is reached.*
[[two-phase-verification]]
==== Two Phase Verification
If the state space of the specification can be exhaustively searched,
check for deadlocks and invariant violations in two phases. To do this,
set "Inspect Existing Nodes" to off and turn either "Check for
Deadlocks" or "Check for Invariant Violations" on and the other off.
Perform the temporal model check until all the deadlocks (resp.
invariant violations) are detected or shown to be absent. To recheck the
whole state space, either turn on the option "Inspect Existing Nodes"
or purge the state space already computed by reopening the machine. Now
deselect the previous property checked, and select the alternative
property for checking. Now perform a temporal model check again to
search for a violation of the second property.
HINT: At any time during animation and model checking, the user can
reopen the the B specification to purge the state space.
[[interleaved-deadlock-and-invariant-violation-checking]]
==== Interleaved deadlock and invariant violation checking
If you wish to determine if an already encountered invariant violation
is also a deadlocked node, turn the option "Inspect Existing Nodes"
on, turn "Detect Invariant Violations" off, and ensure that "Detect
Deadlocks" is on. Performing a temporal model check now will traverse
the state space including the previously found node that violates the
invariant.
WARNING: Enabling "Inspect Existing Nodes" will continually report
the first error it encounters until that error is corrected.
[[specifying-goals-and-assertions]]
== Specifying Goals and Assertions
The ASSERTIONS clause of a B machine enables the user to define
predicates that are supposed to be deducible from the INVARIANT or
PROPERTIES clauses. If the B specification opened in ProB contains an
ASSERTIONS clause, the model checking pop-up window enables to check if
the assertion can be violated. If enabled and a state corresponding to
the violation of the assertion is found, a message "Error state was
found for new node: assertion violation" is displayed, and then ProB
displays this state in the animation panes
A feature that is similar to the assertions is the notion of a goal. A
goal is a macro in the DEFINITIONS section whose name is GOAL and whose
content is a predicate. If the B specification defines such a macro, the
model checking pop-up window enables to check if a state satisfies this
goal. If enabled and a state corresponding to the goal is found, a
message "State satisfying GOAL predicate was found" is displayed, and
then ProB displays this state in the animation panes.
It is also possible to find a state of the B machine that satisfies such
a goal without defining it explicitly in the B specification. The
"Verify|Advanced Find..." command enables the user to type a predicate
directly in a text field. ProB then searches for a state of the state
space currently computed that satisfies this goal.
src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc deleted 100644 → 0
+ 0
− 97
View file @ 53de0a44
[[distributed-model-checking]]
= Distributed Model Checking
Distributed Model Checking allows to check invariants and
deadlock-freedom (and assertions) with additional computational power.
The distributed version of ProB is named _distb_. In the following, we
will document how to run it.
== Overview
_distb_ consists of three components.
* A master which coordinates the model checking process. Per distributed
model checking, it must run exactly once.
* A proxy which coordinates workers on its machine. It should run (at
least, but usually) once per participating machine.
* A worker which does the actual work. A good number of workers usually
is close to the amount of available (physical) CPU cores of a
participating machine.
[[setting-up-shared-memory]]
== Setting up shared memory
It might be necessary to increase the limits of how much shared memory
may be allocated, both per segment and overall. This is, to our
knowledge, required for Mac OS X and older versions of Ubuntu. You can
view the limits by running:
`sysctl -a | grep shm`
Per default, recent versions of Ubuntu set the following values:
----
kernel.shmall = 18446744073692774399
kernel.shmmax = 18446744073692774399
kernel.shmmni = 4096
----
On Mac OS X, the keys might be different and you can set them by
executing:
----
sudo sysctl -w kern.sysv.shmmax=18446744073692774399
sudo sysctl -w kern.sysv.shmseg=4096
sudo sysctl -w kern.sysv.shmall=18446744073692774399
----
== Running _distb_
Run once per machine:
`/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER`
Note that on Linux systems you might need to set the LD_LIBRARY_PATH
variable to find the ZeroMQ libraries beforehand (for all components):
`export LD_LIBRARY_PATH=/path/to/prob/lib`
Run once per model checking:
`/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL`
Run as many workers as you want:
`/path/to/prob/probcli -zmq_worker <unique identifier> &`
== Additional Preferences
You can fine-tune the following parameters by adding `-p NAME VALUE` to
the corresponding call (e.g.: `./probcli -zmq_worker worker1 -p port 5010
-p max_states_in_memory 100`) :
[cols=",,,",options="header",]
|=======================================================================
|Parameter |Default |Description |Applicable for...
|port |5000 |TCP ports should be used starting at... |master, worker
|ip |localhost |IP of the master component |master
|max_states |0 |How many states should be checked at most (0 means all)
|master
|tmpdir |/tmp/ |Directory for temporary files |master, worker
|logdir |./distb-logs |Directory for log output (must exist) |master,
worker
|proxynumber |0 |Which proxy should the component connect to (if
multiple run on the same machine) |worker
|max_states_in_memory |1000 |How many states may be kept in memory
before written into a database |worker
|hash_cycle |25 |Minimum amount of milliseconds that has to pass between
hash code updates from the master |master
|=======================================================================
src/docs/chapter/user/20_Validation/MC/11_DMC.adoc deleted 100644 → 0
+ 0
− 50
View file @ 53de0a44
[[distributed-model-checking-experimental-evaluation]]
= Distributed Model Checking : Experimental evaluation
We used three different setups to evaluate the distributed version of ProB.
* A standalone multi core computer
* Amazon EC2 Instances
* The HILBERT cluster
== Multicore Computer
We used a hexacore 3.33GHz Mac Pro with 16GB of RAM. On this computer we
benchmarked all models regardless whether we expected them to be
scalable or not. We varied the number of used cores from 1 up to 12
hyperthreads. Each experiment was repeated at least 5 times.
== Amazon EC2 Instances
We used c3.8xlarge instances, each of which has 32 virtual CPUs and is
equipped with 64 GB of RAM. We used the Mac Pro to get an impression if
and how well the B models scale. From the experiments, we chose those
models that seemed to scale well and ran the benchmarks on the Amazon EC
computer with a higher number of workers. Models that did not scale on
the Mac Pro were not considered as they would not scale on more
processors. We used 2 or 4 instances connected with 10 GBit ethernet
connection. Each experiment was repeated at least 5 times.
== HILBERT
We used the high performance cluster at the university of Düsseldorf
(HILBERT) for a single model. The model could not be cheked using a
single core because it would have taken too long. Based on a partial
execution, it would take about 17 days on a single core on the Mac Pro.
The model was checked with different numbers of cores on the HILBERT
cluster. We varied between 44 and 140 cores. On the cluster we only
executed the experiments once but all experiments on the other platforms
indicated that the variation between experiments could be ignored. Also
the execution times of all 6 experiments seem to be consistent.
== Models
We cannot make all models public, because they we provided by industrial
partners from various research projects. The models that could be make
available can be downloaded https://www3.hhu.de/stups/models/parb/[here].
== Results
The results of the experiments are shown in Jens Bendisposto's
dissertation. The dissertation is available https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=34472[here].
src/docs/chapter/user/20_Validation/MC/12_ParB.adoc deleted 100644 → 0
+ 0
− 95
View file @ 53de0a44
[[parb]]
= ParB
This page explains how to run the distributed model checking prototype.
Note that the implementation does not work with Windows, only Linux
andMac OS are supported.
It is required to set the limits for shared memory on some systems, this
can be done using sysctl. Here is a little script that sets the limits.
It takes the size of shared memory as parameter (usually the size of
your memory in GB). You need to run the script with root rights.
----
#!/bin/bash
if [ $# -gt 0 ]; then
echo "Setting SHM sizes:"
sysctl -w kern.sysv.shmmax=`perl -e "print 1073741824*$1"`
sysctl -w kern.sysv.shmseg=4096
sysctl -w kern.sysv.shmall=`perl -e "print 262144*$1"`
echo "Here are the current values:"
sysctl -a | grep shm
else
echo "You need to provide the size of shared memort (in full GB)"
fi
----
After setting up shared memory, you can use the `parB.sh` script that
comes with the ProB distribution (see <<download,Download>>).
Usage
`./parB <Nr. of workers> <logfile> <file>`
Example usage:
`$ ./parB.sh 2 ~/parB.log scheduler.mch`
[[running-in-the-cloudcluster]]
== Running in the Cloud/Cluster
The script can only be used for computation on a single physical
computer. If you want to use multiple computers, the setup is a bit more
complex:
* On each physical computer you need to start exactly one copy of
`lib/hasher`.
`lib/hasher <MASTER_IP> <MASTER_PORT> 1`
* Multiple Copies of `probcli` configured as workers:
`probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0`
* A single instance of `probcli` configured as the master:
`probcli -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>`
The minimal queue length is used to determine if a worker is allowed to
share its queue. The experiments have shown, that a number between 10
and 100 is fine. parB will stop after (at least) the maximal number of
states have been explored, a value of -1 will explore all states (beware
of this, if the state space is infinite!).
As a rule of thumb use one real core for each of the processes. On
hyperthreads the model checking still becomes faster, but the speedup is
only 1/4 for each additional hyperthread.
We plan to develop a control interface that allows configuring the
logical network in a more convenient way and running the model checker
from within ProB.
[[options-for-parb]]
== Options
You can use preferences in parB.sh (and the master) :
----
./parB <Nr. of workers> <logfile> <file> <additional probcli options>
./probcli <additional probcli options> -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE> <additional probcli options>
----
If you use -strict, parB will stop as soon as a violation is found,
otherwise parB will explore the full state space (up to the maximal
number of states)
[[cleaning-up]]
== Cleaning up
If something goes wrong it may be necessary to clean up your shared
memory. You can find out if there are still memory blocks occupied using
`ipcs`. Removal can be done using:
`ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'``
src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc deleted 100644 → 0
+ 0
− 535
View file @ 53de0a44
This diff is collapsed.
src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc deleted 100644 → 0
+ 0
− 130
View file @ 53de0a44
[[symmetry-reduction]]
= Symmetry Reduction
ProB can make use of symmetries induced
by the use of deferred sets in B (and given sets in Z).
== Static Symmetry Reduction
ProB will perform a limited form of symmetry reduction for constants
which are elements of deferred sets. Take the following example:
----
MACHINE m SETS D
CONSTANTS a,b,c,d
PROPERTIES a:D & b:D & a/=b & c:D & d:D & card(D)=6
END
----
Elements of a deferred set D of cardinality n are given a number between
1 and n (the pretty printer of ProB renders those elements as D1,...,Dn
respectively). Thus, in the example above we could have 1080 solutions
(6*6*6*6 = 1296 solutions, if we ignore the constraint `a/=b`). Luckily,
symmetry reduction will reduce this to 10 possibilities.
In a first phase ProB will detect, for every deferred set D, a maximal
set ds of type D which are disjoint. In the example above, such a set ds
is `{a,b}`. These elements will be fixed, in the sense that they will
get the numbers 1..k, where k is the size of ds. Thus, a will denote D1,
b will denote D2. ProB's pretty printer will actually use a instead of
D1, and b instead of D2 (and a and b will actually disappear from the
list of constants visible in the state properties view). This reduces
the number of possibilities already to 36.
As of version 1.5, ProB will also further restrict the possible numbers
of the remaining constants. It is an adapted technique described in
Section 6 of the article "New Techniques that Improve MACE-style Finite
Model Finding"
(http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf[PDF]).
Basically, the technique ensures that c will not use the index 4 and
that d will use the index 4 only if the index 3 was used by c. Thus only
the 10 following possibilities are generated by ProB:
----
a b c d
----------------
a b a a
a b a b
a b D3 D4
a b a D3
a b b a
a b b b
a b b D3
a b D3 a
a b D3 b
a b D3 D3
----
As of version 1.8, ProB will furthermore detect partition constraints
for the deferred sets. This symmetry reduction is applied to the free,
unconstrained deferred set elements. For the example above, these would
be all elements with index 5 or higher (D5, D6, ...). For the example
above, if we have a constraint
`D = A \/ B & A /\ B = {}`
the free deferred set elements D5,D6,... will be allocated in order to A
and B. In other words, we can have D5 in A and D6 in B, but not D6 in A
and D5 in B.
In the machine below all deferred set elements are free:
----
MACHINE m SETS D
CONSTANTS A,B
PROPERTIES D = A \/ B & A /\ B = {} & card(D)=6 & card(A) = 3
END
----
Hence, here ProB 1.8 will only generate one possible setup of the
constants:
----
A = {D1,D2,D3}
B = {D4,D5,D6}
----
== Symmetry Reduction during Model Checking
In addition to the above, you can also turn of stronger symmetry
reduction for model checking.
Warning: turning on symmetry reduction will also influence the way that
animation works. In other words, when executing an operation, the
animator may transfer you to an equivalent symmetric state (rather than
to the one you may have expected).
In the "Symmetry" menu of the "Preferences" menu you can choose the
following:
* "off": symmetry reduction is turned off.
* "flood": This performs permutation flooding, whereby all
permutations of a newly added state are automatically added (and marked
as already treated). This does not reduce the number of states of the
state space, but it may still considerably reduce the number of
transitions and the number of states which need to be checked (for
invariant violations and for computing outgoing transitions). More
details: footnote:[Michael Leuschel, Michael Butler, Corinna Spermann
and Edd Turner: Symmetry Reduction for B by Permutation Flooding,
Proceedings of the 7th International B Conference (B2007),2007,pp.
79-93,LNCS 4355,Springer,
https://www3.hhu.de/stups/downloads/pdf/LeBuSpTu07_209.pdf]
* "nauty": This approach translates a B state into a graph and uses
the nauty package in order to compute a canonical form of this graph. If
two states have the same canonical form, they are considered equivalent
and only one of them is explored footnote:[Corinna Spermann and Michael
Leuschel: ProB gets Nauty: Effective Symmetry Reduction for B and Z
Models, Proceedings Symposium TASE 2008,June,2008,pp. 15-22,IEEE].
Warning: nauty sometimes can take a long time to compute the canonical
form for complicated states (and in this case it will not respond to
ProB's standard time-out mechanism).
* "hash": This approach computes a symbolic hash value for every
state, having the important property that two symmetric states have the
same hash value. Note that this is an "approximate" method, as two
non-symmetric states may also be mapped to the same hash
valuefootnote:[Michael Leuschel and Thierry Massart: ProB gets Nauty:
Efficient Approximate Verification of B via Symmetry Markers,
Proceedings International Symmetry Conference,Januar,2007,Verlag,
https://www3.hhu.de/stups/downloads/pdf/LeMa07_212.pdf].
This is typically the most efficient method.
src/docs/chapter/user/20_Validation/MC/40_LTSmin deleted 100644 → 0
+ 0
− 13
View file @ 53de0a44
[[lts-min-extension]]
= LTSmin Extension
In order to set up LTSmin, do the following:
* Download the latest LTSmin release: https://github.com/utwente-fmt/ltsmin/releases and extract it
* (Linux only) start ProB via `LD_LIBRARY_PATH=lib/ ./prob` if you have not installed ZeroMQ and CZMQ
* In ProB, go to Preferences > All Preferences (alphabetical)...
* Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive
* Start Model Checking via Verify > External Tools > Model Checking with LTSmin
Note that the LTSmin extension is not available for Windows.
src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc deleted 100644 → 0
+ 0
− 201
View file @ 53de0a44
[[tutorial-directed-model-checking]]
= Tutorial Directed Model Checking
We assume that you have completed
<<tutorial-first-model-checking,Tutorial First Model Checking>> and
<<tutorial-complete-model-checking,Complete model checking>>.
Here we will look a bit closer at the search strategy options of the
ProB model checker. You can set the mode using the `-mc_mode`
command-line switch of
<<using-the-command-line-version-of-prob,probcli>>. In the Tcl/Tk
version you can select the strategy in the model checking dialog box
(which you obtain via the"Model Check..." command in the _Verify_ menu):
image::ProBWinModelCheckDialog.png[]
The following values are possible in all versions of ProB:
* Mixed DF/BF (`mixed` for `mc_mode`) : mixed depth-first /
breadth-first traversal with random choice; currently the default),
* Breadth First (`bf` for `mc_mode`): breadth-first traversal,
* Depth First (`df`) depth-first traversal,
As of version 1.5.1, the following options are also available:
* Heuristic Function / Random (`heuristic` for `mc_mode`) : try and use
`HEURISTIC_FUNCTION` provided by user in `DEFINITIONS` clause; states
with the smallest value for the heuristic function are treated first by
the model checker. Some explanations can be found
<<blocks-world-directed-model-checking,in an example about
directed model checking>>.
* Random (`random`) : choosing next node to process completely at
random,
* Hash-Random (`hash`) :similar to random, but uses the Prolog hash
function of a node instead of a random number generator,
* Out-Degree for Deadlock Checking (`out_degree_hash`): prioritise nodes
with fewer outgoing transitions; mainly useful for deadlock checking.
Note that for exhaustive model checking, where you have to look at the
entire state space and no error state is found, the search strategy has
little nor no influence: it does not really matter in which order we
process the states, when we have to examine all of them anyway. In this
case, the depth-first search is probably the most adequate choice: its
memory requirement is smaller. However, when you expect an error (or
goal state) to be found and when the state space is very large (or even
infinite), then the search strategy can make a big difference: the
difference between finding an error state very quickly, or only after a
very long time or possibly never at all.
To illustrate the effect of the search strategy we use the following
simple example:
....
MACHINE phonebook7
SETS
Name; Code = {c1,c2,c3,c4}
VARIABLES db, active, activec
DEFINITIONS
scope_Name == 1..4
INVARIANT
db : Name +-> Code & active:POW(Name) & activec:POW(Code) &
dom(db) = active & ran(db) = activec
ASSERTIONS
card(active) >= card(activec)
INITIALISATION
db := {} || active := {} || activec := {}
OPERATIONS
dd <-- getdom = dd:= dom(db);
cc <-- lookup(nn) =
PRE
nn : Name & nn : active
THEN
cc := db(nn)
END;
add(nn,cc) =
PRE
nn:Name & cc:Code & nn /: active
THEN
db := db \/ {nn |-> cc} || active := active \/ {nn} || activec := activec \/ {cc}
END;
delete(nn,cc) =
PRE
nn:Name & cc:Code & nn: active & cc: activec & db(nn) = cc
THEN
db := db - {nn |-> cc} || active := active - {nn} || activec := db[(active - {nn})]
END
END
....
We will illustrate the state space that ProB generates using the various
search strategies when limiting the search to 10 nodes. For this we use
the command-line version as follows (as there we can provide exactly how
many states should be explored):
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode`
However, you can also obtain a similar effect with the Tcl/Tk version by
starting the model checker and then quickly pressing the Cancel button
and then inspecting the state space (Statespace command in the _Visualize_ menu; see
<<tutorial-first-model-checking,Tutorial_First_Model_Checking>>).
Below we show the output of the above command for the various choices of
.
[[breadth-first]]
== Breadth-First
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode bf`
image::ProB_Phonebook7_spdot_bf.png[]
This mode has the advantage of finding shortest counter examples first.
We also have a guarantee that, provided a counter example exists, a
counter example will sooner or later be found. However, the memory
requirements can be very large and it can take very long to find long
counter examples.
[[depth-first]]
== Depth-First
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode df`
image::ProB_Phonebook7_spdot_df.png[]
The depth-first traversal has the advantage of lower memory requirements
(concerning storing the unprocessed nodes) and can find very deep
counter examples. While it is typically the best choice for exhaustive
model checking, it can be a poor choice for models with errors. Indeed,
if the state space is infinite, then depth-first may progress infinitely
in one direction, and never find existing counter examples. Also, when
depth-first search finds a counter example, it is typically very long
and possibly hard to understand for the user. The next search strategy,
tries to combine the advantages of breadth-first and depth-first search.
[[mixed-dfbf]]
== Mixed DF/BF
The mixed search strategy, tries to combine the advantages of
breadth-first and depth-first search. It is the default setting for
ProB. It has the advantage of ensuring the exploration of some branches
in depth, to find errors which require long counter examples (e.g.,
starvation, resource exhaustion kind of bugs). But it also ensures that
we examine the specification more systematically in breadth, and is thus
also good at finding counter examples which require exhaustively to test
all operations (e.g., many errors simply require a particular faulty B
operation to be executed).
`$ probcli phonebook7.mch -p MAX_OPERATIONS 200 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode mixed`
The result will vary from one run of ProB to another:
image::ProB_Phonebook7_spdot_mixed1.png[]
image::ProB_Phonebook7_spdot_mixed2.png[]
It is interesting to compare this result with the random search
strategy, which we show next.
[[random]]
== Random
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode random`
Here are two sample results:
image::ProB_Phonebook7_spdot_random1.png[]
image::ProB_Phonebook7_spdot_random2.png[]
Compared to the `mixed` option one can notice that the mixed option has
more of a tendency to explore certain branches in depth.
[[hash]]
== Hash
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode hash`
image::ProB_Phonebook7_spdot_hash.png[]
The difference with the `random` option is that this will always return
the same result, as the hash value of the states do not change from one
run of ProB to another.
[[out-degree]]
== Out-Degree
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode dlk`
image::ProB_Phonebook7_spdot_dlk.png[]
One can notice that ProB here has a tendency to go into depth, as the
number of enabled operations decreases: if we add a name to the
phonebook, four enabled operations disappear and only two appear (lookup
and delete). Note: here it is important to set the `MAX_OPERATIONS` high
enough, otherwise the resulting state space could be different.
[[more-examples]]
== More examples
A further illustration of directed model checking can be found in our
<<blocks-world-directed-model-checking,"Blocks World" example>>.
src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc deleted 100644 → 0
+ 0
− 2
View file @ 53de0a44
:leveloffset: -1
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment