diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 1d7e68a3d..6c17d073f 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -471,7 +471,8 @@ namespace spot { private: bool - get_alone_mark(bool& fin, acc_cond::mark_t& mark, bool& conj, acc_code& code) + get_alone_mark(bool& fin, acc_cond::mark_t& mark, bool& conj, + acc_code& code) { auto elements = top_conjuncts(); conj = (elements.size() > 1); @@ -510,19 +511,25 @@ namespace spot auto elements = result.top_disjuncts(); if (elements.size() < 2) elements = result.top_conjuncts(); - result = std::accumulate(elements.begin(), elements.end(), code, + acc_code init_code; + if (conj) + init_code = acc_code::t(); + else + init_code = acc_code::f(); + bool keeped_code = false; + result = std::accumulate(elements.rbegin(), elements.rend(), + init_code, [&](acc_code a, acc_code b) { - if (b != code) - { - b = b.remove(mark, !fin); - if (conj) - return a & b; - else - return a | b; - } - return a; - }); + if (b != code || keeped_code) + b = b.remove(mark, fin == conj); + if (b == code) + keeped_code = true; + if (conj) + return a & b; + else + return a | b; + }); } std::vector elements = result.top_disjuncts(); if (elements.size() < 2) @@ -534,7 +541,8 @@ namespace spot init_code = acc_code::t(); else init_code = acc_code::f(); - result = std::accumulate(elements.begin(), elements.end(), init_code, + result = std::accumulate(elements.rbegin(), elements.rend(), + init_code, [&](acc_code a, acc_code b) { if (conj) diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 8065cc8f6..8a3772c8b 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -619,8 +619,13 @@ namespace spot simplify_complementary_marks_here(aut); fuse_marks_here(aut); } - aut->set_acceptance(aut->acc().propagate_fin_inf()); cleanup_acceptance_here(aut, true); + auto prop_cond = aut->acc().propagate_fin_inf(); + if (prop_cond != aut->acc()) + { + aut->set_acceptance(prop_cond); + cleanup_acceptance_here(aut, true); + } return aut; } diff --git a/tests/core/accsimpl.test b/tests/core/accsimpl.test index 1feb8fed4..2339690bc 100755 --- a/tests/core/accsimpl.test +++ b/tests/core/accsimpl.test @@ -49,5 +49,5 @@ State: 0 EOF autfilt --simplify-acceptance 325 > 325s -exp='4 Fin(0) | (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))' +exp='3 Fin(0) | (Fin(1) & Inf(2))' test "$exp" = "`autfilt --stats='%a %g' 325s`" diff --git a/tests/core/remfin.test b/tests/core/remfin.test index c50272339..0b387d8e0 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -336,27 +336,24 @@ State: 3 [!0&!1] 3 {0} --END-- HOA: v1 -States: 4 +States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 4 (Inf(0)&Inf(1)) | Inf(0) | (Inf(2)&Inf(3)) +Acceptance: 3 (Inf(1)&Inf(2)) | Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 -[t] 0 {3} -[0] 1 {3} -[!0] 2 {0 3} +[t] 0 {2} +[0] 1 {2} +[!0] 2 {0 2} State: 1 -[1] 0 {3} -[0&1] 1 {0 3} -[!0&1] 2 {2 3} +[1] 0 {2} +[0&1] 1 {0 2} +[!0&1] 2 {1 2} State: 2 [!1] 0 [0&!1] 1 {0} [!0&!1] 2 {0} -[!0&!1] 3 -State: 3 -[!0&!1] 3 {0 1} --END-- HOA: v1 States: 1 @@ -942,7 +939,7 @@ State: 3 [!0&!1] 3 {0} --END-- HOA: v1 -States: 4 +States: 3 Start: 0 AP: 2 "a" "b" acc-name: Buchi @@ -961,9 +958,6 @@ State: 2 [!1] 0 [0&!1] 1 {0} [!0&!1] 2 {0} -[!0&!1] 3 -State: 3 -[!0&!1] 3 {0} --END-- HOA: v1 States: 1 diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 56472b1f5..61971c52e 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -33,11 +33,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -56,129 +56,129 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b & !d\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b & !c & d\n", + "\n", + "\n", + "b & !c & d\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde0062f990> >" + " *' at 0x7fa0443228a0> >" ] }, "execution_count": 2, @@ -211,146 +211,146 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b & !d\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b & !c & d\n", + "\n", + "\n", + "b & !c & d\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" @@ -389,21 +389,21 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "cluster_0\n", - "\n", + "\n", "\n", "\n", "cluster_1\n", - "\n", + "\n", "\n", "\n", "cluster_2\n", @@ -427,125 +427,125 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "b & c & d\n", + "\n", + "\n", + "b & c & d\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b & !d\n", + "\n", + "\n", + "b & !d\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "b & !c & d\n", + "\n", + "\n", + "b & !c & d\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c & d\n", - "\n", + "\n", + "\n", + "c & d\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!d\n", - "\n", + "\n", + "\n", + "!d\n", + "\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!c & d\n", - "\n", + "\n", + "\n", + "!c & d\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "c & d\n", + "\n", + "\n", + "c & d\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!d\n", + "\n", + "\n", + "!d\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!c & d\n", + "\n", + "\n", + "!c & d\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" @@ -607,11 +607,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -630,34 +630,34 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde0062f9f0> >" + " *' at 0x7fa044322570> >" ] }, "execution_count": 6, @@ -683,11 +683,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -706,34 +706,34 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde006764b0> >" + " *' at 0x7fa0443309c0> >" ] }, "execution_count": 7, @@ -766,12 +766,12 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", @@ -790,33 +790,33 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde00676e70> >" + " *' at 0x7fa044330ab0> >" ] }, "execution_count": 8, @@ -872,11 +872,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -921,15 +921,15 @@ "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "c\n", "\n", "\n", @@ -949,9 +949,9 @@ "\n", "\n", "3->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n" @@ -983,199 +983,199 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "6\n", - "\n", - "\n", - "6\n", + "\n", + "\n", + "6\n", "\n", "\n", "\n", "I->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "5\n", + "\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "4->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" @@ -1214,14 +1214,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1238,118 +1238,118 @@ "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde00641300> >" + " *' at 0x7fa044336bd0> >" ] }, "execution_count": 12, @@ -1386,10 +1386,10 @@ " viewBox=\"0.00 0.00 165.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1421,7 +1421,7 @@ "0->1\n", "\n", "\n", - "b\n", + "b\n", "\n", "\n", "\n", @@ -1441,14 +1441,14 @@ "1->1\n", "\n", "\n", - "!b\n", + "!b\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "b\n", + "b\n", "\n", "\n", "\n", @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde006418d0> >" + " *' at 0x7fa0443364e0> >" ] }, "execution_count": 13, @@ -1496,11 +1496,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -1533,7 +1533,7 @@ "0->1\n", "\n", "\n", - "b\n", + "b\n", "\n", "\n", "\n", @@ -1554,19 +1554,19 @@ "1->1\n", "\n", "\n", - "b\n", + "b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", + "\n", + "\n", "!b\n", "\n", "\n", @@ -1579,22 +1579,22 @@ "\n", "\n", "3->1\n", - "\n", - "\n", + "\n", + "\n", "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde00641540> >" + " *' at 0x7fa044336e70> >" ] }, "execution_count": 14, @@ -1692,128 +1692,128 @@ "\n", "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ") & Fin(\n", - "\n", - ")) | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde00641b10> >" + " *' at 0x7fa0442cea20> >" ] }, "metadata": {}, @@ -1828,142 +1828,122 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | Inf(\n", - "\n", - ") | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - "))\n", - "[Fin-less 4]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + "))\n", + "[Fin-less 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde00676780> >" + " *' at 0x7fa0442ce9c0> >" ] }, "metadata": {}, @@ -1978,339 +1958,239 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a | b\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fde00641630> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", - "1->3\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "4\n", - "\n", - "\n", "\n", - "1->4\n", - "\n", - "\n", - "!a & b\n", + "1->3\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", "\n", - "4->0\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "!a & !b\n", + "3->3\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde00641870> >" + " *' at 0x7fa0442ce1e0> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fa0442ceb70> >" ] }, "metadata": {}, @@ -2348,155 +2228,155 @@ "\n", "\n", - "\n", - "\n", - "\n", - "(Inf(\n", - "\n", - ") & Fin(\n", - "\n", - ") & Fin(\n", - "\n", - ")) | (Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")) | Inf(\n", - "\n", - ")\n", + "\n", + "\n", + "\n", + "(Inf(\n", + "\n", + ") & Fin(\n", + "\n", + ") & Fin(\n", + "\n", + ")) | (Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")) | Inf(\n", + "\n", + ")\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", + "\n", + "\n", + "a\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde006768d0> >" + " *' at 0x7fa0442c6360> >" ] }, "execution_count": 19, @@ -2526,7 +2406,7 @@ " viewBox=\"0.00 0.00 173.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", "\n", - "[Büchi]\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2572,7 +2452,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde006417e0> >" + " *' at 0x7fa0442c69c0> >" ] }, "execution_count": 20, @@ -2629,10 +2509,10 @@ " viewBox=\"0.00 0.00 165.00 130.42\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", "\n", - "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "Inf(\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2690,14 +2570,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "Inf(\n", - "\n", - ")\n", - "[Büchi]\n", + "\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -2716,35 +2596,35 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!c\n", + "\n", + "\n", + "!c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c\n", - "\n", + "\n", + "\n", + "c\n", + "\n", "\n", "\n", "\n", @@ -2766,15 +2646,15 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", "[gen. Büchi 2]\n", "\n", "\n", @@ -2794,99 +2674,99 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "a & b\n", - "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "1,1\n", + "\n", + "1,1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !c\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & c\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & c\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -2896,16 +2776,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", @@ -2927,105 +2807,105 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "a & !b\n", "\n", "\n", "\n", "\n", "1\n", "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "a & b\n", - "\n", + "\n", "\n", "\n", "\n", "2\n", "\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !c\n", - "\n", + "\n", + "\n", + "a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & !c\n", + "\n", + "\n", + "!a & !c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a & c\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & c\n", - "\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", "\n", @@ -3076,7 +2956,7 @@ " viewBox=\"0.00 0.00 169.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", "\n", - "[Büchi]\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3122,7 +3002,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde006412d0> >" + " *' at 0x7fa0442e1e40> >" ] }, "metadata": {}, @@ -3162,12 +3042,12 @@ " viewBox=\"0.00 0.00 170.00 140.47\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -3222,7 +3102,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde00641360> >" + " *' at 0x7fa0442c64e0> >" ] }, "execution_count": 24, @@ -3255,47 +3135,47 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "Fin(\n", - "\n", - ")\n", + "\n", + ")\n", "[co-Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde00641090> >" + " *' at 0x7fa0442e9960> >" ] }, "execution_count": 25, @@ -3332,10 +3212,10 @@ " viewBox=\"0.00 0.00 182.74 130.74\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", "\n", - "Fin(\n", - "\n", - ")\n", - "[co-Büchi]\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -3421,52 +3301,52 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", + "\n", "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[parity max odd 3]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde006419c0> >" + " *' at 0x7fa0442f2540> >" ] }, "execution_count": 27, @@ -3503,7 +3383,7 @@ " viewBox=\"0.00 0.00 169.00 124.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n", "\n", "\n", - "[Büchi]\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3549,7 +3429,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fde006412d0> >" + " *' at 0x7fa0442e1e40> >" ] }, "metadata": {}, @@ -3564,11 +3444,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3587,34 +3467,34 @@ "0->0\n", "\n", "\n", - "b\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde006412d0> >" + " *' at 0x7fa0442e1e40> >" ] }, "metadata": {}, @@ -3651,11 +3531,11 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "[Büchi]\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3674,34 +3554,34 @@ "0->0\n", "\n", "\n", - "b\n", + "b\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "a & b & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fde006412d0> >" + " *' at 0x7fa0442e1e40> >" ] }, "execution_count": 29, @@ -3734,7 +3614,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.5" + "version": "3.8.2" } }, "nbformat": 4, diff --git a/tests/python/merge.py b/tests/python/merge.py index 5d0997a25..161b9b6fd 100644 --- a/tests/python/merge.py +++ b/tests/python/merge.py @@ -78,7 +78,7 @@ assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -Acceptance: 2 Fin(1) | (Inf(0)&Inf(1)) +Acceptance: 2 Fin(1) | Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 diff --git a/tests/python/toparity.py b/tests/python/toparity.py index d6159ae83..95c01ad61 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -19,6 +19,7 @@ # along with this program. If not, see . import spot +import itertools # Tests for the new version of to_parity @@ -89,8 +90,9 @@ options = [ ] -def test(aut, full=True): - for opt in options: +def test(aut, expected_num_states=[], full=True): + for (opt, expected_num) in\ + itertools.zip_longest(options, expected_num_states): p1 = spot.to_parity(aut, search_ex = opt.search_ex, use_last = opt.use_last, @@ -105,6 +107,8 @@ def test(aut, full=True): pretty_print = opt.pretty_print, ) assert spot.are_equivalent(aut, p1) + if (expected_num != None): + assert(p1.num_states() == expected_num) if full: # Make sure passing opt is the same as setting # each argument individually @@ -191,7 +195,7 @@ State: 13 [0&1] 5 [!0&!1] 10 {0 1 3 5} [0&!1] 13 {1 3} ---END--""")) +--END--"""), [35, 28, 23, 30, 29, 25, 22]) test(spot.automaton(""" HOA: v1 @@ -209,7 +213,7 @@ State: 1 [0&!1] 1 {4} [!0&1] 1 {0 1 2 3} [!0&!1] 1 {0 3} ---END--""")) +--END--"""), [7, 5, 3, 6, 5, 5, 3]) for i,f in enumerate(spot.randltl(10, 400)): @@ -250,7 +254,7 @@ State: 3 [!0&1] 2 {1 4} [0&1] 3 {0} --END-- -""")) +"""), [80, 22, 80, 80, 80, 17, 10]) test(spot.automaton(""" HOA: v1 @@ -284,7 +288,7 @@ State: 4 [0&!1] 4 [0&1] 4 {1 2 4} --END-- -""")) +"""), [9, 6, 6, 6, 7, 6, 6]) test(spot.automaton(""" HOA: v1 @@ -306,7 +310,7 @@ State: 1 [0&!1] 1 {2 3} [0&1] 1 {1 2 4} --END-- -""")) +"""), [11, 6, 3, 7, 7, 4, 3]) # Tests both the old and new version of to_parity @@ -337,8 +341,7 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} p = spot.to_parity_old(a, True) assert p.num_states() == 22 assert spot.are_equivalent(a, p) -test(a) -assert spot.to_parity(a).num_states() == 6 +test(a, [8, 7, 8, 8, 6, 7, 6]) for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") @@ -354,4 +357,4 @@ for f in spot.randltl(5, 2000): a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') b = spot.to_parity_old(a, True) assert a.equivalent_to(b) -test(a) +test(a, [7, 7, 3, 7, 8, 7, 3])