From 2fb93faa4ed3c07f5ea47d5fcc35c67b5c7cbeeb Mon Sep 17 00:00:00 2001 From: Michael Weber Date: Thu, 25 Mar 2010 21:44:03 +0000 Subject: [PATCH 01/19] [buddy] Addref in fdd_intaddvarblock * src/fdd.c (fdd_intaddvarblock): Add missing addref. Signed-off-by: Jaco van de Pol Signed-off-by: Michael Weber --- buddy/src/fdd.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/buddy/src/fdd.c b/buddy/src/fdd.c index 46c1ba758..7085530f0 100644 --- a/buddy/src/fdd.c +++ b/buddy/src/fdd.c @@ -954,6 +954,8 @@ int fdd_intaddvarblock(int first, int last, int fixed) res = tmp; } + bdd_addref(res); // Added by Jaco van de Pol, 25 march 2010 + err = bdd_addvarblock(res, fixed); bdd_delref(res); From ba15788a94f9b93da676b14353fc05458a872d46 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Apr 2017 13:23:40 +0200 Subject: [PATCH 02/19] [buddy] fix previous patch * src/fdd.c: C++ comments are not supported in C90. --- buddy/src/fdd.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/buddy/src/fdd.c b/buddy/src/fdd.c index 7085530f0..270d74b14 100644 --- a/buddy/src/fdd.c +++ b/buddy/src/fdd.c @@ -954,7 +954,7 @@ int fdd_intaddvarblock(int first, int last, int fixed) res = tmp; } - bdd_addref(res); // Added by Jaco van de Pol, 25 march 2010 + bdd_addref(res); /* Added by Jaco van de Pol, 25 march 2010 */ err = bdd_addvarblock(res, fixed); From f02ca87f07dcadbd2fa6c8854d4810647403ecfd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Apr 2017 18:46:35 +0200 Subject: [PATCH 03/19] sbacc: fix a serious bug Reported by Thibaud Michaud * spot/twaalgos/sbacc.cc: Do not label rejecting SCCs with the empty mark, as it might be accepting. * tests/core/sbacc.test: Add test cases. * NEWS: Mention the bug. --- NEWS | 5 +++- spot/twaalgos/sbacc.cc | 17 ++++++++++- tests/core/sbacc.test | 65 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 85 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index ea74dac0e..51839d344 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.3.3.dev (not yet released) - Nothing yet. + Bugs fixed: + + - the transformation to state-based acceptance (spot::sbacc()) was + incorrect on automata where the empty acceptance mark is accepting. New in spot 2.3.3 (2017-04-11) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 93acc554c..89df387be 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -22,6 +22,7 @@ #include #include #include +#include namespace spot { @@ -33,6 +34,18 @@ namespace spot throw std::runtime_error ("sbacc() does not support alternation"); + // We will need a mark that is rejecting to mark rejecting states. + // If no such mark exist, our work is actually quite simple: we + // just have to copy the automaton and give it "t" as acceptance + // condition. + auto unsat_mark = old->acc().unsat_mark(); + if (!unsat_mark.first) + { + auto res = make_twa_graph(old, twa::prop_set::all()); + strip_acceptance_here(res); + return res; + } + scc_info si(old); unsigned ns = old->num_states(); @@ -97,7 +110,7 @@ namespace spot { unsigned scc_dst = si.scc_of(t.dst); acc_cond::mark_t acc = 0U; - bool dst_acc = si.is_accepting_scc(scc_dst); + bool dst_acc = !si.is_rejecting_scc(scc_dst); if (maybe_accepting && scc_src == scc_dst) acc = t.acc - common_out[t.src]; else if (dst_acc) @@ -106,6 +119,8 @@ namespace spot acc = one_in[t.dst]; if (dst_acc) acc |= common_out[t.dst]; + else + acc = unsat_mark.second; res->new_edge(one.second, new_state(t.dst, acc), t.cond, one.first.second); } diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 8c080d538..ca960a9ae 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -159,3 +159,68 @@ randltl --weak-fairness -n 20 2 | "$ltl2tgba -H %f | $autfilt -H >%O" test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s` + + +# Test case from Thibaud Michaud. This used to fail, because sbacc() +# would remove acceptance marks from all rejecting SCCS... +cat >tm.hoa < out.hoa +autfilt -q --equivalent-to out.hoa tm.hoa + +# Tautological acceptances are converted to "t" +cat >taut.hoa <expect.hoa < out.hoa +diff out.hoa expect.hoa From 6ac91286991fc845a288ca01eb3b29966752685f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Apr 2017 20:00:46 +0200 Subject: [PATCH 04/19] org: typos * doc/org/concepts.org: Fix some typos. --- doc/org/concepts.org | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/org/concepts.org b/doc/org/concepts.org index f3a8d4d08..1c7632b98 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1126,8 +1126,8 @@ custom destructor as a third parameter to =twa::set_named_prop()=. These properties should be considered short-lived. They are usually not propagated to new automata that are created via transformation, -unless the algorithme has been explicitely implemented to preserve -that property. Algorithm that update the automaton in place should +unless the algorithm has been explicitly implemented to preserve that +property. Algorithms that update the automaton in place should probably call =release_named_properties()= to ensure they do not inadvertently keep a stale property. From aff3d09015308e03294ffb6284334b640b653230 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 22 Apr 2017 11:04:32 +0200 Subject: [PATCH 05/19] bin: remove unsupported %b stats from --help * bin/common_aoutput.cc: Here. * NEWS: Mention it. --- NEWS | 3 +++ bin/common_aoutput.cc | 2 -- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 51839d344..53daf5ec5 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,9 @@ New in spot 2.3.3.dev (not yet released) - the transformation to state-based acceptance (spot::sbacc()) was incorrect on automata where the empty acceptance mark is accepting. + - the --help output of randaut and ltl2tgba was showing an + unsupported %b stat. + New in spot 2.3.3 (2017-04-11) Tools: diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 862cc70b5..182caf2ba 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -234,8 +234,6 @@ static const argp_option o_options[] = "number of transitions", 0 }, { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, - { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of acceptance sets", 0 }, { "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "acceptance condition (in HOA syntax)", 0 }, { "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, From cbfb79e343efbdda6dc82b0b175357bb095f62da Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 23 Apr 2017 11:28:28 +0200 Subject: [PATCH 06/19] typos: familly -> family * bench/ltlcounter/README, doc/org/upgrade2.org: Here. --- bench/ltlcounter/README | 2 +- doc/org/upgrade2.org | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/bench/ltlcounter/README b/bench/ltlcounter/README index d3e30ad66..5ccd08ffc 100644 --- a/bench/ltlcounter/README +++ b/bench/ltlcounter/README @@ -16,7 +16,7 @@ describing counters was used to stress many translators. For a description of these formulae, you may also see http://ti.arc.nasa.gov/m/profile/kyrozier/benchmarking_scripts/node5.html -This benchmark used this familly of formulae to plot the performance +This benchmark used this family of formulae to plot the performance of the ltl2tgba_fm algorithm. Studying the behaviour of ltl2tgba_fm on this class of formulae helped us to improve the translation. diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 942b05eaf..6dced8000 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -74,7 +74,7 @@ experience of updating a couple of projects that are using Spot. 7. [[*Various renamings][Several class, functions, and methods, have been renamed]]. Some have been completely reimplemented, with different interfaces. - In particular the =tgba_explicit_*= familly of classes + In particular the =tgba_explicit_*= family of classes (=tgba_explicit_formula=, =tgba_explicit_number=, =tgba_explicit_string= used to encode a TGBA using a graph whose state was named using LTL formulas, integers, or strings) are From b8065a7947b5c25805717a485ce96786ebcb669a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Apr 2017 09:04:27 +0200 Subject: [PATCH 07/19] * doc/org/concepts.org: Typos in property flag names. --- doc/org/concepts.org | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 1c7632b98..f08cbf320 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1059,10 +1059,10 @@ automaton, and that can be queried or set by algorithms: | =state_acc= | automaton should be considered has having state-based acceptance | | =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | | =weak= | transitions of an SCC all belong to the same acceptance sets | -| =very-weak= | weak automaton where all SCCs have size 1 | +| =very_weak= | weak automaton where all SCCs have size 1 | | =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs | | =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | -| =semi-deterministic= | any nondeterminism occurs before entering an accepting SCC | +| =semi_deterministic= | any nondeterminism occurs before entering an accepting SCC | | =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | | =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | From b9ca038850b1735e92d2fc09ab69a892e663410f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 May 2017 10:47:38 +0200 Subject: [PATCH 08/19] [buddy] fix libbddx.pc generation Report from Jeroen Meijer. * src/Makefile.am (libbddx.pc): Depends on Makefile. Use a temporary. Declare in CLEANFILES instead of DISTCLEANFILES. --- buddy/src/Makefile.am | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/buddy/src/Makefile.am b/buddy/src/Makefile.am index 0cab3ddce..5a089a93e 100644 --- a/buddy/src/Makefile.am +++ b/buddy/src/Makefile.am @@ -36,12 +36,12 @@ EXTRA_DIST = $(srcdir)/libbddx.pc.in pkgconfigdir = $(libdir)/pkgconfig nodist_pkgconfig_DATA = libbddx.pc -libbddx.pc: $(srcdir)/libbddx.pc.in +libbddx.pc: $(srcdir)/libbddx.pc.in Makefile sed -e 's![@]prefix[@]!$(prefix)!g' \ -e 's![@]exec_prefix[@]!$(exec_prefix)!g' \ -e 's![@]includedir[@]!$(includedir)!g' \ -e 's![@]libdir[@]!$(libdir)!g' \ -e 's![@]PACKAGE_VERSION[@]!$(PACKAGE_VERSION)!g' \ - $(srcdir)/libbddx.pc.in > $@ + $(srcdir)/libbddx.pc.in >$@.tmp && mv $@.tmp $@ -DISTCLEANFILES = libbddx.pc +CLEANFILES = libbddx.pc From cd87be15958e671cf06a0f3f162148f01d7fa0fb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 May 2017 11:03:53 +0200 Subject: [PATCH 09/19] fix libspot.pc and libspotltsmin.pc generation Report from Jeroen Meijer. * spot/Makefile.am (libspot.pc): Depends on Makefile. Use a temporary. Declare in CLEANFILES instead of DISTCLEANFILES. * spot/ltsmin/Makefile.am (libspotltsmin.pc): Likewise. --- spot/Makefile.am | 6 +++--- spot/ltsmin/Makefile.am | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/spot/Makefile.am b/spot/Makefile.am index 871523d72..003900e90 100644 --- a/spot/Makefile.am +++ b/spot/Makefile.am @@ -54,12 +54,12 @@ EXTRA_DIST = $(srcdir)/libspot.pc.in pkgconfigdir = $(libdir)/pkgconfig nodist_pkgconfig_DATA = libspot.pc -libspot.pc: $(srcdir)/libspot.pc.in +libspot.pc: $(srcdir)/libspot.pc.in Makefile sed -e 's![@]prefix[@]!$(prefix)!g' \ -e 's![@]exec_prefix[@]!$(exec_prefix)!g' \ -e 's![@]includedir[@]!$(includedir)!g' \ -e 's![@]libdir[@]!$(libdir)!g' \ -e 's![@]PACKAGE_VERSION[@]!$(PACKAGE_VERSION)!g' \ - $(srcdir)/libspot.pc.in > $@ + $(srcdir)/libspot.pc.in > $@.tmp && mv $@.tmp $@ -DISTCLEANFILES = libspot.pc +CLEANFILES = libspot.pc diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am index 728280882..fee392da7 100644 --- a/spot/ltsmin/Makefile.am +++ b/spot/ltsmin/Makefile.am @@ -40,12 +40,12 @@ EXTRA_DIST = $(srcdir)/libspotltsmin.pc.in pkgconfigdir = $(libdir)/pkgconfig nodist_pkgconfig_DATA = libspotltsmin.pc -libspotltsmin.pc: $(srcdir)/libspotltsmin.pc.in +libspotltsmin.pc: $(srcdir)/libspotltsmin.pc.in Makefile sed -e 's![@]prefix[@]!$(prefix)!g' \ -e 's![@]exec_prefix[@]!$(exec_prefix)!g' \ -e 's![@]includedir[@]!$(includedir)!g' \ -e 's![@]libdir[@]!$(libdir)!g' \ -e 's![@]PACKAGE_VERSION[@]!$(PACKAGE_VERSION)!g' \ - $(srcdir)/libspotltsmin.pc.in > $@ + $(srcdir)/libspotltsmin.pc.in > $@.tmp && mv $@.tmp $@ -DISTCLEANFILES = libspotltsmin.pc +CLEANFILES = libspotltsmin.pc From 4b72e2b4c5bc0be2f58ae1ead032661a5cea2001 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 May 2017 13:32:52 +0200 Subject: [PATCH 10/19] [buddy] rename ChangeLog We generate ChangeLog from git log now. * ChangeLog: Rename as... * ChangeLog.1: ... this. * Makefile.am: Distribute the latter. --- buddy/ChangeLog | 383 ---------------------------------------------- buddy/ChangeLog.1 | 383 ++++++++++++++++++++++++++++++++++++++++++++++ buddy/Makefile.am | 2 +- 3 files changed, 384 insertions(+), 384 deletions(-) create mode 100644 buddy/ChangeLog.1 diff --git a/buddy/ChangeLog b/buddy/ChangeLog index d81429667..e69de29bb 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,383 +0,0 @@ -2014-01-06 Alexandre Duret-Lutz - - Enable C++11 and add a move constructor/assignment operator. - - * configure.ac: Enable C++11 mode. - * src/bdd.hh: Use noexport, and add a move constructor and - move assignment operator. The move version of these method - do not have to increment the reference counter, saving time. - On a small test run, this change saved 24% of the calls to - bdd_addref_nc(). - -2013-06-23 Alexandre Duret-Lutz - - Restrict the number of exported symbols. - - * src/bdd.hh, src/bvec.hh, src/fdd.hh: Declare all exported - symbols using BUDDY_API, a new macro that sets visibility=default. - * src/Makefile.am: Compile with -fvisibility=hidden by default, - and compile the C++ part with -fvisibility-inlines-hidden as well. - -2012-06-20 Alexandre Duret-Lutz - - Fix the recent Automake workaround for VPATH builds. - - * examples/bddcalc/Makefile.am (ACLOCAL_AMFLAGS): Add -I. for - parse.c. Reported by Pierre Parutto. - -2012-06-13 Alexandre Duret-Lutz - - Add a function bdd_implies to decide implications between BDDs. - - * src/bdd.h (bdd_implies): New function. - * src/bddop.c (bdd_implies): Implement it. - (CACHEID_IMPLIES, IMPLIES_HASH): New helper macros. - -2012-06-08 Alexandre Duret-Lutz - - Reduce the size of bddNode to improve cache efficiency. - - The unicity table was mixed with the bddNode table for now - apparent reason. After the hash of some node is computed, - bddnodes[hash] did only contain some random node (not the one - looked for) whose .hash member would point to the actual node with - this hash. So that's a two step lookup. With this patch, we sill - have a two step lookup, but the .hash member have been moved to a - separate array. A consequence is that bddNode is now 16-byte long - (instead of 20) so it will never span across two cache lines. - - * src/kernel.hh (bddNode): Remove the hash member, and move it... - (bddhash): ... as this new separate table. - * src/kernel.cc, src/reorder.cc: Adjust all code. - -2012-06-19 Alexandre Duret-Lutz - - Adjust parser construction to support Automake 1.11 and 1.12. - - * examples/bddcalc/parser.yxx: Rename as ... - * examples/bddcalc/parser.y: ... this. - * examples/bddcalc/parser_.cxx: New file that includes parser.c. - * examples/bddcalc/Makefile.am: Adjust. - * examples/bddcalc/parser.hxx: Delete this unused file. - -2011-11-12 Alexandre Duret-Lutz - - * src/kernel.h (PAIR, TRIPLE): Redefine these hash functions using - something that is simpler to compute. - -2011-08-28 Alexandre Duret-Lutz - - * examples/adder/adder.cxx (test_vector): Add parentheses to - remove a clang++-2.9 warning. - -2011-08-27 Alexandre Duret-Lutz - - * src/bddop.c (bdd_support): Speedup using a cache. - -2011-06-10 Alexandre Duret-Lutz - - * src/bddop.c (apply_rec, appquant_rec): Improve caching by - reordering operands of commutative operators. - -2011-06-09 Alexandre Duret-Lutz - - Remove some valgrind warnings about uninitialized memory when - BddCache_lookup return an entry from a Not operation. - - * src/bddop.c (apply_rec, simplify_rec): When checking the cache - entry, always check entry->a and entry->c before checking - entry->b, because the "not_rec()" function does not initialize - the latter. - -2011-06-07 Alexandre Duret-Lutz - - * examples/cmilner/cmilner.c (A, transitions, initial_state) - (reachable_states, has_deadlocks): Declare as static functions, - to suppress a GCC warning. - -2011-04-30 Alexandre Duret-Lutz - - Inline the "is bdd constant" check performed in copies/constructors. - - This avoids a library call to bdd_addref or bdd_delref. - - * src/kernel.c (bdd_delref_nc, bdd_addref_nc): New function, - that work only on BDD that are not constant. - * src/cpext.cxx (bdd::operator=): Move... - * src/bdd.hh (bdd::operator=): ... here. - (bdd::bdd, bdd::~bdd, bdd::operator=): Inline the "is bdd constant" - check and call bdd_delref_nc/bdd_addref_nc only otherwise. - -2011-04-30 Alexandre Duret-Lutz - - Hint gcc about likely/unlikely branches. - - * src/bdd.h (__likely, __unlikely): Introduce these two macros. - * src/bddop.c, src/kerner.c: Use them in many situations. - -2011-04-30 Alexandre Duret-Lutz - - * src/pairs.c (bdd_pairalloc): Fix prototype. - -2011-04-10 Alexandre Duret-Lutz - - Fix some warnings reported by gcc. - - * buddy/src/kernel.c (errorstrings): Mark these as const. - * buddy/src/reorder.c (reorder_gbc): Fix prototype. - (siftTestCmp): Add missing const in cast. - (bdd_reorder_auto): Actually call bdd_reorder_ready(). - -2011-04-10 Alexandre Duret-Lutz - - Add support for --enable-devel and similar macros. - - * m4/debug.m4: Rename to ... - * m4/bdebug.m4: ... this. - * m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New file. - * m4/gccwarns.m4: Fix usage of cache variable. Fix shell - syntax. Do not check for -Waggregate-return. Update CFLAGS. - * configure.ac: Adjust to handle --enable-devel and similar macros - in the same way as Spot. - -2011-04-04 Alexandre Duret-Lutz - - Tag functions with attributes pure, const, or noreturn. - - * src/bdd.h (__purefn, __constfn, __noreturnfn): Define - new macros. - * src/bdd.h, src/bddio.c, src/bvec.h, src/imatrix.h: Use them - to tag many functions as suggested by -Wsuggest-attribute=pure, - -Wsuggest-attribute=const, -Wsuggest-attribute=noreturn. - -2011-04-04 Alexandre Duret-Lutz - - Remove more sanity checks when NDEBUG is set. - - * src/kernel.h (CHECKnc): New macro. - * src/kernel.c (bdd_var, bdd_low, bdd_high, bdd_ithvar, - bdd_nithvar): Use it. - -2011-04-03 Alexandre Duret-Lutz - - * src/kernel.h (CHECK, CHECKa, CHECKn): Disable if NDEBUG is set. - -2011-04-03 Alexandre Duret-Lutz - - Fix declaration of bddproduced. - - * src/reorder.c (bddproduced): Declare a longint, to match - the definition in kerner.c. - -2011-04-03 Alexandre Duret-Lutz - - * buddy/src/kernel.c (bdd_addref, bdd_delref): Disable sanity - checks when compiled with NDEBUG. - -2011-02-27 Alexandre Duret-Lutz - - * examples/cmilner/Makefile.am (cmilner_LDADD): Link with -lm, to - find the pow() function. - -2010-11-07 Alexandre Duret-Lutz - - * src/bddop.c (bdd_setxor): New function. - * src/bdd.h (bdd_setxor): New function. - -2010-01-22 Alexandre Duret-Lutz - - Get rid of some "deprecated conversion from string constant to - `char*'" warnings. - - * examples/bddcalc/parser_.h (yyerror): Declare the format - as a "const char*". - * examples/bddcalc/parser.yxx (yyerror): Likewise. - -2010-01-21 Alexandre Duret-Lutz - - * src/bddio.c (bdd_load): Check the return value of fscanf() to - kill a warning. - -2009-11-23 Alexandre Duret-Lutz - - Introduce bdd_satprefix, to speedup spot::minato(). - - * src/bdd.h (bdd_satprefix): New function. - * src/bddop.c (bdd_satprefix, bdd_sat_prefixrec): New functions. - -2009-10-01 Alexandre Duret-Lutz - - Fix the previous patch in reorder.c: I missread the - function name in the Clang report... - - * src/reorder.c (reorder_win3): Do initialize THIS. - (reorder_win3ite): Do not initialize THIS, its - initial value is never read. - -2009-09-07 Alexandre Duret-Lutz - - Fix some issues reported by LLVM/Clang's static analyser. - - * src/bddop.c (bdd_operator_varresize): Do not write into - quantvarset if it could not be allocated. - * src/reorder.c (reorder_win3): Do not initialize THIS, its - initial value is never read. - -2009-08-28 Alexandre Duret-Lutz - - * configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and - add an AC_CONFIG_MACRO_DIR call. - -2009-06-12 Guillaume Sadegh - - Adjust to support the Intel compiler (icc). - - * configure.ac: Adjust to call... - * m4/intel.m4: ...this new macro. - -2008-03-13 Alexandre Duret-Lutz - - * src/bddtest.cxx: Include to compile with g++-4.3. - -2007-09-19 Alexandre Duret-Lutz - - * src/kernel.c (bdd_default_gbchandler): Log garbage collection to - stderr, not stdout. Reported by Kristin Yvonne Rozier - . - -2004-07-23 Alexandre Duret-Lutz - - * configure.ac: Call AC_LIBTOOL_WIN32_DLL - * src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined. - -2004-07-12 Alexandre Duret-Lutz - - * examples/bddcalc/parser.yxx (actionSeq, varlist): Rewrite as - left-recursive rules. - -2004-06-28 Alexandre Duret-Lutz - - Merge BuDDy 2.3. - * examples/calculator/, examples/internal/: Were renamed as ... - * examples/bddcalc/, examples/bddtest/: ... these. - * configure.ac: Adjust version and output Makefiles. - * examples/Makefile.am (SUBDIRS): Adjust subdir renaming. - * examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were - renamed as ... - * examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these. - * examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust - accordingly. - * src/Makefile.am (AM_CPPFLAGS): Define VERSION. - -2004-01-07 Alexandre Duret-Lutz - - * src/bddop.c (bdd_support): Free supportSet if it needs to be - reallocated. This fixes a memory leak reported by - Souheib.Baarir@lip6.fr. - -2003-11-14 Alexandre Duret-Lutz - - * examples/Makefile.def (AM_CPPFLAGS): Add -I$(srcdir). - -2003-08-06 Alexandre Duret-Lutz - - * doc/Makefile.am (EXTRA_DIST): Replace buddy.ps by buddy.pdf - (the latter has been rebuilt and on Jørn's request it explicitly - mentions the differences with the 2.2 manual). - - * src/bddop.c (bdd_forallcomp, bdd_uniquecomp): Fix documentation. - -2003-07-17 Alexandre Duret-Lutz - - * src/bdd.h (bdd_existcomp, bdd_forallcomp, - bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp, - bdd_appunicomp): Declare for C and C++. - * src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC, - CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC, - CACHEID_APPUNCC): New macros. - (quatvarsetcomp): New variables. - (varset2vartable): Take a second argument to indicate negation, - set quatvarsetcomp. - (INVARSET): Honor quatvarsetcomp. - (quantify): New function, extracted from bdd_exist, bdd_forall, - and bdd_appunicomp. - (bdd_exist, bdd_forall, bdd_appunicomp): Use quantify. - (bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions. - (appquantify): New function, extracted from bdd_appex, bdd_appall, - and bdd_appuni. - (bdd_appex, bdd_appall, bdd_appuni): Use appquantify. - (bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions. - - * src/bddop.c (bdd_support): Return bddtrue when the support - is empty, because variable sets are conjunctions. - -2003-05-22 Alexandre Duret-Lutz - - * src/pairs.c (bdd_mergepairs): New function. - (bdd_copypair): Revert 2003-05-20's change. Use bdd_addref - to copy result variables. - * src/bdd.h (BDD_INVMERGE): New error code. - (bdd_mergepairs): Declare. - * src/kernel.c (errorstrings): Add string of BDDINV. - - * src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/. - -2003-05-20 Alexandre Duret-Lutz - - * src/pairs.c (bdd_copypair): Use memcpy to copy from->result, - and correctly copy p->last from from->last. - - * src/pairs.c (bdd_setbddpair): Fix prototype in documentation. - -2003-05-19 Alexandre Duret-Lutz - - * src/bdd.h: Declare bdd_copypair(). - * src/pairs.c (bdd_copypair, bdd_pairalloc): New functions. - (bdd_newpair): Use bdd_pairalloc. - -2003-05-12 Alexandre Duret-Lutz - - * src/kernel.c (bdd_default_errhandler): Call abort(), not exit(1). - -2003-05-07 Alexandre Duret-Lutz - - * src/bddop.c (bdd_allsat): Fix description. - -2003-05-05 Alexandre Duret-Lutz - - * configure.ac: Output config.h. - * src/kernel.h: Include it. - * src/Makefile.am (AM_CPPFLAGS): New variable. - - * configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am, - examples/Makefile.am, examples/Makefile.def, - examples/adder/Makefile.am, examples/calculator/Makefile.am, - examples/cmilner/Makefile.am, examples/fdd/Makefile.am, - examples/internal/Makefile.am, examples/milner/Makefile.am, - examples/money/Makefile.am, examples/queen/Makefile.am, - examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4, - ChangeLog, INSTALL: New files. - * config, makefile, src/makefile, doc/makefile, - examples/adder/makefile, examples/calculator/makefile - examples/cmilner/makefile, examples/fdd/makefile, - examples/internal/makefile, examples/milner/makefile, - examples/money/makefile, examples/queen/makefile, - examples/solitare/makefile : Delete. - * examples/adder/adder.cxx, examples/fdd/statespace.cxx, - examples/internal/bddtest.cxx, examples/milner/milner.cxx, - examples/money/money.cxx, examples/queen/queen.cxx, - examples/solitare/solitare.cxx: Include iostream. - * examples/calculator/parser.y: Rename as ... - * examples/calculator/parser.yxx: ... this. Remove spurious - comas in %token, %right, and %left arguments. - * examples/calculator/parser.h: Rename as ... - * examples/calculator/parser_.h: ... this, because the bison - rule with output parser.h (not tokens.h) from parser.y. - * examples/calculator/lexer.l: Rename as ... - * examples/calculator/lexer.lxx: ... this. Include parser.h - instead of tokens.h. - * examples/calculator/slist.h - (voidSList::voisSListElem, SList::ite): Fix friend usage. - * src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already - defined. - * README: Update build instruction, and file listing. diff --git a/buddy/ChangeLog.1 b/buddy/ChangeLog.1 new file mode 100644 index 000000000..d81429667 --- /dev/null +++ b/buddy/ChangeLog.1 @@ -0,0 +1,383 @@ +2014-01-06 Alexandre Duret-Lutz + + Enable C++11 and add a move constructor/assignment operator. + + * configure.ac: Enable C++11 mode. + * src/bdd.hh: Use noexport, and add a move constructor and + move assignment operator. The move version of these method + do not have to increment the reference counter, saving time. + On a small test run, this change saved 24% of the calls to + bdd_addref_nc(). + +2013-06-23 Alexandre Duret-Lutz + + Restrict the number of exported symbols. + + * src/bdd.hh, src/bvec.hh, src/fdd.hh: Declare all exported + symbols using BUDDY_API, a new macro that sets visibility=default. + * src/Makefile.am: Compile with -fvisibility=hidden by default, + and compile the C++ part with -fvisibility-inlines-hidden as well. + +2012-06-20 Alexandre Duret-Lutz + + Fix the recent Automake workaround for VPATH builds. + + * examples/bddcalc/Makefile.am (ACLOCAL_AMFLAGS): Add -I. for + parse.c. Reported by Pierre Parutto. + +2012-06-13 Alexandre Duret-Lutz + + Add a function bdd_implies to decide implications between BDDs. + + * src/bdd.h (bdd_implies): New function. + * src/bddop.c (bdd_implies): Implement it. + (CACHEID_IMPLIES, IMPLIES_HASH): New helper macros. + +2012-06-08 Alexandre Duret-Lutz + + Reduce the size of bddNode to improve cache efficiency. + + The unicity table was mixed with the bddNode table for now + apparent reason. After the hash of some node is computed, + bddnodes[hash] did only contain some random node (not the one + looked for) whose .hash member would point to the actual node with + this hash. So that's a two step lookup. With this patch, we sill + have a two step lookup, but the .hash member have been moved to a + separate array. A consequence is that bddNode is now 16-byte long + (instead of 20) so it will never span across two cache lines. + + * src/kernel.hh (bddNode): Remove the hash member, and move it... + (bddhash): ... as this new separate table. + * src/kernel.cc, src/reorder.cc: Adjust all code. + +2012-06-19 Alexandre Duret-Lutz + + Adjust parser construction to support Automake 1.11 and 1.12. + + * examples/bddcalc/parser.yxx: Rename as ... + * examples/bddcalc/parser.y: ... this. + * examples/bddcalc/parser_.cxx: New file that includes parser.c. + * examples/bddcalc/Makefile.am: Adjust. + * examples/bddcalc/parser.hxx: Delete this unused file. + +2011-11-12 Alexandre Duret-Lutz + + * src/kernel.h (PAIR, TRIPLE): Redefine these hash functions using + something that is simpler to compute. + +2011-08-28 Alexandre Duret-Lutz + + * examples/adder/adder.cxx (test_vector): Add parentheses to + remove a clang++-2.9 warning. + +2011-08-27 Alexandre Duret-Lutz + + * src/bddop.c (bdd_support): Speedup using a cache. + +2011-06-10 Alexandre Duret-Lutz + + * src/bddop.c (apply_rec, appquant_rec): Improve caching by + reordering operands of commutative operators. + +2011-06-09 Alexandre Duret-Lutz + + Remove some valgrind warnings about uninitialized memory when + BddCache_lookup return an entry from a Not operation. + + * src/bddop.c (apply_rec, simplify_rec): When checking the cache + entry, always check entry->a and entry->c before checking + entry->b, because the "not_rec()" function does not initialize + the latter. + +2011-06-07 Alexandre Duret-Lutz + + * examples/cmilner/cmilner.c (A, transitions, initial_state) + (reachable_states, has_deadlocks): Declare as static functions, + to suppress a GCC warning. + +2011-04-30 Alexandre Duret-Lutz + + Inline the "is bdd constant" check performed in copies/constructors. + + This avoids a library call to bdd_addref or bdd_delref. + + * src/kernel.c (bdd_delref_nc, bdd_addref_nc): New function, + that work only on BDD that are not constant. + * src/cpext.cxx (bdd::operator=): Move... + * src/bdd.hh (bdd::operator=): ... here. + (bdd::bdd, bdd::~bdd, bdd::operator=): Inline the "is bdd constant" + check and call bdd_delref_nc/bdd_addref_nc only otherwise. + +2011-04-30 Alexandre Duret-Lutz + + Hint gcc about likely/unlikely branches. + + * src/bdd.h (__likely, __unlikely): Introduce these two macros. + * src/bddop.c, src/kerner.c: Use them in many situations. + +2011-04-30 Alexandre Duret-Lutz + + * src/pairs.c (bdd_pairalloc): Fix prototype. + +2011-04-10 Alexandre Duret-Lutz + + Fix some warnings reported by gcc. + + * buddy/src/kernel.c (errorstrings): Mark these as const. + * buddy/src/reorder.c (reorder_gbc): Fix prototype. + (siftTestCmp): Add missing const in cast. + (bdd_reorder_auto): Actually call bdd_reorder_ready(). + +2011-04-10 Alexandre Duret-Lutz + + Add support for --enable-devel and similar macros. + + * m4/debug.m4: Rename to ... + * m4/bdebug.m4: ... this. + * m4/debug.m4, m4/devel.m4, m4/gccoptim.m4, m4/ndebug.m4: New file. + * m4/gccwarns.m4: Fix usage of cache variable. Fix shell + syntax. Do not check for -Waggregate-return. Update CFLAGS. + * configure.ac: Adjust to handle --enable-devel and similar macros + in the same way as Spot. + +2011-04-04 Alexandre Duret-Lutz + + Tag functions with attributes pure, const, or noreturn. + + * src/bdd.h (__purefn, __constfn, __noreturnfn): Define + new macros. + * src/bdd.h, src/bddio.c, src/bvec.h, src/imatrix.h: Use them + to tag many functions as suggested by -Wsuggest-attribute=pure, + -Wsuggest-attribute=const, -Wsuggest-attribute=noreturn. + +2011-04-04 Alexandre Duret-Lutz + + Remove more sanity checks when NDEBUG is set. + + * src/kernel.h (CHECKnc): New macro. + * src/kernel.c (bdd_var, bdd_low, bdd_high, bdd_ithvar, + bdd_nithvar): Use it. + +2011-04-03 Alexandre Duret-Lutz + + * src/kernel.h (CHECK, CHECKa, CHECKn): Disable if NDEBUG is set. + +2011-04-03 Alexandre Duret-Lutz + + Fix declaration of bddproduced. + + * src/reorder.c (bddproduced): Declare a longint, to match + the definition in kerner.c. + +2011-04-03 Alexandre Duret-Lutz + + * buddy/src/kernel.c (bdd_addref, bdd_delref): Disable sanity + checks when compiled with NDEBUG. + +2011-02-27 Alexandre Duret-Lutz + + * examples/cmilner/Makefile.am (cmilner_LDADD): Link with -lm, to + find the pow() function. + +2010-11-07 Alexandre Duret-Lutz + + * src/bddop.c (bdd_setxor): New function. + * src/bdd.h (bdd_setxor): New function. + +2010-01-22 Alexandre Duret-Lutz + + Get rid of some "deprecated conversion from string constant to + `char*'" warnings. + + * examples/bddcalc/parser_.h (yyerror): Declare the format + as a "const char*". + * examples/bddcalc/parser.yxx (yyerror): Likewise. + +2010-01-21 Alexandre Duret-Lutz + + * src/bddio.c (bdd_load): Check the return value of fscanf() to + kill a warning. + +2009-11-23 Alexandre Duret-Lutz + + Introduce bdd_satprefix, to speedup spot::minato(). + + * src/bdd.h (bdd_satprefix): New function. + * src/bddop.c (bdd_satprefix, bdd_sat_prefixrec): New functions. + +2009-10-01 Alexandre Duret-Lutz + + Fix the previous patch in reorder.c: I missread the + function name in the Clang report... + + * src/reorder.c (reorder_win3): Do initialize THIS. + (reorder_win3ite): Do not initialize THIS, its + initial value is never read. + +2009-09-07 Alexandre Duret-Lutz + + Fix some issues reported by LLVM/Clang's static analyser. + + * src/bddop.c (bdd_operator_varresize): Do not write into + quantvarset if it could not be allocated. + * src/reorder.c (reorder_win3): Do not initialize THIS, its + initial value is never read. + +2009-08-28 Alexandre Duret-Lutz + + * configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and + add an AC_CONFIG_MACRO_DIR call. + +2009-06-12 Guillaume Sadegh + + Adjust to support the Intel compiler (icc). + + * configure.ac: Adjust to call... + * m4/intel.m4: ...this new macro. + +2008-03-13 Alexandre Duret-Lutz + + * src/bddtest.cxx: Include to compile with g++-4.3. + +2007-09-19 Alexandre Duret-Lutz + + * src/kernel.c (bdd_default_gbchandler): Log garbage collection to + stderr, not stdout. Reported by Kristin Yvonne Rozier + . + +2004-07-23 Alexandre Duret-Lutz + + * configure.ac: Call AC_LIBTOOL_WIN32_DLL + * src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined. + +2004-07-12 Alexandre Duret-Lutz + + * examples/bddcalc/parser.yxx (actionSeq, varlist): Rewrite as + left-recursive rules. + +2004-06-28 Alexandre Duret-Lutz + + Merge BuDDy 2.3. + * examples/calculator/, examples/internal/: Were renamed as ... + * examples/bddcalc/, examples/bddtest/: ... these. + * configure.ac: Adjust version and output Makefiles. + * examples/Makefile.am (SUBDIRS): Adjust subdir renaming. + * examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were + renamed as ... + * examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these. + * examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust + accordingly. + * src/Makefile.am (AM_CPPFLAGS): Define VERSION. + +2004-01-07 Alexandre Duret-Lutz + + * src/bddop.c (bdd_support): Free supportSet if it needs to be + reallocated. This fixes a memory leak reported by + Souheib.Baarir@lip6.fr. + +2003-11-14 Alexandre Duret-Lutz + + * examples/Makefile.def (AM_CPPFLAGS): Add -I$(srcdir). + +2003-08-06 Alexandre Duret-Lutz + + * doc/Makefile.am (EXTRA_DIST): Replace buddy.ps by buddy.pdf + (the latter has been rebuilt and on Jørn's request it explicitly + mentions the differences with the 2.2 manual). + + * src/bddop.c (bdd_forallcomp, bdd_uniquecomp): Fix documentation. + +2003-07-17 Alexandre Duret-Lutz + + * src/bdd.h (bdd_existcomp, bdd_forallcomp, + bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp, + bdd_appunicomp): Declare for C and C++. + * src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC, + CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC, + CACHEID_APPUNCC): New macros. + (quatvarsetcomp): New variables. + (varset2vartable): Take a second argument to indicate negation, + set quatvarsetcomp. + (INVARSET): Honor quatvarsetcomp. + (quantify): New function, extracted from bdd_exist, bdd_forall, + and bdd_appunicomp. + (bdd_exist, bdd_forall, bdd_appunicomp): Use quantify. + (bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions. + (appquantify): New function, extracted from bdd_appex, bdd_appall, + and bdd_appuni. + (bdd_appex, bdd_appall, bdd_appuni): Use appquantify. + (bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions. + + * src/bddop.c (bdd_support): Return bddtrue when the support + is empty, because variable sets are conjunctions. + +2003-05-22 Alexandre Duret-Lutz + + * src/pairs.c (bdd_mergepairs): New function. + (bdd_copypair): Revert 2003-05-20's change. Use bdd_addref + to copy result variables. + * src/bdd.h (BDD_INVMERGE): New error code. + (bdd_mergepairs): Declare. + * src/kernel.c (errorstrings): Add string of BDDINV. + + * src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/. + +2003-05-20 Alexandre Duret-Lutz + + * src/pairs.c (bdd_copypair): Use memcpy to copy from->result, + and correctly copy p->last from from->last. + + * src/pairs.c (bdd_setbddpair): Fix prototype in documentation. + +2003-05-19 Alexandre Duret-Lutz + + * src/bdd.h: Declare bdd_copypair(). + * src/pairs.c (bdd_copypair, bdd_pairalloc): New functions. + (bdd_newpair): Use bdd_pairalloc. + +2003-05-12 Alexandre Duret-Lutz + + * src/kernel.c (bdd_default_errhandler): Call abort(), not exit(1). + +2003-05-07 Alexandre Duret-Lutz + + * src/bddop.c (bdd_allsat): Fix description. + +2003-05-05 Alexandre Duret-Lutz + + * configure.ac: Output config.h. + * src/kernel.h: Include it. + * src/Makefile.am (AM_CPPFLAGS): New variable. + + * configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am, + examples/Makefile.am, examples/Makefile.def, + examples/adder/Makefile.am, examples/calculator/Makefile.am, + examples/cmilner/Makefile.am, examples/fdd/Makefile.am, + examples/internal/Makefile.am, examples/milner/Makefile.am, + examples/money/Makefile.am, examples/queen/Makefile.am, + examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4, + ChangeLog, INSTALL: New files. + * config, makefile, src/makefile, doc/makefile, + examples/adder/makefile, examples/calculator/makefile + examples/cmilner/makefile, examples/fdd/makefile, + examples/internal/makefile, examples/milner/makefile, + examples/money/makefile, examples/queen/makefile, + examples/solitare/makefile : Delete. + * examples/adder/adder.cxx, examples/fdd/statespace.cxx, + examples/internal/bddtest.cxx, examples/milner/milner.cxx, + examples/money/money.cxx, examples/queen/queen.cxx, + examples/solitare/solitare.cxx: Include iostream. + * examples/calculator/parser.y: Rename as ... + * examples/calculator/parser.yxx: ... this. Remove spurious + comas in %token, %right, and %left arguments. + * examples/calculator/parser.h: Rename as ... + * examples/calculator/parser_.h: ... this, because the bison + rule with output parser.h (not tokens.h) from parser.y. + * examples/calculator/lexer.l: Rename as ... + * examples/calculator/lexer.lxx: ... this. Include parser.h + instead of tokens.h. + * examples/calculator/slist.h + (voidSList::voisSListElem, SList::ite): Fix friend usage. + * src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already + defined. + * README: Update build instruction, and file listing. diff --git a/buddy/Makefile.am b/buddy/Makefile.am index 51b6aaa85..d59ea33a8 100644 --- a/buddy/Makefile.am +++ b/buddy/Makefile.am @@ -2,4 +2,4 @@ ACLOCAL_AMFLAGS = -I m4 SUBDIRS = src examples doc -EXTRA_DIST = CHANGES m4/debug.m4 m4/gccwarns.m4 +EXTRA_DIST = CHANGES ChangeLog.1 m4/debug.m4 m4/gccwarns.m4 From e21499ea7c6a49cc0c94ff9e59b9afebc65cb743 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 May 2017 13:33:52 +0200 Subject: [PATCH 11/19] * Makefile.am (gen-ChangeLog): Generate BuDDy's ChangeLog. --- Makefile.am | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/Makefile.am b/Makefile.am index d76361ccd..8bc2df201 100644 --- a/Makefile.am +++ b/Makefile.am @@ -71,6 +71,7 @@ EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog \ dist-hook: gen-ChangeLog gen_start = 2012-03-10 +gen_start_buddy = 2014-02-13 .PHONY: gen-ChangeLog deb gen-ChangeLog: if test -d .git; then \ @@ -78,15 +79,25 @@ gen-ChangeLog: git log --since=$(gen_start) --pretty=oneline | \ ## Filter out commits whose subject start with '['. These are usually ## [buddy] or [lbtt] tags to indicate we are committing on a subproject. - grep -v '........................................ \[' | \ + grep -v '........................................ \[' | \ ## Keep the SHA1 cut -c 1-40 | \ ## Feed all that to gitlog-to-changelog - $(top_srcdir)/tools/gitlog-to-changelog \ + $(top_srcdir)/tools/gitlog-to-changelog \ --no-cluster --format='%s%n%n%b%n' -- \ - --stdin --no-walk > $(distdir)/cl-t; \ - rm -f $(distdir)/ChangeLog; \ - mv $(distdir)/cl-t $(distdir)/ChangeLog; \ + --stdin --no-walk > $(distdir)/cl-t; \ + rm -f $(distdir)/ChangeLog; \ + mv $(distdir)/cl-t $(distdir)/ChangeLog; \ +## Now do the same for BuDDy + git log --since=$(gen_start_buddy) --pretty=oneline | \ + grep '........................................ \[buddy\]' | \ + cut -c 1-40 | \ + $(top_srcdir)/tools/gitlog-to-changelog \ + --no-cluster --format='%s%n%n%b%n' -- \ + --stdin --no-walk | \ + sed 's/^ \[buddy\] / /g' >$(distdir)/cl-t; \ + rm -f $(distdir)/buddy/ChangeLog; \ + mv $(distdir)/cl-t $(distdir)/buddy/ChangeLog; \ fi # Build Debian packages. From 04640af135144c735e6086fa8d96abf7d8aaf861 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 May 2017 14:40:32 +0200 Subject: [PATCH 12/19] bin: remove temporary files even on errors Fixes #259. * bin/common_setup.cc: Register a cleanup_tmpfiles() via atexit. * tests/core/ltldo.test: Add a test case. * NEWS: Mention the bug. --- NEWS | 3 +++ bin/common_setup.cc | 9 +++++++++ tests/core/ltldo.test | 15 +++++++++++++-- 3 files changed, 25 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 53daf5ec5..d7de6b731 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,9 @@ New in spot 2.3.3.dev (not yet released) - the --help output of randaut and ltl2tgba was showing an unsupported %b stat. + - ltldo and ltlcross could leave temporary files behind when + aborting on error. + New in spot 2.3.3 (2017-04-11) Tools: diff --git a/bin/common_setup.cc b/bin/common_setup.cc index fd90a2719..4d7c518e8 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -43,8 +43,16 @@ This is free software: you are free to change and redistribute it.\n\ There is NO WARRANTY, to the extent permitted by law.\n", stream); } +// This is called on normal exit (i.e., when leaving +// main or calling exit(), even via error()). +static void atexit_cleanup() +{ + spot::cleanup_tmpfiles(); +} #ifdef HAVE_SIGACTION +// This is called on abnormal exit, i.e. when the process is killed by +// some signal. static void sig_handler(int sig) { spot::cleanup_tmpfiles(); @@ -92,6 +100,7 @@ setup(char** argv) setup_default_output_format(); setup_sig_handler(); + atexit(atexit_cleanup); } diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index 5dab1e4a3..c02465881 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -152,3 +152,14 @@ genltl --rv-counter=9 | ltldo ltl2tgba --stats=' print("%[up]R + %[uc]R + %[sp]R + %[sc]R - %R\n"); die if abs(%[up]R + %[uc]R + %[sp]R + %[sc]R - %R) > 0.02;' > code.pl perl code.pl + +# ltldo should not leave temporary files behind itself on errors +ltldo -f a 'ltl2dstar --ltl2nba=spin:ltl2tgba@-DS' && exit 2 +for i in lcr-*; do + case $i in + 'lcr-*');; + *) + echo $i should not be here; + exit 2;; + esac +done From 7e4238149ba20c004efa380e17ca098cc7c5bb30 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 May 2017 18:15:58 +0200 Subject: [PATCH 13/19] debian: fix the changelog of buddy * debian/rules (override_dh_installchangelogs): New rule. --- debian/rules | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/debian/rules b/debian/rules index 6976acd4e..dde038b05 100755 --- a/debian/rules +++ b/debian/rules @@ -98,6 +98,11 @@ override_dh_auto_build: dh_auto_build $(MAKE) -C tests nb-html +# BuDDy has its own changelog +override_dh_installchangelogs: + dh_installchangelogs -plibbddx0 -plibbddx-dev buddy/ChangeLog + dh_installchangelogs -Nlibbddx0 -Nlibbddx-dev ChangeLog + # https://mail.scipy.org/pipermail/ipython-user/2015-August/014016.html override_dh_compress: dh_compress -X.ipynb From 8968bf6c4e9dc2e4bf884fdbfa2298dc88ab6ff4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 8 May 2017 10:28:13 +0200 Subject: [PATCH 14/19] simplify: fix related to event_univ handling MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #260. Reported by FrantiÅ¡ek Blahoudek. The simplification F(f)|q = F(f|q), where q designates an event_univ formula, was not always applied because of a couple of issue: (1) the mospliter was ignoring event_univ unless favor_event_univ was set, (2) when processing formulas from res_EventUniv they were not put back into res_F or res_G to be subject to the F/G rules. * spot/tl/simplify.cc: Improve handling of the above points. * tests/core/reduccmp.test: Adjust and add test case. * tests/core/ltl2tgba2.test, tests/python/atva16-fig2a.ipynb: Adjust. --- NEWS | 4 + spot/tl/simplify.cc | 64 ++++++------- tests/core/ltl2tgba2.test | 2 +- tests/core/reduccmp.test | 7 +- tests/python/atva16-fig2a.ipynb | 159 ++++++++++++++------------------ 5 files changed, 113 insertions(+), 123 deletions(-) diff --git a/NEWS b/NEWS index d7de6b731..232303d06 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,10 @@ New in spot 2.3.3.dev (not yet released) - ltldo and ltlcross could leave temporary files behind when aborting on error. + - The LTL simplifcation rule that turns F(f)|q into F(f|q) + when q is a subformula that is both eventual and universal + was documented but not applied in some forgotten cases. + New in spot 2.3.3 (2017-04-11) Tools: diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index af5b2e225..3c03666fe 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de -// Recherche et Developpement de l'Epita (LRDE). +// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -698,7 +698,7 @@ namespace spot { bool e = f.is_eventual(); bool u = f.is_universal(); - bool eu = res_EventUniv && e & u && c_->options.favor_event_univ; + bool eu = res_EventUniv && e & u && c_->options.event_univ; switch (f.kind()) { case op::X: @@ -2137,30 +2137,24 @@ namespace spot vec eu; bool seen_g = false; for (auto f: *s.res_EventUniv) - { - if (f.is_eventual() && f.is_universal()) - { - if (f.is(op::G)) - { - seen_g = true; - eu.emplace_back(f[0]); - } - else - { - eu.emplace_back(f); - } - } - else - { - s.res_other->emplace_back(f); - } - } + if (f.is(op::G)) + { + seen_g = true; + eu.emplace_back(f[0]); + } + else + { + eu.emplace_back(f); + } if (seen_g) { eu.emplace_back(allFG); allFG = nullptr; - s.res_other->emplace_back(unop_multop(op::G, op::And, - eu)); + formula andeu = formula::multop(op::And, eu); + if (!opt_.favor_event_univ) + s.res_G->emplace_back(andeu); + else + s.res_other->emplace_back(formula::G(andeu)); } else { @@ -2673,6 +2667,11 @@ namespace spot formula allGF = unop_unop_multop(op::G, op::F, op::Or, std::move(*s.res_GF)); + bool eu_has_F = false; + for (auto f: *s.res_EventUniv) + if (f.is(op::F)) + eu_has_F = true; + // Xa | Xb = X(a | b) // Xa | Xb | GF(c) = X(a | b | GF(c)) // For Universal&Eventual formula f1...fn we also have: @@ -2686,7 +2685,7 @@ namespace spot s.res_EventUniv->end()); } else if (!opt_.favor_event_univ - && !s.res_F->empty() + && (!s.res_F->empty() || eu_has_F) && s.res_G->empty() && s.res_U_or_W->empty() && s.res_R_or_M->empty() @@ -2715,9 +2714,8 @@ namespace spot // these differences) s.res_F->emplace_back(allGF); allGF = nullptr; - s.res_F->insert(s.res_F->end(), - s.res_EventUniv->begin(), - s.res_EventUniv->end()); + for (auto f: *s.res_EventUniv) + s.res_F->emplace_back(f.is(op::F) ? f[0] : f); } else if (opt_.favor_event_univ) { @@ -2726,7 +2724,7 @@ namespace spot bool seen_f = false; if (s.res_EventUniv->size() > 1) { - // If some of the EventUniv formulae start + // If some of the EventUniv formulas start // with an F, Gather them all under the // same F. Striping any leading F. for (auto& f: *s.res_EventUniv) @@ -2750,9 +2748,13 @@ namespace spot } else { - s.res_other->insert(s.res_other->end(), - s.res_EventUniv->begin(), - s.res_EventUniv->end()); + for (auto f: *s.res_EventUniv) + { + if (f.is(op::F)) + s.res_F->emplace_back(f[0]); + else + s.res_other->emplace_back(f); + } } // Xa | Xb | f1...fn = X(a | b | f1...fn) // is built at the end of this multop::Or case. diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index ae8eb7d2b..71eaba050 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -272,7 +272,7 @@ p-patterns,20, 1,8, 1,8, 3,24, 3,24 !sb-patterns,5, 2,7, 2,7, 3,12, 3,12 !sb-patterns,6, 3,11, 4,14, 3,11, 4,14 !sb-patterns,7, 4,16, 4,16, 4,16, 4,16 -!sb-patterns,9, 4,19, 4,19, 6,27, 6,27 +!sb-patterns,9, 3,13, 3,13, 5,21, 5,21 !sb-patterns,10, 2,6, 2,6, 2,6, 2,6 !sb-patterns,11, 1,0, 1,0, 1,0, 1,0 !sb-patterns,12, 1,0, 1,0, 1,0, 1,0 diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test index 7188a79ea..74308ecba 100755 --- a/tests/core/reduccmp.test +++ b/tests/core/reduccmp.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2016 Laboratoire de -# Recherche et Developpement de l'Epita (LRDE). +# Copyright (C) 2009-2014, 2016-2017 Laboratoire de Recherche et +# Developpement de l'Epita (LRDE). # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -179,7 +179,8 @@ G(a | GFb), Ga | GFb F(a & GFb & c), F(a & GFb & c) G(a | GFb | c), G(a | c) | GFb -GFa <=> GFb, G(Fa&Fb)|FG(!a&!b) +GFa <=> GFb, F(G(Fa&Fb)|G(!a&!b)) +FGa | (GFa & GFb), F(Ga | (G(Fa & Fb))) Gb W a, Gb|a Fb M Fa, Fa & Fb diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb index 8e2b789aa..6fa7be833 100644 --- a/tests/python/atva16-fig2a.ipynb +++ b/tests/python/atva16-fig2a.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.2rc1" + "version": "3.5.3" }, "name": "" }, @@ -86,113 +86,96 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")&Inf(\n", - "\u2776\n", - ")\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "1->2\n", + "\n", + "\n", + "a | b\n", "\n", - "\n", - "3\n", - "\n", - "3\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\u2776\n", "\n", - "\n", - "0->3\n", - "\n", - "\n", - "1\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & b\n", + "\u2776\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", - "\u2776\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "2->2\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\u24ff\n", - "\u2776\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f77f87ba300> >" + " *' at 0x7f79506d2900> >" ] } ], From d3d2364ad0fc912fc9b0f32852e16868e5c323f3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 9 May 2017 14:29:42 +0200 Subject: [PATCH 15/19] org: list ltlfilt's transformation * doc/org/ltlfilt.org: A the list of transformation option. Suggested by Yann Thierry-Mieg. --- doc/org/ltlfilt.org | 43 +++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 41 insertions(+), 2 deletions(-) diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index edc128108..5698e099e 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -55,6 +55,44 @@ ltlfilt --lbt-input -F scheck.ltl * Altering the formula +The following options can be used to modify the formulas that have +been read. + +#+BEGIN_SRC sh :results verbatim :exports results +ltlfilt --help | sed -n '/Transformation options.*:/,/^$/p' | sed '1d;$d' +#+END_SRC +#+RESULTS: +#+begin_example + --boolean-to-isop rewrite Boolean subformulas as irredundant sum of + products (implies at least -r1) + --define[=FILENAME] when used with --relabel or --relabel-bool, output + the relabeling map using #define statements + --exclusive-ap=AP,AP,... if any of those APs occur in the formula, add + a term ensuring two of them may not be true at the + same time. Use this option multiple times to + declare independent groups of exclusive + propositions. + --from-ltlf[=alive] transform LTLf (finite LTL) to LTL by introducing + some 'alive' proposition + --negate negate each formula + --nnf rewrite formulas in negative normal form + --relabel[=abc|pnn] relabel all atomic propositions, alphabetically + unless specified otherwise + --relabel-bool[=abc|pnn] relabel Boolean subexpressions, alphabetically + unless specified otherwise + --remove-wm rewrite operators W and M using U and R (this is + an alias for --unabbreviate=WM) + --remove-x remove X operators (valid only for + stutter-insensitive properties) + -r, --simplify[=LEVEL] simplify formulas according to LEVEL (see below); + LEVEL is set to 3 if omitted + --unabbreviate[=STR] remove all occurrences of the operators specified + by STR, which must be a substring of "eFGiMRW^", + where 'e', 'i', and '^' stand respectively for + <->, ->, and xor. If no argument is passed, the + subset "eFGiMW^" is used. +#+end_example + As with [[file:randltl.org][=randltl=]], the =-r= option can be used to simplify formulas. #+BEGIN_SRC sh :results verbatim :exports both @@ -188,8 +226,9 @@ words the original set of formulas contains 9 different patterns. An option that can be used in combination with =--relabel= or -=--relabel-bool= is =--define=. This causes the correspondence of old -a new names to be printed as a set of =#define= statements. +=--relabel-bool= is =--define=. This causes the correspondence +between old and new names to be printed as a set of =#define= +statements. #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f '(a & !b) & GF(a & !b) & FG(!c)' --relabel-bool=pnn --define --spin From aa40482352aa48393b6bd93ce28dbf8df9075484 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 May 2017 15:59:58 +0200 Subject: [PATCH 16/19] ltl2tgba: clear simplification cache between translations The cache used in formula simplification will keep atomic propositions defined between several translations, and may impact variable order. Reported by Maximilien Colange. * spot/tl/simplify.hh, spot/tl/simplify.cc, spot/twaalgos/translate.cc, spot/twaalgos/translate.hh (clear_cache): New method. * bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call it. * spot/twaalgos/stats.cc: Do not keep a point to the formula after printing statistics. * tests/core/ltl2tgba.test: Add a test case. * tests/core/readsave.test: Adjust one formula. * NEWS: Mention the issue. --- NEWS | 4 ++++ bin/ltl2tgba.cc | 6 +++++- bin/ltl2tgta.cc | 8 ++++++-- spot/tl/simplify.cc | 9 +++++++++ spot/tl/simplify.hh | 9 +++++++-- spot/twaalgos/stats.cc | 6 +++++- spot/twaalgos/translate.cc | 9 +++++++-- spot/twaalgos/translate.hh | 3 +++ tests/core/ltl2tgba.test | 18 +++++++++++++----- tests/core/readsave.test | 2 +- 10 files changed, 60 insertions(+), 14 deletions(-) diff --git a/NEWS b/NEWS index 232303d06..aa525ad61 100644 --- a/NEWS +++ b/NEWS @@ -15,6 +15,10 @@ New in spot 2.3.3.dev (not yet released) when q is a subformula that is both eventual and universal was documented but not applied in some forgotten cases. + - Because of some caching inside of ltl2tgba, translating multiple + formula in single ltl2tgba run could produce automata different + from those produced by individual runs. + New in spot 2.3.3 (2017-04-11) Tools: diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 41beae20d..44cd1dca4 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -146,6 +146,10 @@ namespace printer.print(aut, timer, f, filename, linenum, nullptr, prefix, suffix); + // If we keep simplification caches around, atomic propositions + // will still be defined, and one translation may influence the + // variable order of the next one. + trans.clear_caches(); return 0; } }; diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index 469344e2b..3c61926c2 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -211,6 +211,10 @@ namespace tgta = spot::minimize_tgta(tgta); spot::print_dot(std::cout, tgta->get_ta()); } + // If we keep simplification caches around, atomic propositions + // will still be defined, and one translation may influence the + // variable order of the next one. + trans.clear_caches(); flush_cout(); return 0; } diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 3c03666fe..6732c36bc 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -3481,4 +3481,13 @@ namespace spot cache_->clear_as_bdd_cache(); cache_->lcc.clear(); } + + void + tl_simplifier::clear_caches() + { + tl_simplifier_cache* c = + new tl_simplifier_cache(get_dict(), cache_->options); + std::swap(c, cache_); + delete c; + } } diff --git a/spot/tl/simplify.hh b/spot/tl/simplify.hh index c2f6a3c36..d06a3d5c7 100644 --- a/spot/tl/simplify.hh +++ b/spot/tl/simplify.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de -// Recherche et Developpement de l'Epita (LRDE). +// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -176,6 +176,11 @@ namespace spot /// This also clears the language containment cache. void clear_as_bdd_cache(); + /// \brief Clear all caches. + /// + /// This empties all the cache used by the simplifier. + void clear_caches(); + /// Return the bdd_dict used. bdd_dict_ptr get_dict() const; diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index 5ff628e62..e521c7efe 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -385,7 +385,11 @@ namespace spot } auto& os = format(format_); - scc_.reset(); // Make sure we do not hold a pointer to the automaton + // Make sure we do not hold a pointer to the automaton or the + // formula, as these may prevent atomic proposition to be freed + // before a next job. + scc_.reset(); + form_ = nullptr; return os; } diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 4ec085524..dc117490d 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -106,4 +106,9 @@ namespace spot return run(&f); } + void translator::clear_caches() + { + simpl_->clear_caches(); + } + } diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 545474ba7..569c87218 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -132,6 +132,9 @@ namespace spot /// by the simplified version. twa_graph_ptr run(formula* f); + /// \brief Clear the LTL simplification caches. + void clear_caches(); + protected: void setup_opt(const option_map* opt); void build_simplifier(const bdd_dict_ptr& dict); diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index bdfbd0805..7b82b172c 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -1,10 +1,10 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 -# Laboratoire de Recherche et Développement de l'Epita (LRDE). -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# Copyright (C) 2009-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# Copyright (C) 2003-2004 Laboratoire d'Informatique de Paris 6 +# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +# Pierre et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -230,3 +230,11 @@ ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1 # of the test-suite where this resize is triggered, so do not remove # it unless you can find another place that triggers that. genltl --go-theta=18 | ltl2tgba --low --any -q + +# Calling ltl2tgba once for two formulas should give the same result +# as calling twice on each formula. We had a problem where the order +# of atomic propositions would be sensible to the formulas seen +# before. +(ltl2tgba Fb ; ltl2tgba 'GFa & GFb') >out1 +ltl2tgba Fb 'GFa & GFb' >out2 +diff out1 out2 diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 40cf0e634..0fd2efe60 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -122,7 +122,7 @@ cat >expected <, 5, 1 , 5, 1 , 4, 1 -, 4, 1 +, 4, 1 , 4, 1 , 6, 1 <(a & !b & (b | (!b M F!a))) | (!a & (b | (!b & (b W Ga)))), 3 states>, 5, 1 From 762dd4555d8ae763f94ea7912fc3e55273fb9e4d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 10 May 2017 17:24:35 +0200 Subject: [PATCH 17/19] parseaut: misc cleanups * spot/parseaut/parseaut.yy: Remove extra ;. * spot/parseaut/scanaut.ll: Use nullptr instead of 0. --- spot/parseaut/parseaut.yy | 2 +- spot/parseaut/scanaut.ll | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index a3a81f75c..3e1c9874c 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -2439,7 +2439,7 @@ namespace spot if (r.h->aut && !r.h->aut->is_existential()) r.h->aut->merge_univ_dests(); return r.h; - }; + } parsed_aut_ptr parse_aut(const std::string& filename, const bdd_dict_ptr& dict, diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index 1b7b58286..71db33836 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2017 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -90,7 +90,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* [0-9]+[ \t][0-9]+[ts]? { BEGIN(in_LBTT_HEADER); - char* end = 0; + char* end = nullptr; errno = 0; unsigned long n = strtoul(yytext, &end, 10); yylval->num = n; From 52b5491b8ecac4aa79304a649deb8f87f32c4545 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 11 May 2017 10:10:48 +0200 Subject: [PATCH 18/19] Release Spot 2.3.4 * NEWS, configure.ac, doc/org/setup.org: Update version to 2.3.4. --- NEWS | 6 +++--- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/NEWS b/NEWS index aa525ad61..c6e6f3997 100644 --- a/NEWS +++ b/NEWS @@ -1,11 +1,11 @@ -New in spot 2.3.3.dev (not yet released) +New in spot 2.3.4 (2017-05-11) Bugs fixed: - - the transformation to state-based acceptance (spot::sbacc()) was + - The transformation to state-based acceptance (spot::sbacc()) was incorrect on automata where the empty acceptance mark is accepting. - - the --help output of randaut and ltl2tgba was showing an + - The --help output of randaut and ltl2tgba was showing an unsupported %b stat. - ltldo and ltlcross could leave temporary files behind when diff --git a/configure.ac b/configure.ac index 3e5a3bfe3..8245caada 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.3.3.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.4], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/setup.org b/doc/org/setup.org index b60d61ef2..9e28e96ca 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,8 +1,8 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.3.3 -#+MACRO: LASTRELEASE 2.3.3 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.3.tar.gz][=spot-2.3.3.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-3/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-04-11 +#+MACRO: SPOTVERSION 2.3.4 +#+MACRO: LASTRELEASE 2.3.4 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.4.tar.gz][=spot-2.3.4.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-4/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2017-05-11 From b9c250894bb74d03291dc1426e809b57531e6fd1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 11 May 2017 10:16:03 +0200 Subject: [PATCH 19/19] * NEWS, configure.ac: Bump version number. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index c6e6f3997..90cf66bb0 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.3.4.dev (not yet released) + + Nothing yet. + New in spot 2.3.4 (2017-05-11) Bugs fixed: diff --git a/configure.ac b/configure.ac index 8245caada..9489dcf03 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.3.4], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.4.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])