From 0bf0a99d6d9dc83e4f2ce4807be490b09b6ec742 Mon Sep 17 00:00:00 2001
From: Laurent XU <laurent.xu@lrde.epita.fr>
Date: Wed, 1 Jun 2016 14:34:19 +0200
Subject: [PATCH] parity: add spot::colorize_parity()

These functions colorize automata with parity acceptance. They output
parity automata.

* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here
* tests/core/parity.cc: Add tests for spot::colorize_parity()
* tests/python/parity.ipynb: Add documentation about
spot::colorize_parity()
---
 spot/twaalgos/parity.cc   |  56 ++++
 spot/twaalgos/parity.hh   |  22 ++
 tests/core/parity.cc      |  42 +++
 tests/python/parity.ipynb | 649 +++++++++++++++++++++++++++++++++++++-
 4 files changed, 767 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc
index 43f48a9a3..eb835fac6 100644
--- a/spot/twaalgos/parity.cc
+++ b/spot/twaalgos/parity.cc
@@ -146,4 +146,60 @@ namespace spot
                change_style, output_max, current_max);
     return aut;
   }
+
+  twa_graph_ptr
+  colorize_parity(const const_twa_graph_ptr& aut, bool keep_style)
+  {
+    return colorize_parity_here(make_twa_graph(aut, twa::prop_set::all()),
+                                keep_style);
+  }
+
+  twa_graph_ptr
+  colorize_parity_here(twa_graph_ptr aut, bool keep_style)
+  {
+    bool current_max;
+    bool current_odd;
+    if (!aut->acc().is_parity(current_max, current_odd, true))
+      throw new std::invalid_argument("colorize_parity: input "
+                                      "must have a parity acceptance.");
+
+    bool has_empty = false;
+    for (const auto& e: aut->edges())
+      if (!e.acc)
+        {
+          has_empty = true;
+          break;
+        }
+    auto num_sets = aut->num_sets();
+    int incr = 0;
+    if (has_empty)
+      {
+        // If the automaton has a transition that belong to any set, we need to
+        // introduce a new acceptance set.
+        // We may want to add a second acceptance set to keep the style of
+        // the parity acceptance
+        incr = 1 + (keep_style && current_max);
+        num_sets += incr;
+        bool new_style = current_odd == (keep_style || !current_max);
+        auto new_acc = acc_cond::acc_code::parity(current_max,
+                                                  new_style, num_sets);
+        aut->set_acceptance(num_sets, new_acc);
+      }
+    if (current_max)
+      {
+        --incr;
+        for (auto& e: aut->edges())
+          {
+            auto maxset = e.acc.max_set();
+            e.acc = acc_cond::mark_t{maxset ? maxset + incr : incr};
+          }
+      }
+    else
+      {
+        auto unused_mark = num_sets - incr;
+        for (auto& e: aut->edges())
+          e.acc = e.acc ? e.acc.lowest() : acc_cond::mark_t{unused_mark};
+      }
+    return aut;
+  }
 }
diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh
index 385805d2d..df04af9fe 100644
--- a/spot/twaalgos/parity.hh
+++ b/spot/twaalgos/parity.hh
@@ -87,5 +87,27 @@ namespace spot
   SPOT_API twa_graph_ptr
   change_parity_here(twa_graph_ptr aut, parity_kind kind, parity_style style);
   /// @}
+
+  /// \brief Colorize an automaton with parity acceptance
+  ///
+  /// An automaton is said colored iff all the transitions belong to exactly one
+  /// acceptance set. The algorithm achieves thiat by removing superfluous
+  /// acceptance marks. It may introduce a new set to mark the transitions with
+  /// no acceptance sets and a second set may be introduced to keep the style.
+  /// The input must be an automaton with a parity acceptance, otherwise an
+  /// invalid_argument exception is thrown.
+  ///
+  /// \param aut the input automaton
+  ///
+  /// \param keep_style whether the style of the parity acc is kept.
+  ///
+  /// \return the colorized automaton
+  /// @{
+  SPOT_API twa_graph_ptr
+  colorize_parity(const const_twa_graph_ptr& aut, bool keep_style = false);
+
+  SPOT_API twa_graph_ptr
+  colorize_parity_here(twa_graph_ptr aut, bool keep_style = false);
+  /// @}
   /// @}
 }
