move ltsmin tests to tests/ltsmin/
* 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.
This commit is contained in:
Alexandre Duret-Lutz
parent
7e6bfd0e8f
commit
ddc424f5a3
19 changed files with 264 additions and 325 deletions
2
tests/ltsmin/.gitignore
vendored
Normal file
2
tests/ltsmin/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
defs
|
||||
modelcheck
|
||||
201
tests/ltsmin/README
Normal file
201
tests/ltsmin/README
Normal file
|
|
@ -0,0 +1,201 @@
|
|||
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.
|
||||
63
tests/ltsmin/beem-peterson.4.dve
Normal file
63
tests/ltsmin/beem-peterson.4.dve
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
// peterson mutual exclusion protocol for N processes
|
||||
|
||||
// Comes from http://anna.fi.muni.cz/models/cgi/model_info.cgi?name=peterson
|
||||
// Also distributed with DiVinE (using dual GPL and BSD licences)
|
||||
|
||||
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;};
|
||||
}
|
||||
process P_1 {
|
||||
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[1] = j;},
|
||||
q2 -> q3 { effect step[j-1] = 1, k = 0; },
|
||||
q3 -> q3 { guard k < 4 && (k == 1 || pos[k] < j); effect k = k+1;},
|
||||
q3 -> wait { guard step[j-1] != 1 || k == 4; effect j = j+1;},
|
||||
wait -> CS { guard j == 4; },
|
||||
CS -> NCS { effect pos[1] = 0;};
|
||||
}
|
||||
process P_2 {
|
||||
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[2] = j;},
|
||||
q2 -> q3 { effect step[j-1] = 2, k = 0; },
|
||||
q3 -> q3 { guard k < 4 && (k == 2 || pos[k] < j); effect k = k+1;},
|
||||
q3 -> wait { guard step[j-1] != 2 || k == 4; effect j = j+1;},
|
||||
wait -> CS { guard j == 4; },
|
||||
CS -> NCS { effect pos[2] = 0;};
|
||||
}
|
||||
process P_3 {
|
||||
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[3] = j;},
|
||||
q2 -> q3 { effect step[j-1] = 3, k = 0; },
|
||||
q3 -> q3 { guard k < 4 && (k == 3 || pos[k] < j); effect k = k+1;},
|
||||
q3 -> wait { guard step[j-1] != 3 || k == 4; effect j = j+1;},
|
||||
wait -> CS { guard j == 4; },
|
||||
CS -> NCS { effect pos[3] = 0;};
|
||||
}
|
||||
|
||||
|
||||
system async;
|
||||
83
tests/ltsmin/check.test
Executable file
83
tests/ltsmin/check.test
Executable file
|
|
@ -0,0 +1,83 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
# Spot is free software; you can redistribute it and/or modify it
|
||||
# under the terms of the GNU General Public License as published by
|
||||
# the Free Software Foundation; either version 3 of the License, or
|
||||
# (at your option) any later version.
|
||||
#
|
||||
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
# License for more details.
|
||||
#
|
||||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
divine compile > output 2>&1
|
||||
|
||||
if grep -i ltsmin output; then
|
||||
:
|
||||
else
|
||||
echo "divine not installed, or no ltsmin interface"
|
||||
exit 77
|
||||
fi
|
||||
|
||||
if ! test -x "$(which spins)"; then
|
||||
echo "spins not installed."
|
||||
exit 77
|
||||
fi
|
||||
|
||||
set -e
|
||||
|
||||
# Promela
|
||||
for opt in '' '-z'; do
|
||||
|
||||
run 0 ../modelcheck $opt -E $srcdir/elevator2.1.pm \
|
||||
'!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
|
||||
run 0 ../modelcheck $opt -e $srcdir/elevator2.1.pm \
|
||||
'F("p==2")'
|
||||
done
|
||||
|
||||
# dve2
|
||||
for opt in '' '-z'; do
|
||||
# The three examples from the README.
|
||||
# (Don't run the first one using "run 0" because it would take too much
|
||||
# time with valgrind.).
|
||||
|
||||
../modelcheck $opt -E $srcdir/beem-peterson.4.dve \
|
||||
'!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
|
||||
| grep -v pages > stdout1
|
||||
# same formula, different syntax.
|
||||
../modelcheck $opt -E $srcdir/beem-peterson.4.dve \
|
||||
'!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \
|
||||
| grep -v pages > stdout2
|
||||
cmp stdout1 stdout2
|
||||
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve \
|
||||
'!G(P_0.wait -> F P_0.CS)'
|
||||
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
|
||||
done
|
||||
|
||||
# Now check some error messages.
|
||||
run 1 ../modelcheck foo.dve "F(P_0.CS)" 2>stderr
|
||||
cat stderr
|
||||
grep 'Cannot open' stderr
|
||||
# the dve2C file was generated in the current directory
|
||||
run 1 ../modelcheck beem-peterson.4.dve2C \
|
||||
'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
|
||||
cat stderr
|
||||
grep 'variable `foo' stderr
|
||||
grep "state \`f'.*P_0" stderr
|
||||
grep "Unexpected.*\`xx'" stderr
|
||||
grep 'Possible.*CS' stderr
|
||||
grep 'Possible.*NCS' stderr
|
||||
grep 'Possible.*q2' stderr
|
||||
grep 'Possible.*q3' stderr
|
||||
grep 'Possible.*wait' stderr
|
||||
61
tests/ltsmin/elevator2.1.pm
Normal file
61
tests/ltsmin/elevator2.1.pm
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
byte req[4];
|
||||
int t=0;
|
||||
int p=0;
|
||||
byte v=0;
|
||||
|
||||
|
||||
active proctype cabin() {
|
||||
|
||||
idle: if
|
||||
:: v>0; goto mov;
|
||||
|
||||
fi;
|
||||
mov: if
|
||||
:: t==p; goto open;
|
||||
|
||||
:: d_step {t<p;p = p-1;} goto mov;
|
||||
|
||||
:: d_step {t>p;p = p+1;} goto mov;
|
||||
|
||||
fi;
|
||||
open: if
|
||||
:: d_step {req[p] = 0;v = 0;} goto idle;
|
||||
|
||||
fi;
|
||||
}
|
||||
|
||||
active proctype environment() {
|
||||
|
||||
read: if
|
||||
:: d_step {req[0]==0;req[0] = 1;} goto read;
|
||||
|
||||
:: d_step {req[1]==0;req[1] = 1;} goto read;
|
||||
|
||||
:: d_step {req[2]==0;req[2] = 1;} goto read;
|
||||
|
||||
:: d_step {req[3]==0;req[3] = 1;} goto read;
|
||||
|
||||
fi;
|
||||
}
|
||||
|
||||
active proctype controller() {
|
||||
byte ldir=0;
|
||||
|
||||
wait: if
|
||||
:: d_step {v==0;t = t+(2*ldir)-1;} goto work;
|
||||
|
||||
fi;
|
||||
work: if
|
||||
:: d_step {t<0 || t==4;ldir = 1-ldir;} goto wait;
|
||||
|
||||
:: t>=0 && t<4 && req[t]==1; goto done;
|
||||
|
||||
:: d_step {t>=0 && t<4 && req[t]==0;t = t+(2*ldir)-1;} goto work;
|
||||
|
||||
fi;
|
||||
done: if
|
||||
:: v = 1; goto wait;
|
||||
|
||||
fi;
|
||||
}
|
||||
|
||||
11
tests/ltsmin/finite.dve
Executable file
11
tests/ltsmin/finite.dve
Executable file
|
|
@ -0,0 +1,11 @@
|
|||
process P {
|
||||
int a = 0, b = 0;
|
||||
state x;
|
||||
init x;
|
||||
|
||||
trans
|
||||
x -> x { guard a < 3 && b < 3; effect a = a + 1; },
|
||||
x -> x { guard a < 3 && b < 3; effect b = b + 1; };
|
||||
}
|
||||
|
||||
system async;
|
||||
8
tests/ltsmin/finite.pm
Normal file
8
tests/ltsmin/finite.pm
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
active proctype P() {
|
||||
int a = 0;
|
||||
int b = 0;
|
||||
x: if
|
||||
:: d_step {a < 3 && b < 3; a = a + 1; } goto x;
|
||||
:: d_step {a < 3 && b < 3; b = b + 1; } goto x;
|
||||
fi;
|
||||
}
|
||||
58
tests/ltsmin/finite.test
Executable file
58
tests/ltsmin/finite.test
Executable file
|
|
@ -0,0 +1,58 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
# Spot is free software; you can redistribute it and/or modify it
|
||||
# under the terms of the GNU General Public License as published by
|
||||
# the Free Software Foundation; either version 3 of the License, or
|
||||
# (at your option) any later version.
|
||||
#
|
||||
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
# License for more details.
|
||||
#
|
||||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
divine compile > output 2>&1
|
||||
|
||||
if grep -i 'ltsmin ' output; then
|
||||
:
|
||||
else
|
||||
echo "divine not installed, or no ltsmin interface"
|
||||
exit 77
|
||||
fi
|
||||
|
||||
set -e
|
||||
run 0 ../modelcheck -gm $srcdir/finite.dve '"P.a < 10"' > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 25
|
||||
test `grep 'P.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2
|
||||
cmp stdout stdout2
|
||||
|
||||
run 0 ../modelcheck -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P.a=' stdout | wc -l` = 15
|
||||
|
||||
# the same with compressed states
|
||||
run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck -ddead -E $srcdir/finite.dve \
|
||||
'!(G(dead -> ("P.a==3" | "P.b==3")))'
|
||||
|
||||
run 0 ../modelcheck -ddead -e $srcdir/finite.dve \
|
||||
'!(G(dead -> ("P.a==2" | "P.b==3")))'
|
||||
|
||||
# This used to segfault because of a bug in
|
||||
# twa_product::transition_annotation.
|
||||
run 0 ../modelcheck -gp $srcdir/finite.dve true
|
||||
54
tests/ltsmin/finite2.test
Executable file
54
tests/ltsmin/finite2.test
Executable file
|
|
@ -0,0 +1,54 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
# Spot is free software; you can redistribute it and/or modify it
|
||||
# under the terms of the GNU General Public License as published by
|
||||
# the Free Software Foundation; either version 3 of the License, or
|
||||
# (at your option) any later version.
|
||||
#
|
||||
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
# License for more details.
|
||||
#
|
||||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#These are the same tests as in finite.test, except with Spins' interface
|
||||
|
||||
. ./defs
|
||||
|
||||
# Compile the model beforehand to avoid compiler's output interference.
|
||||
if ! spins $srcdir/finite.pm; then
|
||||
echo "spins not functionnal."
|
||||
exit 77
|
||||
fi
|
||||
|
||||
run 0 ../modelcheck -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 25
|
||||
test `grep 'P_0.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck -dtrue -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout2
|
||||
diff stdout stdout2
|
||||
|
||||
run 0 ../modelcheck -dfalse -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P_0.a=' stdout | wc -l` = 15
|
||||
|
||||
# the same with compressed states
|
||||
run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.pm '"P_0.a < 10"' \
|
||||
> stdout
|
||||
test `grep ' -> ' stdout | wc -l` = 19
|
||||
test `grep 'P_0.a=' stdout | wc -l` = 15
|
||||
|
||||
run 0 ../modelcheck -ddead -E $srcdir/finite.pm \
|
||||
'!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
|
||||
|
||||
run 0 ../modelcheck -ddead -e $srcdir/finite.pm \
|
||||
'!(G(dead -> ("P_0.a==2" | "P_0.b==3")))'
|
||||
|
||||
run 0 ../modelcheck -gp $srcdir/finite.pm true
|
||||
42
tests/ltsmin/kripke.test
Executable file
42
tests/ltsmin/kripke.test
Executable file
|
|
@ -0,0 +1,42 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement
|
||||
# de l'Epita (LRDE)
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
# Spot is free software; you can redistribute it and/or modify it
|
||||
# under the terms of the GNU General Public License as published by
|
||||
# the Free Software Foundation; either version 3 of the License, or
|
||||
# (at your option) any later version.
|
||||
#
|
||||
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
# License for more details.
|
||||
#
|
||||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
divine compile > output 2>&1
|
||||
|
||||
if grep -i 'ltsmin ' output; then
|
||||
:
|
||||
else
|
||||
echo "divine not installed, or no ltsmin interface"
|
||||
exit 77
|
||||
fi
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../modelcheck -gK $srcdir/finite.dve 'F("P.a > 5")' > output
|
||||
run 0 ../../core/parse_print output | tr -d '"' > output2
|
||||
tr -d '"' < output >outputF
|
||||
cmp outputF output2
|
||||
|
||||
../modelcheck -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP
|
||||
../../core/ikwiad -e -KPoutputP '!G("pos[1] < 3")'
|
||||
369
tests/ltsmin/modelcheck.cc
Normal file
369
tests/ltsmin/modelcheck.cc
Normal file
|
|
@ -0,0 +1,369 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
// et Developpement de l'Epita (LRDE)
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 3 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <spot/ltsmin/ltsmin.hh>
|
||||
#include <spot/twaalgos/dot.hh>
|
||||
#include <spot/tl/defaultenv.hh>
|
||||
#include <spot/tl/parse.hh>
|
||||
#include <spot/twaalgos/translate.hh>
|
||||
#include <spot/twaalgos/emptiness.hh>
|
||||
#include <spot/twaalgos/postproc.hh>
|
||||
#include <spot/twa/twaproduct.hh>
|
||||
#include <spot/misc/timer.hh>
|
||||
#include <spot/misc/memusage.hh>
|
||||
#include <cstring>
|
||||
#include <spot/kripke/kripkegraph.hh>
|
||||
#include <spot/twaalgos/hoa.hh>
|
||||
|
||||
static void
|
||||
syntax(char* prog)
|
||||
{
|
||||
// Display the supplied name unless it appears to be a libtool wrapper.
|
||||
char* slash = strrchr(prog, '/');
|
||||
if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
|
||||
prog = slash + 4;
|
||||
|
||||
std::cerr << "usage: " << prog << " [options] model formula\n\
|
||||
\n\
|
||||
Options:\n\
|
||||
-dDEAD use DEAD as property for marking DEAD states\n\
|
||||
(by default DEAD = true)\n\
|
||||
-e[ALGO] run emptiness check, expect an accepting run\n\
|
||||
-E[ALGO] run emptiness check, expect no accepting run\n\
|
||||
-C compute an accepting run (Counterexample) if it exists\n\
|
||||
-D favor a deterministic translation over a small transition\n\
|
||||
-gf output the automaton of the formula in dot format\n\
|
||||
-gm output the model state-space in dot format\n\
|
||||
-gK output the model state-space in Kripke format\n\
|
||||
-gp output the product state-space in dot format\n\
|
||||
-T time the different phases of the execution\n\
|
||||
-z compress states to handle larger models\n\
|
||||
-Z compress states (faster) assuming all values in [0 .. 2^28-1]\n\
|
||||
";
|
||||
exit(1);
|
||||
}
|
||||
|
||||
static int
|
||||
checked_main(int argc, char **argv)
|
||||
{
|
||||
spot::timer_map tm;
|
||||
|
||||
bool use_timer = false;
|
||||
|
||||
enum { DotFormula, DotModel, DotProduct, EmptinessCheck, Kripke }
|
||||
output = EmptinessCheck;
|
||||
bool accepting_run = false;
|
||||
bool expect_counter_example = false;
|
||||
bool deterministic = false;
|
||||
char *dead = nullptr;
|
||||
int compress_states = 0;
|
||||
|
||||
const char* echeck_algo = "Cou99";
|
||||
|
||||
int dest = 1;
|
||||
int n = argc;
|
||||
for (int i = 1; i < n; ++i)
|
||||
{
|
||||
char* opt = argv[i];
|
||||
if (*opt == '-')
|
||||
{
|
||||
switch (*++opt)
|
||||
{
|
||||
case 'C':
|
||||
accepting_run = true;
|
||||
break;
|
||||
case 'd':
|
||||
dead = opt + 1;
|
||||
break;
|
||||
case 'D':
|
||||
deterministic = true;
|
||||
break;
|
||||
case 'e':
|
||||
case 'E':
|
||||
{
|
||||
echeck_algo = opt + 1;
|
||||
if (!*echeck_algo)
|
||||
echeck_algo = "Cou99";
|
||||
|
||||
expect_counter_example = (*opt == 'e');
|
||||
output = EmptinessCheck;
|
||||
break;
|
||||
}
|
||||
case 'g':
|
||||
switch (opt[1])
|
||||
{
|
||||
case 'm':
|
||||
output = DotModel;
|
||||
break;
|
||||
case 'p':
|
||||
output = DotProduct;
|
||||
break;
|
||||
case 'f':
|
||||
output = DotFormula;
|
||||
break;
|
||||
case 'K':
|
||||
output = Kripke;
|
||||
break;
|
||||
default:
|
||||
goto error;
|
||||
}
|
||||
break;
|
||||
case 'T':
|
||||
use_timer = true;
|
||||
break;
|
||||
case 'z':
|
||||
compress_states = 1;
|
||||
break;
|
||||
case 'Z':
|
||||
compress_states = 2;
|
||||
break;
|
||||
default:
|
||||
error:
|
||||
std::cerr << "Unknown option `" << argv[i] << "'." << std::endl;
|
||||
exit(1);
|
||||
}
|
||||
--argc;
|
||||
}
|
||||
else
|
||||
{
|
||||
argv[dest++] = argv[i];
|
||||
}
|
||||
}
|
||||
|
||||
if (argc != 3)
|
||||
syntax(argv[0]);
|
||||
|
||||
spot::default_environment& env =
|
||||
spot::default_environment::instance();
|
||||
|
||||
|
||||
spot::atomic_prop_set ap;
|
||||
auto dict = spot::make_bdd_dict();
|
||||
spot::const_kripke_ptr model = nullptr;
|
||||
spot::const_twa_ptr prop = nullptr;
|
||||
spot::const_twa_ptr product = nullptr;
|
||||
spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
|
||||
int exit_code = 0;
|
||||
spot::postprocessor post;
|
||||
spot::formula deadf = nullptr;
|
||||
spot::formula f = nullptr;
|
||||
|
||||
if (!dead || !strcasecmp(dead, "true"))
|
||||
{
|
||||
deadf = spot::formula::tt();
|
||||
}
|
||||
else if (!strcasecmp(dead, "false"))
|
||||
{
|
||||
deadf = spot::formula::ff();
|
||||
}
|
||||
else
|
||||
{
|
||||
deadf = env.require(dead);
|
||||
}
|
||||
|
||||
if (output == EmptinessCheck)
|
||||
{
|
||||
const char* err;
|
||||
echeck_inst = spot::make_emptiness_check_instantiator(echeck_algo, &err);
|
||||
if (!echeck_inst)
|
||||
{
|
||||
std::cerr << "Failed to parse argument of -e/-E near `"
|
||||
<< err << "'\n";
|
||||
exit_code = 1;
|
||||
goto safe_exit;
|
||||
}
|
||||
}
|
||||
|
||||
tm.start("parsing formula");
|
||||
{
|
||||
spot::parse_error_list pel;
|
||||
f = spot::parse_infix_psl(argv[2], pel, env, false);
|
||||
exit_code = spot::format_parse_errors(std::cerr, argv[2], pel);
|
||||
}
|
||||
tm.stop("parsing formula");
|
||||
|
||||
if (exit_code)
|
||||
goto safe_exit;
|
||||
|
||||
tm.start("translating formula");
|
||||
{
|
||||
spot::translator trans(dict);
|
||||
if (deterministic)
|
||||
trans.set_pref(spot::postprocessor::Deterministic);
|
||||
|
||||
prop = trans.run(&f);
|
||||
}
|
||||
tm.stop("translating formula");
|
||||
|
||||
atomic_prop_collect(f, &ap);
|
||||
|
||||
if (output != DotFormula)
|
||||
{
|
||||
tm.start("loading ltsmin model");
|
||||
model = spot::load_ltsmin(argv[1], dict, &ap, deadf,
|
||||
compress_states, true);
|
||||
tm.stop("loading ltsmin model");
|
||||
|
||||
if (!model)
|
||||
{
|
||||
exit_code = 1;
|
||||
goto safe_exit;
|
||||
}
|
||||
|
||||
if (output == DotModel)
|
||||
{
|
||||
tm.start("dot output");
|
||||
spot::print_dot(std::cout, model);
|
||||
tm.stop("dot output");
|
||||
goto safe_exit;
|
||||
}
|
||||
if (output == Kripke)
|
||||
{
|
||||
tm.start("kripke output");
|
||||
spot::print_hoa(std::cout, model, "k");
|
||||
tm.stop("kripke output");
|
||||
goto safe_exit;
|
||||
}
|
||||
}
|
||||
|
||||
if (output == DotFormula)
|
||||
{
|
||||
tm.start("dot output");
|
||||
spot::print_dot(std::cout, prop);
|
||||
tm.stop("dot output");
|
||||
goto safe_exit;
|
||||
}
|
||||
|
||||
product = spot::otf_product(model, prop);
|
||||
|
||||
if (output == DotProduct)
|
||||
{
|
||||
tm.start("dot output");
|
||||
spot::print_dot(std::cout, product);
|
||||
tm.stop("dot output");
|
||||
goto safe_exit;
|
||||
}
|
||||
|
||||
assert(echeck_inst);
|
||||
|
||||
{
|
||||
auto ec = echeck_inst->instantiate(product);
|
||||
bool search_many = echeck_inst->options().get("repeated");
|
||||
assert(ec);
|
||||
do
|
||||
{
|
||||
int memused = spot::memusage();
|
||||
tm.start("running emptiness check");
|
||||
spot::emptiness_check_result_ptr res;
|
||||
try
|
||||
{
|
||||
res = ec->check();
|
||||
}
|
||||
catch (std::bad_alloc)
|
||||
{
|
||||
std::cerr << "Out of memory during emptiness check."
|
||||
<< std::endl;
|
||||
if (!compress_states)
|
||||
std::cerr << "Try option -z for state compression." << std::endl;
|
||||
exit_code = 2;
|
||||
exit(exit_code);
|
||||
}
|
||||
tm.stop("running emptiness check");
|
||||
memused = spot::memusage() - memused;
|
||||
|
||||
ec->print_stats(std::cout);
|
||||
std::cout << memused << " pages allocated for emptiness check"
|
||||
<< std::endl;
|
||||
|
||||
if (expect_counter_example == !res &&
|
||||
(!expect_counter_example || ec->safe()))
|
||||
exit_code = 1;
|
||||
|
||||
if (!res)
|
||||
{
|
||||
std::cout << "no accepting run found";
|
||||
if (!ec->safe() && expect_counter_example)
|
||||
{
|
||||
std::cout << " even if expected" << std::endl;
|
||||
std::cout << "this may be due to the use of the bit"
|
||||
<< " state hashing technique" << std::endl;
|
||||
std::cout << "you can try to increase the heap size "
|
||||
<< "or use an explicit storage"
|
||||
<< std::endl;
|
||||
}
|
||||
std::cout << std::endl;
|
||||
break;
|
||||
}
|
||||
else if (accepting_run)
|
||||
{
|
||||
|
||||
spot::twa_run_ptr run;
|
||||
tm.start("computing accepting run");
|
||||
try
|
||||
{
|
||||
run = res->accepting_run();
|
||||
}
|
||||
catch (std::bad_alloc)
|
||||
{
|
||||
std::cerr << "Out of memory while looking for counterexample."
|
||||
<< std::endl;
|
||||
exit_code = 2;
|
||||
exit(exit_code);
|
||||
}
|
||||
tm.stop("computing accepting run");
|
||||
|
||||
if (!run)
|
||||
{
|
||||
std::cout << "an accepting run exists" << std::endl;
|
||||
}
|
||||
else
|
||||
{
|
||||
tm.start("reducing accepting run");
|
||||
run = run->reduce();
|
||||
tm.stop("reducing accepting run");
|
||||
tm.start("printing accepting run");
|
||||
std::cout << run;
|
||||
tm.stop("printing accepting run");
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
std::cout << "an accepting run exists "
|
||||
<< "(use -C to print it)" << std::endl;
|
||||
}
|
||||
}
|
||||
while (search_many);
|
||||
}
|
||||
|
||||
safe_exit:
|
||||
if (use_timer)
|
||||
tm.print(std::cout);
|
||||
tm.reset_all(); // This helps valgrind.
|
||||
return exit_code;
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char **argv)
|
||||
{
|
||||
auto exit_code = checked_main(argc, argv);
|
||||
|
||||
// Additional checks to debug reference counts in formulas.
|
||||
assert(spot::fnode::instances_check());
|
||||
exit(exit_code);
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue