From 697c94605f2a208baf48a17b64f8ad7217c4081f Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Tue, 19 Sep 2017 14:47:31 +0100 Subject: [PATCH 01/14] Fix: Remove SBAcc option in bin/ltlfilt * bin/ltlfilt.cc: Remove SBAcc option as rabin_to_buchi_maybe() works with transition-based acceptance as well. --- bin/ltlfilt.cc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 351b60aa4..d956f049b 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -751,8 +751,7 @@ namespace // BA will preserve determinism if possible. spot::postprocessor p; p.set_type(spot::postprocessor::Generic); - p.set_pref(spot::postprocessor::Deterministic - | spot::postprocessor::SBAcc); + p.set_pref(spot::postprocessor::Deterministic); p.set_level(spot::postprocessor::Low); auto dra = p.run(aut); if (dra->acc().is_generalized_buchi()) From 86560f6bd7f79b75650c9830b3322857bd0d50cc Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Fri, 12 May 2017 22:48:11 +0200 Subject: [PATCH 02/14] typos * spot/twaalgos/alternation.hh: Typos. * spot/twa/twa.hh: Typos. --- spot/twa/twa.hh | 6 +++--- spot/twaalgos/alternation.hh | 4 +++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index cfc6007f0..74893e13a 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -947,7 +947,7 @@ namespace spot /// \brief Set generalized Büchi acceptance /// - /// \param num the number of acceptance sets to used + /// \param num the number of acceptance sets to use /// /// The acceptance formula of the form /// \code @@ -969,8 +969,8 @@ namespace spot /// acceptance. The returned mark \c {0} can be used to tag /// accepting transition. /// - /// Note that this does not make the automaton as using - /// state-based acceptance. If you want to create a Büchi + /// Note that this does not mark the automaton as using + /// state-based acceptance. If you want to create a Büchi /// automaton with state-based acceptance, call /// \code /// prop_state_acc(true) diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index f4ba737fd..40eb5c6e1 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -27,7 +27,7 @@ namespace spot /// \brief Helper class combine outgoing edges in alternating /// automata /// - /// The idea is that you can the operator() on some state to get an + /// The idea is that you can call the operator() on some state to get an /// BDD representation of its outgoing edges (labels and /// destinations, but not acceptance marks). The BDD representation /// of different states can combined using & or | to build a new @@ -65,6 +65,7 @@ namespace spot /// Acceptance marks are dropped. /// /// The results is very likely to be alternating. + /// @} template SPOT_API unsigned states_and(const twa_graph_ptr& aut, I begin, I end) @@ -97,6 +98,7 @@ namespace spot /// acceptance is only used in presence of size-1 rejecting-SCCs.) /// /// \param named_states name each state for easier debugging + /// @} SPOT_API twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut, bool named_states = false); From bd34f3c6297e0c594e73719b4701046aa62b9fe5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Sep 2017 14:41:17 +0200 Subject: [PATCH 03/14] postproc: fix a comment * spot/twaalgos/postproc.cc: Here. --- spot/twaalgos/postproc.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index af882590d..ca28d2ed8 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -152,7 +152,7 @@ namespace spot if (scc_filter_ == 0) return a; // If the automaton is weak, using transition-based acceptance - // won't help, so let's preserve it. + // won't help, so let's preserve state-based acceptance. if ((state_based_ || a->prop_inherently_weak().is_true()) && a->prop_state_acc().is_true()) return scc_filter_states(a, arg); From cdfe78f178c15cb5cb7fea1381ebfc91bb05801d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Sep 2017 16:06:41 +0200 Subject: [PATCH 04/14] twa_graph: do not order BDDs by IDs in merge_edges() Fixes #282. * spot/misc/bddlt.hh (bdd_less_than_stable): New function. * spot/twa/twagraph.cc (merge_edges): Use it. * tests/core/complement.test, tests/core/degenid.test, tests/core/ltldo.test, tests/core/prodor.test, tests/core/readsave.test, tests/core/sbacc.test, tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb, tests/python/decompose.ipynb, tests/python/dualize.py, tests/python/highlighting.ipynb, tests/python/piperead.ipynb, tests/python/product.ipynb, tests/python/simstate.py, tests/python/tra2tba.py: Adjust all expected outputs. * NEWS: Mention the bug. --- NEWS | 8 + spot/misc/bddlt.hh | 45 ++- spot/twa/twagraph.cc | 14 +- tests/core/complement.test | 2 +- tests/core/degenid.test | 18 +- tests/core/ltldo.test | 6 +- tests/core/prodor.test | 16 +- tests/core/readsave.test | 6 +- tests/core/sbacc.test | 40 +-- tests/python/atva16-fig2a.ipynb | 26 +- tests/python/automata.ipynb | 406 +++++++++++++-------------- tests/python/decompose.ipynb | 74 ++--- tests/python/dualize.py | 20 +- tests/python/highlighting.ipynb | 312 ++++++++++----------- tests/python/piperead.ipynb | 43 +-- tests/python/product.ipynb | 471 ++++++++++++++++---------------- tests/python/simstate.py | 2 +- tests/python/tra2tba.py | 4 +- 18 files changed, 788 insertions(+), 725 deletions(-) diff --git a/NEWS b/NEWS index fd2d45167..6e9f6462b 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,14 @@ New in spot 2.4.0.dev (not yet released) Nothing yet. + Bugs fixed: + + - The twa_graph::mege_edges() function relied on BDD IDs to sort + edges. This in turn caused some algorithm (like the + degeneralization) to produce slighltly different outputs (but + still correct outputs) depending on the BDD operations performed + before. + New in spot 2.4 (2017-09-06) Build: diff --git a/spot/misc/bddlt.hh b/spot/misc/bddlt.hh index ee547024d..2abc94fee 100644 --- a/spot/misc/bddlt.hh +++ b/spot/misc/bddlt.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2011, 2014, 2017 Laboratoire de Recherche et +// Developpement 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. @@ -29,6 +29,10 @@ namespace spot { /// \ingroup misc_tools /// \brief Comparison functor for BDDs. + /// + /// This comparison function use BDD ids for efficiency. An + /// algorithm depending on this order may return different results + /// depending on how the BDD library has been used before. struct bdd_less_than : public std::binary_function { @@ -39,6 +43,43 @@ namespace spot } }; + /// \ingroup misc_tools + /// \brief Comparison functor for BDDs. + /// + /// This comparison function actually check for BDD variables, so as + /// long as the variable order is the same, the output of this + /// comparison will be stable and independent on previous BDD + /// operations. + struct bdd_less_than_stable : + public std::binary_function + { + bool + operator()(const bdd& left, const bdd& right) const + { + int li = left.id(); + int ri = right.id(); + if (li == ri) + return false; + if (li <= 1 || ri <= 1) + return li < ri; + { + int vl = bdd_var(left); + int vr = bdd_var(right); + if (vl != vr) + return vl < vr; + } + // We check the high side before low, this way + // !a&b comes before a&!b and a&b + { + bdd hl = bdd_high(left); + bdd hr = bdd_high(right); + if (hl != hr) + return operator()(hl, hr); + return operator()(bdd_low(left), bdd_low(right)); + } + } + }; + /// \ingroup misc_tools /// \brief Hash functor for BDDs. struct bdd_hash : diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index f99f13771..f4330b078 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -19,6 +19,7 @@ #include #include +#include #include #include @@ -79,11 +80,11 @@ namespace spot delete namer; } - /// \brief Merge universal destinations - /// - /// If several states have the same universal destination, merge - /// them all. Also remove unused destination, and any redundant - /// state in each destination. + /// \brief Merge universal destinations + /// + /// If several states have the same universal destination, merge + /// them all. Also remove unused destination, and any redundant + /// state in each destination. void twa_graph::merge_univ_dests() { auto& g = get_graph(); @@ -198,7 +199,8 @@ namespace spot return true; if (lhs.dst > rhs.dst) return false; - return lhs.cond.id() < rhs.cond.id(); + bdd_less_than_stable lt; + return lt(lhs.cond, rhs.cond); // Do not sort on acceptance, we'll merge // them. }); diff --git a/tests/core/complement.test b/tests/core/complement.test index 2ef1566ac..3ca643564 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -62,10 +62,10 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {0 1} [!0&!1] 0 [!0&1] 0 {1} [0&!1] 0 {0} +[0&1] 0 {0 1} --END-- HOA: v1 States: 4 diff --git a/tests/core/degenid.test b/tests/core/degenid.test index 1bc11d89f..8e69a35c8 100755 --- a/tests/core/degenid.test +++ b/tests/core/degenid.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2011, 2013, 2014, 2015, 2017 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -242,15 +242,15 @@ State: 0 [0] 1 State: 1 {0} [1&2] 1 -[!1&2] 2 -[!2] 3 +[!2] 2 +[!1&2] 3 State: 2 -[1] 1 -[!1] 2 -State: 3 [1&2] 1 -[!1&2] 2 -[!2] 3 +[!2] 2 +[!1&2] 3 +State: 3 +[1] 1 +[!1] 3 --END-- EOF diff out expected diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index c02465881..aeaa15c0f 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -82,8 +82,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0] 0 {0} [!0] 0 +[0] 0 {0} --END-- EOF diff output expected @@ -103,8 +103,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0] 0 {0} [!0] 0 +[0] 0 {0} --END-- EOF diff output expected @@ -124,8 +124,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic --BODY-- State: 0 -[0] 0 {0} [!0] 0 +[0] 0 {0} --END-- EOF diff output expected diff --git a/tests/core/prodor.test b/tests/core/prodor.test index 3684aa5ec..23fb05dbd 100755 --- a/tests/core/prodor.test +++ b/tests/core/prodor.test @@ -65,18 +65,18 @@ properties: trans-labels explicit-labels trans-acc complete properties: stutter-invariant --BODY-- State: 0 -[0] 0 {1} [!0] 0 -[0&1] 1 {1} +[0] 0 {1} [!0&1] 1 +[0&1] 1 {1} State: 1 -[0&1] 1 {0 1} [!0&1] 1 {0} -[0&!1] 2 {0 1} +[0&1] 1 {0 1} [!0&!1] 2 {0} +[0&!1] 2 {0 1} State: 2 -[0] 2 {1} [!0] 2 +[0] 2 {1} --END-- EOF diff por.hoa exp @@ -96,13 +96,13 @@ Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc stutter-invariant --BODY-- State: 0 -[0] 0 {1} [!0] 0 -[0&1] 1 {1} +[0] 0 {1} [!0&1] 1 +[0&1] 1 {1} State: 1 -[0&1] 1 {0 1} [!0&1] 1 {0} +[0&1] 1 {0 1} --END-- EOF diff pand.hoa exp diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 13f055bce..f2820bb53 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -363,10 +363,10 @@ digraph G { I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 0 [label="a & b\n{0,1}"] 0 -> 0 [label="!a & !b"] 0 -> 0 [label="!a & b\n{1}"] 0 -> 0 [label="a & !b\n{0}"] + 0 -> 0 [label="a & b\n{0,1}"] } EOF diff output expected @@ -382,10 +382,10 @@ digraph G { I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 0 [label="a & b\n⓿❶"] 0 -> 0 [label="!a & !b"] 0 -> 0 [label="!a & b\n❶"] 0 -> 0 [label="a & !b\n⓿"] + 0 -> 0 [label="a & b\n⓿❶"] } EOF diff output expected @@ -407,10 +407,10 @@ digraph G { I [label="", style=invis, width=0] I -> 0 0 [label=<0>] - 0 -> 0 [label=$zero$one>] 0 -> 0 [label=] 0 -> 0 [label=$one>] 0 -> 0 [label=$zero>] + 0 -> 0 [label=$zero$one>] } EOF diff output expected diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 5de70b724..65482b54f 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -37,26 +37,26 @@ Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels state-acc complete properties: deterministic stutter-invariant --BODY-- -State: 0 {0} -[0&!1] 0 -[0&1] 1 -[!0&!1] 2 -[!0&1] 3 -State: 1 {0 1} -[0&!1] 0 -[0&1] 1 -[!0&!1] 2 -[!0&1] 3 -State: 2 -[0&!1] 0 -[0&1] 1 -[!0&!1] 2 -[!0&1] 3 -State: 3 {1} -[0&!1] 0 -[0&1] 1 -[!0&!1] 2 -[!0&1] 3 +State: 0 {0 1} +[0&1] 0 +[!0&!1] 1 +[!0&1] 2 +[0&!1] 3 +State: 1 +[0&1] 0 +[!0&!1] 1 +[!0&1] 2 +[0&!1] 3 +State: 2 {1} +[0&1] 0 +[!0&!1] 1 +[!0&1] 2 +[0&!1] 3 +State: 3 {0} +[0&1] 0 +[!0&!1] 1 +[!0&1] 2 +[0&!1] 3 --END-- EOF diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb index d87cfc61d..0e0e3038a 100644 --- a/tests/python/atva16-fig2a.ipynb +++ b/tests/python/atva16-fig2a.ipynb @@ -140,29 +140,29 @@ "1->1\n", "\n", "\n", - "!a & b\n", - "\u2776\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & b\n", + "\u2776\n", "\n", "\n", "1->1\n", "\n", "\n", - "a & b\n", - "\u24ff\n", - "\u2776\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "2->2\n", @@ -176,7 +176,7 @@ "\n" ], "text": [ - " *' at 0x7ffb2c16a630> >" + " *' at 0x7f0d2406cc00> >" ] } ], diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 54d68707c..c35c748b1 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -64,11 +64,11 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", @@ -117,25 +117,25 @@ "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "4->4\n", @@ -145,39 +145,39 @@ "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!c & d\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f0d8c2c98a0> >" + " *' at 0x7f23c1786450> >" ] } ], @@ -204,113 +204,113 @@ "output_type": "pyout", "prompt_number": 3, "svg": [ - "\n", + "\n", "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!c & d\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!c\n", "\n", "\n", "" @@ -358,35 +358,35 @@ "\n", "\n", "cluster_2\n", - "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "4\n", @@ -395,70 +395,70 @@ "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", - "\u24ff\n", + "\n", + "\n", + "c & d\n", + "\u24ff\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!c & d\n", - "\u24ff\n", + "\n", + "\n", + "!d\n", + "\u24ff\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!d\n", - "\u24ff\n", + "\n", + "\n", + "!c & d\n", + "\u24ff\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!d\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", - "3->1\n", - "\n", - "\n", - "c & d\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!c & d\n", + "3->1\n", + "\n", + "\n", + "c\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!c\n", "\n", "\n", "4->4\n", @@ -570,7 +570,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c2561e0> >" + " *' at 0x7f23c17168d0> >" ] } ], @@ -640,7 +640,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c256d50> >" + " *' at 0x7f23c1716330> >" ] } ], @@ -716,7 +716,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c256ae0> >" + " *' at 0x7f23c1716180> >" ] } ], @@ -1126,14 +1126,14 @@ "1->1\n", "\n", "\n", - "b\n", - "\u24ff\n", + "!b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "2->2\n", @@ -1176,7 +1176,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c2567e0> >" + " *' at 0x7f23c1716b10> >" ] } ], @@ -1257,14 +1257,14 @@ "1->1\n", "\n", "\n", - "b\n", - "\u24ff\n", + "!b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "2->2\n", @@ -1277,7 +1277,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c34f780> >" + " *' at 0x7f23c1716990> >" ] } ], @@ -1310,38 +1310,39 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "2\n", @@ -1351,27 +1352,26 @@ "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "b\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "2->2\n", @@ -1381,21 +1381,21 @@ "\n", "\n", "3->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f0d8c2567b0> >" + " *' at 0x7f23c1716960> >" ] } ], @@ -1494,7 +1494,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c256e10> >" + " *' at 0x7f23c1716b40> >" ] } ], @@ -1964,7 +1964,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c23ee70> >" + " *' at 0x7f23c1716ba0> >" ] } ], @@ -2580,7 +2580,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c34f900> >" + " *' at 0x7f23c1716bd0> >" ] } ], @@ -2736,7 +2736,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c2770c0> >" + " *' at 0x7f23c17164e0> >" ] } ], @@ -2806,7 +2806,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c277120> >" + " *' at 0x7f23c1716900> >" ] } ], @@ -2954,7 +2954,7 @@ "\n", "0\n", "\n", - "1,1\n", + "1,1\n", "\n", "\n", "I->0\n", @@ -2971,7 +2971,7 @@ "\n", "1\n", "\n", - "0,0\n", + "0,0\n", "\n", "\n", "0->1\n", @@ -2983,7 +2983,7 @@ "\n", "2\n", "\n", - "0,1\n", + "0,1\n", "\n", "\n", "0->2\n", @@ -2995,7 +2995,7 @@ "\n", "3\n", "\n", - "1,0\n", + "1,0\n", "\n", "\n", "0->3\n", @@ -3237,7 +3237,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c256960> >" + " *' at 0x7f23c1716bd0> >" ] }, { @@ -3406,7 +3406,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c277090> >" + " *' at 0x7f23c1716a20> >" ] } ], @@ -3495,7 +3495,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c277090> >" + " *' at 0x7f23c1716a20> >" ] } ], @@ -3584,7 +3584,7 @@ "\n" ], "text": [ - " *' at 0x7f0d8c277090> >" + " *' at 0x7f23c1716a20> >" ] } ], diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 80ccdd004..c6c99f630 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -212,7 +212,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e720> >" + " *' at 0x7effc5466510> >" ] } ], @@ -330,7 +330,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e6f0> >" + " *' at 0x7effc4bca420> >" ] } ], @@ -472,7 +472,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e5d0> >" + " *' at 0x7effc4bca1b0> >" ] } ], @@ -563,7 +563,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e600> >" + " *' at 0x7effc5466330> >" ] } ], @@ -628,20 +628,20 @@ "0->0\n", "\n", "\n", - "a & !c\n", + "!a & !c\n", + "\u24ff\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & !c\n", - "\u24ff\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f71e062ef60> >" + " *' at 0x7effc4bca180> >" ] } ], @@ -758,7 +758,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e540> >" + " *' at 0x7effc4bca360> >" ] }, { @@ -883,7 +883,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e5a0> >" + " *' at 0x7effc4bca120> >" ] }, { @@ -1027,7 +1027,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e450> >" + " *' at 0x7effc4bca390> >" ] } ], @@ -1433,7 +1433,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d4b0> >" + " *' at 0x7effc4bec1e0> >" ] } ], @@ -1759,7 +1759,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d480> >" + " *' at 0x7effc4bca450> >" ] }, { @@ -1957,7 +1957,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062eed0> >" + " *' at 0x7effc4bca360> >" ] }, { @@ -2138,7 +2138,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e450> >" + " *' at 0x7effc4bcac30> >" ] } ], @@ -2474,7 +2474,7 @@ "\n" ], "text": [ - " *' at 0x7f71e376f660> >" + " *' at 0x7effc5466300> >" ] } ], @@ -2619,7 +2619,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d540> >" + " *' at 0x7effc4bcac90> >" ] }, { @@ -2739,7 +2739,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062ef00> >" + " *' at 0x7effc4bca270> >" ] }, { @@ -2920,7 +2920,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e480> >" + " *' at 0x7effc4bca120> >" ] } ], @@ -3278,7 +3278,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d480> >" + " *' at 0x7effc4bec2d0> >" ] } ], @@ -3569,7 +3569,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d540> >" + " *' at 0x7effc4bcac30> >" ] }, { @@ -3722,7 +3722,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e3f0> >" + " *' at 0x7effc4bca330> >" ] }, { @@ -3860,7 +3860,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062ef00> >" + " *' at 0x7effc4bca120> >" ] } ], @@ -4164,7 +4164,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d5d0> >" + " *' at 0x7effc4bec540> >" ] } ], @@ -4276,7 +4276,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d810> >" + " *' at 0x7effc4bca270> >" ] } ], @@ -4369,7 +4369,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064da20> >" + " *' at 0x7effc4bcac30> >" ] }, { @@ -4436,7 +4436,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e3f0> >" + " *' at 0x7effc4bcac30> >" ] } ], @@ -4523,7 +4523,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064da80> >" + " *' at 0x7effc4bec870> >" ] } ], @@ -4679,7 +4679,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064db40> >" + " *' at 0x7effc4bec270> >" ] } ], @@ -4809,7 +4809,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064dc00> >" + " *' at 0x7effc4bca2d0> >" ] }, { @@ -4898,7 +4898,7 @@ "\n" ], "text": [ - " *' at 0x7f71e062e3f0> >" + " *' at 0x7effc4bec630> >" ] }, { @@ -5016,7 +5016,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064dcc0> >" + " *' at 0x7effc4bec930> >" ] } ], @@ -5200,7 +5200,7 @@ "\n" ], "text": [ - " *' at 0x7f71e05e74b0> >" + " *' at 0x7effc4b87210> >" ] }, { @@ -5311,7 +5311,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d780> >" + " *' at 0x7effc4bec7b0> >" ] } ], @@ -5402,7 +5402,7 @@ "\n" ], "text": [ - " *' at 0x7f71e064d420> >" + " *' at 0x7effc4bec180> >" ] } ], diff --git a/tests/python/dualize.py b/tests/python/dualize.py index de434f8f4..0d0e2fcec 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -564,22 +564,22 @@ properties: deterministic univ-branch State: 0 [0] 1 [!0] 1&2 -State: 1 -[0&!1] 1 -[0&1] 4 -[!0&1] 2&4 -[!0&!1] 1&2 +State: 1 {0} +[0&1] 1 +[0&!1] 4 +[!0&!1] 2&4 +[!0&1] 1&2 State: 2 [!0&1] 3 [0 | !1] 5 State: 3 {0} [!0] 3 [0] 5 -State: 4 {0} -[0&!1] 1 -[0&1] 4 -[!0&1] 2&4 -[!0&!1] 1&2 +State: 4 +[0&1] 1 +[0&!1] 4 +[!0&!1] 2&4 +[!0&1] 1&2 State: 5 [t] 5 --END--""" diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 4e15e2d6e..d0381a51e 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -254,7 +254,7 @@ "\n" ], "text": [ - " *' at 0x7f55143d98a0> >" + " *' at 0x7fedf009e390> >" ] } ], @@ -356,7 +356,7 @@ "\n" ], "text": [ - " *' at 0x7f55143d9750> >" + " *' at 0x7fede8fc5270> >" ] } ], @@ -533,27 +533,27 @@ "2->2\n", "\n", "\n", - "b\n", + "!b\n", + "\u24ff\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!b\n", - "\u24ff\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->3\n", "\n", "\n", - "a & b\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4->2\n", @@ -571,7 +571,7 @@ "\n" ], "text": [ - " *' at 0x7f5514366600> >" + " *' at 0x7fede8f54420> >" ] } ], @@ -710,29 +710,29 @@ "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "\u24ff\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!b\n", - "\u24ff\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->3\n", "\n", "\n", - "a & b\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4->2\n", @@ -750,7 +750,7 @@ "\n" ], "text": [ - " *' at 0x7f5514366600> >" + " *' at 0x7fede8f54420> >" ] } ], @@ -830,7 +830,7 @@ "\n" ], "text": [ - " *' at 0x7f55143666f0> >" + " *' at 0x7fede8f54600> >" ] }, { @@ -863,20 +863,20 @@ "0->0\n", "\n", "\n", - "a\n", - "\u24ff\n", + "!a\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f5514366ae0> >" + " *' at 0x7fede8f544e0> >" ] } ], @@ -902,67 +902,67 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\u2776\n", + "\n", + "\n", + "a & !b\n", + "\u2776\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\u2776\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & b\n", + "\u2776\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f5514366de0> >" + " *' at 0x7fede8f54900> >" ] } ], @@ -984,9 +984,11 @@ "text": [ "Prefix:\n", " 1,0\n", - " | a & b\t{1}\n", + " | !a & b\n", "Cycle:\n", " 0,0\n", + " | !a\t{0}\n", + " 0,0\n", " | a\t{0,1}" ] } @@ -1027,67 +1029,67 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", - "\u2776\n", + "\n", + "\n", + "a & !b\n", + "\u2776\n", "\n", "\n", "1\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\u2776\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & b\n", + "\u2776\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "\u24ff\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f5514366de0> >" + " *' at 0x7fede8f54900> >" ] }, { @@ -1144,7 +1146,7 @@ "\n" ], "text": [ - " *' at 0x7f55143666f0> >" + " *' at 0x7fede8f54600> >" ] }, { @@ -1177,20 +1179,20 @@ "0->0\n", "\n", "\n", - "a\n", - "\u24ff\n", + "!a\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f5514366ae0> >" + " *' at 0x7fede8f544e0> >" ] } ], @@ -1255,7 +1257,7 @@ "\n", "0\n", "\n", - "0 * 3\n", + "0 * 3\n", "\n", "\n", "I->0\n", @@ -1265,7 +1267,7 @@ "\n", "1\n", "\n", - "1 * 2\n", + "1 * 2\n", "\n", "\n", "0->1\n", @@ -1276,7 +1278,7 @@ "\n", "2\n", "\n", - "2 * 2\n", + "2 * 2\n", "\n", "\n", "0->2\n", @@ -1287,7 +1289,7 @@ "\n", "3\n", "\n", - "1 * 1\n", + "1 * 1\n", "\n", "\n", "1->3\n", @@ -1305,7 +1307,7 @@ "\n", "4\n", "\n", - "2 * 1\n", + "2 * 1\n", "\n", "\n", "2->4\n", @@ -1316,7 +1318,7 @@ "\n", "5\n", "\n", - "1 * 0\n", + "1 * 0\n", "\n", "\n", "3->5\n", @@ -1334,7 +1336,7 @@ "\n", "6\n", "\n", - "2 * 0\n", + "2 * 0\n", "\n", "\n", "4->6\n", @@ -1345,7 +1347,7 @@ "\n", "7\n", "\n", - "1 * 4\n", + "1 * 4\n", "\n", "\n", "5->7\n", @@ -1363,7 +1365,7 @@ "\n", "8\n", "\n", - "2 * 4\n", + "2 * 4\n", "\n", "\n", "6->8\n", @@ -1397,7 +1399,7 @@ "\n" ], "text": [ - " *' at 0x7f5514366e10> >" + " *' at 0x7fede8fc51b0> >" ] }, { @@ -1471,7 +1473,7 @@ "\n" ], "text": [ - " *' at 0x7f55143668a0> >" + " *' at 0x7fede8f54330> >" ] }, { @@ -1555,7 +1557,7 @@ "\n" ], "text": [ - " *' at 0x7f5514366c60> >" + " *' at 0x7fede8f54840> >" ] } ], @@ -1663,27 +1665,27 @@ "2->2\n", "\n", "\n", - "b\n", + "!b\n", + "\u24ff\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!b\n", - "\u24ff\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->3\n", "\n", "\n", - "a & b\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & !b\n", - "\u24ff\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "4->2\n", @@ -1701,7 +1703,7 @@ "\n" ], "text": [ - " *' at 0x7f5514366f00> >" + " *' at 0x7fede8f54b10> >" ] } ], @@ -1774,14 +1776,14 @@ "0->0\n", "\n", "\n", - "!b\n", - "\u24ff\n", + "b\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "\u24ff\n", "\n", "\n", "1->0\n", @@ -1833,20 +1835,20 @@ "2->2\n", "\n", "\n", - "a & !b\n", - "\u24ff\n", + "a & b\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f5514366f00> >" + " *' at 0x7fede8f54b10> >" ] } ], @@ -1917,14 +1919,14 @@ "0->0\n", "\n", "\n", - "!b\n", - "\u24ff\n", + "b\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "\u24ff\n", "\n", "\n", "1->0\n", @@ -1976,20 +1978,20 @@ "2->2\n", "\n", "\n", - "a & !b\n", - "\u24ff\n", + "a & b\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f5514366f00> >" + " *' at 0x7fede8f54b10> >" ] }, { @@ -2004,7 +2006,7 @@ "\n", "0\n", "\n", - "4\n", + "4\n", "\n", "\n", "I->0\n", @@ -2080,14 +2082,14 @@ "3->3\n", "\n", "\n", - "a & !b\n", - "\u24ff\n", + "a & b\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", "\n", "\n", "" @@ -2108,7 +2110,7 @@ "\n", "0\n", "\n", - "4\n", + "4\n", "\n", "\n", "I->0\n", diff --git a/tests/python/piperead.ipynb b/tests/python/piperead.ipynb index 19e2612f8..8859d5f57 100644 --- a/tests/python/piperead.ipynb +++ b/tests/python/piperead.ipynb @@ -15,7 +15,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.5.3" + "version": "3.5.4" }, "name": "" }, @@ -110,7 +110,7 @@ "\n" ], "text": [ - " *' at 0x7f2bb6866420> >" + " *' at 0x7f549852d270> >" ] }, { @@ -161,7 +161,7 @@ "\n" ], "text": [ - " *' at 0x7f2bb47205d0> >" + " *' at 0x7f549852d450> >" ] }, { @@ -194,20 +194,20 @@ "0->0\n", "\n", "\n", - "a\n", - "\u24ff\n", + "!a\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f2bb4720360> >" + " *' at 0x7f549852d270> >" ] }, { @@ -251,20 +251,20 @@ "1->1\n", "\n", "\n", - "b\n", - "\u24ff\n", + "!b\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "b\n", + "\u24ff\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f2bb47203f0> >" + " *' at 0x7f549852d120> >" ] } ], @@ -341,7 +341,7 @@ "\n" ], "text": [ - " *' at 0x7f2bb4720660> >" + " *' at 0x7f549852d1b0> >" ] } ], @@ -445,7 +445,7 @@ "\n" ], "text": [ - " *' at 0x7f2bb4720570> >" + " *' at 0x7f549852d360> >" ] }, { @@ -497,6 +497,15 @@ } ], "prompt_number": 6 + }, + { + "cell_type": "code", + "collapsed": true, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": null } ], "metadata": {} diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index 26e020965..947bd17e4 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -152,16 +152,16 @@ "0->0\n", "\n", "\n", - "b\n", - "\u24ff\n", - "\u2776\n", + "!b & c\n", + "\u24ff\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "1\n", @@ -178,16 +178,16 @@ "1->0\n", "\n", "\n", - "b & c\n", - "\u24ff\n", - "\u2776\n", + "!b & c\n", + "\u24ff\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "1->1\n", @@ -218,44 +218,44 @@ "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", "\n", - "0,0\n", + "0,0\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "2\n", "\n", - "0,1\n", + "0,1\n", "\n", "\n", "0->2\n", - "\n", + "\n", "\n", - "!b & !c\n", + "!b & !c\n", "\n", "\n", "1->1\n", @@ -275,7 +275,7 @@ "\n", "3\n", "\n", - "2,0\n", + "2,0\n", "\n", "\n", "1->3\n", @@ -313,7 +313,7 @@ "\n", "4\n", "\n", - "2,1\n", + "2,1\n", "\n", "\n", "2->4\n", @@ -327,18 +327,18 @@ "3->3\n", "\n", "\n", - "b\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "3->4\n", @@ -351,18 +351,18 @@ "4->3\n", "\n", "\n", - "b & c\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "4->4\n", @@ -500,16 +500,16 @@ "0->0\n", "\n", "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1\n", @@ -526,16 +526,16 @@ "1->0\n", "\n", "\n", - "b & c\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1->1\n", @@ -566,44 +566,44 @@ "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", "\n", - "0,0\n", + "0,0\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "2\n", "\n", - "0,1\n", + "0,1\n", "\n", "\n", "0->2\n", - "\n", + "\n", "\n", - "!b & !c\n", + "!b & !c\n", "\n", "\n", "1->1\n", @@ -623,7 +623,7 @@ "\n", "3\n", "\n", - "2,0\n", + "2,0\n", "\n", "\n", "1->3\n", @@ -661,7 +661,7 @@ "\n", "4\n", "\n", - "2,1\n", + "2,1\n", "\n", "\n", "2->4\n", @@ -675,18 +675,18 @@ "3->3\n", "\n", "\n", - "b\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "3->4\n", @@ -699,18 +699,18 @@ "4->3\n", "\n", "\n", - "b & c\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "4->4\n", @@ -895,16 +895,16 @@ "0->0\n", "\n", "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1\n", @@ -921,16 +921,16 @@ "1->0\n", "\n", "\n", - "b & c\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1->1\n", @@ -955,13 +955,13 @@ "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", @@ -970,15 +970,15 @@ "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "b\n", "\n", "\n", "2\n", @@ -987,9 +987,9 @@ "\n", "\n", "0->2\n", - "\n", + "\n", "\n", - "!b & !c\n", + "!b & !c\n", "\n", "\n", "1->1\n", @@ -1047,13 +1047,13 @@ "3->3\n", "\n", "\n", - "b\n", + "!b & c\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "b\n", "\n", "\n", "3->4\n", @@ -1065,13 +1065,13 @@ "4->3\n", "\n", "\n", - "b & c\n", + "!b & c\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "4->4\n", @@ -1282,16 +1282,16 @@ "0->0\n", "\n", "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1\n", @@ -1308,16 +1308,16 @@ "1->0\n", "\n", "\n", - "b & c\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1->1\n", @@ -1348,13 +1348,13 @@ "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", @@ -1363,18 +1363,18 @@ "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "2\n", @@ -1383,7 +1383,7 @@ "\n", "\n", "0->2\n", - "\n", + "\n", "\n", "!b & !c\n", "\n", @@ -1457,18 +1457,18 @@ "3->3\n", "\n", "\n", - "b\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "3->4\n", @@ -1481,18 +1481,18 @@ "4->3\n", "\n", "\n", - "b & c\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "4->4\n", @@ -1792,16 +1792,16 @@ "0->0\n", "\n", "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1\n", @@ -1818,16 +1818,16 @@ "1->0\n", "\n", "\n", - "b & c\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "1->1\n", @@ -1858,44 +1858,44 @@ "\n", "\n", "0\n", - "\n", - "1,0\n", + "\n", + "1,0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", "\n", - "0,0\n", + "0,0\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b\n", - "\u2776\n", - "\u2777\n", + "\n", + "\n", + "!b & c\n", + "\u2776\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!b & c\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "2\n", "\n", - "0,1\n", + "0,1\n", "\n", "\n", "0->2\n", - "\n", + "\n", "\n", - "!b & !c\n", + "!b & !c\n", "\n", "\n", "1->1\n", @@ -1915,7 +1915,7 @@ "\n", "3\n", "\n", - "2,0\n", + "2,0\n", "\n", "\n", "1->3\n", @@ -1953,7 +1953,7 @@ "\n", "4\n", "\n", - "2,1\n", + "2,1\n", "\n", "\n", "2->4\n", @@ -1967,18 +1967,18 @@ "3->3\n", "\n", "\n", - "b\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "3->4\n", @@ -1991,18 +1991,18 @@ "4->3\n", "\n", "\n", - "b & c\n", - "\u24ff\n", - "\u2776\n", - "\u2777\n", + "!b & c\n", + "\u24ff\n", + "\u2776\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!b & c\n", - "\u24ff\n", - "\u2776\n", + "\n", + "\n", + "b & c\n", + "\u24ff\n", + "\u2776\n", + "\u2777\n", "\n", "\n", "4->4\n", @@ -2060,7 +2060,7 @@ "output_type": "stream", "stream": "stdout", "text": [ - "1000 loops, best of 3: 233 \u00b5s per loop\n" + "1000 loops, best of 3: 216 \u00b5s per loop\n" ] } ], @@ -2079,7 +2079,8 @@ "output_type": "stream", "stream": "stdout", "text": [ - "100000 loops, best of 3: 11 \u00b5s per loop\n" + "The slowest run took 4.86 times longer than the fastest. This could mean that an intermediate result is being cached.\n", + "100000 loops, best of 3: 10.3 \u00b5s per loop\n" ] } ], diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 96eaea273..36ade4e3c 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -183,6 +183,6 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 "[1,8,9]" -[1] 0 [!1] 0 {0} +[1] 0 --END--""" diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index 0f7852f3d..715fdeafe 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -582,10 +582,10 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[0] 0 {0} [!0] 0 -[0&!1] 1 {0} +[0] 0 {0} [!0&!1] 1 +[0&!1] 1 {0} State: 1 [!1] 1 {0} --END--""" From f45112a235972c12474882f2e2f2f964e4678f61 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Mon, 25 Sep 2017 14:12:12 +0200 Subject: [PATCH 05/14] Fix a bug in scc_info, and clarify documentation * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Implement it * tests/python/sccinfo.py: Test it * NEWS: Document the fix --- NEWS | 5 +++-- spot/twaalgos/sccinfo.cc | 44 +++++++++++++++++++++++----------------- spot/twaalgos/sccinfo.hh | 13 +++++++++--- tests/python/sccinfo.py | 33 ++++++++++++++++++++++++++++-- 4 files changed, 69 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index 6e9f6462b..2c5c5ccbf 100644 --- a/NEWS +++ b/NEWS @@ -1,9 +1,10 @@ New in spot 2.4.0.dev (not yet released) - Nothing yet. - Bugs fixed: + - spot::scc_info::determine_unknown_acceptance() incorrectly + considered some rejecting SCC as accepting. + - The twa_graph::mege_edges() function relied on BDD IDs to sort edges. This in turn caused some algorithm (like the degeneralization) to produce slighltly different outputs (but diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index eda86b5b8..957afa7fb 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -368,26 +368,32 @@ namespace spot void scc_info::determine_unknown_acceptance() { std::vector k; - unsigned n = scc_count(); + unsigned s = scc_count(); bool changed = false; - for (unsigned s = 0; s < n; ++s) - if (!is_rejecting_scc(s) && !is_accepting_scc(s)) - { - if (!aut_->is_existential()) - throw std::runtime_error("scc_info::determine_unknown_acceptance() " - "does not support alternating automata"); - auto& node = node_[s]; - if (k.empty()) - k.resize(aut_->num_states()); - for (auto i: node.states_) - k[i] = true; - if (mask_keep_accessible_states(aut_, k, node.states_.front()) - ->is_empty()) - node.rejecting_ = true; - else - node.accepting_ = true; - changed = true; - } + // iterate over SCCs in topological order + do + { + --s; + if (!is_rejecting_scc(s) && !is_accepting_scc(s)) + { + if (!aut_->is_existential()) + throw std::runtime_error( + "scc_info::determine_unknown_acceptance() " + "does not support alternating automata"); + auto& node = node_[s]; + if (k.empty()) + k.resize(aut_->num_states()); + for (auto i: node.states_) + k[i] = true; + if (mask_keep_accessible_states(aut_, k, node.states_.front()) + ->is_empty()) + node.rejecting_ = true; + else + node.accepting_ = true; + changed = true; + } + } + while (s); if (changed) determine_usefulness(); } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 0b2d18e37..084a014bf 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -246,19 +246,21 @@ namespace spot return trivial_; } - /// \brief True if we are sure that the SCC is accepting + /// \brief True if we know that the SCC has an accepting cycle /// /// Note that both is_accepting() and is_rejecting() may return /// false if an SCC interesects a mix of Fin and Inf sets. + /// Call determine_unknown_acceptance() to decide. bool is_accepting() const { return accepting_; } - // True if we are sure that the SCC is rejecting + /// \brief True if we know that all cycles in the SCC are rejecting /// /// Note that both is_accepting() and is_rejecting() may return /// false if an SCC interesects a mix of Fin and Inf sets. + /// Call determine_unknown_acceptance() to decide. bool is_rejecting() const { return rejecting_; @@ -295,9 +297,14 @@ namespace spot /// /// This takes twa_graph as input and compute its SCCs. This /// class maps all input states to their SCCs, and vice-versa. - /// It allows iterating over all SCCs of the automaton, and check + /// It allows iterating over all SCCs of the automaton, and checks /// their acceptance or non-acceptance. /// + /// SCC are numbered in reverse topological order, i.e. the SCC of the + /// initial state has the highest number, and if s1 is reachable from + /// s2, then s1 < s2. Many algorithms depend on this property to + /// determine in what order to iterate the SCCs. + /// /// Additionally this class can be used on alternating automata, but /// in this case, universal transitions are handled like existential /// transitions. It still make sense to check which states belong diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py index 16267fdf4..264a308f7 100644 --- a/tests/python/sccinfo.py +++ b/tests/python/sccinfo.py @@ -52,8 +52,6 @@ l3 = si.states_of(3) l = sorted(list(l0) + list(l1) + list(l2) + list(l3)) assert l == [0, 1, 2, 3, 4] - - i = si.initial() todo = {i} seen = {i} @@ -77,3 +75,34 @@ assert transi == [(0, 0, 1), (0, 3, 4), (3, 0, 7), (3, 3, 9), (1, 1, 5), (2, 2, 6), (4, 4, 12)] assert not spot.is_weak_automaton(a, si) + + +a = spot.automaton(""" +HOA: v1 +States: 4 +Start: 0 +AP: 1 "a" +Acceptance: 2 Inf(0)&Fin(1) +--BODY-- +State: 0 +[t] 0 {1} +[t] 1 {0} +State: 1 +[t] 1 {1} +[t] 0 {1} +[t] 2 +State: 2 +[t] 2 {1} +[t] 3 {0} +State: 3 +[t] 3 {1} +[t] 2 +--END-- +""") +si = spot.scc_info(a) +si.determine_unknown_acceptance() +assert si.scc_count() == 2 +assert si.is_accepting_scc(0) +assert not si.is_rejecting_scc(0) +assert si.is_rejecting_scc(1) +assert not si.is_accepting_scc(1) From cfa80ed842f90e1cfb6edb5bae16e63f60a38d22 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Sep 2017 10:54:09 +0200 Subject: [PATCH 06/14] tests: avoid some superfluous calls to remove_alternation() * tests/python/toweak.py: Here. --- tests/python/toweak.py | 32 ++++++++++---------------------- 1 file changed, 10 insertions(+), 22 deletions(-) diff --git a/tests/python/toweak.py b/tests/python/toweak.py index c1b3ade93..b21827a83 100644 --- a/tests/python/toweak.py +++ b/tests/python/toweak.py @@ -30,30 +30,20 @@ GF!b (b & GF!b) | (!b & FGb) b | (a & XF(b R a)) | (!a & XG(!b U !a))""" -phi1 = phi1.split('\n') - -bdddict = spot.make_bdd_dict() - def equivalent(a, phi): - negphi = spot.formula.Not(phi) - nega = spot.dualize(a) - a2 = spot.translate(phi, 'TGBA', 'SBAcc' ) - nega2 = spot.translate(negphi, 'TGBA', 'SBAcc') - ra = spot.remove_alternation(a) - ran = spot.remove_alternation(nega) - return spot.product(spot.remove_alternation(a), nega2).is_empty()\ - and spot.product(spot.remove_alternation(nega), a2).is_empty() + negphi = spot.formula.Not(phi) + nega = spot.dualize(a) + return not (spot.translate(negphi).intersects(a) + or spot.translate(phi).intersects(nega)) def test_phi(phi): - a = spot.translate(phi, 'TGBA', 'SBAcc') - a0 = spot.dualize(a) - - res = spot.to_weak_alternating(a0) - assert equivalent(res, spot.formula.Not(spot.formula(phi))) - -for p in phi1: - test_phi(p) + a = spot.translate(phi, 'TGBA', 'SBAcc') + res = spot.to_weak_alternating(spot.dualize(a)) + assert equivalent(res, spot.formula.Not(spot.formula(phi))) +for p in phi1.split('\n'): + print(p) + test_phi(p) phi2 = spot.formula("(G((F a) U b)) W a") a2 = spot.automaton(""" @@ -99,5 +89,3 @@ State: 6 """) a2 = spot.to_weak_alternating(a2) assert equivalent(a2, phi2) - - From 32087f29ad6c547e2cbbe007a913458718026f17 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 26 Sep 2017 17:17:17 +0200 Subject: [PATCH 07/14] streett_to_generalized_buchi: fix incorrect algorithm Fixes #284, reported by Juraj Major. * spot/twaalgos/totgba.cc: Fix the algorithm. * spot/twa/acc.hh: More doc for future generations. * tests/core/scc.test: More test cases. * NEWS: Mention the issues. --- NEWS | 7 ++++++ spot/twa/acc.hh | 9 +++++++ spot/twaalgos/totgba.cc | 24 ++++++++++++------- tests/core/scc.test | 53 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 85 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 2c5c5ccbf..de0c76ca5 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,13 @@ New in spot 2.4.0.dev (not yet released) - spot::scc_info::determine_unknown_acceptance() incorrectly considered some rejecting SCC as accepting. + - spot::streett_to_generalized_buchi() could generate automata with + empty language if some Fin set did not intersect all accepting + SCCs. As a consequence, some Streett-like automata were + considered empty even though they were not. Also, the same + function could crash on input that had a Streett-like acceptance + not using all declared sets. + - The twa_graph::mege_edges() function relied on BDD IDs to sort edges. This in turn caused some algorithm (like the degeneralization) to produce slighltly different outputs (but diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index eaaf8419a..5c0535974 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1046,6 +1046,15 @@ namespace spot // Returns a number of pairs (>=0) if Streett, or -1 else. int is_streett() const; + /// \brief Rabin/streett pairs used by is_rabin_like and is_streett_like. + /// + /// These pairs hold two marks which can each contain one or no set. + /// + /// For instance is_streett_like() rewrites Inf(0)&(Inf(2)|Fin(1))&Fin(3) + /// as three pairs: [(fin={},inf={0}),(fin={1},inf={2}),(fin={3},inf={})]. + /// + /// Empty marks should be interpreted in a way that makes them + /// false in Streett, and true in Rabin. struct SPOT_API rs_pair { rs_pair() = default; diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index ea8f981ac..8021cd903 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -130,7 +130,9 @@ namespace spot acc_cond::mark_t fin; std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets(); unsigned p = inf.count(); - acc_cond::mark_t fin_not_inf = fin - inf; + // At some point we will remove anything that is not used as Inf. + acc_cond::mark_t to_strip = in->acc().all_sets() - inf; + acc_cond::mark_t inf_alone = 0U; if (!p) return remove_fin(in); @@ -140,8 +142,11 @@ namespace spot std::vector inf_to_finpairs(numsets, 0U); for (auto pair: pairs) { - for (unsigned mark: pair.fin.sets()) - fin_to_infpairs[mark] |= pair.inf; + if (pair.fin) + for (unsigned mark: pair.fin.sets()) + fin_to_infpairs[mark] |= pair.inf; + else + inf_alone |= pair.inf; for (unsigned mark: pair.inf.sets()) inf_to_finpairs[mark] |= pair.fin; @@ -231,11 +236,14 @@ namespace spot for (unsigned mark: (t.acc & fin).sets()) pend |= fin_to_infpairs[mark]; + // If we see some Inf set immediately, they are not + // pending anymore. pend -= t.acc & inf; + // Label this transition with all non-pending // inf sets. The strip will shift everything // to the correct numbers in the targets. - acc = (inf - pend).strip(fin - inf); + acc = (inf - pend).strip(to_strip); // Adjust the pending sets to what will be necessary // required on the destination state. if (sbacc) @@ -248,14 +256,14 @@ namespace spot pend -= a & inf; } - pend |= scc_inf_wo_fin; + pend |= inf_alone; } else if (no_fin && maybe_acc) { // If the acceptance is (Fin(0) | Inf(1)) & Inf(2) - // but we do not see any Fin set in this SCC, an + // but we do not see any Fin set in this SCC, a // mark {2} should become {1,2} before striping. - acc = (t.acc | (inf - scc_inf_wo_fin)).strip(fin_not_inf); + acc = (t.acc | (inf - scc_inf_wo_fin)).strip(to_strip); } assert((acc & out->acc().all_sets()) == acc); @@ -291,7 +299,7 @@ namespace spot stpend -= a & inf; } - st2gba_state d(t.dst, stpend | scc_inf_wo_fin); + st2gba_state d(t.dst, stpend | inf_alone); // Have we already seen this destination? unsigned dest; auto dres = bs2num.emplace(d, 0); diff --git a/tests/core/scc.test b/tests/core/scc.test index 8835402c5..b1a8704f2 100755 --- a/tests/core/scc.test +++ b/tests/core/scc.test @@ -139,3 +139,56 @@ State: 3 {1} --END-- EOF test 2 = `autfilt --stats=%[a]c in.hoa` + +# From issue #284, reported by Juraj Major. +cat >in.hoa <out +cat >exp < Date: Tue, 26 Sep 2017 17:30:54 +0200 Subject: [PATCH 08/14] formula: fix building of {a->c[*]} MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #285, reported by Florian Perlié-Long. * NEWS: Mention the issue. * spot/tl/formula.cc: Fix it. * tests/core/kind.test: Document it. * THANKS: Add Florian. --- NEWS | 3 +++ THANKS | 1 + spot/tl/formula.cc | 3 ++- tests/core/kind.test | 5 +++-- 4 files changed, 9 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index de0c76ca5..0788216ea 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,9 @@ New in spot 2.4.0.dev (not yet released) Bugs fixed: + - The formula class failed to build {a->c[*]} althought it is + alowed in our grammar. + - spot::scc_info::determine_unknown_acceptance() incorrectly considered some rejecting SCC as accepting. diff --git a/THANKS b/THANKS index 7a4d7d938..7a235bdc6 100644 --- a/THANKS +++ b/THANKS @@ -11,6 +11,7 @@ Ernesto Posse Étienne Renault Fabrice Kordon Felix Klaedtke +Florian Perlié-Long František Blahoudek Gerard J. Holzmann Heikki Tauriainen diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 0b0dced0f..2a5238a95 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1281,7 +1281,8 @@ namespace spot props = children[0]->props & children[1]->props; is_.eventual = false; is_.universal = false; - is_.sere_formula = is_.boolean; + is_.sere_formula = (children[0]->is_boolean() + && children[1]->is_sere_formula()); is_.sugar_free_boolean = false; is_.in_nenoform = false; is_.syntactic_safety = (children[0]->is_syntactic_guarantee() diff --git a/tests/core/kind.test b/tests/core/kind.test index b0733bc2d..416eb0c1d 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2012, 2015, 2017 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -133,6 +133,7 @@ Fa M b,&!xLPgopra {p[+]:p[+]},&!xfPsoprla (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla {b[+][:*0..3]},&!fPsopra +{a->c[*]},fPsopra EOF run 0 ../kind input From 7987d71ae83799f2b7979461ffa23950aa359931 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 26 Sep 2017 22:27:35 +0200 Subject: [PATCH 09/14] * spot/twaalgos/totgba.cc: Typos in comment. --- spot/twaalgos/totgba.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 8021cd903..6f3081265 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -284,7 +284,7 @@ namespace spot // Nondeterministically jump to level ∅. We need to do // that only once per cycle. As an approximation, we - // only to that for transition where t.src >= t.dst as + // only do that for transitions where t.src >= t.dst as // this has to occur at least once per cycle. if (pend == orig_copy && (t.src >= t.dst) && maybe_acc && !no_fin) { From 7e394506b60c41c3af3aea35eedb9e15b378b6fb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 Sep 2017 20:38:13 +0200 Subject: [PATCH 10/14] simulation: incorrect setting of non-deterministic property Fixes #286. * spot/twaalgos/simulation.cc: Only set the deterministic property, not the non-deterministic one. * tests/core/ltl2tgba.test: Add test case. * NEWS: Mention the issue. --- NEWS | 3 +++ spot/twaalgos/simulation.cc | 10 +++++++--- tests/core/ltl2tgba.test | 5 +++++ 3 files changed, 15 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 0788216ea..e7272c0e6 100644 --- a/NEWS +++ b/NEWS @@ -21,6 +21,9 @@ New in spot 2.4.0.dev (not yet released) still correct outputs) depending on the BDD operations performed before. + - spot::simulation() would occasionally incorrectly flag an + automaton as non-deterministic. + New in spot 2.4 (2017-09-06) Build: diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index d6828f8bb..cddc529cc 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -582,7 +582,9 @@ namespace spot res->set_init_state(gb->get_state(previous_class_ [a_->get_init_state_number()].id())); - res->merge_edges(); // FIXME: is this really needed? + res->merge_edges(); // This helps merging some edges with + // identical conditions, but different + // mark sets. // Mark all accepting state in a second pass, when // dealing with SBA in cosimulation. @@ -616,8 +618,10 @@ namespace spot true, // stutter inv. }); // !unambiguous and !semi-deterministic are not preserved - if (!Cosimulation) - res->prop_universal(nb_minato == nb_satoneset); + if (!Cosimulation && nb_minato == nb_satoneset) + // Note that nb_minato != nb_satoneset does not imply + // non-deterministic, because of the merge_edges() above. + res->prop_universal(true); if (Sba) res->prop_state_acc(true); return res; diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index 50703a1a1..6a7131774 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -265,3 +265,8 @@ ltl2tgba -xsimul=1 --low "$f1" "$f2" > res2 diff res1 res2 test 3 = `ltl2tgba -f 'G(Fa & Fb) U a' --stats=%s` + +# issue #286, the following automaton caused the print_hoa() function to +# report inconsistent "universal" property. +ltl2tgba --low 'X(((1) U (p1)) | (((p1) | (F(p0))) U ((0) R ((p2) M (p1)))))'>o +grep deterministic o From 7b6346d38d5c21beab603223691992e9ad350780 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Mon, 2 Oct 2017 10:58:30 +0200 Subject: [PATCH 11/14] Typos * NEWS: typos --- NEWS | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/NEWS b/NEWS index e7272c0e6..fc81e3185 100644 --- a/NEWS +++ b/NEWS @@ -2,8 +2,8 @@ New in spot 2.4.0.dev (not yet released) Bugs fixed: - - The formula class failed to build {a->c[*]} althought it is - alowed in our grammar. + - The formula class failed to build {a->c[*]} although it is + allowed by our grammar. - spot::scc_info::determine_unknown_acceptance() incorrectly considered some rejecting SCC as accepting. @@ -15,14 +15,13 @@ New in spot 2.4.0.dev (not yet released) function could crash on input that had a Streett-like acceptance not using all declared sets. - - The twa_graph::mege_edges() function relied on BDD IDs to sort - edges. This in turn caused some algorithm (like the - degeneralization) to produce slighltly different outputs (but - still correct outputs) depending on the BDD operations performed - before. + - The twa_graph::merge_edges() function relied on BDD IDs to sort + edges. This in turn caused some algorithms (like the + degeneralization) to produce slighltly different (but still correct) + outputs depending on the BDD operations performed before. - - spot::simulation() would occasionally incorrectly flag an - automaton as non-deterministic. + - spot::simulation() could incorrectly flag an automaton as + non-deterministic. New in spot 2.4 (2017-09-06) From 89c312cb57329b531855af34b61b266c21eca4e2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Florian=20Perli=C3=A9-Long?= Date: Tue, 3 Oct 2017 08:57:42 +0200 Subject: [PATCH 12/14] * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos --- HACKING | 2 +- doc/tl/tl.tex | 6 +++--- spot/tl/formula.hh | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/HACKING b/HACKING index ec7cacf85..9dae74a74 100644 --- a/HACKING +++ b/HACKING @@ -609,7 +609,7 @@ SPOT macros that a compiler might not see as unreachable. * Use SPOT_API in front of functions and class that should be - exported by the shared library. See "Exporting symbolss" above. + exported by the shared library. See "Exporting symbols" above. * Use SPOT_ASSERT(...) if you ever have to put an assertion in some header file. See "Assertions" above. diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 1831e66ab..dbaad34ce 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -206,7 +206,7 @@ Let $\N=\{0,1,2,\ldots\}$ denote the set of natural numbers and $\omega\not\in\N$ the first transfinite ordinal. We extend the $<$ -relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in N,\, +relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in \N,\, n<\omega$. Similarly let us extend the addition and subtraction with $\forall n\in\N,\,\omega+n = \omega-n = \omega+\omega = \omega$. @@ -1323,8 +1323,8 @@ rewriting arrange any PSL formula into negative normal form. \NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)& \NOT(\sere{r} \Esuffix f) &\equiv \sere{r} \Asuffix \NOT f \end{align*} -\noindent Recall the that negated weak closure $\nsere{r}$ is actually -implemented as a specific operator, so it not actually prefixed by the +\noindent Recall that the negated weak closure $\nsere{r}$ is actually +implemented as a specific operator, so it is not actually prefixed by the $\NOT$ operator. \begin{align*} f \XOR g & \equiv ((\NOT f)\AND g)\OR(f\AND\NOT g) & diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 4b299ba58..28c04216e 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -72,7 +72,7 @@ namespace spot G, ///< Globally Closure, ///< PSL Closure NegClosure, ///< Negated PSL Closure - NegClosureMarked, ///< marked version of the Negated PSL Clusure + NegClosureMarked, ///< marked version of the Negated PSL Closure // binary operators Xor, ///< Exclusive Or Implies, ///< Implication From d2c4e596d158d3b149cb23d1452dee96e8172a09 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Oct 2017 15:44:14 +0200 Subject: [PATCH 13/14] org: fix the dot2tex example * doc/org/oaut.org: Fix the call to convert. --- doc/org/oaut.org | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 70e2c3bd5..dac51f0a2 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -899,7 +899,7 @@ following figure: #+BEGIN_SRC sh :results silent :exports results ltl2tgba 'p0 U p1' --dot=x | dot2tex --autosize --nominsize > dot2tex.tex latexmk --pdf dot2tex.tex - convert -density 300 -scale='50%' -trim dot2tex.pdf dot2tex.png + convert -density 300 -scale '50%' -trim dot2tex.pdf dot2tex.png latexmk -C dot2tex.tex rm -f dot2tex.tex #+END_SRC @@ -914,7 +914,7 @@ ltl2tgba -G -D '!a & FGa' --dot=sbarx | dot2tex --autosize --nominsize > out.tex #+BEGIN_SRC sh :results silent :exports results ltl2tgba -G -D '!a & FGa' --dot=sbarx | dot2tex --autosize --nominsize > dot2tex2.tex latexmk --pdf dot2tex2.tex - convert -density 300 -scale='50%' -trim dot2tex2.pdf dot2tex2.png + convert -density 300 -scale '50%' -trim dot2tex2.pdf dot2tex2.png latexmk -C dot2tex2.tex rm -f dot2tex2.tex #+END_SRC From 5c22db3c73d08b4f35cb80188f1c91fb3a8cc3e8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Oct 2017 15:49:43 +0200 Subject: [PATCH 14/14] Release Spot 2.4.1 * NEWS, configure.ac, doc/org/setup.org: Bump version. --- NEWS | 2 +- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index fc81e3185..f86ad9c94 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.4.0.dev (not yet released) +New in spot 2.4.1 (2017-10-05) Bugs fixed: diff --git a/configure.ac b/configure.ac index e018ad886..aac8ae758 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.4.0.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.4.1], [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 d4c14b803..f3a078913 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.4 -#+MACRO: LASTRELEASE 2.4 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.4.tar.gz][=spot-2.4.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-4/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-09-06 +#+MACRO: SPOTVERSION 2.4.1 +#+MACRO: LASTRELEASE 2.4.1 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.4.1.tar.gz][=spot-2.4.1.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-4-1/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2017-10-05