From 8df5f5137e618973034bf5fde0e903fde4e440cf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 18 Jun 2019 10:06:56 +0200 Subject: [PATCH] gfguarantee: fix #357 again The previous patch triggered this issue again, failing core/ltl2tgba2.test. * spot/twaalgos/gfguarantee.cc: Separate the replaying of history from the modification of the automaton. * NEWS: Mention the bug. * tests/python/twagraph-internals.ipynb, tests/python/automata.ipynb: Adjust. --- NEWS | 6 + spot/twaalgos/gfguarantee.cc | 207 +- tests/python/automata.ipynb | 417 ++- tests/python/twagraph-internals.ipynb | 4142 ++++++++++++------------- 4 files changed, 2379 insertions(+), 2393 deletions(-) diff --git a/NEWS b/NEWS index 6a6990aed..3cbbe0331 100644 --- a/NEWS +++ b/NEWS @@ -132,6 +132,12 @@ New in spot 2.7.5.dev (not yet released) properties. This can be altered with the SPOT_PR_CHECK environment variable. + Bugs fixed: + + - The gf_guarantee_to_ba() is relying on an inplace algorithm that + could produce a different number of edges for the same input in + two different transition order. + New in spot 2.7.5 (2019-06-05) Build: diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index aa26fb88b..85738ab2c 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -185,13 +185,92 @@ namespace spot // } } - unsigned nedges = aut->num_edges(); unsigned new_init = -1U; - // The loop might add new edges, but we just want to iterate - // on the initial ones. - for (unsigned edge = 1; edge <= nedges; ++edge) + // We do two the rewrite in two passes. The first one + // replays histories to detect the new source the edges + // should synchronize with. We used to have single + // loop, but replaying history on edges that have been modified + // result in different automaton depending on the edge order. + std::vector redirect_src; + if (is_det) + { + redirect_src.resize(aut->edge_vector().size()); + for (auto& e: aut->edges()) + { + unsigned edge = aut->edge_number(e); + redirect_src[edge] = e.src; // no change by default + // Don't bother with terminal states, they won't be + // reachable anymore. + if (term[si.scc_of(e.src)]) + continue; + // It will not loop + if (!term[si.scc_of(e.dst)]) + continue; + // It will loop. + + // If initial state cannot be reached from another + // state of the automaton, we can get rid of it by + // combining the edge reaching the terminal state + // with the edges leaving the initial state. + // + // However if we have some histories for e.src + // (which implies that the automaton is + // deterministic), we can try to replay that from + // the initial state first. + // + // One problem with those histories, is that we do + // not know how much of it to replay. It's possible + // that we cannot find a matching transition (e.g. if + // the history if "b" but the choices are "!a" or "a"), + // and its also possible to that playing too much of + // history will get us back the terminal state. In both + // cases, we should try again with a smaller history. + unsigned moved_init = init; + bdd econd = e.cond; + + auto& h = histories[e.src]; + int hsize = h.size(); + for (int hlen = hsize - 1; hlen >= 0; --hlen) + { + for (int pos = hlen - 1; pos >= 0; --pos) + { + for (auto& e: aut->out(moved_init)) + if (bdd_implies(h[pos], e.cond)) + { + if (term[si.scc_of(e.dst)]) + goto failed; + moved_init = e.dst; + goto moved; + } + // if we reach this place, we failed to follow + // one step of the history. + goto failed; + moved: + continue; + } + + // Make sure no successor of the new initial + // state will reach a terminal state; if + // that is the case, we have to shorten the + // history further. + if (hlen > 0) + for (auto& ei: aut->out(moved_init)) + if ((ei.cond & econd) != bddfalse + && term[si.scc_of(ei.dst)]) + goto failed; + + redirect_src[edge] = moved_init; + break; + failed: + moved_init = init; + continue; + } + } + } + + // No we do the redirection. + for (auto& e: aut->edges()) { - auto& e = aut->edge_storage(edge); // Don't bother with terminal states, they won't be // reachable anymore. if (term[si.scc_of(e.src)]) @@ -235,95 +314,55 @@ namespace spot bool first; if (is_det) { - auto& h = histories[e.src]; - int hsize = h.size(); - for (int hlen = hsize - 1; hlen >= 0; --hlen) + unsigned edge = aut->edge_number(e); + moved_init = redirect_src[edge]; + + first = true; + for (auto& ei: aut->out(moved_init)) { - for (int pos = hlen - 1; pos >= 0; --pos) + bdd cond = ei.cond & econd; + if (cond != bddfalse) { - for (auto& e: aut->out(moved_init)) - if (bdd_implies(h[pos], e.cond)) - { - if (term[si.scc_of(e.dst)]) - goto failed; - moved_init = e.dst; - goto moved; - } - // if we reach this place, we failed to follow - // one step of the history. - goto failed; - moved: - continue; - } - - // Make sure no successor of the new initial - // state will reach a terminal state; if - // that is the case, we have to shorten the - // history further. - if (hlen > 0) - for (auto& ei: aut->out(moved_init)) - if ((ei.cond & econd) != bddfalse - && term[si.scc_of(ei.dst)]) - goto failed; - - // we have successfully played all history - // to a non-terminal state. - // - // Combine this edge with any compatible - // edge from the initial state. - first = true; - for (auto& ei: aut->out(moved_init)) - { - bdd cond = ei.cond & econd; - if (cond != bddfalse) + // We should never reach the terminal state, + // unless the history is empty. In that + // case (ts=true) we have to make a loop to + // the initial state without any + // combination. + bool ts = term[si.scc_of(ei.dst)]; + if (ts) { - // We should never reach the terminal state, - // unless the history is empty. In that - // case (ts=true) we have to make a loop to - // the initial state without any - // combination. - bool ts = term[si.scc_of(ei.dst)]; - if (ts) + want_merge_edges = true; + } + if (first) + { + e.acc = {0}; + e.cond = cond; + first = false; + if (!ts) { - assert(hlen == 0); - want_merge_edges = true; - } - if (first) - { - e.acc = {0}; - e.cond = cond; - first = false; - if (!ts) - { - e.dst = ei.dst; - if (new_init == -1U) - new_init = e.src; - } - else - { - new_init = e.dst = init; - } + e.dst = ei.dst; + if (new_init == -1U) + new_init = e.src; } else { - if (ts) - { - aut->new_edge(e.src, init, cond, {0}); - new_init = init; - } - else - { - aut->new_edge(e.src, ei.dst, - cond, {0}); - } + new_init = e.dst = init; + } + } + else + { + if (ts) + { + aut->new_edge(e.src, init, cond, {0}); + new_init = init; + } + else + { + aut->new_edge(e.src, ei.dst, + cond, {0}); } - } } - break; - failed: - moved_init = init; - continue; } } else diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index ac2718107..0b24a89bc 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6034a960> >" + " *' at 0x7fb70857f7e0> >" ] }, "execution_count": 2, @@ -643,7 +643,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a60301210> >" + " *' at 0x7fb708536540> >" ] }, "execution_count": 6, @@ -719,7 +719,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a60301bd0> >" + " *' at 0x7fb708536c90> >" ] }, "execution_count": 7, @@ -802,7 +802,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a60301690> >" + " *' at 0x7fb7085369f0> >" ] }, "execution_count": 8, @@ -1321,7 +1321,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a603010c0> >" + " *' at 0x7fb708536a20> >" ] }, "execution_count": 12, @@ -1435,7 +1435,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a60301090> >" + " *' at 0x7fb7085362a0> >" ] }, "execution_count": 13, @@ -1566,7 +1566,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a60301c90> >" + " *' at 0x7fb70857f8a0> >" ] }, "execution_count": 14, @@ -1785,7 +1785,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6030f4b0> >" + " *' at 0x7fb708544600> >" ] }, "metadata": {}, @@ -1935,7 +1935,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a60392630> >" + " *' at 0x7fb708544390> >" ] }, "metadata": {}, @@ -2107,7 +2107,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6030f930> >" + " *' at 0x7fb708544900> >" ] }, "metadata": {}, @@ -2282,7 +2282,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6030f870> >" + " *' at 0x7fb7085449c0> >" ] }, "metadata": {}, @@ -2468,7 +2468,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6030fbd0> >" + " *' at 0x7fb708544b10> >" ] }, "execution_count": 19, @@ -2544,7 +2544,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6030f150> >" + " *' at 0x7fb708544c00> >" ] }, "execution_count": 20, @@ -2616,7 +2616,7 @@ "0->0\n", "\n", "\n", - "!a\n", + "a\n", "\n", "\n", "\n", @@ -2630,21 +2630,21 @@ "0->1\n", "\n", "\n", - "a\n", + "!a\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "!a\n", + "a\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "a\n", + "!a\n", "\n", "\n", "\n", @@ -2716,316 +2716,257 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,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", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "1,0\n", + "\n", + "1,1\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "1,1\n", - "\n", - "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b\n", + "0->2\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", "\n", - "1->3\n", - "\n", - "\n", - "a & !c\n", + "1->2\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & c\n", - "\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "3->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "\n", "\n", - "0->3\n", - "\n", - "\n", - "a & b\n", + "0->2\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", "\n", - "1->3\n", - "\n", - "\n", - "a & !c\n", + "1->2\n", + "\n", + "\n", + "!a & !c\n", "\n", - "\n", + "\n", "\n", - "1->3\n", - "\n", - "\n", - "a & c\n", - "\n", + "1->2\n", + "\n", + "\n", + "!a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", - "\n", - "2->2\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & b\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", - "\n", + "\n", "\n", - "3->1\n", - "\n", - "\n", - "!a & !c\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & !c\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "2->2\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", "\n", "
" @@ -3121,7 +3062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6034ad20> >" + " *' at 0x7fb708544690> >" ] }, "metadata": {}, @@ -3221,7 +3162,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a60301ba0> >" + " *' at 0x7fb708536d80> >" ] }, "execution_count": 24, @@ -3294,7 +3235,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6030f9c0> >" + " *' at 0x7fb708544e40> >" ] }, "execution_count": 25, @@ -3458,7 +3399,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6030f750> >" + " *' at 0x7fb708536bd0> >" ] }, "execution_count": 27, @@ -3541,7 +3482,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6034ad20> >" + " *' at 0x7fb708544690> >" ] }, "metadata": {}, @@ -3606,7 +3547,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6034ad20> >" + " *' at 0x7fb708544690> >" ] }, "metadata": {}, @@ -3693,7 +3634,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f5a6034ad20> >" + " *' at 0x7fb708544690> >" ] }, "execution_count": 29, diff --git a/tests/python/twagraph-internals.ipynb b/tests/python/twagraph-internals.ipynb index dbd366d7c..dcd5d3588 100644 --- a/tests/python/twagraph-internals.ipynb +++ b/tests/python/twagraph-internals.ipynb @@ -56,16 +56,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -84,7 +84,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -92,7 +92,7 @@ "0->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -106,14 +106,14 @@ "0->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -121,14 +121,14 @@ "1->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -136,7 +136,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -144,14 +144,14 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "execution_count": 3, @@ -217,142 +217,142 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -454,16 +454,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -495,7 +495,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -503,7 +503,7 @@ "0->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -517,14 +517,14 @@ "0->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -532,14 +532,14 @@ "1->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -547,7 +547,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -555,14 +555,14 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "metadata": {}, @@ -619,154 +619,154 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", "\n", "\n", "9\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -840,16 +840,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -881,7 +881,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -889,7 +889,7 @@ "0->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -897,7 +897,7 @@ "0->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -911,7 +911,7 @@ "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -919,14 +919,14 @@ "1->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -934,7 +934,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -942,14 +942,14 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "metadata": {}, @@ -1006,154 +1006,154 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", "\n", "\n", "9\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -1200,16 +1200,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -1241,7 +1241,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1263,7 +1263,7 @@ "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1271,14 +1271,14 @@ "1->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1286,7 +1286,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1294,14 +1294,14 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "metadata": {}, @@ -1358,138 +1358,138 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "b\n", - "\n", - "a & !b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", + "\n", + "a & !b\n", + "\n", + "b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -1542,16 +1542,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -1583,7 +1583,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1605,7 +1605,7 @@ "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1613,14 +1613,14 @@ "1->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1628,7 +1628,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1636,7 +1636,7 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -1652,7 +1652,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "metadata": {}, @@ -1709,27 +1709,27 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", @@ -1738,67 +1738,67 @@ "9\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "b\n", - "\n", - "a & !b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", + "\n", + "a & !b\n", + "\n", + "b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "{0,1}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", @@ -1807,53 +1807,53 @@ "1\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "9\n", "\n", "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -2072,27 +2072,27 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", @@ -2101,67 +2101,67 @@ "9\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "b\n", - "\n", - "a & !b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", + "\n", + "a & !b\n", + "\n", + "b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "{0,1}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", @@ -2170,53 +2170,53 @@ "1\n", "\n", "next_succ\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "9\n", "\n", "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -2391,24 +2391,24 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", "\n", "\n", "7\n", @@ -2417,60 +2417,60 @@ "8\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{0,1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "1\n", @@ -2479,47 +2479,47 @@ "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "1\n", @@ -2559,10 +2559,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -2604,144 +2604,144 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "0\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "cond\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "0\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "" @@ -2813,10 +2813,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -2858,128 +2858,128 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "cond\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "" @@ -3023,16 +3023,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -3064,7 +3064,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3078,7 +3078,7 @@ "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3099,7 +3099,7 @@ "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3107,7 +3107,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3115,7 +3115,7 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -3174,7 +3174,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "execution_count": 22, @@ -3198,10 +3198,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -3255,191 +3255,191 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "~3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -3458,26 +3458,26 @@ "\n", "\n", "props\n", - "prop_state_acc:\n", - "maybe\n", - "prop_inherently_weak:\n", - "maybe\n", - "prop_terminal:\n", - "maybe\n", - "prop_weak:\n", - "maybe\n", - "prop_very_weak:\n", - "maybe\n", - "prop_complete:\n", - "maybe\n", - "prop_universal:\n", - "maybe\n", - "prop_unambiguous:\n", - "maybe\n", - "prop_semi_deterministic:\n", - "maybe\n", - "prop_stutter_invariant:\n", - "maybe\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", "\n", "\n", "\n", @@ -3627,16 +3627,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -3690,7 +3690,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3698,7 +3698,7 @@ "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3719,7 +3719,7 @@ "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3727,7 +3727,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3735,7 +3735,7 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -3801,7 +3801,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "execution_count": 28, @@ -3838,10 +3838,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -3895,208 +3895,208 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", "\n", "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "~3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "\n", - "~6\n", - "\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "#3\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", @@ -4115,26 +4115,26 @@ "\n", "\n", "props\n", - "prop_state_acc:\n", - "maybe\n", - "prop_inherently_weak:\n", - "maybe\n", - "prop_terminal:\n", - "maybe\n", - "prop_weak:\n", - "maybe\n", - "prop_very_weak:\n", - "maybe\n", - "prop_complete:\n", - "maybe\n", - "prop_universal:\n", - "maybe\n", - "prop_unambiguous:\n", - "maybe\n", - "prop_semi_deterministic:\n", - "maybe\n", - "prop_stutter_invariant:\n", - "maybe\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", "\n", "\n", "\n", @@ -4174,16 +4174,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -4237,7 +4237,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4245,7 +4245,7 @@ "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4266,7 +4266,7 @@ "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4274,7 +4274,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4282,7 +4282,7 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -4373,7 +4373,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "metadata": {}, @@ -4382,10 +4382,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -4436,240 +4436,240 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", - "\n", - "\n", - "10\n", - "\n", - "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "~10\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "10\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "cond\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "~10\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "10\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "\n", - "~6\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "~10\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "#3\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "~10\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", @@ -4704,16 +4704,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -4767,7 +4767,7 @@ "0->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4775,7 +4775,7 @@ "0->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4796,7 +4796,7 @@ "1->0\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4804,7 +4804,7 @@ "1->1\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4812,7 +4812,7 @@ "1->1\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -4886,7 +4886,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7e3c439b10> >" + " *' at 0x7f349c744a80> >" ] }, "metadata": {}, @@ -4895,10 +4895,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -4949,227 +4949,227 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", - "\n", - "\n", - "10\n", - "\n", - "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "!a\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "~0\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "10\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "cond\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "!a\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "~0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "10\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "\n", - "~6\n", - "\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "#3\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", @@ -5302,7 +5302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7e3c3cf030> >" + " *' at 0x7f349c661510> >" ] }, "metadata": {}, @@ -5593,7 +5593,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7e3c3cf030> >" + " *' at 0x7f349c661510> >" ] }, "metadata": {},