...
 
Commits (2)
......@@ -9,6 +9,41 @@ New in spot 2.9.0.dev (not yet released)
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
synchronized product. The only work with operands that are
deterministic automata, and build automata whose language are
......
......@@ -202,6 +202,33 @@ AC_CHECK_PROGS([SWIG], [swig3.0 swig], [swig])
AC_SUBST([CROSS_COMPILING], [$cross_compiling])
AC_CANONICAL_HOST
build_linux=no
build_windows=no
build_mac=no
# Detect the target system
case "${host_os}" in
linux*)
build_linux=yes
;;
cygwin*|mingw*)
build_windows=yes
;;
darwin*)
build_mac=yes
;;
*)
AC_MSG_ERROR(["OS $host_os is not supported"])
;;
esac
# Pass the conditionals to automake
AM_CONDITIONAL([LINUX], [test "$build_linux" = "yes"])
AM_CONDITIONAL([WINDOWS], [test "$build_windows" = "yes"])
AM_CONDITIONAL([OSX], [test "$build_mac" = "yes"])
AC_SUBST([GITPATCH], [$(if (git rev-parse) >/dev/null 2>&1; then
echo ".$(git rev-list $(git rev-list --tags='spot-*' --no-walk \
--max-count=1)..HEAD --count)"
......
......@@ -23,7 +23,7 @@
AUTOMAKE_OPTIONS = subdir-objects
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) -lpthread -latomic -DSWIG_TYPE_TABLE=spot
$(BUDDY_CPPFLAGS) -lpthread -DSWIG_TYPE_TABLE=spot
SWIGFLAGS = -c++ -python -py3 -O -MD
......@@ -71,7 +71,7 @@ am__depfiles_remade = ./$(DEPDIR)/buddy_wrap.Plo \
spot__impl_la_SOURCES = spot/impl_wrap.cxx
spot__impl_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS)
spot__impl_la_LIBADD = $(top_builddir)/spot/libspot.la -lpthread -latomic
spot__impl_la_LIBADD = $(top_builddir)/spot/libspot.la -lpthread
am__depfiles_remade += ./spot/$(DEPDIR)/impl_wrap.Pcxx
@AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/impl_wrap.Pcxx@am__quote@ # am--include-marker
......@@ -92,7 +92,7 @@ spot__ltsmin_la_SOURCES = spot/ltsmin_wrap.cxx
spot__ltsmin_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS)
spot__ltsmin_la_LIBADD = $(top_builddir)/spot/libspot.la \
$(top_builddir)/spot/ltsmin/libspotltsmin.la \
-lpthread -latomic
-lpthread
am__depfiles_remade += ./spot/$(DEPDIR)/ltsmin_wrap.Pcxx
@AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/ltsmin_wrap.Pcxx@am__quote@ # am--include-marker
......@@ -111,7 +111,15 @@ spot__gen_la_SOURCES = spot/gen_wrap.cxx
spot__gen_la_LDFLAGS = -avoid-version -module $(SYMBOLIC_LDFLAGS)
spot__gen_la_LIBADD = $(top_builddir)/spot/libspot.la \
$(top_builddir)/spot/gen/libspotgen.la \
-lpthread -latomic
-lpthread
if !OSX
AM_CPPFLAGS += -latomic
spot__impl_la_LIBADD += -latomic
spot__ltsmin_la_LIBADD += -latomic
spot__gen_la_LIBADD += -latomic
endif
am__depfiles_remade += ./spot/$(DEPDIR)/gen_wrap.Pcxx
@AMDEP_TRUE@@am__include@ @am__quote@./spot/$(DEPDIR)/gen_wrap.Pcxx@am__quote@ # am--include-marker
......
......@@ -27,7 +27,7 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) \
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
LDADD = $(top_builddir)/spot/libspot.la \
$(top_builddir)/buddy/src/libbddx.la \
$(LIBLTDL) -lpthread -latomic
$(LIBLTDL) -lpthread
# Explicitely set it to avoid default value ".test"
TEST_EXTENSIONS =
......@@ -461,7 +461,7 @@ check_PROGRAMS += ltsmin/modelcheck
check_PROGRAMS += ltsmin/testconvert
ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread -latomic
ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread
ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc
ltsmin_modelcheck_LDADD = \
$(top_builddir)/bin/libcommon.a \
......@@ -471,7 +471,15 @@ ltsmin_modelcheck_LDADD = \
ltsmin_testconvert_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
ltsmin_testconvert_CXXFLAGS = $(CXXFLAGS) -pthread -latomic
ltsmin_testconvert_CXXFLAGS = $(CXXFLAGS) -pthread
if !OSX
LDADD += -latomic
ltsmin_modelcheck_CXXFLAGS += -latomic
ltsmin_testconvert_ += -latomic
endif
ltsmin_testconvert_SOURCES = ltsmin/testconvert.cc
ltsmin_testconvert_LDADD = \
$(top_builddir)/bin/libcommon.a \
......