diff --git a/tests/core/parity.cc b/tests/core/parity.cc
index 49193e3a1..0c7e2904b 100644
--- a/tests/core/parity.cc
+++ b/tests/core/parity.cc
@@ -22,6 +22,7 @@
 #include <vector>
 #include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/iscolored.hh>
 #include <spot/twaalgos/parity.hh>
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/randomgraph.hh>
@@ -269,6 +270,32 @@ static bool is_almost_colored(spot::const_twa_graph_ptr aut)
   return true;
 }
 
+static bool is_colored_printerr(spot::const_twa_graph_ptr aut)
+{
+  bool result = is_colored(aut);
+  if (!result)
+    {
+      std::cerr << "======Not colored======" << std::endl;
+      spot::print_hoa(std::cerr, aut);
+      std::cerr << std::endl;
+    }
+  return result;
+}
+
+static spot::parity_kind to_parity_kind(bool is_max)
+{
+  if (is_max)
+    return spot::parity_kind_max;
+  return spot::parity_kind_min;
+}
+
+static spot::parity_style to_parity_style(bool is_odd)
+{
+  if (is_odd)
+    return spot::parity_style_odd;
+  return spot::parity_style_even;
+}
+
 int main()
 {
   auto current_bdd = spot::make_bdd_dict();
@@ -323,6 +350,21 @@ int main()
                   assert(is_almost_colored(output)
                          && "change_parity: too many acc on a transition");
                 }
+            // Check colorize_parity
+            for (auto keep_style: { true, false })
+              {
+                auto output = spot::colorize_parity(aut, keep_style);
+                assert(is_colored_printerr(output)
+                       && "colorize_parity: not colored.");
+                assert(are_equiv(aut, output)
+                       && "colorize_parity: not equivalent.");
+                auto target_kind = to_parity_kind(is_max);
+                auto target_style = keep_style ? to_parity_style(is_odd)
+                                    : spot::parity_style_any;
+                assert(is_right_parity(output, target_kind, target_style,
+                                       is_max, is_odd, acc_num_sets)
+                       && "change_parity: wrong acceptance.");
+              }
           }
         }
   return 0;
diff --git a/tests/python/parity.ipynb b/tests/python/parity.ipynb
index a04270c08..1fe189586 100644
--- a/tests/python/parity.ipynb
+++ b/tests/python/parity.ipynb
@@ -123,8 +123,8 @@
      "cell_type": "markdown",
      "metadata": {},
      "source": [
-      "##To toggle **style**\n",
-      "###A new acceptance set is introduced and all the existing sets' indexes are increased by 1.\n",
+      "## To toggle **style**\n",
+      "### A new acceptance set is introduced and all the existing sets' indexes are increased by 1.\n",
       "#### Parity max odd 5 -> Parity max even\n",
       "If the acceptance is a parity **max**, all the transitions that do not belong to any acceptance set will belong to the new set."
      ]
