diff --git a/NEWS b/NEWS index d2547dd2e..e187230d7 100644 --- a/NEWS +++ b/NEWS @@ -173,6 +173,9 @@ New in spot 2.9.6.dev (not yet released) cut the size of the powerset automaton by 2^|sinks| in favorable cases. + - twa_graph::merge_edges() had its two passes swapped. Doing so + improves the determinism of some automata. + Python: - Bindings for functions related to games. diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 38e302c96..f0299698a 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -140,117 +140,153 @@ namespace spot if (!is_existential()) merge_univ_dests(); - typedef graph_t::edge_storage_t tr_t; - g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) - { - if (lhs.src < rhs.src) - return true; - if (lhs.src > rhs.src) - return false; - if (lhs.dst < rhs.dst) - return true; - if (lhs.dst > rhs.dst) - return false; - return lhs.acc < rhs.acc; - // Do not sort on conditions, we'll merge - // them. - }); - auto& trans = this->edge_vector(); unsigned orig_size = trans.size(); unsigned tend = orig_size; - unsigned out = 0; - unsigned in = 1; - // Skip any leading false edge. - while (in < tend && trans[in].cond == bddfalse) - ++in; - if (in < tend) + + // When two transitions have the same (src,colors,dst), + // we can marge their conds. + auto merge_conds_and_remove_false = [&]() + { + typedef graph_t::edge_storage_t tr_t; + g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) { - ++out; - if (out != in) - trans[out] = trans[in]; - for (++in; in < tend; ++in) - { - if (trans[in].cond == bddfalse) // Unusable edge - continue; - // Merge edges with the same source, destination, and - // acceptance. (We test the source last, because this is the - // most likely test to be true as edges are ordered by - // sources and then destinations.) - if (trans[out].dst == trans[in].dst - && trans[out].acc == trans[in].acc - && trans[out].src == trans[in].src) - { - trans[out].cond |= trans[in].cond; - } - else - { - ++out; - if (in != out) - trans[out] = trans[in]; - } - } - } - if (++out != tend) - trans.resize(out); + if (lhs.src < rhs.src) + return true; + if (lhs.src > rhs.src) + return false; + if (lhs.dst < rhs.dst) + return true; + if (lhs.dst > rhs.dst) + return false; + return lhs.acc < rhs.acc; + // Do not sort on conditions, we'll merge + // them. + }); - tend = out; - out = 1; - in = 2; + unsigned out = 0; + unsigned in = 1; + // Skip any leading false edge. + while (in < tend && trans[in].cond == bddfalse) + ++in; + if (in < tend) + { + ++out; + if (out != in) + trans[out] = trans[in]; + for (++in; in < tend; ++in) + { + if (trans[in].cond == bddfalse) // Unusable edge + continue; + // Merge edges with the same source, destination, and + // colors. (We test the source last, because this is the + // most likely test to be true as edges are ordered by + // sources and then destinations.) + if (trans[out].dst == trans[in].dst + && trans[out].acc == trans[in].acc + && trans[out].src == trans[in].src) + { + trans[out].cond |= trans[in].cond; + } + else + { + ++out; + if (in != out) + trans[out] = trans[in]; + } + } + } + if (++out != tend) + { + tend = out; + trans.resize(tend); + } + }; + + // When two transitions have the same (src,cond,dst), we can marge + // their colors. This only works for Fin-less acceptance. + // // FIXME: We could should also merge edges when using // fin_acceptance, but the rule for Fin sets are different than // those for Inf sets, (and we need to be careful if a set is used // both as Inf and Fin) - if ((in < tend) && !acc().uses_fin_acceptance()) + auto merge_colors = [&]() + { + if (tend < 2 || acc().uses_fin_acceptance()) + return; + typedef graph_t::edge_storage_t tr_t; + g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) { - typedef graph_t::edge_storage_t tr_t; - g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) - { - if (lhs.src < rhs.src) - return true; - if (lhs.src > rhs.src) - return false; - if (lhs.dst < rhs.dst) - return true; - if (lhs.dst > rhs.dst) - return false; - bdd_less_than_stable lt; - return lt(lhs.cond, rhs.cond); - // Do not sort on acceptance, we'll merge - // them. - }); + if (lhs.src < rhs.src) + return true; + if (lhs.src > rhs.src) + return false; + if (lhs.dst < rhs.dst) + return true; + if (lhs.dst > rhs.dst) + return false; + bdd_less_than_stable lt; + return lt(lhs.cond, rhs.cond); + // Do not sort on acceptance, we'll merge them. + }); - for (; in < tend; ++in) - { - // Merge edges with the same source, destination, - // and conditions. (We test the source last, for the - // same reason as above.) - if (trans[out].dst == trans[in].dst - && trans[out].cond.id() == trans[in].cond.id() - && trans[out].src == trans[in].src) - { - trans[out].acc |= trans[in].acc; - } - else - { - ++out; - if (in != out) - trans[out] = trans[in]; - } - } - if (++out != tend) - trans.resize(out); - } + // Start on the second position and try to merge it into the + // first one + unsigned out = 1; + unsigned in = 2; + for (; in < tend; ++in) + { + // Merge edges with the same source, destination, + // and conditions. (We test the source last, for the + // same reason as above.) + if (trans[out].dst == trans[in].dst + && trans[out].cond.id() == trans[in].cond.id() + && trans[out].src == trans[in].src) + { + trans[out].acc |= trans[in].acc; + } + else + { + ++out; + if (in != out) + trans[out] = trans[in]; + } + } + if (++out != tend) + { + tend = out; + trans.resize(tend); + } + }; + + // These next two lines used to be done in the opposite order in + // 2.9.x and before. + // + // However merging colors first is more likely to + // make parallel non-deterministic transition disappear. + // + // Consider: + // (1)--a-{1}--->(2) + // (1)--a-{2}--->(2) + // (1)--!a-{1}-->(2) + // If colors are merged first, the first two transitions become one, + // and the result is more deterministic: + // (1)--a-{1,2}->(2) + // (1)--!a-{1}-->(2) + // If conditions were merged first, we would get the following + // non-deterministic transitions instead: + // (1)--1-{1}--->(2) + // (1)--a-{2}--->(2) + merge_colors(); + merge_conds_and_remove_false(); + + // Merging some edges may turn a non-deterministic automaton + // into a deterministic one. + if (prop_universal().is_false() && tend != orig_size) + prop_universal(trival::maybe()); g_.chain_edges_(); - - // Did we actually reduce the number of edges? - if (trans.size() != orig_size) - // Merging some edges may turn a non-deterministic automaton - // into a deterministic one. - if (prop_universal().is_false()) - prop_universal(trival::maybe()); } void twa_graph::merge_states() diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index d2dc9d739..72cf886e8 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -552,15 +552,15 @@ namespace spot /// This makes two passes over the automaton to reduce the number /// of edges with an identical pair of source and destination. /// - /// In the first pass, edges that share their source, destination, - /// and acceptance marks are merged into a single edge whose condition - /// is the conjunction of the conditions of the original edges. - /// - /// In the second pass, which is performed only on automata with + /// In the first pass, which is performed only on automata with /// Fin-less acceptance, edges with the same source, destination, /// and conditions are merged into a single edge whose set of /// acceptance marks is the intersection of the sets of the edges. /// + /// In the second pass, edges that share their source, destination, + /// and acceptance marks are merged into a single edge whose condition + /// is the conjunction of the conditions of the original edges. + /// /// If the automaton uses some universal edges, the method /// merge_univ_dests() is also called. void merge_edges(); diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 8970848bb..ec6b8a511 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016-2018, 2020 Laboratoire de Recherche et +# Copyright (C) 2016-2018, 2020-2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -196,11 +196,12 @@ AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete +properties: deterministic --BODY-- State: 0 [t] 1 State: 1 -[t] 1 +[!0] 1 [0] 1 {0} --END-- EOF diff --git a/tests/core/parity2.test b/tests/core/parity2.test index 471793355..aeb86463f 100755 --- a/tests/core/parity2.test +++ b/tests/core/parity2.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2018-2019, 2021 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -56,8 +56,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {0} [!1] 0 +[0&1] 0 {0} [!0&1] 1 State: 1 [0] 0 {0} @@ -115,8 +115,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 +[0&1] 0 {1} [!0&1] 1 State: 1 [0] 0 {1} @@ -174,8 +174,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {0} [!1] 0 +[0&1] 0 {0} [!0&1] 1 State: 1 [0] 0 {0} @@ -233,8 +233,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 {0} +[0&1] 0 {1} [!0&1] 1 {0} State: 1 [0] 0 {1} @@ -292,8 +292,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 {2} +[0&1] 0 {1} [!0&1] 1 {2} State: 1 [0] 0 {1} @@ -351,8 +351,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {2} [!1] 0 {1} +[0&1] 0 {2} [!0&1] 1 {1} State: 1 [0] 0 {2} @@ -417,8 +417,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {0} [!1] 0 +[0&1] 0 {0} [!0&1] 1 State: 1 [0] 0 {0} @@ -478,8 +478,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 +[0&1] 0 {1} [!0&1] 1 State: 1 [0] 0 {1} @@ -539,8 +539,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {0} [!1] 0 +[0&1] 0 {0} [!0&1] 1 State: 1 [0] 0 {0} @@ -600,8 +600,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 {0} +[0&1] 0 {1} [!0&1] 1 {0} State: 1 [0] 0 {1} @@ -661,8 +661,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 {2} +[0&1] 0 {1} [!0&1] 1 {2} State: 1 [0] 0 {1} @@ -722,8 +722,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {2} [!1] 0 {1} +[0&1] 0 {2} [!0&1] 1 {1} State: 1 [0] 0 {2} @@ -1158,8 +1158,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {0} [!1] 0 +[0&1] 0 {0} [!0&1] 1 State: 1 [0] 0 {0} @@ -1219,8 +1219,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 +[0&1] 0 {1} [!0&1] 1 State: 1 [0] 0 {1} @@ -1280,8 +1280,8 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {0} [!1] 0 +[0&1] 0 {0} [!0&1] 1 State: 1 [0] 0 {0} @@ -1341,8 +1341,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 {0} +[0&1] 0 {1} [!0&1] 1 {0} State: 1 [0] 0 {1} @@ -1403,8 +1403,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {1} [!1] 0 {2} +[0&1] 0 {1} [!0&1] 1 {2} State: 1 [0] 0 {1} @@ -1465,8 +1465,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic stutter-invariant --BODY-- State: 0 -[0&1] 0 {2} [!1] 0 {1} +[0&1] 0 {2} [!0&1] 1 {1} State: 1 [0] 0 {2} diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 2f9b424f9..977210991 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2014-2020 Laboratoire de +# Copyright (C) 2009, 2010, 2012, 2014-2021 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -364,8 +364,8 @@ digraph "G(Fa & Fb)" { I -> 0 0 [label="0"] 0 -> 0 [label="!a & !b"] - 0 -> 0 [label="!a & b\n{1}"] 0 -> 0 [label="a & !b\n{0}"] + 0 -> 0 [label="!a & b\n{1}"] 0 -> 0 [label="a & b\n{0,1}"] } EOF @@ -383,8 +383,8 @@ digraph "G(Fa & Fb)" { I -> 0 0 [label="0"] 0 -> 0 [label="!a & !b"] - 0 -> 0 [label="!a & b\n❶"] 0 -> 0 [label="a & !b\n⓿"] + 0 -> 0 [label="!a & b\n❶"] 0 -> 0 [label="a & b\n⓿❶"] } EOF @@ -402,8 +402,8 @@ digraph "G(Fa & Fb)" { I -> 0 0 [label="0"] 0 -> 0 [label=""] - 0 -> 0 [label="❶"] 0 -> 0 [label="⓿"] + 0 -> 0 [label="❶"] 0 -> 0 [label="⓿❶"] } EOF @@ -428,8 +428,8 @@ digraph "G(Fa & Fb)" { I -> 0 0 [label=<0>] 0 -> 0 [label=] - 0 -> 0 [label=$one>] 0 -> 0 [label=$zero>] + 0 -> 0 [label=$one>] 0 -> 0 [label=$zero$one>] } EOF diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 1d57a74a0..d694fa831 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2017, 2020 Laboratoire de Recherche et +# Copyright (C) 2015-2017, 2020-2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -37,23 +37,23 @@ properties: deterministic stutter-invariant State: 0 {0 1} [0&1] 0 [!0&!1] 1 -[!0&1] 2 -[0&!1] 3 +[0&!1] 2 +[!0&1] 3 State: 1 [0&1] 0 [!0&!1] 1 -[!0&1] 2 -[0&!1] 3 -State: 2 {1} +[0&!1] 2 +[!0&1] 3 +State: 2 {0} [0&1] 0 [!0&!1] 1 -[!0&1] 2 -[0&!1] 3 -State: 3 {0} +[0&!1] 2 +[!0&1] 3 +State: 3 {1} [0&1] 0 [!0&!1] 1 -[!0&1] 2 -[0&!1] 3 +[0&!1] 2 +[!0&1] 3 --END-- EOF diff --git a/tests/python/_product_susp.ipynb b/tests/python/_product_susp.ipynb index a8bd194d0..a0de91f95 100644 --- a/tests/python/_product_susp.ipynb +++ b/tests/python/_product_susp.ipynb @@ -36,130 +36,130 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", @@ -167,123 +167,123 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a & c\n", - "⓿\n", + "\n", + "\n", + "a & c\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & c\n", - "⓿\n", + "\n", + "\n", + "a & c\n", + "⓿\n", "\n", "\n", "\n", @@ -302,130 +302,130 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", @@ -433,164 +433,164 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "c\n", - "⓿\n", + "\n", + "\n", + "c\n", + "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!a & !b & !c\n", - "⓿\n", + "\n", + "\n", + "!a & !b & !c\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "c\n", - "⓿\n", + "\n", + "\n", + "c\n", + "⓿\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "!a & !c\n", - "⓿\n", + "\n", + "\n", + "!a & !c\n", + "⓿\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "a & !c\n", - "⓿\n", + "\n", + "\n", + "a & !c\n", + "⓿\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", @@ -621,245 +621,245 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "6\n", - "\n", - "\n", - "6\n", + "\n", + "\n", + "6\n", "\n", "\n", "\n", "I->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "5\n", + "\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", @@ -867,247 +867,247 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & b & c\n", - "⓿\n", + "\n", + "\n", + "a & b & c\n", + "⓿\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "a & !b & !c\n", - "⓿\n", + "\n", + "\n", + "a & !b & !c\n", + "⓿\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "a & !b & c\n", - "⓿\n", + "\n", + "\n", + "a & !b & c\n", + "⓿\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a & b & !c\n", - "⓿\n", + "\n", + "\n", + "a & b & !c\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & c\n", - "⓿\n", + "\n", + "\n", + "a & c\n", + "⓿\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !b & c\n", - "⓿\n", + "\n", + "\n", + "a & !b & c\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b & c\n", - "⓿\n", + "\n", + "\n", + "a & b & c\n", + "⓿\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "a & b & !c\n", - "⓿\n", + "\n", + "\n", + "a & b & !c\n", + "⓿\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "a & !c\n", - "⓿\n", + "\n", + "\n", + "a & !c\n", + "⓿\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & c\n", - "⓿\n", + "\n", + "\n", + "a & c\n", + "⓿\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", @@ -1126,245 +1126,245 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "6\n", - "\n", - "\n", - "6\n", + "\n", + "\n", + "6\n", "\n", "\n", "\n", "I->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "\n", "\n", "\n", "0\n", - "\n", - "\n", - "0\n", + "\n", + "\n", + "0\n", "\n", "\n", "\n", "6->0\n", - "\n", - "\n", - "!a & !b & c\n", + "\n", + "\n", + "!a & !b & c\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "!a & b & c\n", + "\n", + "\n", + "!a & b & c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", "4\n", - "\n", - "\n", - "4\n", + "\n", + "\n", + "4\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b & c\n", + "\n", + "\n", + "a & !b & c\n", "\n", "\n", "\n", "5\n", - "\n", - "\n", - "5\n", + "\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "a & b & !c\n", + "\n", + "\n", + "a & b & !c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "c\n", + "\n", + "\n", + "c\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!b & c\n", + "\n", + "\n", + "!b & c\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b & c\n", + "\n", + "\n", + "b & c\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "b & !c\n", + "\n", + "\n", + "b & !c\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "4->0\n", - "\n", - "\n", - "!a & c\n", + "\n", + "\n", + "!a & c\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "a & !c\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a & c\n", + "\n", + "\n", + "a & c\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", @@ -1372,318 +1372,318 @@ "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & b & c\n", + "\n", + "\n", + "a & b & c\n", "⓿\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a & !b & c\n", - "⓿\n", + "\n", + "\n", + "!a & !b & c\n", + "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b & c\n", - "⓿\n", + "\n", + "\n", + "!a & b & c\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!a & b & !c\n", - "⓿\n", + "\n", + "\n", + "!a & b & !c\n", + "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "a & !b & !c\n", - "⓿\n", + "\n", + "\n", + "a & !b & !c\n", + "⓿\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "a & !b & c\n", - "⓿\n", + "\n", + "\n", + "a & !b & c\n", + "⓿\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a & b & !c\n", - "⓿\n", + "\n", + "\n", + "a & b & !c\n", + "⓿\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "0->7\n", - "\n", - "\n", - "!a & !b & !c\n", - "⓿\n", + "\n", + "\n", + "!a & !b & !c\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "c\n", - "⓿\n", + "\n", + "\n", + "c\n", + "⓿\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a & !c\n", - "⓿\n", + "\n", + "\n", + "!a & !c\n", + "⓿\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "a & !c\n", - "⓿\n", + "\n", + "\n", + "a & !c\n", + "⓿\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!b & c\n", - "⓿\n", + "\n", + "\n", + "!b & c\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b & c\n", - "⓿\n", + "\n", + "\n", + "b & c\n", + "⓿\n", "\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "b & !c\n", - "⓿\n", + "\n", + "\n", + "b & !c\n", + "⓿\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "!a & !b & !c\n", - "⓿\n", + "\n", + "\n", + "!a & !b & !c\n", + "⓿\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "a & !b & !c\n", - "⓿\n", + "\n", + "\n", + "a & !b & !c\n", + "⓿\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "3->7\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "4->7\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!a & c\n", - "⓿\n", + "\n", + "\n", + "!a & c\n", + "⓿\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "a & !c\n", - "⓿\n", + "\n", + "\n", + "a & !c\n", + "⓿\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "a & c\n", - "⓿\n", + "\n", + "\n", + "a & c\n", + "⓿\n", "\n", "\n", "\n", "5->7\n", - "\n", - "\n", - "!a & !c\n", - "⓿\n", + "\n", + "\n", + "!a & !c\n", + "⓿\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "6->4\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "7->7\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", @@ -1714,203 +1714,203 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", @@ -1929,262 +1929,262 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "⓿\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -2213,243 +2213,243 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\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", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "a\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a\n", - "❶\n", + "\n", + "\n", + "!a\n", + "❶\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a\n", - "❶\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "❶\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -2468,243 +2468,243 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ") | Inf(\n", - "❶\n", - ")\n", - "[Fin-less 2]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ") | Inf(\n", + "❶\n", + ")\n", + "[Fin-less 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "a\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a\n", - "❶\n", + "\n", + "\n", + "!a\n", + "❶\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", - "\n", + "\n", "2->3\n", - "\n", - "\n", - "a\n", - "❶\n", + "\n", + "\n", + "a\n", + "❶\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "!a\n", + "⓿\n", + "❶\n", "\n", "\n", - "\n", + "\n", "3->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -2733,190 +2733,190 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", @@ -2935,146 +2935,146 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -3103,132 +3103,132 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", @@ -3247,203 +3247,203 @@ "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "
\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "⓿\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a\n", - "⓿\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a\n", + "⓿\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -3460,6 +3460,13 @@ "source": [ "test(spot.translate('(Ga | GF!a)'), spot.translate('false'))" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -3478,7 +3485,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5+" + "version": "3.9.1+" } }, "nbformat": 4, diff --git a/tests/python/alternation.ipynb b/tests/python/alternation.ipynb index 0117da723..96fcbf2c9 100644 --- a/tests/python/alternation.ipynb +++ b/tests/python/alternation.ipynb @@ -3667,14 +3667,14 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -3706,7 +3706,7 @@ "1->1\n", "\n", "\n", - "1\n", + "!a\n", "\n", "\n", "\n", @@ -4296,7 +4296,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.9.1+" } }, "nbformat": 4, diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb index 2024d5ccd..1a62abff7 100644 --- a/tests/python/atva16-fig2a.ipynb +++ b/tests/python/atva16-fig2a.ipynb @@ -51,111 +51,111 @@ "\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", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a | b\n", + "\n", + "\n", + "a | b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!a & b\n", - "❶\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & b\n", + "❶\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & b\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "a & b\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", + "❶\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f62d41ff690> >" + " *' at 0x7f12cf944300> >" ] }, "execution_count": 3, @@ -238,7 +238,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.7" + "version": "3.9.1+" } }, "nbformat": 4, diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index e827ff3f2..4382c10f1 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -200,7 +200,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000ab150> >" + " *' at 0x7f09cc092f00> >" ] }, "execution_count": 2, @@ -330,7 +330,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb015474e0> >" + " *' at 0x7f09cc211360> >" ] }, "execution_count": 3, @@ -489,7 +489,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000ab360> >" + " *' at 0x7f09cc23f3c0> >" ] }, "execution_count": 4, @@ -587,7 +587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000ab840> >" + " *' at 0x7f09cc0ea4e0> >" ] }, "execution_count": 5, @@ -655,21 +655,21 @@ "0->0\n", "\n", "\n", - "!a & !c\n", - "⓿\n", + "a & !c\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "!a & !c\n", + "⓿\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fbb000abb40> >" + " *' at 0x7f09cc0ea840> >" ] }, "execution_count": 6, @@ -796,7 +796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000abd50> >" + " *' at 0x7f09cc0eaab0> >" ] }, "metadata": {}, @@ -941,7 +941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000abf00> >" + " *' at 0x7f09cc20bc60> >" ] }, "metadata": {}, @@ -1109,7 +1109,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00d0fd80> >" + " *' at 0x7f09cc092cc0> >" ] }, "metadata": {}, @@ -1512,7 +1512,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000ab390> >" + " *' at 0x7f09cc0ea570> >" ] }, "execution_count": 8, @@ -1942,7 +1942,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00064e40> >" + " *' at 0x7f09cc0eaa50> >" ] }, "metadata": {}, @@ -1957,8 +1957,8 @@ "\n", "\n", - "\n", + "\n", "\n", "strictly weak\n", "\n", @@ -2174,7 +2174,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00064e10> >" + " *' at 0x7f09cc092cc0> >" ] }, "metadata": {}, @@ -2384,7 +2384,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000abed0> >" + " *' at 0x7f09cc21dea0> >" ] }, "metadata": {}, @@ -2772,7 +2772,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00cd01e0> >" + " *' at 0x7f09cc0ea7b0> >" ] }, "execution_count": 10, @@ -2793,7 +2793,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -2933,7 +2933,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000798a0> >" + " *' at 0x7f09cc0ab3f0> >" ] }, "metadata": {}, @@ -3072,7 +3072,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079660> >" + " *' at 0x7f09cc211570> >" ] }, "metadata": {}, @@ -3224,7 +3224,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079750> >" + " *' at 0x7f09cc23fa80> >" ] }, "metadata": {}, @@ -3252,7 +3252,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 12, "metadata": {}, "outputs": [ { @@ -3577,10 +3577,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00d0f0f0> >" + " *' at 0x7f09cc21d750> >" ] }, - "execution_count": 13, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } @@ -3641,7 +3641,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -3960,7 +3960,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079420> >" + " *' at 0x7f09cc0ea480> >" ] }, "metadata": {}, @@ -4137,7 +4137,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb01538de0> >" + " *' at 0x7f09cc23fae0> >" ] }, "metadata": {}, @@ -4295,7 +4295,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00d0f360> >" + " *' at 0x7f09cc092c00> >" ] }, "metadata": {}, @@ -4320,7 +4320,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -4644,10 +4644,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000abd50> >" + " *' at 0x7f09cc0ea3c0> >" ] }, - "execution_count": 15, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -4673,7 +4673,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -4767,10 +4767,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079330> >" + " *' at 0x7f09cc23fbd0> >" ] }, - "execution_count": 16, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -4781,7 +4781,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 16, "metadata": {}, "outputs": [], "source": [ @@ -4791,7 +4791,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -4865,7 +4865,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079660> >" + " *' at 0x7f09cc0eac90> >" ] }, "metadata": {}, @@ -4941,7 +4941,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000abea0> >" + " *' at 0x7f09cc21d7e0> >" ] }, "metadata": {}, @@ -4962,7 +4962,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -5035,10 +5035,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000791b0> >" + " *' at 0x7f09cc0eaab0> >" ] }, - "execution_count": 19, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -5065,7 +5065,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -5185,10 +5185,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079300> >" + " *' at 0x7f09cc0ab6f0> >" ] }, - "execution_count": 20, + "execution_count": 19, "metadata": {}, "output_type": "execute_result" } @@ -5226,7 +5226,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -5345,7 +5345,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079d50> >" + " *' at 0x7f09cc0abb70> >" ] }, "metadata": {}, @@ -5447,7 +5447,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000abcf0> >" + " *' at 0x7f09cc092c00> >" ] }, "metadata": {}, @@ -5582,7 +5582,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000abe70> >" + " *' at 0x7f09cc0abae0> >" ] }, "metadata": {}, @@ -5611,7 +5611,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -5786,7 +5786,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000ab930> >" + " *' at 0x7f09cc0ea1e0> >" ] }, "metadata": {}, @@ -5927,10 +5927,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb00079db0> >" + " *' at 0x7f09cc0ea630> >" ] }, - "execution_count": 22, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } @@ -5953,7 +5953,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 22, "metadata": {}, "outputs": [ { @@ -6030,10 +6030,10 @@ "\n" ], "text/plain": [ - " *' at 0x7fbb000792d0> >" + " *' at 0x7f09cc0eae70> >" ] }, - "execution_count": 23, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -6041,13 +6041,6 @@ "source": [ "spot.decompose_scc(si, 'a2')" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -6066,7 +6059,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.5" + "version": "3.9.1+" } }, "nbformat": 4, diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 3b69aa3ff..12077b8c9 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -247,7 +247,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da043c8d0> >" + " *' at 0x7efc20027d80> >" ] }, "execution_count": 4, @@ -359,7 +359,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0446d20> >" + " *' at 0x7efc2002e2a0> >" ] }, "execution_count": 5, @@ -469,7 +469,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da043c8d0> >" + " *' at 0x7efc20027d80> >" ] }, "execution_count": 6, @@ -659,30 +659,30 @@ "1->1\n", "\n", "\n", - "!b\n", - "⓿\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", - "a & !b\n", - "⓿\n", + "a & b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", @@ -702,7 +702,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0446e70> >" + " *' at 0x7efc2002e360> >" ] }, "execution_count": 8, @@ -852,32 +852,32 @@ "\n", "\n", "1->1\n", - "\n", - "\n", - "!b\n", - "⓿\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", - "a & !b\n", - "⓿\n", + "a & b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", @@ -897,7 +897,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0446e70> >" + " *' at 0x7efc2002e360> >" ] }, "execution_count": 11, @@ -1235,7 +1235,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da045a150> >" + " *' at 0x7efc2002edb0> >" ] }, "metadata": {}, @@ -1250,9 +1250,9 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "\n", "Fin(\n", "❺\n", @@ -1496,7 +1496,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0446510> >" + " *' at 0x7efc20027de0> >" ] }, "metadata": {}, @@ -1679,7 +1679,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da044c6f0> >" + " *' at 0x7efc2002e570> >" ] }, "metadata": {}, @@ -1796,7 +1796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da044cb10> >" + " *' at 0x7efc2002e480> >" ] }, "metadata": {}, @@ -1851,7 +1851,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da044ca20> >" + " *' at 0x7efc2002e6c0> >" ] }, "metadata": {}, @@ -1945,7 +1945,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da04520f0> >" + " *' at 0x7efc2002ec60> >" ] }, "execution_count": 14, @@ -2074,7 +2074,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da04520f0> >" + " *' at 0x7efc2002ec60> >" ] }, "metadata": {}, @@ -2139,7 +2139,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da044cb10> >" + " *' at 0x7efc2002e480> >" ] }, "metadata": {}, @@ -2194,7 +2194,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da044ca20> >" + " *' at 0x7efc2002e6c0> >" ] }, "metadata": {}, @@ -2425,7 +2425,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0468a50> >" + " *' at 0x7efc20044780> >" ] }, "metadata": {}, @@ -2510,7 +2510,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0468de0> >" + " *' at 0x7efc200449c0> >" ] }, "metadata": {}, @@ -2607,7 +2607,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0468bd0> >" + " *' at 0x7efc200448d0> >" ] }, "metadata": {}, @@ -2733,30 +2733,30 @@ "1->1\n", "\n", "\n", - "!b\n", - "⓿\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "⓿\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", - "a & !b\n", - "⓿\n", + "a & b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", @@ -2776,7 +2776,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0461210> >" + " *' at 0x7efc20044f30> >" ] }, "execution_count": 19, @@ -2861,15 +2861,15 @@ "0->0\n", "\n", "\n", - "a & !b\n", - "⓿\n", + "a & b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", @@ -2882,15 +2882,15 @@ "1->1\n", "\n", "\n", - "!b\n", - "⓿\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "⓿\n", "\n", "\n", "\n", @@ -2944,7 +2944,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0461210> >" + " *' at 0x7efc20044f30> >" ] }, "execution_count": 20, @@ -3024,15 +3024,15 @@ "0->0\n", "\n", "\n", - "a & !b\n", - "⓿\n", + "a & b\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", @@ -3045,15 +3045,15 @@ "1->1\n", "\n", "\n", - "!b\n", - "⓿\n", + "b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "⓿\n", "\n", "\n", "\n", @@ -3107,7 +3107,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f7da0461210> >" + " *' at 0x7efc20044f30> >" ] }, "metadata": {}, @@ -3212,15 +3212,15 @@ "2->2\n", "\n", "\n", - "!b\n", - "⓿\n", + "b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", + "⓿\n", "\n", "\n", "\n", @@ -3615,7 +3615,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.9.1+" } }, "nbformat": 4, diff --git a/tests/python/mergedge.py b/tests/python/mergedge.py index e6a2e0008..e1dffc80a 100644 --- a/tests/python/mergedge.py +++ b/tests/python/mergedge.py @@ -26,3 +26,30 @@ Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""") assert aut.num_edges() == 2 aut.merge_edges() assert aut.num_edges() == 1 + +aut = spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +--BODY-- +State: 0 +[!0] 0 {0} +[0] 1 {0} +State: 1 +[!0&!1] 0 {0} +[0 | 1] 1 +[0&!1] 1 {0} +--END--""") +assert aut.num_edges() == 5 +aut.merge_edges() +assert aut.num_edges() == 5 +assert not spot.is_deterministic(aut) +aut = spot.split_edges(aut) +assert aut.num_edges() == 9 +aut.merge_edges() +assert aut.num_edges() == 5 +assert spot.is_deterministic(aut) diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb index 3e9c7c8b1..4cec11ad3 100644 --- a/tests/python/satmin.ipynb +++ b/tests/python/satmin.ipynb @@ -143,28 +143,28 @@ "!a\n", "\n", "\n", - "\n", + "\n", "4->6\n", "\n", "\n", "b\n", "\n", "\n", - "\n", + "\n", "4->4\n", "\n", "\n", "a & !b\n", "\n", "\n", - "\n", + "\n", "4->5\n", "\n", "\n", "!a & !b\n", "\n", "\n", - "\n", + "\n", "5->6\n", "\n", "\n", @@ -177,7 +177,7 @@ "2\n", "\n", "\n", - "\n", + "\n", "5->2\n", "\n", "\n", @@ -190,7 +190,7 @@ "3\n", "\n", "\n", - "\n", + "\n", "5->3\n", "\n", "\n", @@ -211,42 +211,42 @@ "!a\n", "\n", "\n", - "\n", + "\n", "2->6\n", "\n", "\n", "!b\n", "\n", "\n", - "\n", + "\n", "2->4\n", "\n", "\n", "a & b\n", "\n", "\n", - "\n", + "\n", "2->5\n", "\n", "\n", "!a & b\n", "\n", "\n", - "\n", + "\n", "3->6\n", "\n", "\n", "!b\n", "\n", "\n", - "\n", + "\n", "3->2\n", "\n", "\n", "a & b\n", "\n", "\n", - "\n", + "\n", "3->3\n", "\n", "\n", @@ -256,7 +256,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c465a80> >" + " *' at 0x7fe138232480> >" ] }, "execution_count": 3, @@ -289,162 +289,162 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\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", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "a & b\n", + "\n", + "\n", + "a & !b\n", + "⓿\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "a & !b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "a & b\n", + "\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", "1->3\n", - "\n", - "\n", - "!a & !b\n", - "⓿\n", + "\n", + "\n", + "!a & !b\n", + "⓿\n", "\n", "\n", "\n", "2->0\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "a & b\n", - "⓿\n", + "\n", + "\n", + "a & b\n", + "⓿\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "!a & b\n", - "⓿\n", + "\n", + "\n", + "!a & b\n", + "⓿\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "!a & !b\n", + "\n", + "\n", + "!a & !b\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f461c462d80> >" + " *' at 0x7fe1381dadb0> >" ] }, "execution_count": 4, @@ -680,7 +680,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c46dc60> >" + " *' at 0x7fe138232030> >" ] }, "execution_count": 5, @@ -720,9 +720,9 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "& | F G a F b F G c\n", "\n", "(Fin(\n", @@ -913,7 +913,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c46dab0> >" + " *' at 0x7fe1382323f0> >" ] }, "execution_count": 6, @@ -1062,7 +1062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c46dd20> >" + " *' at 0x7fe1382325d0> >" ] }, "execution_count": 7, @@ -1234,7 +1234,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c511270> >" + " *' at 0x7fe1382327e0> >" ] }, "execution_count": 8, @@ -1393,7 +1393,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c46de40> >" + " *' at 0x7fe138232a20> >" ] }, "execution_count": 9, @@ -1465,8 +1465,8 @@ " NaN\n", " 996\n", " 48806\n", - " 2\n", - " 0\n", + " 3\n", + " 1\n", " 1\n", " 0\n", " \n", @@ -1479,9 +1479,9 @@ " 40\n", " 2760\n", " 224707\n", - " 9\n", + " 12\n", " 0\n", - " 7\n", + " 9\n", " 0\n", " \n", " \n", @@ -1493,7 +1493,7 @@ " 32\n", " 2008\n", " 155020\n", - " 6\n", + " 8\n", " 0\n", " 7\n", " 0\n", @@ -1509,9 +1509,9 @@ "2 5 4 4 11 32 2008 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 48806 2 0 1 0 \n", - "1 224707 9 0 7 0 \n", - "2 155020 6 0 7 0 " + "0 48806 3 1 1 0 \n", + "1 224707 12 0 9 0 \n", + "2 155020 8 0 7 0 " ] }, "metadata": {}, @@ -1652,7 +1652,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c462cc0> >" + " *' at 0x7fe138232750> >" ] }, "execution_count": 10, @@ -1722,7 +1722,7 @@ " 15974\n", " 1\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -1734,9 +1734,9 @@ " 40\n", " 960\n", " 73187\n", - " 3\n", + " 4\n", " 0\n", - " 2\n", + " 3\n", " 0\n", " \n", " \n", @@ -1748,9 +1748,9 @@ " 32\n", " 616\n", " 37620\n", - " 1\n", + " 3\n", + " 0\n", " 0\n", - " 1\n", " 0\n", " \n", " \n", @@ -1764,9 +1764,9 @@ "2 2 4 4 11 32 616 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 15974 1 0 0 0 \n", - "1 73187 3 0 2 0 \n", - "2 37620 1 0 1 0 " + "0 15974 1 0 1 0 \n", + "1 73187 4 0 3 0 \n", + "2 37620 3 0 0 0 " ] }, "metadata": {}, @@ -1907,7 +1907,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fde18360> >" + " *' at 0x7fe138b8ac30> >" ] }, "execution_count": 11, @@ -1977,9 +1977,9 @@ " 40\n", " 2300\n", " 288887\n", - " 13\n", - " 1\n", - " 12\n", + " 19\n", + " 0\n", + " 25\n", " 0\n", " \n", " \n", @@ -2021,7 +2021,7 @@ "2 2 1 NaN NaN NaN 92 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 288887 13 1 12 0 \n", + "0 288887 19 0 25 0 \n", "1 18569 1 0 1 0 \n", "2 2337 0 0 0 0 " ] @@ -2121,7 +2121,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fde18bd0> >" + " *' at 0x7fe138232f60> >" ] }, "execution_count": 12, @@ -2189,9 +2189,9 @@ " 40\n", " 2742\n", " 173183\n", - " 7\n", + " 9\n", " 0\n", - " 4\n", + " 7\n", " 0\n", " \n", " \n", @@ -2203,9 +2203,9 @@ " 32\n", " 964\n", " 45412\n", - " 3\n", - " 0\n", + " 2\n", " 0\n", + " 2\n", " 0\n", " \n", " \n", @@ -2217,7 +2217,7 @@ " NaN\n", " 363\n", " 10496\n", - " 0\n", + " 1\n", " 0\n", " 0\n", " 0\n", @@ -2233,9 +2233,9 @@ "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173183 7 0 4 0 \n", - "1 45412 3 0 0 0 \n", - "2 10496 0 0 0 0 " + "0 173183 9 0 7 0 \n", + "1 45412 2 0 2 0 \n", + "2 10496 1 0 0 0 " ] }, "metadata": {}, @@ -2372,7 +2372,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fde18d20> >" + " *' at 0x7fe138b8a1b0> >" ] }, "execution_count": 13, @@ -2453,10 +2453,10 @@ " NaN\n", " 2747\n", " 173427\n", + " 8\n", + " 0\n", " 6\n", - " 0\n", - " 2\n", - " 0\n", + " 1\n", " \n", " \n", " 1\n", @@ -2469,7 +2469,7 @@ " 173427\n", " 0\n", " 0\n", - " 1\n", + " 2\n", " 0\n", " \n", " \n", @@ -2483,7 +2483,7 @@ " 173427\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -2497,9 +2497,9 @@ "2 6 4 4 12 32 2747 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173427 6 0 2 0 \n", - "1 173427 0 0 1 0 \n", - "2 173427 0 0 0 0 " + "0 173427 8 0 6 1 \n", + "1 173427 0 0 2 0 \n", + "2 173427 0 0 1 0 " ] }, "metadata": {}, @@ -2643,7 +2643,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fde2a750> >" + " *' at 0x7fe120556e10> >" ] }, "execution_count": 14, @@ -2713,9 +2713,9 @@ " 40\n", " 2742\n", " 173183\n", - " 7\n", + " 9\n", " 0\n", - " 3\n", + " 6\n", " 0\n", " \n", " \n", @@ -2727,9 +2727,9 @@ " 32\n", " 2742\n", " 173279\n", - " 1\n", " 0\n", - " 1\n", + " 0\n", + " 2\n", " 0\n", " \n", " \n", @@ -2743,7 +2743,7 @@ " 173327\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -2757,9 +2757,9 @@ "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173183 7 0 3 0 \n", - "1 173279 1 0 1 0 \n", - "2 173327 0 0 0 0 " + "0 173183 9 0 6 0 \n", + "1 173279 0 0 2 0 \n", + "2 173327 0 0 1 0 " ] }, "metadata": {}, @@ -2903,7 +2903,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fde183f0> >" + " *' at 0x7fe138232bd0> >" ] }, "execution_count": 15, @@ -3069,7 +3069,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fde2ad80> >" + " *' at 0x7fe120556d50> >" ] }, "metadata": {}, @@ -3120,9 +3120,9 @@ " 40\n", " 2742\n", " 173183\n", - " 7\n", + " 9\n", " 0\n", - " 3\n", + " 7\n", " 0\n", " HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", " \n", @@ -3137,7 +3137,7 @@ " 173279\n", " 0\n", " 0\n", - " 0\n", + " 2\n", " 0\n", " HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", " \n", @@ -3167,8 +3167,8 @@ "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \\\n", - "0 173183 7 0 3 0 \n", - "1 173279 0 0 0 0 \n", + "0 173183 9 0 7 0 \n", + "1 173279 0 0 2 0 \n", "2 173327 1 0 0 0 \n", "\n", " automaton \n", @@ -3357,7 +3357,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fddb33f0> >" + " *' at 0x7fe1205266c0> >" ] }, "metadata": {}, @@ -3508,7 +3508,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fddb3480> >" + " *' at 0x7fe120526cc0> >" ] }, "metadata": {}, @@ -3547,9 +3547,9 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "& | F G a F b F G c\n", "\n", "(Fin(\n", @@ -3740,7 +3740,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f461c46dab0> >" + " *' at 0x7fe1382323f0> >" ] }, "execution_count": 18, @@ -3808,7 +3808,7 @@ " NaN\n", " 687\n", " 21896\n", - " 1\n", + " 2\n", " 0\n", " 0\n", " 0\n", @@ -3822,9 +3822,9 @@ " 32\n", " 1905\n", " 100457\n", - " 4\n", - " 0\n", - " 3\n", + " 6\n", + " 1\n", + " 5\n", " 0\n", " \n", " \n", @@ -3837,8 +3837,8 @@ "1 6 5 4 12 32 1905 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 21896 1 0 0 0 \n", - "1 100457 4 0 3 0 " + "0 21896 2 0 0 0 \n", + "1 100457 6 1 5 0 " ] }, "metadata": {}, @@ -3853,8 +3853,8 @@ "\n", "\n", - "\n", + "\n", "\n", "\n", "Fin(\n", @@ -3982,7 +3982,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fddb3ab0> >" + " *' at 0x7fe138b8aa50> >" ] }, "execution_count": 19, @@ -4044,9 +4044,9 @@ " 32\n", " 1220\n", " 51612\n", - " 2\n", + " 3\n", " 0\n", - " 1\n", + " 2\n", " 0\n", " \n", "
\n", @@ -4072,10 +4072,10 @@ " NaN\n", " 363\n", " 10496\n", + " 0\n", + " 0\n", " 1\n", " 0\n", - " 0\n", - " 0\n", "
\n", " \n", "\n", @@ -4088,9 +4088,9 @@ "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 51612 2 0 1 0 \n", + "0 51612 3 0 2 0 \n", "1 3129 0 0 0 0 \n", - "2 10496 1 0 0 0 " + "2 10496 0 0 1 0 " ] }, "metadata": {}, @@ -4234,7 +4234,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fddb3c30> >" + " *' at 0x7fe120526990> >" ] }, "execution_count": 20, @@ -4305,9 +4305,9 @@ " 56\n", " 1379\n", " 89168\n", - " 3\n", + " 5\n", " 0\n", - " 1\n", + " 4\n", " 0\n", " \n", " \n", @@ -4319,7 +4319,7 @@ "0 2 7 7 23 56 1379 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 89168 3 0 1 0 " + "0 89168 5 0 4 0 " ] }, "metadata": {}, @@ -4559,7 +4559,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f45fddb3750> >" + " *' at 0x7fe120556f00> >" ] }, "execution_count": 21, @@ -4588,7 +4588,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.9.1+" } }, "nbformat": 4, diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 8e5e1c712..1ca625d61 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017-2018, 2020 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2015, 2017-2018, 2020-2021 Laboratoire de Recherche +# et Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -185,6 +185,6 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 "[1,7]" -[!1] 0 {0} [1] 0 +[!1] 0 {0} --END--"""