diff --git a/NEWS b/NEWS index 7df22e3e5..39fa6fcdb 100644 --- a/NEWS +++ b/NEWS @@ -114,6 +114,9 @@ New in spot 2.7.5.dev (not yet released) a better replacement for cleanup_parity() and colorize_parity(). See https://spot.lrde.epita.fr/ipynb/parity.html for examples. + - The postprocessor and translator classes are now using + reduce_parity() for further simplifications. + New in spot 2.7.5 (2019-06-05) Build: diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 76749fdba..7ea8cb307 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -198,8 +198,7 @@ namespace spot tmp = sbacc(tmp); if (want_parity) { - if (COLORED_) - colorize_parity_here(tmp); + reduce_parity_here(tmp, COLORED_); parity_kind kind = parity_kind_any; parity_style style = parity_style_any; if ((type_ & ParityMin) == ParityMin) @@ -241,16 +240,18 @@ namespace spot { if (PREF_ == Any && level_ == Low) return in; - if (!(want_parity && in->acc().is_parity())) + bool isparity = in->acc().is_parity(); + if (isparity && in->is_existential() + && (type_ == Generic || want_parity)) + return reduce_parity(in); + if (!(want_parity && isparity)) { if (level_ == High) return simplify_acceptance(in); else return cleanup_acceptance(in); } - if (level_ == High) - return cleanup_parity(in); - return in; + return cleanup_parity(in); }; a = simplify_acc(a); diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 41f6dd34d..325c87c36 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -28,6 +28,7 @@ #include #include #include +#include namespace spot { @@ -230,7 +231,9 @@ namespace spot om = *opt_; om.set("ltl-split", 0); translator translate_without_split(simpl_, &om); - translate_without_split.set_pref(pref_); + // Never force colored automata at intermediate steps. + // This is best added at the very end. + translate_without_split.set_pref(pref_ & ~Colored); translate_without_split.set_level(level_); translate_without_split.set_type(type_); auto transrun = [&](formula f) @@ -302,6 +305,11 @@ namespace spot aut = product_susp(aut, susp_aut); else aut = product_or_susp(aut, susp_aut); + //if (aut && susp_aut) + // { + // print_hoa(std::cerr << "AUT\n", aut) << '\n'; + // print_hoa(std::cerr << "SUSPAUT\n", susp_aut) << '\n'; + // } } if (leading_x > 0) { diff --git a/tests/core/genltl.test b/tests/core/genltl.test index b73a40236..c0078a3be 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement +# Copyright (C) 2016-2019 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -185,28 +185,28 @@ cat >exp<expected4<expected <\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -84,17 +84,16 @@ "0->0\n", "\n", "\n", - "a & b\n", - "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", - "a & !b\n", - "\n", - "\n", + "a & b\n", + "\n", "\n", "\n", "\n", @@ -137,23 +136,22 @@ "1->1\n", "\n", "\n", - "!a & b\n", - "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "!a & !b\n", - "\n", - "\n", + "!a & b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "execution_count": 3, @@ -219,12 +217,12 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "3\n", @@ -237,18 +235,18 @@ "\n", "\n", "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\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", @@ -257,16 +255,16 @@ "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", - "{1}\n", - "\n", - "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", @@ -275,18 +273,18 @@ "{}\n", "\n", "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "1\n", @@ -299,20 +297,20 @@ "\n", "\n", "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", "\n", "\n", "4\n", @@ -324,19 +322,19 @@ "\n", "\n", "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\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", "0\n", @@ -349,12 +347,12 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -456,16 +454,16 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -497,17 +495,16 @@ "0->0\n", "\n", "\n", - "a & b\n", - "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", - "a & !b\n", - "\n", - "\n", + "a & b\n", + "\n", "\n", "\n", "\n", @@ -550,23 +547,22 @@ "1->1\n", "\n", "\n", - "!a & b\n", - "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "!a & !b\n", - "\n", - "\n", + "!a & b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "metadata": {}, @@ -623,12 +619,12 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "3\n", @@ -641,21 +637,21 @@ "\n", "\n", "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\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", @@ -664,18 +660,18 @@ "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", - "{1}\n", - "\n", - "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", @@ -684,20 +680,20 @@ "{}\n", "\n", "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\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", + "0\n", "\n", "\n", "1\n", @@ -710,23 +706,23 @@ "\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", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", "\n", "\n", "4\n", @@ -738,21 +734,21 @@ "\n", "\n", "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\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", "0\n", @@ -765,12 +761,12 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -844,16 +840,16 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -885,25 +881,24 @@ "0->0\n", "\n", "\n", - "a & b\n", - "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", - "a & !b\n", - "\n", - "\n", + "a & b\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a & b\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", @@ -939,23 +934,22 @@ "1->1\n", "\n", "\n", - "!a & b\n", - "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "!a & !b\n", - "\n", - "\n", + "!a & b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "metadata": {}, @@ -1012,12 +1006,12 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "3\n", @@ -1030,21 +1024,21 @@ "\n", "\n", "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\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", @@ -1053,18 +1047,18 @@ "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", - "{1}\n", - "\n", - "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{1}\n", "\n", @@ -1073,20 +1067,20 @@ "{}\n", "\n", "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\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", + "0\n", "\n", "\n", "0\n", @@ -1099,23 +1093,23 @@ "\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", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", "\n", "\n", "4\n", @@ -1127,21 +1121,21 @@ "\n", "\n", "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\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", "0\n", @@ -1154,12 +1148,12 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -1206,16 +1200,16 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -1247,17 +1241,16 @@ "0->0\n", "\n", "\n", - "b\n", - "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", - "a & !b\n", - "\n", - "\n", + "b\n", + "\n", "\n", "\n", "\n", @@ -1293,23 +1286,22 @@ "1->1\n", "\n", "\n", - "!a & b\n", - "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "!a & !b\n", - "\n", - "\n", + "!a & b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "metadata": {}, @@ -1366,12 +1358,12 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "3\n", @@ -1381,59 +1373,59 @@ "\n", "\n", "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", "\n", "cond\n", - "\n", - "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", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{0}\n", "\n", "{}\n", "\n", "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\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", + "0\n", "\n", "\n", "1\n", @@ -1443,23 +1435,23 @@ "\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", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", "\n", "0\n", "\n", @@ -1468,21 +1460,21 @@ "\n", "\n", "6\n", - "\n", - "\n", - "7\n", - "\n", - "0\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", + "0\n", "\n", "\n", "0\n", @@ -1492,12 +1484,12 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -1550,16 +1542,16 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -1591,17 +1583,16 @@ "0->0\n", "\n", "\n", - "b\n", - "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", - "a & !b\n", - "\n", - "\n", + "b\n", + "\n", "\n", "\n", "\n", @@ -1637,32 +1628,31 @@ "1->1\n", "\n", "\n", - "!a & b\n", - "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "!a & !b\n", - "\n", - "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "metadata": {}, @@ -1719,12 +1709,12 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "3\n", @@ -1734,12 +1724,12 @@ "\n", "\n", "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", @@ -1748,52 +1738,52 @@ "9\n", "\n", "cond\n", - "\n", - "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", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{0}\n", "\n", "{}\n", "\n", "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\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", + "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "1\n", @@ -1803,12 +1793,12 @@ "\n", "\n", "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", @@ -1817,12 +1807,12 @@ "1\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", "\n", "0\n", "\n", @@ -1831,24 +1821,24 @@ "\n", "\n", "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "9\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", + "0\n", "\n", "\n", "0\n", @@ -1858,12 +1848,12 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -2008,8 +1998,8 @@ "name": "stdout", "output_type": "stream", "text": [ - "pos=1, acc={1}, toerase=True\n", - "pos=2, acc={0,1}, toerase=True\n", + "pos=1, acc={0}, toerase=False\n", + "pos=2, acc={1}, toerase=True\n", "pos=3, acc={0}, toerase=False\n" ] } @@ -2057,7 +2047,7 @@ "succ\n", "\n", "\n", - "3\n", + "1\n", "\n", "\n", "4\n", @@ -2082,12 +2072,12 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "3\n", @@ -2097,12 +2087,12 @@ "\n", "\n", "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", @@ -2111,52 +2101,52 @@ "9\n", "\n", "cond\n", - "\n", - "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", + "!a & !b\n", + "\n", + "!a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{0}\n", "\n", "{}\n", "\n", "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\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", + "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "1\n", @@ -2166,12 +2156,12 @@ "\n", "\n", "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", @@ -2180,12 +2170,12 @@ "1\n", "\n", "next_succ\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", "\n", "0\n", "\n", @@ -2194,24 +2184,24 @@ "\n", "\n", "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "9\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", + "0\n", "\n", "\n", "0\n", @@ -2221,12 +2211,12 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -2295,6 +2285,7 @@ "name": "stdout", "output_type": "stream", "text": [ + "edges[1].src=0, edges[1].dst=0\n", "edges[3].src=0, edges[3].dst=1\n", "edges[4].src=1, edges[4].dst=0\n", "edges[5].src=1, edges[5].dst=0\n", @@ -2325,7 +2316,7 @@ { "data": { "text/plain": [ - "7" + "8" ] }, "execution_count": 16, @@ -2352,10 +2343,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -2378,21 +2369,21 @@ "1\n", "\n", "\n", - "2\n", + "3\n", "\n", "\n", - "6\n", + "8\n", "\n", "succ_tail\n", "\n", "\n", - "1\n", + "2\n", "\n", "\n", - "5\n", + "7\n", "\n", "\n", - "6\n", + "8\n", "\n", "\n", "\n", @@ -2400,109 +2391,141 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\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", + "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", - "1\n", - "\n", - "1\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", - "{}\n", - "\n", - "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{}\n", "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", "\n", "dst\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", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", "\n", "next_succ\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", "\n", "\n", "5\n", - "\n", - "0\n", - "\n", - "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "src\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", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "" @@ -2536,10 +2559,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -2562,131 +2585,163 @@ "1\n", "\n", "\n", - "2\n", + "3\n", "\n", "\n", - "6\n", + "8\n", "\n", "succ_tail\n", "\n", "\n", - "1\n", + "2\n", "\n", "\n", - "5\n", + "7\n", "\n", "\n", - "6\n", + "8\n", "\n", "\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", - "cond\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "0\n", - "\n", - "!a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "dst\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", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\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", + "\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", "" @@ -2714,12 +2769,14 @@ "name": "stdout", "output_type": "stream", "text": [ - "edges[1].src=0, edges[1].dst=1\n", - "edges[2].src=1, edges[2].dst=0\n", + "edges[1].src=0, edges[1].dst=0\n", + "edges[2].src=0, edges[2].dst=1\n", "edges[3].src=1, edges[3].dst=0\n", - "edges[4].src=1, edges[4].dst=1\n", + "edges[4].src=1, edges[4].dst=0\n", "edges[5].src=1, edges[5].dst=1\n", - "edges[6].src=2, edges[6].dst=0\n" + "edges[6].src=1, edges[6].dst=1\n", + "edges[7].src=1, edges[7].dst=1\n", + "edges[8].src=2, edges[8].dst=0\n" ] } ], @@ -2756,10 +2813,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -2782,115 +2839,147 @@ "1\n", "\n", "\n", - "2\n", + "3\n", "\n", "\n", - "5\n", + "7\n", "\n", "succ_tail\n", "\n", "\n", - "1\n", + "2\n", "\n", "\n", - "4\n", + "6\n", "\n", "\n", - "5\n", + "7\n", "\n", "\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", - "cond\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", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "dst\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "next_succ\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\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", "" @@ -2934,16 +3023,16 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -2964,12 +3053,20 @@ "0\n", "\n", "\n", - "\n", + "\n", "2->0\n", "\n", "\n", "1\n", "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", "\n", "\n", "1\n", @@ -2977,12 +3074,12 @@ "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", @@ -2990,7 +3087,7 @@ "\n", "\n", "\n", - "\n", + "\n", "0->-1\n", "\n", "\n", @@ -2998,31 +3095,40 @@ "\n", "\n", "\n", - "\n", + "\n", "1->0\n", "\n", "\n", - "a & b\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "-1->0\n", "\n", "\n", @@ -3034,7 +3140,7 @@ "3\n", "\n", "\n", - "\n", + "\n", "-1->3\n", "\n", "\n", @@ -3045,7 +3151,7 @@ "\n", "\n", "\n", - "\n", + "\n", "3->-4\n", "\n", "\n", @@ -3053,13 +3159,13 @@ "\n", "\n", "\n", - "\n", + "\n", "-4->0\n", "\n", "\n", "\n", "\n", - "\n", + "\n", "-4->1\n", "\n", "\n", @@ -3068,7 +3174,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "execution_count": 22, @@ -3092,10 +3198,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -3121,187 +3227,219 @@ "1\n", "\n", "\n", - "2\n", + "3\n", "\n", "\n", - "5\n", + "7\n", "\n", "\n", - "7\n", + "9\n", "\n", "succ_tail\n", "\n", "\n", - "6\n", + "8\n", "\n", "\n", - "4\n", + "6\n", "\n", "\n", - "5\n", + "7\n", "\n", "\n", - "7\n", + "9\n", "\n", "\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", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "dst\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\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", - "6\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\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", + "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", + "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", + "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", + "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", + "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", + "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", "\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", @@ -3320,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", @@ -3376,10 +3514,12 @@ "name": "stdout", "output_type": "stream", "text": [ + "0\n", "1\n", "0\n", "1\n", "1\n", + "1\n", "0\n", "4294967295\n", "4294967292\n" @@ -3407,10 +3547,12 @@ "name": "stdout", "output_type": "stream", "text": [ + "[0]\n", "[1]\n", "[0]\n", "[1]\n", "[1]\n", + "[1]\n", "[0]\n", "[0, 3]\n", "[0, 1]\n" @@ -3438,10 +3580,12 @@ "name": "stdout", "output_type": "stream", "text": [ + "[0]\n", "[1]\n", "[0]\n", "[1]\n", "[1]\n", + "[1]\n", "[0]\n", "[0, 3]\n", "[0, 1]\n" @@ -3483,164 +3627,181 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", "-7\n", - "\n", + "\n", "\n", "\n", "\n", "I->-7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "-7->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "-7->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "-7->2\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "-1\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "0->-1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "-1->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "-4\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->-4\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "\n", + "\n", "-4->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "-4->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "execution_count": 28, @@ -3677,10 +3838,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -3706,204 +3867,236 @@ "1\n", "\n", "\n", - "2\n", + "3\n", "\n", "\n", - "5\n", + "7\n", "\n", "\n", - "7\n", + "9\n", "\n", "succ_tail\n", "\n", "\n", - "6\n", + "8\n", "\n", "\n", - "4\n", + "6\n", "\n", "\n", - "5\n", + "7\n", "\n", "\n", - "7\n", + "9\n", "\n", "\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", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "dst\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\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", - "6\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\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", + "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", + "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", + "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", + "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", + "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", + "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", "\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", @@ -3922,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", @@ -3981,189 +4174,206 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", "-7\n", - "\n", + "\n", "\n", "\n", "\n", "I->-7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "-7->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "-7->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "-7->2\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "-1\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "0->-1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "-1->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "-4\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->-4\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "-11\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->-11\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", - "\n", + "\n", "-4->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "-4->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "-11->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "-11->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "metadata": {}, @@ -4172,262 +4382,294 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", - "\n", - "\n", - "states\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "succ\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "7\n", - "\n", - "succ_tail\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "9\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "10\n", "\n", "\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", - "!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", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "dst\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\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", - "6\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "8\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\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", @@ -4462,172 +4704,189 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", "-7\n", - "\n", + "\n", "\n", "\n", "\n", "I->-7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "-7->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "-7->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "-7->2\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!a & !b\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", "\n", "\n", "\n", "-1\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "0->-1\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", - "\n", - "1->0\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", "\n", - "1->1\n", - "\n", - "\n", - "!a & b\n", - "\n", + "1->0\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "-1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "-1->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->-1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "-4\n", - "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->-4\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", - "\n", + "\n", "-4->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "-4->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f616c1788a0> >" + " *' at 0x7f2950267b40> >" ] }, "metadata": {}, @@ -4636,249 +4895,281 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", - "\n", - "\n", - "states\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "succ\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "succ_tail\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "states\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "succ\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "succ_tail\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "10\n", "\n", "\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\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", - "{1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "dst\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", - "~3\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", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "8\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", - "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", @@ -5011,7 +5302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f616c0b3bd0> >" + " *' at 0x7f2950267270> >" ] }, "metadata": {}, @@ -5302,7 +5593,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f616c0b3bd0> >" + " *' at 0x7f2950267270> >" ] }, "metadata": {}, @@ -5511,7 +5802,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.6" + "version": "3.6.4" } }, "nbformat": 4,