@@ -1303,6 +1303,651 @@
       }
      ],
      "prompt_number": 10
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "# Colorize parity\n",
+      "An automaton with a parity acceptance is not necessarily a parity automaton. It must be colored to be qualified like this.\n",
+      "## Parity max\n",
+      "Transitions with multiple acceptance sets are purified by keeping only the set with the greatest index.\n",
+      "<br>\n",
+      "If there is a transition that do not belong to any acceptance set, a new acceptance set is introduced at the least significant place.\n",
+      "<br>\n",
+      "The least significant place of a parity max acceptance is where the indexes are the lowest, so all the existing acceptance sets' indexes will be shifted.\n",
+      "#### Colorize parity max odd 4"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "aut_max_odd4 = tuple(spot.automata(\"randaut -A 'parity max odd 4' -Q4 2|\"))[0]\n",
+      "display(aut_max_odd4.show(\".a\"))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"173pt\" viewBox=\"0.00 0.00 498.00 172.97\" width=\"498pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 168.967)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-168.967 494,-168.967 494,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"131\" y=\"-150.767\">Inf(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"153\" y=\"-150.767\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-150.767\">) | (Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212\" y=\"-150.767\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"228\" y=\"-150.767\">) &amp; (Inf(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"275\" y=\"-150.767\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"291\" y=\"-150.767\">) | Fin(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"331\" y=\"-150.767\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"347\" y=\"-150.767\">)))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"187.5\" y=\"-136.767\">[parity max odd 4]</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-34.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-31.2672\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.15491,-34.9672C2.79388,-34.9672 17.1543,-34.9672 30.6317,-34.9672\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-34.9672 30.9419,-38.1173 34.4419,-34.9673 30.9419,-34.9673 30.9419,-34.9673 30.9419,-34.9673 34.4419,-34.9673 30.9418,-31.8173 37.9419,-34.9672 37.9419,-34.9672\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"341\" cy=\"-54.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"341\" y=\"-51.2672\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M69.4499,-47.0403C88.8327,-64.9003 128.25,-97.5832 169,-109.967 223.827,-126.629 288.046,-91.0362 319.928,-69.6185\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"325.861,-65.5436 321.874,-72.1033 322.976,-67.5252 320.091,-69.5068 320.091,-69.5068 320.091,-69.5068 322.976,-67.5252 318.307,-66.9102 325.861,-65.5436 325.861,-65.5436\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-117.767\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"198.5\" cy=\"-34.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"198.5\" y=\"-31.2672\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
+        "<path d=\"M74.2281,-34.9672C98.9818,-34.9672 144.734,-34.9672 173,-34.9672\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"180.131,-34.9672 173.131,-38.1173 176.631,-34.9673 173.131,-34.9673 173.131,-34.9673 173.131,-34.9673 176.631,-34.9673 173.131,-31.8173 180.131,-34.9672 180.131,-34.9672\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-38.7672\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
+        "<ellipse cx=\"472\" cy=\"-21.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"472\" y=\"-18.2672\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M358.945,-53.1953C378.006,-50.9067 409.731,-46.204 436,-37.9672 440.351,-36.6029 444.87,-34.8289 449.158,-32.9605\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"455.648,-29.9922 450.592,-35.7682 452.465,-31.4479 449.282,-32.9036 449.282,-32.9036 449.282,-32.9036 452.465,-31.4479 447.972,-30.0389 455.648,-29.9922 455.648,-29.9922\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379\" y=\"-53.7672\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M216.448,-37.3797C241.237,-40.9085 287.508,-47.4951 315.852,-51.5298\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"322.992,-52.5462 315.618,-54.6782 319.527,-52.0529 316.062,-51.5596 316.062,-51.5596 316.062,-51.5596 319.527,-52.0529 316.506,-48.4411 322.992,-52.5462 322.992,-52.5462\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246\" y=\"-52.7672\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
+        "<path d=\"M186.254,-48.6342C181.355,-59.6235 185.438,-70.9672 198.5,-70.9672 208.705,-70.9672 213.429,-64.0436 212.672,-55.7744\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"210.746,-48.6342 215.61,-54.5727 211.657,-52.0135 212.569,-55.3928 212.569,-55.3928 212.569,-55.3928 211.657,-52.0135 209.527,-56.213 210.746,-48.6342 210.746,-48.6342\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171\" y=\"-89.7672\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-74.7672\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
+        "<path d=\"M454.855,-15.8181C449.005,-13.8784 442.289,-11.9787 436,-10.9672 324.273,7.00199 222.337,-1.62898 169,-7.96725 137.816,-11.673 102.754,-20.9893 80.3007,-27.6402\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.4747,-29.6954 79.2693,-24.6609 76.8261,-28.6863 80.1775,-27.6772 80.1775,-27.6772 80.1775,-27.6772 76.8261,-28.6863 81.0856,-30.6934 73.4747,-29.6954 73.4747,-29.6954\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248\" y=\"-19.7672\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-5.76725\">\u24ff</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"275.5\" y=\"-5.76725\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
+        "<path d=\"M454.009,-18.6202C434.631,-15.5892 402.355,-12.9681 377,-22.9672 369.877,-25.7764 363.31,-30.7676 357.836,-35.9848\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"352.745,-41.2049 355.377,-33.9942 355.189,-38.6992 357.632,-36.1934 357.632,-36.1934 357.632,-36.1934 355.189,-38.6992 359.887,-38.3927 352.745,-41.2049 352.745,-41.2049\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377\" y=\"-26.7672\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 11
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "The new acceptance sets are:\n",
+      "+ \u2205 -> 0\n",
+      "+ 0 -> 1\n",
+      "+ 1 -> 2\n",
+      "+ 2 -> 3\n",
+      "+ 3 -> 4\n",
+      "\n",
+      "#### The result of colorizing the given parity max odd 4 is"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "aut_max_odd4_colored = spot.colorize_parity(aut_max_odd4, False)\n",
+      "display(aut_max_odd4_colored.show(\".a\"))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"192pt\" viewBox=\"0.00 0.00 498.00 192.17\" width=\"498pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 188.174)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-188.174 494,-188.174 494,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-169.974\">Inf(</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"120\" y=\"-169.974\">\u2779</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136\" y=\"-169.974\">) | (Fin(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"179\" y=\"-169.974\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"195\" y=\"-169.974\">) &amp; (Inf(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-169.974\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258\" y=\"-169.974\">) | (Fin(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"301\" y=\"-169.974\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"317\" y=\"-169.974\">) &amp; Inf(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"360\" y=\"-169.974\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"376\" y=\"-169.974\">))))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184.5\" y=\"-155.974\">[parity max even 5]</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-36.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-32.4739\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.15491,-36.1739C2.79388,-36.1739 17.1543,-36.1739 30.6317,-36.1739\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-36.1739 30.9419,-39.324 34.4419,-36.174 30.9419,-36.174 30.9419,-36.174 30.9419,-36.174 34.4419,-36.174 30.9418,-33.024 37.9419,-36.1739 37.9419,-36.1739\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"341\" cy=\"-67.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"341\" y=\"-63.4739\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M68.8658,-49.3629C75.3091,-56.077 83.6495,-64.0842 92,-70.1739 123.326,-93.0188 131.383,-101.783 169,-111.174 228.214,-125.956 249.552,-117.676 305,-92.1739 310.438,-89.6728 315.902,-86.287 320.842,-82.8157\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"326.779,-78.4332 323.018,-85.1249 323.963,-80.5119 321.147,-82.5906 321.147,-82.5906 321.147,-82.5906 323.963,-80.5119 319.276,-80.0563 326.779,-78.4332 326.779,-78.4332\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-136.974\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-121.974\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"198.5\" cy=\"-36.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"198.5\" y=\"-32.4739\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
+        "<path d=\"M74.2281,-36.1739C98.9818,-36.1739 144.734,-36.1739 173,-36.1739\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"180.131,-36.1739 173.131,-39.324 176.631,-36.174 173.131,-36.174 173.131,-36.174 173.131,-36.174 176.631,-36.174 173.131,-33.024 180.131,-36.1739 180.131,-36.1739\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-54.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113.5\" y=\"-39.9739\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
+        "<ellipse cx=\"472\" cy=\"-23.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"472\" y=\"-19.4739\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M359.121,-67.7218C378.619,-67.7008 411.005,-65.6719 436,-54.1739 442.747,-51.07 449.143,-46.2246 454.576,-41.2792\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"459.665,-36.3612 456.82,-43.4907 457.148,-38.7933 454.631,-41.2254 454.631,-41.2254 454.631,-41.2254 457.148,-38.7933 452.443,-38.9602 459.665,-36.3612 459.665,-36.3612\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379\" y=\"-84.9739\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-69.9739\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M216.169,-39.8518C240.991,-45.3286 287.787,-55.6537 316.204,-61.9235\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"323.353,-63.5009 315.838,-65.0686 319.935,-62.7467 316.517,-61.9926 316.517,-61.9926 316.517,-61.9926 319.935,-62.7467 317.196,-58.9166 323.353,-63.5009 323.353,-63.5009\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246\" y=\"-76.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-61.9739\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
+        "<path d=\"M186.254,-49.8409C181.355,-60.8302 185.438,-72.1739 198.5,-72.1739 208.705,-72.1739 213.429,-65.2502 212.672,-56.981\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"210.746,-49.8409 215.61,-55.7793 211.657,-53.2202 212.569,-56.5995 212.569,-56.5995 212.569,-56.5995 211.657,-53.2202 209.527,-57.4197 210.746,-49.8409 210.746,-49.8409\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171\" y=\"-90.9739\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-75.9739\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
+        "<path d=\"M455.252,-16.574C449.326,-14.4123 442.458,-12.2821 436,-11.1739 323.418,8.1465 222.082,-2.86597 169,-9.17391 137.816,-12.8797 102.754,-22.1959 80.3007,-28.8468\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.4747,-30.902 79.2693,-25.8676 76.8261,-29.8929 80.1775,-28.8838 80.1775,-28.8838 80.1775,-28.8838 76.8261,-29.8929 81.0856,-31.9001 73.4747,-30.902 73.4747,-30.902\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248\" y=\"-20.9739\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-5.97391\">\u2778</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
+        "<path d=\"M454.418,-19.2927C434.853,-15.5987 401.846,-12.1988 377,-24.1739 367.603,-28.7031 359.889,-37.1039 354.118,-45.2865\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"350.088,-51.4335 351.292,-43.8524 352.007,-48.5065 353.926,-45.5795 353.926,-45.5795 353.926,-45.5795 352.007,-48.5065 356.56,-47.3067 350.088,-51.4335 350.088,-51.4335\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377\" y=\"-42.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-27.9739\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 12
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "You can notice that the **style** has been toggled.\n",
+      "<br>\n",
+      "To prevent colorize_parity from this we can add one extra acceptance set in the acceptance condition.\n",
+      "\n",
+      "The new acceptance sets are now:\n",
+      "+ \u2205 -> 1\n",
+      "+ 0 -> 2\n",
+      "+ 1 -> 3\n",
+      "+ 2 -> 4\n",
+      "+ 3 -> 5\n",
+      "#### The result of colorizing the given parity max odd 4 without changing the style is"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "aut_max_odd4_colored_bis = spot.colorize_parity(aut_max_odd4, True)\n",
+      "display(aut_max_odd4_colored_bis.show(\".a\"))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"192pt\" viewBox=\"0.00 0.00 498.00 192.17\" width=\"498pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 188.174)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-188.174 494,-188.174 494,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"66.5\" y=\"-169.974\">Inf(</text>\n",
+        "<text fill=\"#e31a1c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"88.5\" y=\"-169.974\">\u277a</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"104.5\" y=\"-169.974\">) | (Fin(</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"147.5\" y=\"-169.974\">\u2779</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"163.5\" y=\"-169.974\">) &amp; (Inf(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210.5\" y=\"-169.974\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.5\" y=\"-169.974\">) | (Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269.5\" y=\"-169.974\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"285.5\" y=\"-169.974\">) &amp; (Inf(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"332.5\" y=\"-169.974\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"348.5\" y=\"-169.974\">) | Fin(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-169.974\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-169.974\">)))))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"187.5\" y=\"-155.974\">[parity max odd 6]</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-36.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-32.4739\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.15491,-36.1739C2.79388,-36.1739 17.1543,-36.1739 30.6317,-36.1739\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-36.1739 30.9419,-39.324 34.4419,-36.174 30.9419,-36.174 30.9419,-36.174 30.9419,-36.174 34.4419,-36.174 30.9418,-33.024 37.9419,-36.1739 37.9419,-36.1739\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"341\" cy=\"-67.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"341\" y=\"-63.4739\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M68.8658,-49.3629C75.3091,-56.077 83.6495,-64.0842 92,-70.1739 123.326,-93.0188 131.383,-101.783 169,-111.174 228.214,-125.956 249.552,-117.676 305,-92.1739 310.438,-89.6728 315.902,-86.287 320.842,-82.8157\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"326.779,-78.4332 323.018,-85.1249 323.963,-80.5119 321.147,-82.5906 321.147,-82.5906 321.147,-82.5906 323.963,-80.5119 319.276,-80.0563 326.779,-78.4332 326.779,-78.4332\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-136.974\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-121.974\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"198.5\" cy=\"-36.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"198.5\" y=\"-32.4739\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
+        "<path d=\"M74.2281,-36.1739C98.9818,-36.1739 144.734,-36.1739 173,-36.1739\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"180.131,-36.1739 173.131,-39.324 176.631,-36.174 173.131,-36.174 173.131,-36.174 173.131,-36.174 176.631,-36.174 173.131,-33.024 180.131,-36.1739 180.131,-36.1739\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-54.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113.5\" y=\"-39.9739\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
+        "<ellipse cx=\"472\" cy=\"-23.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"472\" y=\"-19.4739\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M359.121,-67.7218C378.619,-67.7008 411.005,-65.6719 436,-54.1739 442.747,-51.07 449.143,-46.2246 454.576,-41.2792\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"459.665,-36.3612 456.82,-43.4907 457.148,-38.7933 454.631,-41.2254 454.631,-41.2254 454.631,-41.2254 457.148,-38.7933 452.443,-38.9602 459.665,-36.3612 459.665,-36.3612\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379\" y=\"-84.9739\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-69.9739\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M216.169,-39.8518C240.991,-45.3286 287.787,-55.6537 316.204,-61.9235\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"323.353,-63.5009 315.838,-65.0686 319.935,-62.7467 316.517,-61.9926 316.517,-61.9926 316.517,-61.9926 319.935,-62.7467 317.196,-58.9166 323.353,-63.5009 323.353,-63.5009\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246\" y=\"-76.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-61.9739\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
+        "<path d=\"M186.254,-49.8409C181.355,-60.8302 185.438,-72.1739 198.5,-72.1739 208.705,-72.1739 213.429,-65.2502 212.672,-56.981\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"210.746,-49.8409 215.61,-55.7793 211.657,-53.2202 212.569,-56.5995 212.569,-56.5995 212.569,-56.5995 211.657,-53.2202 209.527,-57.4197 210.746,-49.8409 210.746,-49.8409\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171\" y=\"-90.9739\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-75.9739\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
+        "<path d=\"M455.252,-16.574C449.326,-14.4123 442.458,-12.2821 436,-11.1739 323.418,8.1465 222.082,-2.86597 169,-9.17391 137.816,-12.8797 102.754,-22.1959 80.3007,-28.8468\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.4747,-30.902 79.2693,-25.8676 76.8261,-29.8929 80.1775,-28.8838 80.1775,-28.8838 80.1775,-28.8838 76.8261,-29.8929 81.0856,-31.9001 73.4747,-30.902 73.4747,-30.902\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248\" y=\"-20.9739\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-5.97391\">\u2779</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
+        "<path d=\"M454.418,-19.2927C434.853,-15.5987 401.846,-12.1988 377,-24.1739 367.603,-28.7031 359.889,-37.1039 354.118,-45.2865\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"350.088,-51.4335 351.292,-43.8524 352.007,-48.5065 353.926,-45.5795 353.926,-45.5795 353.926,-45.5795 352.007,-48.5065 356.56,-47.3067 350.088,-51.4335 350.088,-51.4335\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377\" y=\"-42.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-27.9739\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 13
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "## Parity min\n",
+      "Transitions with multiple acceptance sets are purified by keeping only the set with the lowest index.\n",
+      "<br>\n",
+      "If there is a transition that do not belong to any acceptance set, a new acceptance set is introduced at the least significant place.\n",
+      "<br>\n",
+      "The least significant place of a parity min acceptance is where the indexes are the greatest.\n",
+      "#### Colorize parity min odd 4"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "aut_min_odd4 = tuple(spot.automata(\"randaut -A 'parity min odd 4' -Q4 2|\"))[0]\n",
+      "display(aut_min_odd4.show(\".a\"))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"173pt\" viewBox=\"0.00 0.00 498.00 172.97\" width=\"498pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 168.967)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-168.967 494,-168.967 494,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"128\" y=\"-150.767\">Fin(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"153\" y=\"-150.767\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-150.767\">) &amp; (Inf(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"216\" y=\"-150.767\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"232\" y=\"-150.767\">) | (Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"275\" y=\"-150.767\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"291\" y=\"-150.767\">) &amp; Inf(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"334\" y=\"-150.767\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"350\" y=\"-150.767\">)))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188\" y=\"-136.767\">[parity min odd 4]</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-34.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-31.2672\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.15491,-34.9672C2.79388,-34.9672 17.1543,-34.9672 30.6317,-34.9672\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-34.9672 30.9419,-38.1173 34.4419,-34.9673 30.9419,-34.9673 30.9419,-34.9673 30.9419,-34.9673 34.4419,-34.9673 30.9418,-31.8173 37.9419,-34.9672 37.9419,-34.9672\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"341\" cy=\"-54.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"341\" y=\"-51.2672\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M69.4499,-47.0403C88.8327,-64.9003 128.25,-97.5832 169,-109.967 223.827,-126.629 288.046,-91.0362 319.928,-69.6185\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"325.861,-65.5436 321.874,-72.1033 322.976,-67.5252 320.091,-69.5068 320.091,-69.5068 320.091,-69.5068 322.976,-67.5252 318.307,-66.9102 325.861,-65.5436 325.861,-65.5436\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-117.767\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"198.5\" cy=\"-34.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"198.5\" y=\"-31.2672\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
+        "<path d=\"M74.2281,-34.9672C98.9818,-34.9672 144.734,-34.9672 173,-34.9672\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"180.131,-34.9672 173.131,-38.1173 176.631,-34.9673 173.131,-34.9673 173.131,-34.9673 173.131,-34.9673 176.631,-34.9673 173.131,-31.8173 180.131,-34.9672 180.131,-34.9672\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-38.7672\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
+        "<ellipse cx=\"472\" cy=\"-21.9672\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"472\" y=\"-18.2672\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M358.945,-53.1953C378.006,-50.9067 409.731,-46.204 436,-37.9672 440.351,-36.6029 444.87,-34.8289 449.158,-32.9605\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"455.648,-29.9922 450.592,-35.7682 452.465,-31.4479 449.282,-32.9036 449.282,-32.9036 449.282,-32.9036 452.465,-31.4479 447.972,-30.0389 455.648,-29.9922 455.648,-29.9922\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379\" y=\"-53.7672\">!p0 &amp; p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M216.448,-37.3797C241.237,-40.9085 287.508,-47.4951 315.852,-51.5298\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"322.992,-52.5462 315.618,-54.6782 319.527,-52.0529 316.062,-51.5596 316.062,-51.5596 316.062,-51.5596 319.527,-52.0529 316.506,-48.4411 322.992,-52.5462 322.992,-52.5462\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246\" y=\"-52.7672\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
+        "<path d=\"M186.254,-48.6342C181.355,-59.6235 185.438,-70.9672 198.5,-70.9672 208.705,-70.9672 213.429,-64.0436 212.672,-55.7744\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"210.746,-48.6342 215.61,-54.5727 211.657,-52.0135 212.569,-55.3928 212.569,-55.3928 212.569,-55.3928 211.657,-52.0135 209.527,-56.213 210.746,-48.6342 210.746,-48.6342\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171\" y=\"-89.7672\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-74.7672\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
+        "<path d=\"M454.855,-15.8181C449.005,-13.8784 442.289,-11.9787 436,-10.9672 324.273,7.00199 222.337,-1.62898 169,-7.96725 137.816,-11.673 102.754,-20.9893 80.3007,-27.6402\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.4747,-29.6954 79.2693,-24.6609 76.8261,-28.6863 80.1775,-27.6772 80.1775,-27.6772 80.1775,-27.6772 76.8261,-28.6863 81.0856,-30.6934 73.4747,-29.6954 73.4747,-29.6954\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248\" y=\"-19.7672\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-5.76725\">\u24ff</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"275.5\" y=\"-5.76725\">\u2777</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
+        "<path d=\"M454.009,-18.6202C434.631,-15.5892 402.355,-12.9681 377,-22.9672 369.877,-25.7764 363.31,-30.7676 357.836,-35.9848\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"352.745,-41.2049 355.377,-33.9942 355.189,-38.6992 357.632,-36.1934 357.632,-36.1934 357.632,-36.1934 355.189,-38.6992 359.887,-38.3927 352.745,-41.2049 352.745,-41.2049\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377\" y=\"-26.7672\">!p0 &amp; !p1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 14
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "The new acceptance sets are:\n",
+      "+ \u2205 -> 4\n",
+      "+ 0 -> 0\n",
+      "+ 1 -> 1\n",
+      "+ 2 -> 2\n",
+      "+ 3 -> 3\n",
+      "\n",
+      "#### The result of colorizing the given parity max odd 4 is"
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "aut_min_odd4_colored_bis = spot.colorize_parity(aut_min_odd4, True)\n",
+      "display(aut_min_odd4_colored_bis.show(\".a\"))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"192pt\" viewBox=\"0.00 0.00 498.00 192.17\" width=\"498pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 188.174)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-188.174 494,-188.174 494,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"96\" y=\"-169.974\">Fin(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"121\" y=\"-169.974\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"137\" y=\"-169.974\">) &amp; (Inf(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"184\" y=\"-169.974\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"200\" y=\"-169.974\">) | (Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"243\" y=\"-169.974\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259\" y=\"-169.974\">) &amp; (Inf(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"306\" y=\"-169.974\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"322\" y=\"-169.974\">) | Fin(</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"362\" y=\"-169.974\">\u2779</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"378\" y=\"-169.974\">))))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"188\" y=\"-155.974\">[parity min odd 5]</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-36.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-32.4739\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.15491,-36.1739C2.79388,-36.1739 17.1543,-36.1739 30.6317,-36.1739\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-36.1739 30.9419,-39.324 34.4419,-36.174 30.9419,-36.174 30.9419,-36.174 30.9419,-36.174 34.4419,-36.174 30.9418,-33.024 37.9419,-36.1739 37.9419,-36.1739\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>2</title>\n",
+        "<ellipse cx=\"341\" cy=\"-67.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"341\" y=\"-63.4739\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;2</title>\n",
+        "<path d=\"M68.8658,-49.3629C75.3091,-56.077 83.6495,-64.0842 92,-70.1739 123.326,-93.0188 131.383,-101.783 169,-111.174 228.214,-125.956 249.552,-117.676 305,-92.1739 310.438,-89.6728 315.902,-86.287 320.842,-82.8157\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"326.779,-78.4332 323.018,-85.1249 323.963,-80.5119 321.147,-82.5906 321.147,-82.5906 321.147,-82.5906 323.963,-80.5119 319.276,-80.0563 326.779,-78.4332 326.779,-78.4332\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"169\" y=\"-136.974\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-121.974\">\u2779</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>3</title>\n",
+        "<ellipse cx=\"198.5\" cy=\"-36.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"198.5\" y=\"-32.4739\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;3</title>\n",
+        "<path d=\"M74.2281,-36.1739C98.9818,-36.1739 144.734,-36.1739 173,-36.1739\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"180.131,-36.1739 173.131,-39.324 176.631,-36.174 173.131,-36.174 173.131,-36.174 173.131,-36.174 176.631,-36.174 173.131,-33.024 180.131,-36.1739 180.131,-36.1739\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-54.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113.5\" y=\"-39.9739\">\u2779</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>1</title>\n",
+        "<ellipse cx=\"472\" cy=\"-23.1739\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"472\" y=\"-19.4739\">1</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;1</title>\n",
+        "<path d=\"M359.121,-67.7218C378.619,-67.7008 411.005,-65.6719 436,-54.1739 442.747,-51.07 449.143,-46.2246 454.576,-41.2792\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"459.665,-36.3612 456.82,-43.4907 457.148,-38.7933 454.631,-41.2254 454.631,-41.2254 454.631,-41.2254 457.148,-38.7933 452.443,-38.9602 459.665,-36.3612 459.665,-36.3612\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379\" y=\"-84.9739\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-69.9739\">\u2779</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<path d=\"M216.169,-39.8518C240.991,-45.3286 287.787,-55.6537 316.204,-61.9235\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"323.353,-63.5009 315.838,-65.0686 319.935,-62.7467 316.517,-61.9926 316.517,-61.9926 316.517,-61.9926 319.935,-62.7467 317.196,-58.9166 323.353,-63.5009 323.353,-63.5009\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"246\" y=\"-76.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-61.9739\">\u2779</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
+        "<path d=\"M186.254,-49.8409C181.355,-60.8302 185.438,-72.1739 198.5,-72.1739 208.705,-72.1739 213.429,-65.2502 212.672,-56.981\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"210.746,-49.8409 215.61,-55.7793 211.657,-53.2202 212.569,-56.5995 212.569,-56.5995 212.569,-56.5995 211.657,-53.2202 209.527,-57.4197 210.746,-49.8409 210.746,-49.8409\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171\" y=\"-90.9739\">p0 &amp; !p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-75.9739\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
+        "<path d=\"M455.252,-16.574C449.326,-14.4123 442.458,-12.2821 436,-11.1739 323.418,8.1465 222.082,-2.86597 169,-9.17391 137.816,-12.8797 102.754,-22.1959 80.3007,-28.8468\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"73.4747,-30.902 79.2693,-25.8676 76.8261,-29.8929 80.1775,-28.8838 80.1775,-28.8838 80.1775,-28.8838 76.8261,-29.8929 81.0856,-31.9001 73.4747,-30.902 73.4747,-30.902\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"248\" y=\"-20.9739\">!p0 &amp; p1</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"267.5\" y=\"-5.97391\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;2</title>\n",
+        "<path d=\"M454.418,-19.2927C434.853,-15.5987 401.846,-12.1988 377,-24.1739 367.603,-28.7031 359.889,-37.1039 354.118,-45.2865\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"350.088,-51.4335 351.292,-43.8524 352.007,-48.5065 353.926,-45.5795 353.926,-45.5795 353.926,-45.5795 352.007,-48.5065 356.56,-47.3067 350.088,-51.4335 350.088,-51.4335\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"377\" y=\"-42.9739\">!p0 &amp; !p1</text>\n",
+        "<text fill=\"#33a02c\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"398.5\" y=\"-27.9739\">\u2779</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 15
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Remark: colorizing a parity min won't change the **style** of the acceptance."
+     ]
     }
    ],
    "metadata": {}