From 5e5a69488efab441b72796d7ad72d23b6943f032 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Sep 2017 16:06:41 +0200 Subject: [PATCH] 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/genltl.test: Adjust, and add an extra test for the behavior of #282. * 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/genltl.test | 20 +- 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 +- 19 files changed, 798 insertions(+), 735 deletions(-) diff --git a/NEWS b/NEWS index a0cef234b..a8d7f1a9f 100644 --- a/NEWS +++ b/NEWS @@ -76,6 +76,14 @@ New in spot 2.4.0.dev (not yet released) spot::scc_info::marks(), spot::scc_info::marks_of() and spot::scc_info::acc_sets_of() respectively. + 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/genltl.test b/tests/core/genltl.test index f49045af1..0fb4d4b80 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -136,7 +136,7 @@ test $(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16 test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16 genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \ - --format=%F=%L,%f | + --gf-equiv=0..5 --format=%F=%L,%f | ltl2tgba -G -D -F-/2 --stats='%<,%s' > out cat >exp< out -cat >exp< out +diff out exp 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--"""