Add support to load GAL models.
* spot/ltsmin/ltsmin.cc: Handle GAL models. * tests/Makefile.am: Test the new feature. * tests/ltsmin/check.test: Also check GAL. * tests/ltsmin/beem-peterson.4.gal: A new GAL model for tests. * tests/ltsmin/finite.gal: A new GAL model for tests. * tests/ltsmin/finite3.test: A new test for GAL.
This commit is contained in:
Maximilien Colange
parent
ec83e60bb9
commit
c9aabcddab
6 changed files with 268 additions and 9 deletions
|
|
@ -948,7 +948,12 @@ namespace spot
|
|||
std::string command;
|
||||
std::string compiled_ext;
|
||||
|
||||
if (ext == ".prom" || ext == ".pm" || ext == ".pml")
|
||||
if (ext == ".gal")
|
||||
{
|
||||
command = "gal2c " + filename;
|
||||
compiled_ext = "2C";
|
||||
}
|
||||
else if (ext == ".prom" || ext == ".pm" || ext == ".pml")
|
||||
{
|
||||
command = "spins " + filename;
|
||||
compiled_ext = ".spins";
|
||||
|
|
@ -962,7 +967,8 @@ namespace spot
|
|||
{
|
||||
throw std::runtime_error(std::string("Unknown extension '")
|
||||
+ ext + "'. Use '.prom', '.pm', '.pml', "
|
||||
"'.dve', '.dve2C', or '.prom.spins'.");
|
||||
"'.dve', '.dve2C', '.gal', '.gal2C' or "
|
||||
"'.prom.spins'.");
|
||||
}
|
||||
|
||||
struct stat s;
|
||||
|
|
@ -980,7 +986,7 @@ namespace spot
|
|||
struct stat d;
|
||||
if (stat(filename.c_str(), &d) == 0)
|
||||
if (s.st_mtime < d.st_mtime)
|
||||
// The .spins or .dve2C is up-to-date, no need to recompile it.
|
||||
// The .spins or .dve2C or .gal2C is up-to-date, no need to compile.
|
||||
return;
|
||||
|
||||
int res = system(command.c_str());
|
||||
|
|
@ -1002,7 +1008,7 @@ namespace spot
|
|||
file = "./" + file_arg;
|
||||
|
||||
std::string ext = file.substr(file.find_last_of("."));
|
||||
if (ext != ".spins" && ext != ".dve2C")
|
||||
if (ext != ".spins" && ext != ".dve2C" && ext != ".gal2C")
|
||||
compile_model(file, ext);
|
||||
|
||||
if (lt_dlinit())
|
||||
|
|
@ -1020,9 +1026,10 @@ namespace spot
|
|||
d->handle = h;
|
||||
|
||||
// SpinS interface.
|
||||
if ((d->get_initial_state = (void (*)(void*))
|
||||
lt_dlsym(h, "spins_get_initial_state")))
|
||||
if (ext == ".spins")
|
||||
{
|
||||
d->get_initial_state = (void (*)(void*))
|
||||
lt_dlsym(h, "spins_get_initial_state");
|
||||
d->have_property = nullptr;
|
||||
d->get_successors = (int (*)(void*, int*, TransitionCB, void*))
|
||||
lt_dlsym(h, "spins_get_successor_all");
|
||||
|
|
@ -1042,6 +1049,30 @@ namespace spot
|
|||
lt_dlsym(h, "spins_get_type_value_name");
|
||||
}
|
||||
// dve2 interface.
|
||||
else if (ext == ".dve2C")
|
||||
{
|
||||
d->get_initial_state = (void (*)(void*))
|
||||
lt_dlsym(h, "get_initial_state");
|
||||
d->have_property = (int (*)())
|
||||
lt_dlsym(h, "have_property");
|
||||
d->get_successors = (int (*)(void*, int*, TransitionCB, void*))
|
||||
lt_dlsym(h, "get_successors");
|
||||
d->get_state_size = (int (*)())
|
||||
lt_dlsym(h, "get_state_variable_count");
|
||||
d->get_state_variable_name = (const char* (*)(int))
|
||||
lt_dlsym(h, "get_state_variable_name");
|
||||
d->get_state_variable_type = (int (*)(int))
|
||||
lt_dlsym(h, "get_state_variable_type");
|
||||
d->get_type_count = (int (*)())
|
||||
lt_dlsym(h, "get_state_variable_type_count");
|
||||
d->get_type_name = (const char* (*)(int))
|
||||
lt_dlsym(h, "get_state_variable_type_name");
|
||||
d->get_type_value_count = (int (*)(int))
|
||||
lt_dlsym(h, "get_state_variable_type_value_count");
|
||||
d->get_type_value_name = (const char* (*)(int, int))
|
||||
lt_dlsym(h, "get_state_variable_type_value");
|
||||
}
|
||||
// .gal2C interface.
|
||||
else
|
||||
{
|
||||
d->get_initial_state = (void (*)(void*))
|
||||
|
|
|
|||
|
|
@ -375,20 +375,22 @@ check_SCRIPTS += ltsmin/defs
|
|||
|
||||
ltsmin/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in
|
||||
$(top_builddir)/config.status --file ltsmin/defs:core/defs.in
|
||||
endif
|
||||
|
||||
if USE_LTSMIN
|
||||
TESTS_ltsmin = \
|
||||
ltsmin/check.test \
|
||||
ltsmin/finite.test \
|
||||
ltsmin/finite2.test \
|
||||
ltsmin/finite3.test \
|
||||
ltsmin/kripke.test
|
||||
|
||||
EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/elevator2.1.pm \
|
||||
ltsmin/finite.dve ltsmin/finite.pm
|
||||
EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/beem-peterson.4.gal \
|
||||
ltsmin/elevator2.1.pm ltsmin/finite.dve ltsmin/finite.pm ltsmin/finite.gal
|
||||
|
||||
ltlsmin/kripke.log: core/kripkecat$(EXEEXT)
|
||||
endif
|
||||
|
||||
|
||||
############################## SANITY ##############################
|
||||
|
||||
TESTS_sanity = \
|
||||
|
|
|
|||
135
tests/ltsmin/beem-peterson.4.gal
Normal file
135
tests/ltsmin/beem-peterson.4.gal
Normal file
|
|
@ -0,0 +1,135 @@
|
|||
GAL peterson_4_dve
|
||||
{
|
||||
//arrays
|
||||
array[4] pos= (0, 0, 0, 0) ;
|
||||
array[4] step= (0, 0, 0, 0) ;
|
||||
//variables
|
||||
int P_0.state=0;
|
||||
int P_0.j=0;
|
||||
int P_0.k=0;
|
||||
int P_1.state=0;
|
||||
int P_1.j=0;
|
||||
int P_1.k=0;
|
||||
int P_2.state=0;
|
||||
int P_2.j=0;
|
||||
int P_2.k=0;
|
||||
int P_3.state=0;
|
||||
int P_3.j=0;
|
||||
int P_3.k=0;
|
||||
//transitions
|
||||
transition t0 [ ( P_0.state == 0 ) ]
|
||||
{ P_0.state = 2;
|
||||
P_0.j = 1; }
|
||||
|
||||
transition t1 [ ( P_0.state == 1 ) ]
|
||||
{ P_0.state = 0;
|
||||
pos[0] = 0; }
|
||||
|
||||
transition t2 [ ( ( P_0.j < 4 ) && ( P_0.state == 2 ) ) ]
|
||||
{ P_0.state = 3;
|
||||
pos[0] = P_0.j; }
|
||||
|
||||
transition t3 [ ( ( P_0.j == 4 ) && ( P_0.state == 2 ) ) ]
|
||||
{ P_0.state = 1; }
|
||||
|
||||
transition t4 [ ( P_0.state == 3 ) ]
|
||||
{ P_0.state = 4;
|
||||
step[( P_0.j - 1 )] = 0;
|
||||
P_0.k = 0; }
|
||||
|
||||
transition t5 [ ( ( P_0.state == 4 ) && ( P_0.k < 4 ) && ( ( pos[P_0.k] < P_0.j ) || ( P_0.k == 0 ) ) ) ]
|
||||
{ P_0.state = 4;
|
||||
P_0.k = ( 1 + P_0.k ); }
|
||||
|
||||
transition t6 [ ( ( P_0.state == 4 ) && ( ( P_0.k == 4 ) || ( step[( P_0.j - 1 )] != 0 ) ) ) ]
|
||||
{ P_0.state = 2;
|
||||
P_0.j = ( P_0.j + 1 ); }
|
||||
|
||||
transition t7 [ ( P_1.state == 0 ) ]
|
||||
{ P_1.state = 2;
|
||||
P_1.j = 1; }
|
||||
|
||||
transition t8 [ ( P_1.state == 1 ) ]
|
||||
{ P_1.state = 0;
|
||||
pos[1] = 0; }
|
||||
|
||||
transition t9 [ ( ( P_1.j < 4 ) && ( P_1.state == 2 ) ) ]
|
||||
{ P_1.state = 3;
|
||||
pos[1] = P_1.j; }
|
||||
|
||||
transition t10 [ ( ( P_1.j == 4 ) && ( P_1.state == 2 ) ) ]
|
||||
{ P_1.state = 1; }
|
||||
|
||||
transition t11 [ ( P_1.state == 3 ) ]
|
||||
{ P_1.state = 4;
|
||||
step[( P_1.j - 1 )] = 1;
|
||||
P_1.k = 0; }
|
||||
|
||||
transition t12 [ ( ( P_1.state == 4 ) && ( ( pos[P_1.k] < P_1.j ) || ( P_1.k == 1 ) ) && ( P_1.k < 4 ) ) ]
|
||||
{ P_1.state = 4;
|
||||
P_1.k = ( 1 + P_1.k ); }
|
||||
|
||||
transition t13 [ ( ( P_1.state == 4 ) && ( ( step[( P_1.j - 1 )] != 1 ) || ( P_1.k == 4 ) ) ) ]
|
||||
{ P_1.state = 2;
|
||||
P_1.j = ( 1 + P_1.j ); }
|
||||
|
||||
transition t14 [ ( P_2.state == 0 ) ]
|
||||
{ P_2.state = 2;
|
||||
P_2.j = 1; }
|
||||
|
||||
transition t15 [ ( P_2.state == 1 ) ]
|
||||
{ P_2.state = 0;
|
||||
pos[2] = 0; }
|
||||
|
||||
transition t16 [ ( ( P_2.j < 4 ) && ( P_2.state == 2 ) ) ]
|
||||
{ P_2.state = 3;
|
||||
pos[2] = P_2.j; }
|
||||
|
||||
transition t17 [ ( ( P_2.j == 4 ) && ( P_2.state == 2 ) ) ]
|
||||
{ P_2.state = 1; }
|
||||
|
||||
transition t18 [ ( P_2.state == 3 ) ]
|
||||
{ P_2.state = 4;
|
||||
step[( P_2.j - 1 )] = 2;
|
||||
P_2.k = 0; }
|
||||
|
||||
transition t19 [ ( ( P_2.state == 4 ) && ( P_2.k < 4 ) && ( ( pos[P_2.k] < P_2.j ) || ( P_2.k == 2 ) ) ) ]
|
||||
{ P_2.state = 4;
|
||||
P_2.k = ( 1 + P_2.k ); }
|
||||
|
||||
transition t20 [ ( ( P_2.state == 4 ) && ( ( step[( P_2.j - 1 )] != 2 ) || ( P_2.k == 4 ) ) ) ]
|
||||
{ P_2.state = 2;
|
||||
P_2.j = ( 1 + P_2.j ); }
|
||||
|
||||
transition t21 [ ( P_3.state == 0 ) ]
|
||||
{ P_3.state = 2;
|
||||
P_3.j = 1; }
|
||||
|
||||
transition t22 [ ( P_3.state == 1 ) ]
|
||||
{ P_3.state = 0;
|
||||
pos[3] = 0; }
|
||||
|
||||
transition t23 [ ( ( P_3.state == 2 ) && ( P_3.j < 4 ) ) ]
|
||||
{ P_3.state = 3;
|
||||
pos[3] = P_3.j; }
|
||||
|
||||
transition t24 [ ( ( P_3.state == 2 ) && ( P_3.j == 4 ) ) ]
|
||||
{ P_3.state = 1; }
|
||||
|
||||
transition t25 [ ( P_3.state == 3 ) ]
|
||||
{ P_3.state = 4;
|
||||
step[( P_3.j - 1 )] = 3;
|
||||
P_3.k = 0; }
|
||||
|
||||
transition t26 [ ( ( P_3.state == 4 ) && ( P_3.k < 4 ) && ( ( P_3.k == 3 ) || ( pos[P_3.k] < P_3.j ) ) ) ]
|
||||
{ P_3.state = 4;
|
||||
P_3.k = ( 1 + P_3.k ); }
|
||||
|
||||
transition t27 [ ( ( P_3.state == 4 ) && ( ( step[( P_3.j - 1 )] != 3 ) || ( P_3.k == 4 ) ) ) ]
|
||||
{ P_3.state = 2;
|
||||
P_3.j = ( 1 + P_3.j ); }
|
||||
|
||||
// transient predicate
|
||||
TRANSIENT = false;
|
||||
|
||||
}
|
||||
|
|
@ -35,6 +35,11 @@ if ! test -x "$(which spins)"; then
|
|||
exit 77
|
||||
fi
|
||||
|
||||
if ! test -x "$(which gal2c)"; then
|
||||
echo "gal2c not installed."
|
||||
exit 77
|
||||
fi
|
||||
|
||||
set -e
|
||||
|
||||
# Promela
|
||||
|
|
@ -65,6 +70,18 @@ for opt in '' '-z'; do
|
|||
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
|
||||
done
|
||||
|
||||
# gal
|
||||
# TODO also compare gal and dve results
|
||||
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.).
|
||||
|
||||
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.gal \
|
||||
'!G("P_0.state==2" -> F "P_0.state==1")'
|
||||
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.gal '!G("pos[1] < 3")'a
|
||||
done
|
||||
|
||||
# Now check some error messages.
|
||||
run 1 ../modelcheck foo.dve "F(P_0.CS)" 2>stderr
|
||||
cat stderr
|
||||
|
|
|
|||
19
tests/ltsmin/finite.gal
Executable file
19
tests/ltsmin/finite.gal
Executable file
|
|
@ -0,0 +1,19 @@
|
|||
gal finite
|
||||
{
|
||||
//arrays
|
||||
//variables
|
||||
int P.a=0;
|
||||
int P.b=0;
|
||||
//transitions
|
||||
transition t0 [ ( ( P.a < 3 ) && ( P.b < 3 ) ) ]
|
||||
{ P.a = ( 1 + P.a );
|
||||
}
|
||||
|
||||
transition t1 [ ( ( P.a < 3 ) && ( P.b < 3 ) ) ]
|
||||
{ P.b = ( 1 + P.b );
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
||||
55
tests/ltsmin/finite3.test
Executable file
55
tests/ltsmin/finite3.test
Executable file
|
|
@ -0,0 +1,55 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2013, 2014, 2016 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
|
||||
|
||||
# Compile the model beforehand to avoid compiler's output interference.
|
||||
if ! gal2c $srcdir/finite.gal; then
|
||||
echo "gal2c not functionnal."
|
||||
exit 77
|
||||
fi
|
||||
|
||||
set -e
|
||||
run 0 ../modelcheck -gm $srcdir/finite.gal '"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.gal '"P.a < 10"' > stdout2
|
||||
cmp stdout stdout2
|
||||
|
||||
run 0 ../modelcheck -dfalse -gm $srcdir/finite.gal '"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.gal '"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.gal \
|
||||
'!(G(dead -> ("P.a==3" | "P.b==3")))'
|
||||
|
||||
run 0 ../modelcheck -ddead -e $srcdir/finite.gal \
|
||||
'!(G(dead -> ("P.a==2" | "P.b==3")))'
|
||||
|
||||
# This used to segfault because of a bug in a
|
||||
# function that do not exist anymore.
|
||||
run 0 ../modelcheck -gp $srcdir/finite.gal true
|
||||
Loading…
Add table
Add a link
Reference in a new issue