ddc424f5a3
* spot/ltsmin/defs.in: Delete. * spot/ltsmin/README, spot/ltsmin/beem-peterson.4.dve, spot/ltsmin/check.test, spot/ltsmin/elevator2.1.pm, spot/ltsmin/finite.dve, spot/ltsmin/finite.pm, spot/ltsmin/finite.test, spot/ltsmin/finite2.test, spot/ltsmin/kripke.test, spot/ltsmin/modelcheck.cc: Move... * tests/ltsmin/: ... here. * spot/ltsmin/README: Point to tests/ltsmin/README. * README, configure.ac, spot/ltsmin/Makefile.am, tests/.gitignore, tests/Makefile.am, tests/core/defs.in: Adjust.
201 lines
8.1 KiB
Text
201 lines
8.1 KiB
Text
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/
|
|
|
|
The LTSmin group [http://fmt.cs.utwente.nl/tools/ltsmin/] patched
|
|
DiVinE and SpinJa to compile models as dynamic libraries. This dynamic
|
|
library provides a very simple C interface (no C++) and extra
|
|
information about state variables (name, type, possible values). We
|
|
use this interface so you will need to install their version of these
|
|
tools to use Spot with DVE or PROMELA models.
|
|
|
|
The source code for our interface is in spot/ltsmin/ and generate a
|
|
separate library, libspotltsmin.so, that has to be loaded in addition
|
|
to libspot.so. The current directory contains some testing code based
|
|
on a toy modelchecker built upon the above interface: using it require
|
|
an installation of DiVinE or SpinS (preferably both for testing
|
|
purpose).
|
|
|
|
|
|
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
|
|
|
|
|
|
Installation of SpinS
|
|
======================
|
|
|
|
The extended version of SpinJa is called SpinS and should be included
|
|
with LTSmin.
|
|
You can download LTSmin from their website:
|
|
[http://fmt.cs.utwente.nl/tools/ltsmin/] and install it following the
|
|
INSTALL instructions.
|
|
|
|
To compile a promela model, simply run the following command:
|
|
spins model.pm
|
|
|
|
It should create a dynamic library called model.pm.spins in the
|
|
current directory.
|
|
|
|
|
|
Usage with Spot
|
|
===============
|
|
|
|
The function load_dve2() defined in dve2.hh in this directory will
|
|
accept either a model or its compiled version as file argument. In
|
|
the former case, it will call "divine compile --ltsmin model.dve" or
|
|
"spins model.pm" depending on the file extension, only if a compiled
|
|
model with the corresponding file extension (.dve2C or .spins) does
|
|
not exist or is older. Then it will load the compiled model
|
|
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".
|
|
|
|
Comparison operators available are "<", ">", ">=", "<=", "==", and
|
|
"!=". The left operand 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
|
|
expressed 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 distinct atomic propositions with the same
|
|
semantics.
|
|
|
|
|
|
Examples
|
|
========
|
|
|
|
Using the modelcheck program built into this directory, we can verify
|
|
that the critical section is accessed infinitely often by some
|
|
processes using:
|
|
|
|
% ./modelcheck 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:
|
|
|
|
% ./modelcheck 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).
|
|
|
|
% ./modelcheck 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)
|
|
|
|
|
|
Two state-compression techniques have been implemented as experiments.
|
|
Prefer the -Z option if your model use only non-negative value less
|
|
than 2^28, it is way faster than -z (which will work for all values).
|
|
|
|
Activating state compression will often reduce runtime. Compare:
|
|
|
|
% ./modelcheck -T 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
|
|
122102 pages allocated for emptiness check
|
|
no accepting run found
|
|
| user time | sys. time | total |
|
|
name | ticks % | ticks % | ticks % | n
|
|
-------------------------------------------------------------------------------
|
|
loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
running emptiness chec | 1222 100.0 | 18 100.0 | 1240 100.0 | 1
|
|
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
-------------------------------------------------------------------------------
|
|
TOTAL | 1222 100.0 | 18 100.0 | 1240 100.0 |
|
|
|
|
% ./modelcheck -T -Z 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
|
|
78580 pages allocated for emptiness check
|
|
no accepting run found
|
|
| user time | sys. time | total |
|
|
name | ticks % | ticks % | ticks % | n
|
|
-------------------------------------------------------------------------------
|
|
loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
running emptiness chec | 1051 100.0 | 10 100.0 | 1061 100.0 | 1
|
|
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
|
|
-------------------------------------------------------------------------------
|
|
TOTAL | 1051 100.0 | 10 100.0 | 1061 100.0 |
|
|
|
|
It's a 15% speedup in this case, be the improvement can be more
|
|
important on larger models.
|