...
 
Commits (6)
...@@ -9,6 +9,41 @@ New in spot 2.9.0.dev (not yet released) ...@@ -9,6 +9,41 @@ New in spot 2.9.0.dev (not yet released)
Library: Library:
- Historically, Spot labels automata by Boolean formulas over
atomic propositions. These Boolean formulas are represented
as BDDs using the BuDDy library. Since this implementation is
not thread safe, Spot wasn't able, until now, to integrate
parallel algorithms. To bypass this limitation, we introduce the
cube data structure. This structure aims to replace BDDs
everywhere parallelism is required. Contrary to BDDs, this
structure is not able to represent complex boolean formulae, but
can represent very simple disjunctive form of boolean formulae
and can be used in a multithreaded context.
Since both the BDD-based and the cube-based implementations have
benefits and drawbacks, we opted to keep side-by-side the
historical implementation and the new one. As a consequence:
twacube and kripkecube are the new versions of twa and kripke.
We provide conversion back and forth throught the following
functions: twacube_to_twa, twa_to_twa, product_to_twa, and
kripkecube_to_twa. The equivalence between a twa and a twacube
can be checked using are_equivalent.
In addition to the previous conversion, we implemented various
state-of-the-art algorithms: bloemen.16.ppopp, bloemen.16.hvc,
evangeslita.12.atva, renault.13.lpar, holzmann.11.ieee. In order
to ease the manipulation of these algorithms we introduce a
factory mc_instanciator, that provide a nice abstraction for launching,
pinning, and stopping threads inside of parallel model-checking
algorithms. One should note that for performances and genericity
issues, all these algorithms are templated.
Finally, since all these algorithms are templated, a refactoring
of the ltsmin structure has been done in order to introduce the
spins_interface which describes the functions exported by a PINS
file. With this refactoring, we can retrieve both a kripke or a
kripkecube from a PINS file.
- product_xor() and product_xnor() are two new versions of the - product_xor() and product_xnor() are two new versions of the
synchronized product. The only work with operands that are synchronized product. The only work with operands that are
deterministic automata, and build automata whose language are deterministic automata, and build automata whose language are
......
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2010, 2011, 2013-2019 Laboratoire de Recherche ## Copyright (C) 2010, 2011, 2013-2020 Laboratoire de Recherche
## et Development de l'Epita (LRDE). ## et Development de l'Epita (LRDE).
## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
...@@ -23,7 +23,7 @@ ...@@ -23,7 +23,7 @@
AUTOMAKE_OPTIONS = subdir-objects AUTOMAKE_OPTIONS = subdir-objects
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \ AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) -DSWIG_TYPE_TABLE=spot $(BUDDY_CPPFLAGS) -lpthread -latomic -DSWIG_TYPE_TABLE=spot
SWIGFLAGS = -c++ -python -py3 -O -MD SWIGFLAGS = -c++ -python -py3 -O -MD
...@@ -71,7 +71,7 @@ am__depfiles_remade = ./$(DEPDIR)/buddy_wrap.Plo \ ...@@ -71,7 +71,7 @@ am__depfiles_remade = ./$(DEPDIR)/buddy_wrap.Plo \
spot__impl_la_SOURCES = spot/impl_wrap.cxx spot__impl_la_SOURCES = spot/impl_wrap.cxx
spot__impl_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS) spot__impl_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS)
spot__impl_la_LIBADD = $(top_builddir)/spot/libspot.la spot__impl_la_LIBADD = $(top_builddir)/spot/libspot.la -lpthread -latomic
am__depfiles_remade += ./spot/$(DEPDIR)/impl_wrap.Pcxx am__depfiles_remade += ./spot/$(DEPDIR)/impl_wrap.Pcxx
@AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/impl_wrap.Pcxx@am__quote@ # am--include-marker @AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/impl_wrap.Pcxx@am__quote@ # am--include-marker
...@@ -91,7 +91,8 @@ spot/impl.py: spot/impl.i ...@@ -91,7 +91,8 @@ spot/impl.py: spot/impl.i
spot__ltsmin_la_SOURCES = spot/ltsmin_wrap.cxx spot__ltsmin_la_SOURCES = spot/ltsmin_wrap.cxx
spot__ltsmin_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS) spot__ltsmin_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS)
spot__ltsmin_la_LIBADD = $(top_builddir)/spot/libspot.la \ spot__ltsmin_la_LIBADD = $(top_builddir)/spot/libspot.la \
$(top_builddir)/spot/ltsmin/libspotltsmin.la $(top_builddir)/spot/ltsmin/libspotltsmin.la \
-lpthread -latomic
am__depfiles_remade += ./spot/$(DEPDIR)/ltsmin_wrap.Pcxx am__depfiles_remade += ./spot/$(DEPDIR)/ltsmin_wrap.Pcxx
@AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/ltsmin_wrap.Pcxx@am__quote@ # am--include-marker @AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/ltsmin_wrap.Pcxx@am__quote@ # am--include-marker
...@@ -109,7 +110,8 @@ spot/ltsmin.py: spot/ltsmin.i ...@@ -109,7 +110,8 @@ spot/ltsmin.py: spot/ltsmin.i
spot__gen_la_SOURCES = spot/gen_wrap.cxx spot__gen_la_SOURCES = spot/gen_wrap.cxx
spot__gen_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS) spot__gen_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS)
spot__gen_la_LIBADD = $(top_builddir)/spot/libspot.la \ spot__gen_la_LIBADD = $(top_builddir)/spot/libspot.la \
$(top_builddir)/spot/gen/libspotgen.la $(top_builddir)/spot/gen/libspotgen.la \
-lpthread -latomic
am__depfiles_remade += ./spot/$(DEPDIR)/gen_wrap.Pcxx am__depfiles_remade += ./spot/$(DEPDIR)/gen_wrap.Pcxx
@AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/gen_wrap.Pcxx@am__quote@ # am--include-marker @AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/gen_wrap.Pcxx@am__quote@ # am--include-marker
......
...@@ -79,12 +79,10 @@ namespace spot ...@@ -79,12 +79,10 @@ namespace spot
template<typename algo_name, typename kripke_ptr, typename State, template<typename algo_name, typename kripke_ptr, typename State,
typename Iterator, typename Hash, typename Equal> typename Iterator, typename Hash, typename Equal>
static SPOT_API ec_stats instanciate(kripke_ptr sys, static ec_stats instanciate(kripke_ptr sys,
spot::twacube_ptr prop = nullptr, spot::twacube_ptr prop = nullptr,
bool trace = false) bool trace = false)
{ {
// FIXME ensure that algo_name contains all methods
spot::timer_map tm; spot::timer_map tm;
std::atomic<bool> stop(false); std::atomic<bool> stop(false);
unsigned nbth = sys->get_threads(); unsigned nbth = sys->get_threads();
...@@ -246,5 +244,6 @@ namespace spot ...@@ -246,5 +244,6 @@ namespace spot
return instanciate<spot::lpar13<State, Iterator, Hash, Equal>, return instanciate<spot::lpar13<State, Iterator, Hash, Equal>,
kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace); kripke_ptr, State, Iterator, Hash, Equal> (sys, prop, trace);
} }
SPOT_UNREACHABLE();
} }
} }
...@@ -27,7 +27,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \ ...@@ -27,7 +27,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
AM_CXXFLAGS = $(WARNING_CXXFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = $(top_builddir)/spot/libspot.la \ LDADD = $(top_builddir)/spot/libspot.la \
$(top_builddir)/buddy/src/libbddx.la \ $(top_builddir)/buddy/src/libbddx.la \
$(LIBLTDL) -lpthread $(LIBLTDL) -lpthread -latomic
# Explicitely set it to avoid default value ".test" # Explicitely set it to avoid default value ".test"
TEST_EXTENSIONS = TEST_EXTENSIONS =
...@@ -461,7 +461,7 @@ check_PROGRAMS += ltsmin/modelcheck ...@@ -461,7 +461,7 @@ check_PROGRAMS += ltsmin/modelcheck
check_PROGRAMS += ltsmin/testconvert check_PROGRAMS += ltsmin/testconvert
ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib $(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread -latomic
ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc
ltsmin_modelcheck_LDADD = \ ltsmin_modelcheck_LDADD = \
$(top_builddir)/bin/libcommon.a \ $(top_builddir)/bin/libcommon.a \
...@@ -471,12 +471,13 @@ ltsmin_modelcheck_LDADD = \ ...@@ -471,12 +471,13 @@ ltsmin_modelcheck_LDADD = \
ltsmin_testconvert_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ ltsmin_testconvert_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib $(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
ltsmin_testconvert_CXXFLAGS = $(CXXFLAGS) -pthread ltsmin_testconvert_CXXFLAGS = $(CXXFLAGS) -pthread -latomic
ltsmin_testconvert_SOURCES = ltsmin/testconvert.cc ltsmin_testconvert_SOURCES = ltsmin/testconvert.cc
ltsmin_testconvert_LDADD = \ ltsmin_testconvert_LDADD = \
$(top_builddir)/bin/libcommon.a \ $(top_builddir)/bin/libcommon.a \
$(top_builddir)/lib/libgnu.la \ $(top_builddir)/lib/libgnu.la \
$(top_builddir)/spot/libspot.la \ $(top_builddir)/spot/libspot.la \
$(top_builddir)/buddy/src/libbddx.la \
$(top_builddir)/spot/ltsmin/libspotltsmin.la $(top_builddir)/spot/ltsmin/libspotltsmin.la
......
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017, 2019 Laboratoire # Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017, 2019, 2020 Laboratoire
# de Recherche et Développement de l'Epita (LRDE). # de Recherche et Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
...@@ -82,26 +82,29 @@ grep 'Unexpected' stderr ...@@ -82,26 +82,29 @@ grep 'Unexpected' stderr
# Test Deadlock # Test Deadlock
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--csv --has-deadlock -p 1 >stdout --csv --has-deadlock -p 1 | grep -v Thread > stdout
test `grep "#" stdout | awk -F',' '{print $5}'` = "no_deadlock" test `grep "#" stdout | awk -F',' '{print $5}'` = "no_deadlock"
# Test Bloemen # Test Bloemen
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--csv --bloemen -p 1 >stdout --csv --bloemen -p 1 | grep -v Thread > stdout
test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115 test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115
# Test Bloemen # Test Bloemen
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--csv --bloemen -p 3 >stdout --csv --bloemen -p 3 | grep -v Thread > stdout
test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115 test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --bloemen-ec -p 3 >stdout --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv \
--bloemen-ec -p 3 | grep -v Thread > stdout
# Test CNDFS # Test CNDFS
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --cndfs -p 3 >stdout --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv \
--cndfs -p 3 | grep -v Thread >stdout
# Test SWARMING # Test SWARMING
run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv --swarming -p 3 >stdout --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv \
--swarming -p 3 | grep -v Thread > stdout
...@@ -33,7 +33,7 @@ fi ...@@ -33,7 +33,7 @@ fi
set -e set -e
run 0 ../testconvert $srcdir/finite.dve 'true' > output run 0 ../testconvert $srcdir/finite.dve 'true' | grep -v Thread > output
cat << EOF > expected cat << EOF > expected
[CUBE] Model: 15,24 [CUBE] Model: 15,24
[BDD] Model: 15,24 [BDD] Model: 15,24
...@@ -43,7 +43,7 @@ EOF ...@@ -43,7 +43,7 @@ EOF
cmp output expected cmp output expected
run 0 ../testconvert $srcdir/finite.dve 'G "P.a==5"' > output run 0 ../testconvert $srcdir/finite.dve 'G "P.a==5"'| grep -v Thread > output
cat << EOF > expected cat << EOF > expected
[CUBE] Model: 15,24 [CUBE] Model: 15,24
[BDD] Model: 15,24 [BDD] Model: 15,24
......