diff --git a/NEWS b/NEWS index 889cc488b..7df22e3e5 100644 --- a/NEWS +++ b/NEWS @@ -108,6 +108,12 @@ New in spot 2.7.5.dev (not yet released) colorize_parity() learned that coloring transitiant edges does not require the introduction of a new color. + - A new reduce_parity() function implements and generalizes the + algorithm for minimizing parity acceptance by Carton and Maceiras + (Computing the Rabin index of a parity automaton, 1999). This is + a better replacement for cleanup_parity() and colorize_parity(). + See https://spot.lrde.epita.fr/ipynb/parity.html for examples. + New in spot 2.7.5 (2019-06-05) Build: diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index 3446721e7..35ec10a90 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -23,6 +23,7 @@ #include #include #include +#include #include #include #include @@ -386,4 +387,247 @@ namespace spot return aut; } + twa_graph_ptr + reduce_parity(const const_twa_graph_ptr& aut, bool colored) + { + return reduce_parity_here(make_twa_graph(aut, twa::prop_set::all()), + colored); + } + + twa_graph_ptr + reduce_parity_here(twa_graph_ptr aut, bool colored) + { + unsigned num_sets = aut->num_sets(); + if (!colored && num_sets == 0) + return aut; + + bool current_max; + bool current_odd; + if (!aut->acc().is_parity(current_max, current_odd, true)) + input_is_not_parity("reduce_parity"); + if (!aut->is_existential()) + throw std::runtime_error + ("reduce_parity_here() does not support alternation"); + + // The algorithm assumes "max odd" or "max even" parity. "min" + // parity is handled by converting it to "max" while the algorithm + // reads the automaton, and then back to "min" when it writes it. + // + // The main idea of the algorithm is to refine the SCCs of the + // automaton as will peel the parity layers one by one, starting + // with the maximum color. + // + // In the following tree, assume Sᵢ denotes SCCs and t. denotes a + // trivial SCC. Let's assume our original graph is made of one + // SCC S₁. In each SCC, we "peel the maximum layer", i.e., we + // remove the edges with the maximum colors. Doing so, we may + // introduce more sub-SCCs, in which we do this process + // recursively. + // + // S₁ + // | + // max=4 + // ╱ ╲ + // S₂ S₃ + // | | + // max=2 max=1 + // ╱ ╲ | + // S₄ t. t. + // | + // max=0 + // | + // t. + // + // Now the trick assign the same colors to all leaves, and then + // compress consecutive layers with identical parity. Let S₁[3] + // denote the transitions with color 3 in SCC S₁, let C(S₁[3]) + // denote the new color we will assign to those sets. + // + // Assume we decide C(t.)=k=2n, this is arbitrary and imaginary + // (as there are no transitions to color in t.) + // + // Then + // C(S₄[0])=k because 0 and C(t.)=k have same parity + // C(S₂[2])=k because 2 and max(C(S₄[0]),C(t.)) have same parity + // C(S₃[1])=k+1 because 1 and C(t.)=k have different parity + // C(S₁[4])=k+2 because 4 and max(C(S₂[2]),C(S₃[1])) have different parity + // So in the case, the resulting automaton would use 3 colors, k,k+1,k+2. + // + // If we do the same computation with C(t.)=k=2n+1, the result is + // better: + // C(S₄[0])=k+1 because 0 and C(t.)=k have different parity + // C(S₂[2])=k+1 because 2 and max(C(S₄[0]),C(t.)) have same parity + // C(S₃[1])=k because 1 and C(t.)=k have same parity + // C(S₁[4])=k+1 because 4 and max(C(S₂[2]),C(S₃[1])) have same + // Here only two colors are needed. + // + // So the following code evaluates those two possible scenarios, + // using k=0 or k=1. + // + // -2 means the edge was never assigned a color. + std::vector piprime1(aut->num_edges() + 1, -2); // k=1 + std::vector piprime2(aut->num_edges() + 1, -2); // k=0 + bool sba = aut->prop_state_acc().is_true(); + + auto rec = + [&](const scc_and_mark_filter& filter, auto& self) -> std::pair + { + scc_info si(filter); + unsigned numscc = si.scc_count(); + std::pair res = {1, 0}; // k=1, k=0 + for (unsigned scc = 0; scc < numscc; ++scc) + if (!si.is_trivial(scc)) + { + int piri; // π(Rᵢ) + int color; // corresponding color, to deal with "min" kind + if (current_max) + { + piri = color = si.acc_sets_of(scc).max_set() - 1; + } + else + { + color = si.acc_sets_of(scc).min_set() - 1; + if (color < 0) + color = num_sets; + // The algorithm works with max parity, so reverse + // the color range. + piri = num_sets - color - 1; + } + std::pair m; + if (piri < 0) + { + // Uncolored transition. Always odd. + m = {1, 1}; + } + else + { + scc_and_mark_filter filter2(si, scc, {unsigned(color)}); + m = self(filter2, self); + m.first += (piri - m.first) & 1; + m.second += (piri - m.second) & 1; + } + for (unsigned state: si.states_of(scc)) + for (auto& e: aut->out(state)) + if ((sba || si.scc_of(e.dst) == scc) && + ((piri >= 0 && e.acc.has(color)) || (piri < 0 && !e.acc))) + { + unsigned en = aut->edge_number(e); + piprime1[en] = m.first; + piprime2[en] = m.second; + } + res.first = std::max(res.first, m.first); + res.second = std::max(res.second, m.second); + } + return res; + }; + scc_and_mark_filter filter1(aut, {}); + rec(filter1, rec); + + // compute the used range for each vector. + int min1 = num_sets; + int max1 = -2; + for (int m : piprime1) + { + if (m <= -2) + continue; + if (m < min1) + min1 = m; + if (m > max1) + max1 = m; + } + + if (SPOT_UNLIKELY(max1 == -2)) + { + aut->set_acceptance(0, spot::acc_cond::acc_code::f()); + return aut; + } + int min2 = num_sets; + int max2 = -2; + for (int m : piprime2) + { + if (m <= -2) + continue; + if (m < min2) + min2 = m; + if (m > max2) + max2 = m; + } + + unsigned size1 = max1 + 1 - min1; + unsigned size2 = max2 + 1 - min2; + if (size2 < size1) + { + std::swap(size1, size2); + std::swap(min1, min2); + std::swap(piprime1, piprime2); + } + + unsigned new_num_sets = size1; + if (current_max) + { + for (int& m : piprime1) + if (m > -2) + m -= min1; + else + m = 0; + } + else + { + for (int& m : piprime1) + if (m > -2) + m = new_num_sets - (m - min1) - 1; + else + m = new_num_sets - 1; + } + + // The parity style changes if we shift colors by an odd number. + bool new_odd = current_odd ^ (min1 & 1); + if (!current_max) + // Switching from min<->max changes the parity style every time + // the number of colors is even. If the input was "min", we + // switched once to "max" to apply the reduction and once again + // to go back to "min". So there are two points where the + // parity style may have changed. + new_odd ^= !(num_sets & 1) ^ !(new_num_sets & 1); + if (!colored) + { + new_odd ^= current_max; + new_num_sets -= 1; + + // It seems we have nothing to win by changing automata with a + // single set (unless we reduced it to 0 sets, of course). + if (new_num_sets == num_sets && num_sets == 1) + return aut; + } + + aut->set_acceptance(new_num_sets, + acc_cond::acc_code::parity(current_max, new_odd, + new_num_sets)); + if (colored) + for (auto& e: aut->edges()) + { + unsigned n = aut->edge_number(e); + e.acc = acc_cond::mark_t({unsigned(piprime1[n])}); + } + else if (current_max) + for (auto& e: aut->edges()) + { + unsigned n = piprime1[aut->edge_number(e)]; + if (n == 0) + e.acc = acc_cond::mark_t({}); + else + e.acc = acc_cond::mark_t({n - 1}); + } + else + for (auto& e: aut->edges()) + { + unsigned n = piprime1[aut->edge_number(e)]; + if (n >= new_num_sets) + e.acc = acc_cond::mark_t({}); + else + e.acc = acc_cond::mark_t({n}); + } + + return aut; + } } diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index cf0f6c4f9..11b48b6e5 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2016-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -133,4 +133,37 @@ namespace spot SPOT_API twa_graph_ptr colorize_parity_here(twa_graph_ptr aut, bool keep_style = false); /// @} + + + /// \brief Reduce the parity acceptance condition to use a minimal + /// number of colors. + /// + /// This implements an algorithm derived from the following article, + /// but generalized to all types of parity acceptance. + /** \verbatim + @Article{carton.99.ita, + author = {Olivier Carton and Ram{\'o}n Maceiras}, + title = {Computing the {R}abin index of a parity automaton}, + journal = {Informatique théorique et applications}, + year = {1999}, + volume = {33}, + number = {6}, + pages = {495--505} + } + \endverbatim */ + /// + /// The kind of parity (min/max) is preserved, but the style + /// (odd/even) may be altered to reduce the number of colors used. + /// + /// If \a colored is true, colored automata are output (this is what + /// the above paper assumes). Otherwise, the smallest or highest + /// colors (depending on the parity kind) is removed to simplify the + /// acceptance condition. + /// @{ + SPOT_API twa_graph_ptr + reduce_parity(const const_twa_graph_ptr& aut, bool colored = false); + + SPOT_API twa_graph_ptr + reduce_parity_here(twa_graph_ptr aut, bool colored = false); + /// @} } diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 89a24e724..7fd9ba889 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -384,6 +384,23 @@ int main() is_max, is_odd, acc_num_sets)) throw std::runtime_error("cleanup_parity: wrong acceptance."); } + + // Check reduce_parity + for (auto colored: { true, false }) + { + auto output = spot::reduce_parity(aut, colored); + if (!colored && !is_almost_colored(output)) + throw std::runtime_error( + "reduce_parity: too many acc on a transition."); + if (colored && !is_colored_printerr(output)) + throw std::runtime_error("reduce_parity: not colored."); + if (!are_equiv(aut, output)) + throw std::runtime_error("reduce_parity: not equivalent."); + if (!is_right_parity(output, to_parity_kind(is_max), + spot::parity_style_any, + is_max, is_odd, acc_num_sets)) + throw std::runtime_error("reduce_parity: wrong acceptance."); + } } } diff --git a/tests/python/parity.ipynb b/tests/python/parity.ipynb index 78ef0f806..dd78f25fd 100644 --- a/tests/python/parity.ipynb +++ b/tests/python/parity.ipynb @@ -6,7 +6,6 @@ "metadata": {}, "outputs": [], "source": [ - "from IPython.display import display\n", "import spot\n", "spot.setup()\n", "from spot.jupyter import display_inline\n", @@ -293,7 +292,8 @@ "\n", "- [`change_parity()`](#Change-parity) can be used to alter the [*style*](#Changing-the-style), or [*kind*](#Changing-the-kind) of a parity acceptance. For instance if you have an automaton with `parity min even` acceptance and want an automaton with `parity max odd`, this is the function to use.\n", "- [`colorize_parity()`](#Colorize-parity) transforms an automaton with parity acceptance into a colored automaton with parity acceptance (a.k.a., parity automaton).\n", - "- [`cleanup_parity()`](#Cleanup-parity) remove from the acceptance condition colors that are unused in the automaton, while keeping it a parity acceptance." + "- [`cleanup_parity()`](#Cleanup-parity) remove from the acceptance condition colors that are unused in the automaton, while keeping it a parity acceptance.\n", + "- [`reduce_parity()`](#Reduce-parity) minimize the number of colors used in the automaton, producing the smallest parity acceptance condition possible for this automaton." ] }, { @@ -3475,7 +3475,9 @@ "source": [ "# Cleanup parity\n", "\n", - "The `cleanup_parity()` functions remove all useless colors of an automaton with parity acceptance." + "The `cleanup_parity()` function removes useless colors of an automaton with parity acceptance.\n", + "This function is just looking at colors that do not occur in the automaton to perform the simplification.\n", + "For a stronger simplification, see [`reduce_parity()`](#Reduce-parity) below." ] }, { @@ -4217,7 +4219,980 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Here Rabin 1, co-Büchi, and Streett 1, are respectively the same as \"min odd 2\", \"max odd 1\", \"max odd 2\"." + "Here Rabin 1, co-Büchi, and Streett 1, are respectively the same as \"min odd 2\", \"max odd 1\", \"max odd 2\".\n", + "\n", + "# Reduce parity\n", + "\n", + "The `reduce_parity()` function is a more elaborate version of `cleanup_parity()`. It implements an algorithm by Carton and Maceiras (*Computing the Rabin index of a parity automaton*, Informatique théorique et applications, 1999), to obtain the minimal parity acceptance condition for a given automaton. Why the original algorithm assume *max odd* parity, this version with work with the four types of parity acceptance. It will only try to preserve the kind (max/min) and may change the style if it allows saving one color. Furthermore, it can colorize (or uncolorize) automata at the same time,\n", + "making it a very nice replacement for both `cleanup_parity()` and `colorize_parity()`.\n", + "\n", + "It takes two arguments:\n", + "1. the automaton whose parity acceptance condition should be reduced\n", + "2. a Boolean indicating whether the output should be colored (`True`), or if transition with no color can be used (`False`).\n", + "\n", + "By default, the second argument is `False`, because acceptance sets is a scarse ressource in Spot." + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")))\n", + "[parity min odd 4]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "f\n", + "[none]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")))\n", + "[parity min odd 4]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ")\n", + "[co-Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "display2(minodd4, spot.reduce_parity(minodd4))\n", + "display2(minodd4, spot.reduce_parity(minodd4, True))" + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")))\n", + "[parity max even 4]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")\n", + "[parity max even 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & Inf(\n", + "\n", + ")))\n", + "[parity max even 4]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))\n", + "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "display2(maxeven4, spot.reduce_parity(maxeven4))\n", + "display2(maxeven4, spot.reduce_parity(maxeven4, True))" ] } ],