From ebd4c2dc7a598657c50f4bcf82adff50f94d7af5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 20 Jun 2016 13:31:33 +0200 Subject: [PATCH 1/7] * doc/org/citing.org: Typo. --- doc/org/citing.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/org/citing.org b/doc/org/citing.org index 8f9e4dc06..804cc1834 100644 --- a/doc/org/citing.org +++ b/doc/org/citing.org @@ -9,7 +9,7 @@ If you need to cite the Spot project in some academic paper, please use the following reference: -- *Spot 2.0 –- a framework for LTL and ω-automata manipulation*, +- *Spot 2.0 — a framework for LTL and ω-automata manipulation*, /Alexandre Duret-Lutz/, /Alexandre Lewkowicz/, /Amaury Fauchille/, /Thibaud Michaud/, /Etienne Renault/, and /Laurent Xu/. To appear in Proc. of ATVA'16. Chiba, Japan, Oct. 2016. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.16.atva2][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][pdf]]) From a78f5feecfeade73f2624ea452be38999a94f338 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Jun 2016 17:43:46 +0200 Subject: [PATCH 2/7] * tests/core/degenlskip.test: Typo. --- tests/core/degenlskip.test | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/core/degenlskip.test b/tests/core/degenlskip.test index ec099f77c..bbdf0410f 100755 --- a/tests/core/degenlskip.test +++ b/tests/core/degenlskip.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -22,7 +22,7 @@ set -e -# Make sure degen-skip=0 and degen-skip=1 produce the expected +# Make sure degen-lskip=0 and degen-lskip=1 produce the expected # automata for 'GFa & GFb' ltl2tgba -B 'GFa & GFb' --hoa > out1 From a4c7016f52448a5231ae6d480b4de2fb81fafa68 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Jun 2016 18:03:02 +0200 Subject: [PATCH 3/7] degen: fix handling of degen-lcache=1 * spot/twaalgos/degen.cc: Here. * tests/core/degendet.test: Add test case. * tests/core/ltl2ta.test: Adjust expected output. * NEWS: Mention the issue. --- NEWS | 9 +++++++++ spot/twaalgos/degen.cc | 2 ++ tests/core/degendet.test | 11 +++++++++-- tests/core/ltl2ta.test | 36 ++++++++++++++++++------------------ 4 files changed, 38 insertions(+), 20 deletions(-) diff --git a/NEWS b/NEWS index 47bc514b9..198f803c2 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,15 @@ New in spot 2.0.2a (Not yet released) Nothing yet. + Bug fixes: + + * The degen-lcache=1 option of the degeneralization algorithm (which + is a default option) did not behave exactly as documented: instead + of reusing the first level ever created for a state where the + choice of the level is free, it used the last level used. This + caused some posterior simulation-based reductions to be less + efficient at reducing automata (on the average). + New in spot 2.0.2 (2016-06-17) Documentation: diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index b73f2afc1..73663ed32 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -519,6 +519,8 @@ namespace spot lvl = std::max(lvl_cache[d.first].first, lvl); else if (use_lvl_cache == 2) lvl = std::min(lvl_cache[d.first].first, lvl); + else + lvl = lvl_cache[d.first].first; // Do not change } lvl_cache[d.first] = std::make_pair(lvl, true); } diff --git a/tests/core/degendet.test b/tests/core/degendet.test index 89c1dfa32..c335ced42 100755 --- a/tests/core/degendet.test +++ b/tests/core/degendet.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2011, 2015, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,7 +23,7 @@ set -e -# The following command, reported by Tomáš Babiak, used to output many +# The following command, reported by Tomáš Babiak, used to output many # different automata, because state addresses were used to order the # successors in the degeneralization. @@ -36,3 +36,10 @@ for i in 2 3 4 5; do ../ikwiad -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out cmp out out1 || exit 1 done + +# The next formula used to be translated into a 6-state automaton +# instead of a 4-state automaton, because of an error in the +# implementation of the degen-lcache=1 option causing the last level +# used to be reused, instead of the first one. +run 0 ltl2tgba -B -f '(b & Fa) U XXG(a M Gb)' --stats=%s,%t >out +test "4,14" = "`cat out`" diff --git a/tests/core/ltl2ta.test b/tests/core/ltl2ta.test index e95e92513..ec5298a8c 100755 --- a/tests/core/ltl2ta.test +++ b/tests/core/ltl2ta.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -# Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire +# de Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -170,12 +170,12 @@ in: Fa & b & GFc & Gd -TA -DS -RT | 12 | 126 | 5 -TA -DS -lv | 29 | 315 | 13 -TA -DS -lv -RT | 13 | 140 | 4 --TA -DS -sp | 28 | 309 | 12 --TA -DS -sp -RT | 12 | 137 | 3 +-TA -DS -sp | 28 | 306 | 12 +-TA -DS -sp -RT | 12 | 134 | 3 -TA -DS -lv -sp | 29 | 315 | 13 -TA -DS -lv -sp -RT | 13 | 140 | 4 --x -TA -DS -in | 29 | 254 | 9 --x -TA -DS -in -RT | 12 | 96 | 3 +-x -TA -DS -in | 29 | 240 | 9 +-x -TA -DS -in -RT | 12 | 93 | 3 in: Fa & a & GFc & Gc -TGTA | 4 | 8 | XXX -TGTA -RT | 3 | 6 | XXX @@ -401,15 +401,15 @@ in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4) -TA -lv -sp | 45 | 676 | 9 -TA -lv -sp -RT | 35 | 566 | 4 -TA -DS | 54 | 722 | 26 --TA -DS -RT | 42 | 600 | 19 +-TA -DS -RT | 42 | 608 | 18 -TA -DS -lv | 55 | 800 | 19 --TA -DS -lv -RT | 44 | 694 | 13 --TA -DS -sp | 54 | 795 | 18 --TA -DS -sp -RT | 43 | 683 | 12 +-TA -DS -lv -RT | 44 | 702 | 13 +-TA -DS -sp | 54 | 789 | 18 +-TA -DS -sp -RT | 43 | 686 | 12 -TA -DS -lv -sp | 55 | 800 | 19 --TA -DS -lv -sp -RT | 44 | 694 | 13 --x -TA -DS -in | 55 | 700 | 11 --x -TA -DS -in -RT | 39 | 566 | 8 +-TA -DS -lv -sp -RT | 44 | 702 | 13 +-x -TA -DS -in | 55 | 694 | 11 +-x -TA -DS -in -RT | 41 | 597 | 8 in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TGTA | 69 | 1539 | XXX -TGTA -RT | 49 | 935 | XXX @@ -422,15 +422,15 @@ in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2)) -TA -lv -sp | 68 | 1443 | 16 -TA -lv -sp -RT | 56 | 1179 | 15 -TA -DS | 124 | 2964 | 44 --TA -DS -RT | 100 | 2285 | 42 +-TA -DS -RT | 96 | 2099 | 42 -TA -DS -lv | 125 | 3028 | 42 --TA -DS -lv -RT | 101 | 2339 | 40 +-TA -DS -lv -RT | 97 | 2149 | 40 -TA -DS -sp | 124 | 3012 | 41 --TA -DS -sp -RT | 100 | 2324 | 39 +-TA -DS -sp -RT | 96 | 2134 | 39 -TA -DS -lv -sp | 125 | 3028 | 42 --TA -DS -lv -sp -RT | 101 | 2339 | 40 +-TA -DS -lv -sp -RT | 97 | 2149 | 40 -x -TA -DS -in | 125 | 1838 | 25 --x -TA -DS -in -RT | 89 | 1344 | 25 +-x -TA -DS -in -RT | 87 | 1296 | 25 EOF sed -n 's/in: \(.*\)/\1/p' checkta.txt > input.txt From d4a385e341d20473e3f1f5dfa400e1c5fbfc3aaa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Jul 2016 10:55:54 +0200 Subject: [PATCH 4/7] ajax: fix GTA construction * python/ajax/spotcgi.in: Here. * NEWS: Mention it. --- NEWS | 2 ++ python/ajax/spotcgi.in | 10 ++++------ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 198f803c2..b2b4e4211 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,8 @@ New in spot 2.0.2a (Not yet released) choice of the level is free, it used the last level used. This caused some posterior simulation-based reductions to be less efficient at reducing automata (on the average). + * The generalized testing automata displayed by the on-line + translator were incorrect (those output by ltl2tgta were OK). New in spot 2.0.2 (2016-06-17) diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in index a00310088..308c5d840 100755 --- a/python/ajax/spotcgi.in +++ b/python/ajax/spotcgi.in @@ -695,10 +695,8 @@ elif buchi_type == 'i': degen = True neverclaim = True -if output_type == 't': - ta_type = form.getfirst('tf', 't') - if ta_type == 't': - degen = True +if output_type == 't' and ta_type == 't': + degen = True if prune_scc: # Do not suppress all useless acceptance conditions if @@ -769,8 +767,8 @@ if output_type == 't': if bisimulation: tautomaton = spot.minimize_tgta(tautomaton) else: - tautomaton = spot.tgba_to_ta(degen, propset, - True, True, singlepass, livelock) + tautomaton = spot.tgba_to_ta(degen, propset, ta_type == 't', + True, singlepass, livelock) if bisimulation: tautomaton = spot.minimize_ta(tautomaton) dont_run_dot = print_stats(tautomaton, ta = True) From 70064d0b7523c9f168abc256c204d79371c6ffb8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Jul 2016 14:08:59 +0200 Subject: [PATCH 5/7] ltl2tgta: remove options --ba, --tgba, and friends * bin/common_post.cc, bin/common_post.hh: Add a "nooutput" variant of the options. * bin/ltl2tgta.cc: Use it. * NEWS: Mention the fix. --- NEWS | 1 + bin/common_post.cc | 22 +++++++++++++++++++++- bin/common_post.hh | 7 ++++--- bin/ltl2tgta.cc | 2 +- 4 files changed, 27 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index b2b4e4211..dd6b179c3 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,7 @@ New in spot 2.0.2a (Not yet released) efficient at reducing automata (on the average). * The generalized testing automata displayed by the on-line translator were incorrect (those output by ltl2tgta were OK). + * ltl2tgta should not offer options --ba, --monitor, --tgba and such. New in spot 2.0.2 (2016-06-17) diff --git a/bin/common_post.cc b/bin/common_post.cc index 5679f542c..b6796f1b8 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -39,7 +39,7 @@ enum { OPT_TGBA, }; -static const argp_option options[] = +static constexpr const argp_option options[] = { /**************************************************/ { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, @@ -72,6 +72,23 @@ static const argp_option options[] = { nullptr, 0, nullptr, 0, nullptr, 0 } }; +static constexpr const argp_option options_nooutput[] = + { + /**************************************************/ + { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, + { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 }, + { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, + { "any", 'a', nullptr, 0, "no preference, do not bother making it small " + "or deterministic", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Simplification level:", 21 }, + { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 }, + { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 }, + { "high", OPT_HIGH, nullptr, 0, + "all available optimizations (slow, default)", 0 }, + { nullptr, 0, nullptr, 0, nullptr, 0 } + }; + static const argp_option options_disabled[] = { /**************************************************/ @@ -169,3 +186,6 @@ const struct argp post_argp = { options, parse_opt_post, const struct argp post_argp_disabled = { options_disabled, parse_opt_post, nullptr, nullptr, nullptr, nullptr, nullptr }; +const struct argp post_argp_nooutput = { options_nooutput, parse_opt_post, + nullptr, nullptr, nullptr, + nullptr, nullptr }; diff --git a/bin/common_post.hh b/bin/common_post.hh index faaa1fa61..483114a81 100644 --- a/bin/common_post.hh +++ b/bin/common_post.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,8 +23,9 @@ #include #include -extern const struct argp post_argp; // postprocessing enabled +extern const struct argp post_argp; // postprocessing enabled extern const struct argp post_argp_disabled; // postprocessing disabled +extern const struct argp post_argp_nooutput; // no output option extern spot::postprocessor::output_type type; extern spot::postprocessor::output_pref pref; diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index 045c342ea..06c39eceb 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -90,7 +90,7 @@ static const argp_option options[] = const struct argp_child children[] = { { &finput_argp, 0, nullptr, 1 }, - { &post_argp, 0, nullptr, 20 }, + { &post_argp_nooutput, 0, nullptr, 20 }, { &misc_argp, 0, nullptr, -1 }, { nullptr, 0, nullptr, 0 } }; From 2665b5780a3962dff158452b8957ecfb320581d5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 7 Jul 2016 15:57:14 +0200 Subject: [PATCH 6/7] relabel: do not unregister old AP that are also new Reported by Ayrat Khalimov against the trans.html page when using ltl3ba. * spot/twaalgos/relabel.cc: Here. * tests/core/ltl3dra.test: Test it. * NEWS: Mention it. * THANKS: Add Ayrat. --- NEWS | 4 ++++ THANKS | 1 + spot/twaalgos/relabel.cc | 8 +++++++- tests/core/ltl3dra.test | 8 +++++++- 4 files changed, 19 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index dd6b179c3..f732c6002 100644 --- a/NEWS +++ b/NEWS @@ -13,6 +13,10 @@ New in spot 2.0.2a (Not yet released) * The generalized testing automata displayed by the on-line translator were incorrect (those output by ltl2tgta were OK). * ltl2tgta should not offer options --ba, --monitor, --tgba and such. + * the relabel() function could incorrectly unregister old atomic + propositions even if they are still used in the output (e.g., if + a&p0 is relabeled to p0&p1). This could cause ltldo and on-line + translator to report errors. New in spot 2.0.2 (2016-06-17) diff --git a/THANKS b/THANKS index 4c9aa543a..0b5832d1a 100644 --- a/THANKS +++ b/THANKS @@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or suggestions. Akim Demaille +Ayrat Khalimov Caroline Lemieux Christian Dax Christopher Ziegler diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index 0c8fb29fe..906e30795 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -27,6 +27,7 @@ namespace spot bddPair* pairs = bdd_newpair(); auto d = aut->get_dict(); std::vector vars; + std::set newvars; vars.reserve(relmap->size()); for (auto& p: *relmap) { @@ -34,10 +35,15 @@ namespace spot int newv = aut->register_ap(p.second); bdd_setpair(pairs, oldv, newv); vars.push_back(oldv); + newvars.insert(newv); } for (auto& t: aut->edges()) t.cond = bdd_replace(t.cond, pairs); + // Erase all the old variable that are not reused in the new set. + // (E.g., if we relabel a&p0 into p0&p1 we should not unregister + // p0) for (auto v: vars) - aut->unregister_ap(v); + if (newvars.find(v) == newvars.end()) + aut->unregister_ap(v); } } diff --git a/tests/core/ltl3dra.test b/tests/core/ltl3dra.test index e4f7af1fa..5c9b3743f 100755 --- a/tests/core/ltl3dra.test +++ b/tests/core/ltl3dra.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et +# Copyright (C) 2015, 2016 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -35,3 +35,9 @@ ltlcross 'ltl2tgba' 'ltl3dra' -f '(<>((((p0) && && ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3))))))))) && (((p0) && (!(<>(p2)))) || ((!(p0)) && (<>(p2)))))))' + + +# This used to trigger an assertion because the formula "a=0"&p0 was +# relabeled p0&p1, and then p0 was unregistered despite being one of +# the new variables. +ltldo ltl3dra -f '"a=0" & p0' | grep 'AP: 2.*p0' From 2abfd73a3040ff4f7a2e1a4cc1c7432082b5532f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 11 Jul 2016 10:59:23 +0200 Subject: [PATCH 7/7] Release Spot 2.0.3 * NEWS, configure.ac, doc/org/setup.org: Update. --- NEWS | 16 +++++++--------- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/NEWS b/NEWS index f732c6002..f4d2206a9 100644 --- a/NEWS +++ b/NEWS @@ -1,22 +1,20 @@ -New in spot 2.0.2a (Not yet released) - - Nothing yet. +New in spot 2.0.3 (2016-07-11) Bug fixes: * The degen-lcache=1 option of the degeneralization algorithm (which is a default option) did not behave exactly as documented: instead of reusing the first level ever created for a state where the - choice of the level is free, it used the last level used. This - caused some posterior simulation-based reductions to be less + choice of the level is free, it reused the last level ever used. + This caused some posterior simulation-based reductions to be less efficient at reducing automata (on the average). - * The generalized testing automata displayed by the on-line + * The generalized testing automata displayed by the online translator were incorrect (those output by ltl2tgta were OK). * ltl2tgta should not offer options --ba, --monitor, --tgba and such. * the relabel() function could incorrectly unregister old atomic - propositions even if they are still used in the output (e.g., if - a&p0 is relabeled to p0&p1). This could cause ltldo and on-line - translator to report errors. + propositions even when they were still used in the output (e.g., + if a&p0 is relabeled to p0&p1). This could cause ltldo and the + online translator to report errors. New in spot 2.0.2 (2016-06-17) diff --git a/configure.ac b/configure.ac index 3cd608570..f61750d75 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.0.2a], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.0.3], [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 db227b7b2..357b679f0 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.0.2 -#+MACRO: LASTRELEASE 2.0.2 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.0.2.tar.gz][=spot-2.0.2.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0-2/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2016-06-17 +#+MACRO: SPOTVERSION 2.0.3 +#+MACRO: LASTRELEASE 2.0.3 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.0.3.tar.gz][=spot-2.0.3.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0-3/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2016-07-11