diff --git a/README b/README index 98cfb407c..556ae764f 100644 --- a/README +++ b/README @@ -180,7 +180,7 @@ wrap/ Wrappers for other languages. tests/ Tests for these bindings ajax/ LTL-to-TGBA translator with web interface, using Ajax. iface/ Interfaces to other libraries. - dve2/ Interface with DiVinE2. + ltsmin/ Interface with DiVinE2 and SpinS. Third party software -------------------- diff --git a/configure.ac b/configure.ac index fb70d3f1c..eb6bfa0a3 100644 --- a/configure.ac +++ b/configure.ac @@ -169,8 +169,8 @@ AC_CONFIG_FILES([ doc/Makefile doc/tl/Makefile doc/org/init.el - iface/dve2/defs - iface/dve2/Makefile + iface/ltsmin/defs + iface/ltsmin/Makefile iface/Makefile lib/Makefile src/bin/Makefile diff --git a/iface/Makefile.am b/iface/Makefile.am index 743d3e53a..65c23d35b 100644 --- a/iface/Makefile.am +++ b/iface/Makefile.am @@ -17,4 +17,4 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -SUBDIRS = dve2 +SUBDIRS = ltsmin diff --git a/iface/dve2/finite.test b/iface/dve2/finite.test deleted file mode 100755 index a608df512..000000000 --- a/iface/dve2/finite.test +++ /dev/null @@ -1,57 +0,0 @@ -#!/bin/sh -# Copyright (C) 2011, 2013 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 - -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 ../dve2check -gm $srcdir/finite.dve '"P.a < 10"' > stdout -test `grep ' -> ' stdout | wc -l` = 25 -test `grep 'P.a=' stdout | wc -l` = 15 - -run 0 ../dve2check -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2 -cmp stdout stdout2 - -run 0 ../dve2check -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 ../dve2check -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 ../dve2check -ddead -E $srcdir/finite.dve \ - '!(G(dead -> ("P.a==3" | "P.b==3")))' - -run 0 ../dve2check -ddead -e $srcdir/finite.dve \ - '!(G(dead -> ("P.a==2" | "P.b==3")))' - -# This used to segfault because of a bug in -# tgba_product::transition_annotation. -run 0 ../dve2check -gp $srcdir/finite.dve true diff --git a/iface/dve2/.gitignore b/iface/ltsmin/.gitignore similarity index 61% rename from iface/dve2/.gitignore rename to iface/ltsmin/.gitignore index 1f7c4c17b..992655b40 100644 --- a/iface/dve2/.gitignore +++ b/iface/ltsmin/.gitignore @@ -1,5 +1,7 @@ *.dve2C *.dve.cpp -dve2check defs *.dir +*.spins +*.c +check diff --git a/iface/dve2/Makefile.am b/iface/ltsmin/Makefile.am similarity index 78% rename from iface/dve2/Makefile.am rename to iface/ltsmin/Makefile.am index 57a255db7..38a5209e6 100644 --- a/iface/dve2/Makefile.am +++ b/iface/ltsmin/Makefile.am @@ -18,26 +18,26 @@ AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src \ $(BUDDY_CPPFLAGS) -I$(top_srcdir)/ltdl -AM_CXXFLAGS = $(WARNING_CXXFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) -lpthread -dve2dir = $(pkgincludedir)/iface/dve2 +ltsmindir = $(pkgincludedir)/iface/ltsmin -dve2_HEADERS = dve2.hh +ltsmin_HEADERS = ltsmin.hh -lib_LTLIBRARIES = libspotdve2.la -libspotdve2_la_LIBADD = \ +lib_LTLIBRARIES = libspotltsmin.la +libspotltsmin_la_LIBADD = \ $(top_builddir)/src/libspot.la \ $(top_builddir)/ltdl/libltdlc.la -libspotdve2_la_SOURCES = dve2.cc +libspotltsmin_la_SOURCES = ltsmin.cc -noinst_PROGRAMS = dve2check +noinst_PROGRAMS = modelcheck -dve2check_SOURCES = dve2check.cc -dve2check_LDADD = libspotdve2.la +modelcheck_SOURCES = modelcheck.cc +modelcheck_LDADD = libspotltsmin.la check_SCRIPTS = defs -TESTS = dve2check.test finite.test kripke.test +TESTS = check.test finite.test kripke.test EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve kripke.test: $(top_builddir)/src/kripketest/parse_print$(EXEEXT) diff --git a/iface/dve2/README b/iface/ltsmin/README similarity index 80% rename from iface/dve2/README rename to iface/ltsmin/README index 9469940cf..c931a4990 100644 --- a/iface/dve2/README +++ b/iface/ltsmin/README @@ -1,5 +1,5 @@ -This directory contains an interface that presents DiVinE models as -kripke* objects for Spot. +This directory contains an interface that presents DiVinE and PROMELA +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 @@ -9,16 +9,12 @@ processes synchonizing through channels 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. +The LTSmin people [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. @@ -47,14 +43,32 @@ 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 "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 it will - load "model.dve2C" dynamically. + 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 @@ -89,15 +103,15 @@ Usage with Spot "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 + 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 - express using only alphanumeric characters (plus `_' and `.') should - be enclosed in double quote. + 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 diff --git a/iface/dve2/beem-peterson.4.dve b/iface/ltsmin/beem-peterson.4.dve similarity index 100% rename from iface/dve2/beem-peterson.4.dve rename to iface/ltsmin/beem-peterson.4.dve diff --git a/iface/dve2/dve2check.test b/iface/ltsmin/check.test similarity index 70% rename from iface/dve2/dve2check.test rename to iface/ltsmin/check.test index cb1f18b83..05ecf8855 100755 --- a/iface/dve2/dve2check.test +++ b/iface/ltsmin/check.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -29,32 +29,47 @@ else 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.). - ../dve2check $opt -E $srcdir/beem-peterson.4.dve \ + ../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. - ../dve2check $opt -E $srcdir/beem-peterson.4.dve \ + ../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 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \ + run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve \ '!G(P_0.wait -> F P_0.CS)' - run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' + run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' done # Now check some error messages. -run 1 ../dve2check foo.dve "F(P_0.CS)" 2>stderr +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 ../dve2check beem-peterson.4.dve2C \ +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 diff --git a/iface/dve2/defs.in b/iface/ltsmin/defs.in similarity index 100% rename from iface/dve2/defs.in rename to iface/ltsmin/defs.in diff --git a/iface/ltsmin/elevator2.1.pm b/iface/ltsmin/elevator2.1.pm new file mode 100644 index 000000000..0249bec6f --- /dev/null +++ b/iface/ltsmin/elevator2.1.pm @@ -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 {tp;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; +} + diff --git a/iface/dve2/finite.dve b/iface/ltsmin/finite.dve similarity index 100% rename from iface/dve2/finite.dve rename to iface/ltsmin/finite.dve diff --git a/iface/ltsmin/finite.pm b/iface/ltsmin/finite.pm new file mode 100644 index 000000000..17c1dd88e --- /dev/null +++ b/iface/ltsmin/finite.pm @@ -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; +} diff --git a/iface/ltsmin/finite.test b/iface/ltsmin/finite.test new file mode 100755 index 000000000..d8c69e447 --- /dev/null +++ b/iface/ltsmin/finite.test @@ -0,0 +1,90 @@ +#!/bin/sh +# Copyright (C) 2011, 2013 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 + +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 +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 +# tgba_product::transition_annotation. +run 0 ../modelcheck -gp $srcdir/finite.dve true + +# Same tests with finite.pm. +# Compile it beforehand to avoid compiler's output interference. +spins $srcdir/finite.pm +run 0 ../modelcheck -gm $srcdir/finite.pm.spins '"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.spins '"P_0.a < 10"' > stdout2 +diff stdout stdout2 + +run 0 ../modelcheck -dfalse -gm $srcdir/finite.pm.spins '"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.spins '"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.spins \ + '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))' + +run 0 ../modelcheck -ddead -e $srcdir/finite.pm.spins \ + '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))' + +run 0 ../modelcheck -gp $srcdir/finite.pm.spins true diff --git a/iface/dve2/kripke.test b/iface/ltsmin/kripke.test similarity index 88% rename from iface/dve2/kripke.test rename to iface/ltsmin/kripke.test index 7ac73f3bc..a9ddde0bc 100755 --- a/iface/dve2/kripke.test +++ b/iface/ltsmin/kripke.test @@ -33,10 +33,10 @@ fi set -e -run 0 ../dve2check -gK ${srcdir}/finite.dve 'F("P.a > 5")' > output +run 0 ../modelcheck -gK ${srcdir}/finite.dve 'F("P.a > 5")' > output run 0 ${top_builddir}/src/kripketest/parse_print output | tr -d '"' > output2 tr -d '"' < output >outputF cmp outputF output2 -../dve2check -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP +../modelcheck -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP ${top_builddir}/src/tgbatest/ltl2tgba -e -KPoutputP '!G("pos[1] < 3")' diff --git a/iface/dve2/dve2.cc b/iface/ltsmin/ltsmin.cc similarity index 79% rename from iface/dve2/dve2.cc rename to iface/ltsmin/ltsmin.cc index 9122f1796..b3cdcb3c7 100644 --- a/iface/dve2/dve2.cc +++ b/iface/ltsmin/ltsmin.cc @@ -30,21 +30,20 @@ # define WEXITSTATUS(x) ((x) & 0xff) #endif -#include "dve2.hh" +#include "ltsmin.hh" #include "misc/hashfunc.hh" #include "misc/fixpool.hh" #include "misc/mspool.hh" #include "misc/intvcomp.hh" #include "misc/intvcmp2.hh" - namespace spot { namespace { //////////////////////////////////////////////////////////////////////// - // DVE2 --ltsmin interface + // spins interface typedef struct transition_info { int* labels; // edge labels, NULL, or pointer to the edge label(s) @@ -55,29 +54,27 @@ namespace spot transition_info_t *transition_info, int *dst); - struct dve2_interface + struct spins_interface { lt_dlhandle handle; // handle to the dynamic library void (*get_initial_state)(void *to); int (*have_property)(); int (*get_successors)(void* m, int *in, TransitionCB, void *arg); - - int (*get_state_variable_count)(); + int (*get_state_size)(); const char* (*get_state_variable_name)(int var); int (*get_state_variable_type)(int var); - int (*get_state_variable_type_count)(); - const char* (*get_state_variable_type_name)(int type); - int (*get_state_variable_type_value_count)(int type); - const char* (*get_state_variable_type_value)(int type, int value); - int (*get_transition_count)(); + int (*get_type_count)(); + const char* (*get_type_name)(int type); + int (*get_type_value_count)(int type); + const char* (*get_type_value_name)(int type, int value); }; //////////////////////////////////////////////////////////////////////// // STATE - struct dve2_state: public state + struct spins_state: public state { - dve2_state(int s, fixed_size_pool* p) + spins_state(int s, fixed_size_pool* p) : pool(p), size(s), count(1) { } @@ -89,10 +86,10 @@ namespace spot hash_value = wang32_hash(hash_value ^ vars[i]); } - dve2_state* clone() const + spins_state* clone() const { ++count; - return const_cast(this); + return const_cast(this); } void destroy() const @@ -111,7 +108,7 @@ namespace spot { if (this == other) return 0; - const dve2_state* o = down_cast(other); + const spins_state* o = down_cast(other); assert(o); if (hash_value < o->hash_value) return -1; @@ -122,7 +119,7 @@ namespace spot private: - ~dve2_state() + ~spins_state() { } @@ -134,9 +131,9 @@ namespace spot int vars[0]; }; - struct dve2_compressed_state: public state + struct spins_compressed_state: public state { - dve2_compressed_state(int s, multiple_size_pool* p) + spins_compressed_state(int s, multiple_size_pool* p) : pool(p), size(s), count(1) { } @@ -148,10 +145,10 @@ namespace spot hash_value = wang32_hash(hash_value ^ vars[i]); } - dve2_compressed_state* clone() const + spins_compressed_state* clone() const { ++count; - return const_cast(this); + return const_cast(this); } void destroy() const @@ -170,8 +167,8 @@ namespace spot { if (this == other) return 0; - const dve2_compressed_state* o = - down_cast(other); + const spins_compressed_state* o = + down_cast(other); assert(o); if (hash_value < o->hash_value) return -1; @@ -188,7 +185,7 @@ namespace spot private: - ~dve2_compressed_state() + ~spins_compressed_state() { } @@ -223,8 +220,8 @@ namespace spot { callback_context* ctx = static_cast(arg); fixed_size_pool* p = static_cast(ctx->pool); - dve2_state* out = - new(p->allocate()) dve2_state(ctx->state_size, p); + spins_state* out = + new(p->allocate()) spins_state(ctx->state_size, p); memcpy(out->vars, dst, ctx->state_size * sizeof(int)); out->compute_hash(); ctx->transitions.push_back(out); @@ -238,9 +235,9 @@ namespace spot size_t csize = ctx->state_size * 2; ctx->compress(dst, ctx->state_size, ctx->compressed, csize); - void* mem = p->allocate(sizeof(dve2_compressed_state) + void* mem = p->allocate(sizeof(spins_compressed_state) + sizeof(int) * csize); - dve2_compressed_state* out = new(mem) dve2_compressed_state(csize, p); + spins_compressed_state* out = new(mem) spins_compressed_state(csize, p); memcpy(out->vars, ctx->compressed, csize * sizeof(int)); out->compute_hash(); ctx->transitions.push_back(out); @@ -249,11 +246,11 @@ namespace spot //////////////////////////////////////////////////////////////////////// // SUCC_ITERATOR - class dve2_succ_iterator: public kripke_succ_iterator + class spins_succ_iterator: public kripke_succ_iterator { public: - dve2_succ_iterator(const callback_context* cc, + spins_succ_iterator(const callback_context* cc, bdd cond) : kripke_succ_iterator(cond), cc_(cc) { @@ -266,7 +263,7 @@ namespace spot kripke_succ_iterator::recycle(cond); } - ~dve2_succ_iterator() + ~spins_succ_iterator() { delete cc_; } @@ -327,14 +324,14 @@ namespace spot int convert_aps(const ltl::atomic_prop_set* aps, - const dve2_interface* d, + const spins_interface* d, bdd_dict_ptr dict, const ltl::formula* dead, prop_set& out) { int errors = 0; - int state_size = d->get_state_variable_count(); + int state_size = d->get_state_size(); typedef std::map val_map_t; val_map_t val_map; @@ -346,14 +343,14 @@ namespace spot val_map[name] = v; } - int type_count = d->get_state_variable_type_count(); + int type_count = d->get_type_count(); typedef std::map enum_map_t; std::vector enum_map(type_count); for (int i = 0; i < type_count; ++i) { - int enum_count = d->get_state_variable_type_value_count(i); + int enum_count = d->get_type_value_count(i); for (int j = 0; j < enum_count; ++j) - enum_map[i].emplace(d->get_state_variable_type_value(i, j), j); + enum_map[i].emplace(d->get_type_value_name(i, j), j); } for (ltl::atomic_prop_set::const_iterator ap = aps->begin(); @@ -600,15 +597,15 @@ namespace spot //////////////////////////////////////////////////////////////////////// // KRIPKE - class dve2_kripke: public kripke + class spins_kripke: public kripke { public: - dve2_kripke(const dve2_interface* d, const bdd_dict_ptr& dict, + spins_kripke(const spins_interface* d, const bdd_dict_ptr& dict, const prop_set* ps, const ltl::formula* dead, int compress) : kripke(dict), d_(d), - state_size_(d_->get_state_variable_count()), + state_size_(d_->get_state_size()), dict_(dict), ps_(ps), compress_(compress == 0 ? 0 : compress == 1 ? int_array_array_compress @@ -618,8 +615,8 @@ namespace spot : int_array_array_decompress2), uncompressed_(compress ? new int[state_size_ + 30] : 0), compressed_(compress ? new int[state_size_ * 2] : 0), - statepool_(compress ? sizeof(dve2_compressed_state) : - (sizeof(dve2_state) + state_size_ * sizeof(int))), + statepool_(compress ? sizeof(spins_compressed_state) : + (sizeof(spins_state) + state_size_ * sizeof(int))), state_condition_last_state_(0), state_condition_last_cc_(0) { vname_ = new const char*[state_size_]; @@ -632,7 +629,7 @@ namespace spot // output. int type = d->get_state_variable_type(i); format_filter_[i] = - (d->get_state_variable_type_value_count(type) != 1); + (d->get_type_value_count(type) != 1); } // Register the "dead" proposition. There are three cases to @@ -666,7 +663,7 @@ namespace spot } } - ~dve2_kripke() + ~spins_kripke() { if (iter_cache_) { @@ -704,10 +701,10 @@ namespace spot multiple_size_pool* p = const_cast(&compstatepool_); - void* mem = p->allocate(sizeof(dve2_compressed_state) + void* mem = p->allocate(sizeof(spins_compressed_state) + sizeof(int) * csize); - dve2_compressed_state* res = new(mem) - dve2_compressed_state(csize, p); + spins_compressed_state* res = new(mem) + spins_compressed_state(csize, p); memcpy(res->vars, compressed_, csize * sizeof(int)); res->compute_hash(); return res; @@ -715,7 +712,7 @@ namespace spot else { fixed_size_pool* p = const_cast(&statepool_); - dve2_state* res = new(p->allocate()) dve2_state(state_size_, p); + spins_state* res = new(p->allocate()) spins_state(state_size_, p); d_->get_initial_state(res->vars); res->compute_hash(); return res; @@ -828,8 +825,8 @@ namespace spot const int* vars; if (compress_) { - const dve2_compressed_state* s = - down_cast(st); + const spins_compressed_state* s = + down_cast(st); assert(s); decompress_(s->vars, s->size, uncompressed_, state_size_); @@ -837,7 +834,7 @@ namespace spot } else { - const dve2_state* s = down_cast(st); + const spins_state* s = down_cast(st); assert(s); vars = s->vars; } @@ -846,7 +843,7 @@ namespace spot virtual - dve2_succ_iterator* + spins_succ_iterator* succ_iter(const state* st) const { // This may also compute successors in state_condition_last_cc @@ -870,13 +867,13 @@ namespace spot if (iter_cache_) { - dve2_succ_iterator* it = - down_cast(iter_cache_); + spins_succ_iterator* it = + down_cast(iter_cache_); it->recycle(cc, scond); iter_cache_ = nullptr; return it; } - return new dve2_succ_iterator(cc, scond); + return new spins_succ_iterator(cc, scond); } virtual @@ -920,7 +917,7 @@ namespace spot } private: - const dve2_interface* d_; + const spins_interface* d_; int state_size_; bdd_dict_ptr dict_; const char** vname_; @@ -952,13 +949,32 @@ namespace spot // LOADER - // Call divine to compile "foo.dve" as "foo.dve2C" if the latter + // Call spins to compile "foo.prom" as "foo.prom.spins" if the latter // does not exist already or is older. bool - compile_dve2(std::string& filename, bool verbose) + compile_model(std::string& filename, std::string& ext, bool verbose) { + std::string command; + std::string compiled_ext; - std::string command = "divine compile --ltsmin " + filename; + if (ext == ".prom" || ext == ".pm" || ext == ".pml") + { + command = "spins " + filename; + compiled_ext = ".spins"; + } + else if (ext == ".dve") + { + command = "divine compile --ltsmin " + filename; + compiled_ext = "2C"; + } + else + { + if (verbose) + std::cerr << "Unknown extension `" << ext + << "'. Use `.prom', `.pm', `.pml', `.dve', `.dve2C' or"\ + "`.prom.spins'." << std::endl; + return false; + } struct stat s; if (stat(filename.c_str(), &s) != 0) @@ -971,7 +987,7 @@ namespace spot } std::string old = filename; - filename += "2C"; + filename += compiled_ext; // Remove any directory, because the new file will // be compiled in the current directory. @@ -982,7 +998,7 @@ namespace spot struct stat d; if (stat(filename.c_str(), &d) == 0) if (s.st_mtime < d.st_mtime) - // The dve2C is up-to-date, no need to recompile it. + // The .prom.spins is up-to-date, no need to recompile it. return false; int res = system(command.c_str()); @@ -997,9 +1013,8 @@ namespace spot return false; } - kripke_ptr - load_dve2(const std::string& file_arg, const bdd_dict_ptr& dict, + load_model(const std::string& file_arg, const bdd_dict_ptr& dict, const ltl::atomic_prop_set* to_observe, const ltl::formula* dead, int compress, @@ -1012,22 +1027,15 @@ namespace spot file = "./" + file_arg; std::string ext = file.substr(file.find_last_of(".")); - if (ext == ".dve") + if (ext != ".spins" && ext != ".dve2C") { - if (compile_dve2(file, verbose)) - { - if (verbose) - std::cerr << "Failed to compile `" << file_arg - << "'." << std::endl; - return 0; - } - } - else if (ext != ".dve2C") - { - if (verbose) - std::cerr << "Unknown extension `" << ext - << "'. Use `.dve' or `.dve2C'." << std::endl; - return 0; + if (compile_model(file, ext, verbose)) + { + if (verbose) + std::cerr << "Failed to compile `" << file_arg + << "'." << std::endl; + return 0; + } } if (lt_dlinit()) @@ -1046,43 +1054,66 @@ namespace spot return 0; } - dve2_interface* d = new dve2_interface; + spins_interface* d = new spins_interface; d->handle = h; - 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_variable_count = (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_state_variable_type_count = (int (*)()) - lt_dlsym(h, "get_state_variable_type_count"); - d->get_state_variable_type_name = (const char* (*)(int)) - lt_dlsym(h, "get_state_variable_type_name"); - d->get_state_variable_type_value_count = (int (*)(int)) - lt_dlsym(h, "get_state_variable_type_value_count"); - d->get_state_variable_type_value = (const char* (*)(int, int)) - lt_dlsym(h, "get_state_variable_type_value"); - d->get_transition_count = (int (*)()) - lt_dlsym(h, "get_transition_count"); + // SpinS interface. + if ((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"); + d->get_state_size = (int (*)()) + lt_dlsym(h, "spins_get_state_size"); + d->get_state_variable_name = (const char* (*)(int)) + lt_dlsym(h, "spins_get_state_variable_name"); + d->get_state_variable_type = (int (*)(int)) + lt_dlsym(h, "spins_get_state_variable_type"); + d->get_type_count = (int (*)()) + lt_dlsym(h, "spins_get_type_count"); + d->get_type_name = (const char* (*)(int)) + lt_dlsym(h, "spins_get_type_name"); + d->get_type_value_count = (int (*)(int)) + lt_dlsym(h, "spins_get_type_value_count"); + d->get_type_value_name = (const char* (*)(int, int)) + lt_dlsym(h, "spins_get_type_value_name"); + } + // dve2 interface. + else + { + 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"); + } - if (!(d->get_initial_state - && d->have_property + if (!( + d->get_initial_state && d->get_successors - && d->get_state_variable_count + && d->get_state_size && d->get_state_variable_name && d->get_state_variable_type - && d->get_state_variable_type_count - && d->get_state_variable_type_name - && d->get_state_variable_type_value_count - && d->get_state_variable_type_value - && d->get_transition_count)) + && d->get_type_count + && d->get_type_name + && d->get_type_value_count + && d->get_type_value_name)) { if (verbose) std::cerr << "Failed to resolve some symbol while loading `" @@ -1092,14 +1123,14 @@ namespace spot return 0; } - if (d->have_property()) + if (d->have_property && d->have_property()) { - if (verbose) - std::cerr << "Model with an embedded property are not supported." - << std::endl; - delete d; - lt_dlexit(); - return 0; + if (verbose) + std::cerr << "Model with an embedded property are not supported." + << std::endl; + delete d; + lt_dlexit(); + return 0; } prop_set* ps = new prop_set; @@ -1113,6 +1144,6 @@ namespace spot return 0; } - return std::make_shared(d, dict, ps, dead, compress); + return std::make_shared(d, dict, ps, dead, compress); } } diff --git a/iface/dve2/dve2.hh b/iface/ltsmin/ltsmin.hh similarity index 81% rename from iface/dve2/dve2.hh rename to iface/ltsmin/ltsmin.hh index 26c274fa3..f451237a0 100644 --- a/iface/dve2/dve2.hh +++ b/iface/ltsmin/ltsmin.hh @@ -17,8 +17,8 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#ifndef SPOT_IFACE_DVE2_DVE2_HH -# define SPOT_IFACE_DVE2_DVE2_HH +#ifndef SPOT_IFACE_PROMELA_PROMELA_HH +# define SPOT_IFACE_PROMELA_PROMELA_HH #include "kripke/kripke.hh" #include "ltlvisit/apcollect.hh" @@ -28,11 +28,11 @@ namespace spot { - // \brief Load a DVE model. + // \brief Load a PROMELA model. // - // The filename given can be either a *.dve source or a *.dve2C - // dynamic library compiled with "divine compile --ltsmin file". - // When the *.dve source is supplied, the *.dve2C will be updated + // The filename given can be either a *.prom source or a *.spins + // dynamic library compiled with "spins file". + // When the *.prom source is supplied, the *.spins will be updated // only if it is not newer. // // The dead parameter is used to control the behavior of the model @@ -48,8 +48,7 @@ namespace spot // // This function returns 0 on error. // - // \a file the name of the *.dve source file or of the *.dve2C - // dynamic library + // \a file the name of the *.prom source file or the dynamic library // \a to_observe the list of atomic propositions that should be observed // in the model // \a dict the BDD dictionary to use @@ -57,10 +56,10 @@ namespace spot // dead states // \a verbose whether to output verbose messages SPOT_API kripke_ptr - load_dve2(const std::string& file, const bdd_dict_ptr& dict, + load_model(const std::string& file, const bdd_dict_ptr& dict, const ltl::atomic_prop_set* to_observe, const ltl::formula* dead = ltl::constant::true_instance(), int compress = 0, bool verbose = true); } -#endif // SPOT_IFACE_DVE2_DVE2_HH +#endif // SPOT_IFACE_PROMELA_PROMELA_HH diff --git a/iface/dve2/dve2check.cc b/iface/ltsmin/modelcheck.cc similarity index 97% rename from iface/dve2/dve2check.cc rename to iface/ltsmin/modelcheck.cc index 821203264..dfff70e7c 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/ltsmin/modelcheck.cc @@ -17,7 +17,7 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include "dve2.hh" +#include "ltsmin.hh" #include "tgbaalgos/dotty.hh" #include "ltlenv/defaultenv.hh" #include "ltlast/allnodes.hh" @@ -217,9 +217,10 @@ checked_main(int argc, char **argv) if (output != DotFormula) { - tm.start("loading dve2"); - model = spot::load_dve2(argv[1], dict, &ap, deadf, compress_states, true); - tm.stop("loading dve2"); + tm.start("loading spins"); + model = spot::load_model(argv[1], dict, &ap, deadf, + compress_states, true); + tm.stop("loading spins"); if (!model) {