Some documentation of about the dve2 interface.
* iface/dve2/README: New file. * NEWS: Mention it. * THANKS: Add Michael Weber.
This commit is contained in:
Alexandre Duret-Lutz
parent
76cfd57973
commit
e75a73dfb1
3 changed files with 145 additions and 1 deletions
136
iface/dve2/README
Normal file
136
iface/dve2/README
Normal file
|
|
@ -0,0 +1,136 @@
|
|||
This directory contains an interface that presents DiVinE models as
|
||||
kripke* objects for Spot.
|
||||
|
||||
The DiVinE model checker [http://anna.fi.muni.cz/divine/] has a
|
||||
specification language called DVE that makes it easy to model
|
||||
processes synchonizing through channels
|
||||
[http://anna.fi.muni.cz/divine/language.html].
|
||||
|
||||
A lot of models can be found in the BEEM database at
|
||||
http://anna.fi.muni.cz/models/
|
||||
|
||||
For efficient generation of the state space of the model, DiVinE
|
||||
compiles the DVE input into a dynamic library that contains anything
|
||||
needed to generate the state-space.
|
||||
|
||||
The LTSmin people [http://fmt.cs.utwente.nl/tools/ltsmin/] have made a
|
||||
patched version of DiVinE that compiles a dynamic library with a very
|
||||
simple C interface (no C++) and extra information about state
|
||||
variables (name, type, possible values). We are using this interface,
|
||||
therefore you need to install their version of DiVinE in order to use
|
||||
Spot's DVE interface.
|
||||
|
||||
|
||||
|
||||
Installation of DiVinE
|
||||
======================
|
||||
|
||||
Use the following commands to compile and install the patched version
|
||||
of DiVinE.
|
||||
|
||||
git clone http://fmt.cs.utwente.nl/tools/scm/divine2.git
|
||||
cd divine2
|
||||
mkdir _build && cd _build
|
||||
cmake .. -DMURPHI=OFF -DHOARD=OFF -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=$HOME/usr
|
||||
make
|
||||
make install
|
||||
|
||||
The CMAKE_INSTALL_PREFIX variable is the equivalent of the --prefix
|
||||
option of configure scripts. If you decide to install in $HOME/usr
|
||||
like I do, make sure that $HOME/usr/bin is in your PATH. If you omit
|
||||
the CMAKE_INSTALL_PREFIX setting, it will default to /usr/local.
|
||||
|
||||
After installation, you can check that compilation works by running
|
||||
the following command on any DVE model. It should create a file
|
||||
model.dve2C (which is a dynamic library).
|
||||
|
||||
divine compile --ltsmin model.dve
|
||||
|
||||
|
||||
Usage with Spot
|
||||
===============
|
||||
|
||||
The function load_dve2() defined in dve2.hh in this directory
|
||||
will accept "model.dve" or "model.dve2C" as file argument.
|
||||
In the former case, it will call "divine compile --ltsmin"
|
||||
if "model.dve2C" does not exist or is older. Then load
|
||||
"model.dve2C" dynamically.
|
||||
|
||||
load_dve2() also requires a set of atomic propositions that should
|
||||
be observed in the model. These are usually the atomic propositions
|
||||
that occur in the formula to verify, but it might be a larger set.
|
||||
|
||||
There are two kinds of atomic propositions, those that refer to the
|
||||
state of a process, and those that compare the value of a variable.
|
||||
Let's have some example on an excerpt of the beem-peterson.4.dve
|
||||
model included in this directory:
|
||||
|
||||
byte pos[4];
|
||||
byte step[4];
|
||||
|
||||
process P_0 {
|
||||
byte j=0, k=0;
|
||||
state NCS, CS, wait ,q2,q3;
|
||||
init NCS;
|
||||
trans
|
||||
NCS -> wait { effect j = 1; },
|
||||
wait -> q2 { guard j < 4; effect pos[0] = j;},
|
||||
q2 -> q3 { effect step[j-1] = 0, k = 0; },
|
||||
q3 -> q3 { guard k < 4 && (k == 0 || pos[k] < j); effect k = k+1;},
|
||||
q3 -> wait { guard step[j-1] != 0 || k == 4; effect j = j+1;},
|
||||
wait -> CS { guard j == 4; },
|
||||
CS -> NCS { effect pos[0] = 0;};
|
||||
}
|
||||
|
||||
The following atomic propositions could be used in LTL formula:
|
||||
|
||||
P_0.CS Process P_0 is in state CS.
|
||||
"pos[3] < 3" Global variable pos[3] is less than 3.
|
||||
"P_0.j >= 2" Process P_0's variable j is greater or equal to 2.
|
||||
P_0.j This is equivalent to "P_0.j != 0".
|
||||
|
||||
Comparisons operators available are "<", ">", ">=", "<=", "==", and
|
||||
"!=". The left operant should always be a variable and the right
|
||||
operand should always be a number, so you cannot write something
|
||||
like "P_0.j <= P_0.i".
|
||||
|
||||
Because the LTL parser knows nothing about the details of the
|
||||
languages we interface with, every atomic proposition that cannot be
|
||||
express using only alphanumeric characters (plus `_' and `.') should
|
||||
be enclosed in double quote.
|
||||
|
||||
Caveat: "P_0.j >= 2" and " P_0.j>=2" (watch the spaces!) are
|
||||
considered to be two atomic propositions with the same semantics.
|
||||
|
||||
Examples
|
||||
========
|
||||
|
||||
Using the dve2check program built into this directory, we can verify
|
||||
that the critical section is accessed infinitely often by some
|
||||
processes using:
|
||||
|
||||
% ./dve2check beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
|
||||
2239039 unique states visited
|
||||
0 strongly connected components in search stack
|
||||
11449204 transitions explored
|
||||
1024245 items max in DFS search stack
|
||||
no accepting run found
|
||||
|
||||
Process P_0 can starve, waiting to enter in critical section:
|
||||
|
||||
% ./dve2check beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
|
||||
2190 unique states visited
|
||||
34 strongly connected components in search stack
|
||||
4896 transitions explored
|
||||
83 items max in DFS search stack
|
||||
an accepting run exists (use -C to print it)
|
||||
|
||||
Variable pos[1] is not always < 3 (this formula makes no sense, it
|
||||
is just to demonstrate the use of double quote).
|
||||
|
||||
% ./dve2check beem-peterson.4.dve '!G("pos[1] < 3")'
|
||||
130 unique states visited
|
||||
61 strongly connected components in search stack
|
||||
132 transitions explored
|
||||
130 items max in DFS search stack
|
||||
an accepting run exists (use -C to print it)
|
||||
Loading…
Add table
Add a link
Reference in a new issue