From c9aabcddabc6b843ccf93b4c651287f4c7dec505 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Tue, 22 Nov 2016 10:44:20 +0100 Subject: [PATCH] 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. --- spot/ltsmin/ltsmin.cc | 43 ++++++++-- tests/Makefile.am | 8 +- tests/ltsmin/beem-peterson.4.gal | 135 +++++++++++++++++++++++++++++++ tests/ltsmin/check.test | 17 ++++ tests/ltsmin/finite.gal | 19 +++++ tests/ltsmin/finite3.test | 55 +++++++++++++ 6 files changed, 268 insertions(+), 9 deletions(-) create mode 100644 tests/ltsmin/beem-peterson.4.gal create mode 100755 tests/ltsmin/finite.gal create mode 100755 tests/ltsmin/finite3.test diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index d90a7b8d1..955aaaf01 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -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*)) diff --git a/tests/Makefile.am b/tests/Makefile.am index 682be915c..43fc73db5 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 = \ diff --git a/tests/ltsmin/beem-peterson.4.gal b/tests/ltsmin/beem-peterson.4.gal new file mode 100644 index 000000000..534b1933a --- /dev/null +++ b/tests/ltsmin/beem-peterson.4.gal @@ -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; + +} diff --git a/tests/ltsmin/check.test b/tests/ltsmin/check.test index 2f89c8a1a..fe1e7f919 100755 --- a/tests/ltsmin/check.test +++ b/tests/ltsmin/check.test @@ -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 diff --git a/tests/ltsmin/finite.gal b/tests/ltsmin/finite.gal new file mode 100755 index 000000000..91d489e7b --- /dev/null +++ b/tests/ltsmin/finite.gal @@ -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 ); + } + + +} + + diff --git a/tests/ltsmin/finite3.test b/tests/ltsmin/finite3.test new file mode 100755 index 000000000..0f9e430eb --- /dev/null +++ b/tests/ltsmin/finite3.test @@ -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 . + + +. ./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