diff --git a/NEWS b/NEWS index db61afd3b..6a6990aed 100644 --- a/NEWS +++ b/NEWS @@ -105,9 +105,11 @@ New in spot 2.7.5.dev (not yet released) - The LTL simplifier learned the following optional rules: F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ") - G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ") + G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ") F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly") G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly") + GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly") + FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly") - cleanup_parity() and colorize_parity() were cleaned up a bit, resulting in fewer colors used in some cases. In particular, diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 38c19da92..936a17ce6 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -116,7 +116,7 @@ \newcommand{\nsereMarked}[1]{\texttt{!+\{}#1\texttt{\}}} \newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}} -% rewriting rules that enlarge the formula +% rewriting rules that (may) enlarge the formula \newcommand{\equiV}{\stackrel{\star}{\equiv}} % rewriting rules that favors event/univ \newcommand{\equivEU}{\stackrel{\blacktriangleup}{\equiv}} @@ -1463,15 +1463,19 @@ instead of $\equiv$, and they can be disabled by setting the \label{sec:basic-simp-ltl} The following are simplification rules for unary operators (applied -from left to right, as usual): +from left to right, as usual). The terms $\mathsf{dnf}(f)$ and +$\mathsf{cnf}(f)$ denote respectively the disjunctive and conjunctive +normal forms if $f$, handling non-Boolean sub-formulas as if they were +atomic propositions. + \begin{align*} - \X\F\G f & \equiv \F\G f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\ - \X\G\F f & \equiv \G\F f & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g) \\ -\F\X f & \equiv \X\F f & \F\G(f\AND \X g) & \equiv \F\G(f\AND g) & \G\F(f\OR \X g) & \equiv \G\F(f\OR g) \\ -\G\X f & \equiv \X\G f & \F\G(f\AND \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\ - & & \F\G(f\OR\G g) & \equiv \F(\G f\OR\G g) & \G\F(f\AND\F g) & \equiv \G(\F f\AND\F g) \\ - & & \F\G(f\AND\F g) & \equiV \F\G f\AND\G\F g & \G\F(f\AND\G g) & \equiV \G\F f\AND\F\G g \\ - & & \F\G(f\OR\F g) & \equivEU \F\G f\OR\G\F g & \G\F(f\OR\G g) & \equivEU \G\F f\OR\F\G g + \X\F\G f & \equiv \F\G f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\ + \X\G\F f & \equiv \G\F f & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g) \\ +\F\X f & \equiv \X\F f & \F\G(f\AND \X g) & \equiv \F\G(f\AND g) & \G\F(f\OR \X g) & \equiv \G\F(f\OR g) \\ +\G\X f & \equiv \X\G f & \F\G(f\AND \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\ + & & \F\G(f\OR\G g) & \equiv \F(\G f\OR\G g) & \G\F(f\AND\F g) & \equiv \G(\F f\AND\F g) \\ +\G\F f & \equiV \G\F(\mathsf{dnf}(f)) & \F\G(f\AND\F g) & \equiV \F\G f\AND\G\F g & \G\F(f\AND\G g) & \equiV \G\F f\AND\F\G g \\ +\F\G f & \equiV \F\G(\mathsf{cnf}(f)) & \F\G(f\OR\F g) & \equivEU \F\G f\OR\G\F g & \G\F(f\OR\G g) & \equivEU \G\F f\OR\F\G g \end{align*} \begin{align*} \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m) diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 82e354796..db8e5cdef 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -33,6 +33,7 @@ #include #include #include +#include #include #include @@ -45,6 +46,7 @@ namespace spot { typedef std::unordered_map f2f_map; typedef std::unordered_map f2b_map; + typedef std::map b2f_map; typedef std::pair pairf; typedef std::map syntimpl_cache_t; public: @@ -78,13 +80,18 @@ namespace spot << "syntactic implications: " << syntimpl_.size() << " entries\n" << "boolean to bdd: " << as_bdd_.size() << " entries\n" << "star normal form: " << snf_cache_.size() << " entries\n" - << "boolean isop: " << bool_isop_.size() << " entries\n"; + << "boolean isop: " << bool_isop_.size() << " entries\n" + << "as dnf: " << as_dnf_.size() << " entries\n" + << "as cnf: " << as_cnf_.size() << " entries\n"; } void clear_as_bdd_cache() { as_bdd_.clear(); + for (auto p: bdd_to_f_) + dict->unregister_variable(p.first, this); + bdd_to_f_.clear(); } // Convert a Boolean formula into a BDD for easier comparison. @@ -136,7 +143,12 @@ namespace spot break; } default: - SPOT_UNIMPLEMENTED(); + { + unsigned var = dict->register_anonymous_variables(1, this); + bdd_to_f_[var] = f; + result = bdd_ithvar(var); + break; + } } // Cache the result before returning. @@ -144,6 +156,83 @@ namespace spot return result; } + formula as_xnf(formula f, bool cnf) + { + bdd in = as_bdd(f); + if (cnf) + in = !in; + minato_isop isop(in); + bdd cube; + vec clauses; + while ((cube = isop.next()) != bddfalse) + { + vec literals; + while (cube != bddtrue) + { + int var = bdd_var(cube); + const bdd_dict::bdd_info& i = dict->bdd_map[var]; + formula res; + if (i.type == bdd_dict::var) + { + res = i.f; + } + else + { + res = bdd_to_f_[var]; + assert(res); + } + bdd high = bdd_high(cube); + if (high == bddfalse) + { + if (!cnf) + res = formula::Not(res); + cube = bdd_low(cube); + } + else + { + if (cnf) + res = formula::Not(res); + // If bdd_low is not false, then cube was not a + // conjunction. + assert(bdd_low(cube) == bddfalse); + cube = high; + } + assert(cube != bddfalse); + literals.emplace_back(res); + } + if (cnf) + clauses.emplace_back(formula::Or(literals)); + else + clauses.emplace_back(formula::And(literals)); + } + if (cnf) + return formula::And(clauses); + else + return formula::Or(clauses); + } + + formula as_dnf(formula f) + { + auto i = as_dnf_.find(f); + if (i != as_dnf_.end()) + return i->second; + formula r = as_xnf(f, false); + as_dnf_[f] = r; + return r; + } + + formula as_cnf(formula f) + { + auto i = as_cnf_.find(f); + if (i != as_cnf_.end()) + return i->second; + formula r = as_xnf(f, true); + as_cnf_[f] = r; + return r; + } + + + formula lookup_nenoform(formula f) { @@ -303,7 +392,10 @@ namespace spot private: f2b_map as_bdd_; + b2f_map bdd_to_f_; f2f_map simplified_; + f2f_map as_dnf_; + f2f_map as_cnf_; f2f_map nenoform_; syntimpl_cache_t syntimpl_; snf_cache snf_cache_; @@ -987,22 +1079,32 @@ namespace spot return recurse(res); } - // FG(a & Xb) = FG(a & b) - // FG(a & Gb) = FG(a & b) - if (c.is({op::G, op::And})) + // FG(a) = FG(dnf(a)) if a is not Boolean + // and contains some | above non-Boolean subformulas. + if (c.is(op::G) && !c[0].is_boolean()) { formula m = c[0]; - if (!m.is_boolean()) - { - formula out = m.map([](formula f) - { - if (f.is(op::X, op::G)) - return f[0]; - return f; - }); - if (out != m) - return recurse(unop_unop(op::F, op::G, out)); - } + bool want_cnf = m.is(op::And); + if (!want_cnf && m.is(op::Or)) + for (auto cc : m) + if (cc.is(op::And)) + { + want_cnf = true; + break; + } + if (want_cnf && !opt_.reduce_size_strictly) + m = c_->as_cnf(m); + // FG(a & Xb) = FG(a & b) + // FG(a & Gb) = FG(a & b) + if (m.is(op::And)) + m = m.map([](formula f) + { + if (f.is(op::X, op::G)) + return f[0]; + return f; + }); + if (c[0] != m) + return recurse(unop_unop(op::F, op::G, m)); } } // if Fa => a, keep a. @@ -1248,22 +1350,33 @@ namespace spot return recurse(res); } - // GF(a | Xb) = GF(a | b) - // GF(a | Fb) = GF(a | b) - if (c.is({op::F, op::Or})) + + // GF(a) = GF(dnf(a)) if a is not Boolean + // and contains some | above non-Boolean subformulas. + if (c.is(op::F) && !c[0].is_boolean()) { formula m = c[0]; - if (!m.is_boolean()) - { - formula out = m.map([](formula f) - { - if (f.is(op::X, op::F)) - return f[0]; - return f; - }); - if (out != m) - return recurse(unop_unop(op::G, op::F, out)); - } + bool want_dnf = m.is(op::Or); + if (!want_dnf && m.is(op::And)) + for (auto cc : m) + if (cc.is(op::Or)) + { + want_dnf = true; + break; + } + if (want_dnf && !opt_.reduce_size_strictly) + m = c_->as_dnf(m); + // GF(a | Xb) = GF(a | b) + // GF(a | Fb) = GF(a | b) + if (m.is(op::Or)) + m = m.map([](formula f) + { + if (f.is(op::X, op::F)) + return f[0]; + return f; + }); + if (c[0] != m) + return recurse(unop_unop(op::G, op::F, m)); } // GF(f1 & f2 & eu1 & eu2) = G(F(f1 & f2) & eu1 & eu2 if (opt_.event_univ && c.is({op::F, op::And})) diff --git a/tests/Makefile.am b/tests/Makefile.am index ef2430ae4..253b82dc3 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -208,6 +208,7 @@ TESTS_misc = \ core/trival.test TESTS_twa = \ + core/385.test \ core/acc.test \ core/acc2.test \ core/bdddict.test \ diff --git a/tests/core/385.test b/tests/core/385.test new file mode 100755 index 000000000..a3ae9cecb --- /dev/null +++ b/tests/core/385.test @@ -0,0 +1,45 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2019 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs + +set -e + +# Formulas from issue #385. + +ltl2tgba -G --stats=%s,%f> out < (e & X!d)) +G(Gc | Fa | F!G(c | Ge)) +Ge | XGF(Ge & X(c & Fd)) +G!GXXe -> GF(b & c & Gc) +G!(Gd & (c | Fb)) +XF(F(Gc & Xb) -> a) +EOF + +# Some of the following are still not optimal. +cat >expected <formulas < GF(b & c & Gc), F(G(Fb & FGc) | Ge) +GFX((e & XXXa) -> (e & X!d)), GF(!a | !d | !e) +!GFX((e & XXXa) -> (e & X!d)), FG(a & d & e) # Because reduccmp will translate the formula, # this also check for an old bug in ltl2tgba_fm. diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 9209b6991..ac2718107 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c0b2de0> >" + " *' at 0x7f5a6034a960> >" ] }, "execution_count": 2, @@ -643,7 +643,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c02c930> >" + " *' at 0x7f5a60301210> >" ] }, "execution_count": 6, @@ -719,7 +719,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c02c960> >" + " *' at 0x7f5a60301bd0> >" ] }, "execution_count": 7, @@ -802,7 +802,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c02ca80> >" + " *' at 0x7f5a60301690> >" ] }, "execution_count": 8, @@ -1321,7 +1321,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c03ec90> >" + " *' at 0x7f5a603010c0> >" ] }, "execution_count": 12, @@ -1435,7 +1435,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c03edb0> >" + " *' at 0x7f5a60301090> >" ] }, "execution_count": 13, @@ -1566,7 +1566,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c03ecf0> >" + " *' at 0x7f5a60301c90> >" ] }, "execution_count": 14, @@ -1785,7 +1785,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1540> >" + " *' at 0x7f5a6030f4b0> >" ] }, "metadata": {}, @@ -1935,7 +1935,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c02c630> >" + " *' at 0x7f5a60392630> >" ] }, "metadata": {}, @@ -2107,7 +2107,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1780> >" + " *' at 0x7f5a6030f930> >" ] }, "metadata": {}, @@ -2282,7 +2282,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1660> >" + " *' at 0x7f5a6030f870> >" ] }, "metadata": {}, @@ -2468,7 +2468,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1810> >" + " *' at 0x7f5a6030fbd0> >" ] }, "execution_count": 19, @@ -2544,7 +2544,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1930> >" + " *' at 0x7f5a6030f150> >" ] }, "execution_count": 20, @@ -2616,7 +2616,7 @@ "0->0\n", "\n", "\n", - "a\n", + "!a\n", "\n", "\n", "\n", @@ -2630,21 +2630,21 @@ "0->1\n", "\n", "\n", - "!a\n", + "a\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "a\n", + "!a\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", - "!a\n", + "a\n", "\n", "\n", "\n", @@ -2716,257 +2716,316 @@ { "data": { "text/html": [ - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", - "\n", - "0,0\n", + "\n", + "0,0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "0,1\n", + "\n", + "0,1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "1,1\n", + "\n", + "1,0\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "1,1\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !c\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "a & !c\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & c\n", - "\n", + "1->3\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "!a & b\n", "\n", - "\n", + "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & c\n", - "\n", + "2->2\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "3->1\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", - "
\n", - "\n", - "\n", - "Inf(\n", - "\n", - ")&Inf(\n", - "\n", - ")\n", - "[gen. Büchi 2]\n", + "
\n", + "\n", + "\n", + "Inf(\n", + "\n", + ")&Inf(\n", + "\n", + ")\n", + "[gen. Büchi 2]\n", "\n", "\n", "\n", "0\n", "\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "a & b\n", - "\n", + "\n", + "\n", + "!a & b\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & !c\n", - "\n", + "\n", + "\n", + "!a & !c\n", + "\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "a & c\n", - "\n", - "\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & !c\n", + "1->3\n", + "\n", + "\n", + "a & !c\n", "\n", - "\n", + "\n", "\n", - "1->2\n", - "\n", - "\n", - "!a & c\n", - "\n", + "1->3\n", + "\n", + "\n", + "a & c\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "a & !c\n", + "\n", + "\n", + "!a & b\n", "\n", - "\n", + "\n", "\n", - "2->1\n", - "\n", - "\n", - "a & c\n", - "\n", + "2->2\n", + "\n", + "\n", + "a & !b\n", + "\n", "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & !c\n", - "\n", + "2->3\n", + "\n", + "\n", + "a & b\n", + "\n", "\n", - "\n", + "\n", "\n", - "2->2\n", - "\n", - "\n", - "!a & c\n", - "\n", - "\n", + "3->1\n", + "\n", + "\n", + "!a & !c\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a & c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & !c\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "a & c\n", + "\n", + "\n", "\n", "\n", "
" @@ -3062,7 +3121,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1e40> >" + " *' at 0x7f5a6034ad20> >" ] }, "metadata": {}, @@ -3162,7 +3221,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c02c750> >" + " *' at 0x7f5a60301ba0> >" ] }, "execution_count": 24, @@ -3235,7 +3294,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c02c780> >" + " *' at 0x7f5a6030f9c0> >" ] }, "execution_count": 25, @@ -3399,7 +3458,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d1c03ed80> >" + " *' at 0x7f5a6030f750> >" ] }, "execution_count": 27, @@ -3482,7 +3541,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1e40> >" + " *' at 0x7f5a6034ad20> >" ] }, "metadata": {}, @@ -3547,7 +3606,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1e40> >" + " *' at 0x7f5a6034ad20> >" ] }, "metadata": {}, @@ -3634,7 +3693,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f0d077c1e40> >" + " *' at 0x7f5a6034ad20> >" ] }, "execution_count": 29, @@ -3667,7 +3726,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.7" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/twagraph-internals.ipynb b/tests/python/twagraph-internals.ipynb index 594e5c3eb..dbd366d7c 100644 --- a/tests/python/twagraph-internals.ipynb +++ b/tests/python/twagraph-internals.ipynb @@ -56,16 +56,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -84,7 +84,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -92,7 +92,7 @@ "0->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -106,14 +106,14 @@ "0->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -121,14 +121,14 @@ "1->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -136,7 +136,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -144,14 +144,14 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "execution_count": 3, @@ -217,142 +217,142 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -454,16 +454,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -495,7 +495,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -503,7 +503,7 @@ "0->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -517,14 +517,14 @@ "0->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -532,14 +532,14 @@ "1->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -547,7 +547,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -555,14 +555,14 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "metadata": {}, @@ -619,154 +619,154 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", "\n", "\n", "9\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -840,16 +840,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -881,7 +881,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -889,7 +889,7 @@ "0->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", @@ -897,7 +897,7 @@ "0->0\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -911,7 +911,7 @@ "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -919,14 +919,14 @@ "1->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -934,7 +934,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -942,14 +942,14 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "metadata": {}, @@ -1006,154 +1006,154 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", "\n", "\n", "9\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "a & b\n", - "\n", - "!a & b\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "!a & b\n", + "\n", + "a & b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "0\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "0\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -1200,16 +1200,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -1241,7 +1241,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1263,7 +1263,7 @@ "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1271,14 +1271,14 @@ "1->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1286,7 +1286,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1294,14 +1294,14 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "metadata": {}, @@ -1358,138 +1358,138 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "b\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -1542,16 +1542,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -1583,7 +1583,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1605,7 +1605,7 @@ "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1613,14 +1613,14 @@ "1->0\n", "\n", "\n", - "a & b\n", + "!a & b\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -1628,7 +1628,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -1636,7 +1636,7 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -1652,7 +1652,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "metadata": {}, @@ -1709,27 +1709,27 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", @@ -1738,67 +1738,67 @@ "9\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "b\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "{0,1}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", @@ -1807,53 +1807,53 @@ "1\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "9\n", "\n", "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -2072,27 +2072,27 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "\n", "8\n", @@ -2101,67 +2101,67 @@ "9\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "b\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{}\n", "\n", "{0,1}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0\n", @@ -2170,53 +2170,53 @@ "1\n", "\n", "next_succ\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "9\n", "\n", "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "2\n", @@ -2391,24 +2391,24 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", "\n", "\n", "7\n", @@ -2417,60 +2417,60 @@ "8\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", "\n", "1\n", "\n", "1\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", "\n", "{0,1}\n", "\n", "{}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "1\n", @@ -2479,47 +2479,47 @@ "0\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", "\n", "0\n", "\n", "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "1\n", @@ -2559,10 +2559,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -2604,144 +2604,144 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "cond\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "0\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "0\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "" @@ -2813,10 +2813,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -2858,128 +2858,128 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "cond\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "0\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "0\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "" @@ -3023,16 +3023,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -3064,7 +3064,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3078,7 +3078,7 @@ "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3099,7 +3099,7 @@ "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3107,7 +3107,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3115,7 +3115,7 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -3174,7 +3174,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "execution_count": 22, @@ -3198,10 +3198,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -3255,191 +3255,191 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "~3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", @@ -3458,26 +3458,26 @@ "\n", "\n", "props\n", - "prop_state_acc:\n", - "maybe\n", - "prop_inherently_weak:\n", - "maybe\n", - "prop_terminal:\n", - "maybe\n", - "prop_weak:\n", - "maybe\n", - "prop_very_weak:\n", - "maybe\n", - "prop_complete:\n", - "maybe\n", - "prop_universal:\n", - "maybe\n", - "prop_unambiguous:\n", - "maybe\n", - "prop_semi_deterministic:\n", - "maybe\n", - "prop_stutter_invariant:\n", - "maybe\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", "\n", "\n", "\n", @@ -3627,16 +3627,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -3690,7 +3690,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3698,7 +3698,7 @@ "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3719,7 +3719,7 @@ "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -3727,7 +3727,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -3735,7 +3735,7 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -3801,7 +3801,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "execution_count": 28, @@ -3838,10 +3838,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -3895,208 +3895,208 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", "\n", "cond\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", "\n", "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", "\n", "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "~3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", "\n", "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", "\n", "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "\n", - "~6\n", - "\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "#3\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", @@ -4115,26 +4115,26 @@ "\n", "\n", "props\n", - "prop_state_acc:\n", - "maybe\n", - "prop_inherently_weak:\n", - "maybe\n", - "prop_terminal:\n", - "maybe\n", - "prop_weak:\n", - "maybe\n", - "prop_very_weak:\n", - "maybe\n", - "prop_complete:\n", - "maybe\n", - "prop_universal:\n", - "maybe\n", - "prop_unambiguous:\n", - "maybe\n", - "prop_semi_deterministic:\n", - "maybe\n", - "prop_stutter_invariant:\n", - "maybe\n", + "prop_state_acc:\n", + "maybe\n", + "prop_inherently_weak:\n", + "maybe\n", + "prop_terminal:\n", + "maybe\n", + "prop_weak:\n", + "maybe\n", + "prop_very_weak:\n", + "maybe\n", + "prop_complete:\n", + "maybe\n", + "prop_universal:\n", + "maybe\n", + "prop_unambiguous:\n", + "maybe\n", + "prop_semi_deterministic:\n", + "maybe\n", + "prop_stutter_invariant:\n", + "maybe\n", "\n", "\n", "\n", @@ -4174,16 +4174,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -4237,7 +4237,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4245,7 +4245,7 @@ "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4266,7 +4266,7 @@ "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4274,7 +4274,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4282,7 +4282,7 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -4373,7 +4373,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "metadata": {}, @@ -4382,10 +4382,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -4436,240 +4436,240 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", - "\n", - "\n", - "10\n", - "\n", - "cond\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "a\n", - "\n", - "!a\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "~10\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "10\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "a\n", + "\n", + "!a\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "~10\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "10\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "\n", - "~6\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "~10\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "#3\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "~10\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", @@ -4704,16 +4704,16 @@ "\n", "\n", - "\n", + "\n", "\n", - "\n", - "Fin(\n", - "\n", - ") & Inf(\n", - "\n", - ")\n", - "[Rabin 1]\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[Rabin 1]\n", "\n", "\n", "\n", @@ -4767,7 +4767,7 @@ "0->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4775,7 +4775,7 @@ "0->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4796,7 +4796,7 @@ "1->0\n", "\n", "\n", - "a & !b\n", + "!a & !b\n", "\n", "\n", "\n", @@ -4804,7 +4804,7 @@ "1->1\n", "\n", "\n", - "!a & !b\n", + "a & !b\n", "\n", "\n", "\n", @@ -4812,7 +4812,7 @@ "1->1\n", "\n", "\n", - "!a & b\n", + "a & b\n", "\n", "\n", "\n", @@ -4886,7 +4886,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2950267b40> >" + " *' at 0x7f7e3c439b10> >" ] }, "metadata": {}, @@ -4895,10 +4895,10 @@ { "data": { "image/svg+xml": [ - "\n", + "\n", "\n", "g\n", - "\n", + "\n", "\n", "\n", "states\n", @@ -4949,227 +4949,227 @@ "\n", "\n", "edges\n", - "\n", - "\n", - "edges\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "4\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "\n", - "8\n", - "\n", - "\n", - "9\n", - "\n", - "\n", - "10\n", - "\n", - "cond\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "a\n", - "\n", - "a & !b\n", - "\n", - "!a & !b\n", - "\n", - "!a & b\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "!a\n", - "\n", - "1\n", - "\n", - "acc\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "{1}\n", - "\n", - "{0,1}\n", - "\n", - "{}\n", - "\n", - "{0}\n", - "\n", - "{0}\n", - "\n", - "dst\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "~0\n", - "\n", - "next_succ\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "0\n", - "\n", - "\n", - "5\n", - "\n", - "\n", - "6\n", - "\n", - "\n", - "7\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "10\n", - "\n", - "0\n", - "\n", - "src\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "3\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "edges\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "4\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "\n", + "8\n", + "\n", + "\n", + "9\n", + "\n", + "\n", + "10\n", + "\n", + "cond\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a\n", + "\n", + "!a & !b\n", + "\n", + "a & !b\n", + "\n", + "a & b\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "!a\n", + "\n", + "1\n", + "\n", + "acc\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "{1}\n", + "\n", + "{0,1}\n", + "\n", + "{}\n", + "\n", + "{0}\n", + "\n", + "{0}\n", + "\n", + "dst\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "~0\n", + "\n", + "next_succ\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "0\n", + "\n", + "\n", + "5\n", + "\n", + "\n", + "6\n", + "\n", + "\n", + "7\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "10\n", + "\n", + "0\n", + "\n", + "src\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "\n", + "3\n", + "\n", + "\n", + "3\n", "\n", "\n", "\n", "dests\n", - "\n", - "\n", - "dests\n", - "\n", - "\n", - "~0\n", - "\n", - "\n", - "\n", - "\n", - "~3\n", - "\n", - "\n", - "\n", - "\n", - "~6\n", - "\n", - "\n", - "\n", - "\n", - "#cnt/dst\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "3\n", - "\n", - "#2\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "#3\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "dests\n", + "\n", + "\n", + "~0\n", + "\n", + "\n", + "\n", + "\n", + "~3\n", + "\n", + "\n", + "\n", + "\n", + "~6\n", + "\n", + "\n", + "\n", + "\n", + "#cnt/dst\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "3\n", + "\n", + "#2\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "#3\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", @@ -5302,7 +5302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2950267270> >" + " *' at 0x7f7e3c3cf030> >" ] }, "metadata": {}, @@ -5593,7 +5593,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2950267270> >" + " *' at 0x7f7e3c3cf030> >" ] }, "metadata": {}, @@ -5802,7 +5802,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.4" + "version": "3.7.3" } }, "nbformat": 4,