From 172bee495a7c4ee0f5c02acd75eb9d26eeee3437 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 22 Feb 2017 16:30:10 +0100
Subject: [PATCH] minimize_dfa: use the twa_graph interface

Fixes #233, although more cleanup would be welcome.

* spot/twaalgos/minimize.cc: Replace the uses of twa methods by
twa_graph methods, and simplify some data structures.
* tests/core/acc_word.test, tests/core/readsave.test,
tests/python/automata.ipynb: Adjust changed output due
to different data structures.
---
 spot/twaalgos/minimize.cc   | 168 ++++++++-------------
 tests/core/acc_word.test    |  16 +-
 tests/core/readsave.test    |   1 -
 tests/python/automata.ipynb | 287 ++++++++++++++++++------------------
 4 files changed, 215 insertions(+), 257 deletions(-)

diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 01e6ea2f0..61cee9c3b 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -51,21 +51,19 @@ namespace spot
 {
   // This is called hash_set for historical reason, but we need the
   // order inside hash_set to be deterministic.
-  typedef std::set<const state*, state_ptr_less_than> hash_set;
-  typedef state_map<unsigned> hash_map;
+  typedef std::set<unsigned> hash_set;
 
   namespace
   {
     static std::ostream&
     dump_hash_set(const hash_set* hs,
-                  const const_twa_ptr& aut,
                   std::ostream& out)
     {
       out << '{';
       const char* sep = "";
-      for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i)
+      for (auto i: *hs)
         {
-          out << sep << aut->format_state(*i);
+          out << sep << i;
           sep = ", ";
         }
       out << '}';
@@ -73,47 +71,35 @@ namespace spot
     }
 
     static std::string
-    format_hash_set(const hash_set* hs, const_twa_ptr aut)
+    format_hash_set(const hash_set* hs)
     {
       std::ostringstream s;
-      dump_hash_set(hs, aut, s);
+      dump_hash_set(hs, s);
       return s.str();
     }
 
     // Find all states of an automaton.
     static void
-    build_state_set(const const_twa_ptr& a, hash_set* seen)
+    build_state_set(const const_twa_graph_ptr& a, hash_set* seen)
     {
-      std::queue<const state*> tovisit;
-      // Perform breadth-first traversal.
-      const state* init = a->get_init_state();
-      tovisit.push(init);
+      std::stack<unsigned> todo;
+      unsigned init = a->get_init_state_number();
+      todo.push(init);
       seen->insert(init);
-      while (!tovisit.empty())
+      while (!todo.empty())
         {
-          const state* src = tovisit.front();
-          tovisit.pop();
-
-          for (auto sit: a->succ(src))
-            {
-              const state* dst = sit->dst();
-              // Is it a new state ?
-              if (seen->find(dst) == seen->end())
-                {
-                  // Register the successor for later processing.
-                  tovisit.push(dst);
-                  seen->insert(dst);
-                }
-              else
-                dst->destroy();
-            }
+          unsigned s = todo.top();
+          todo.pop();
+          for (auto& e: a->out(s))
+            if (seen->insert(e.dst).second)
+              todo.push(e.dst);
         }
     }
 
     // From the base automaton and the list of sets, build the minimal
     // resulting automaton
     static twa_graph_ptr
-    build_result(const const_twa_ptr& a,
+    build_result(const const_twa_graph_ptr& a,
                  std::list<hash_set*>& sets,
                  hash_set* final)
     {
@@ -122,59 +108,46 @@ namespace spot
       res->copy_ap_of(a);
       res->prop_state_acc(true);
 
-      // For each set, create a state in the resulting automaton.
-      // For a state s, state_num[s] is the number of the state in the minimal
-      // automaton.
-      hash_map state_num;
-      std::list<hash_set*>::iterator sit;
-      for (sit = sets.begin(); sit != sets.end(); ++sit)
-        {
-          hash_set::iterator hit;
-          hash_set* h = *sit;
-          unsigned num = res->new_state();
-          for (hit = h->begin(); hit != h->end(); ++hit)
-            state_num[*hit] = num;
-        }
-
-      // For each transition in the initial automaton, add the corresponding
-      // transition in res.
+      // For each set, create a state in the output automaton.  For an
+      // input state s, state_num[s] is the corresponding the state in
+      // the output automaton.
+      std::vector<unsigned> state_num(a->num_states(), -1U);
+      {
+        unsigned num = res->new_states(sets.size());
+        for (hash_set* h: sets)
+          {
+            for (unsigned s: *h)
+              state_num[s] = num;
+            ++num;
+          }
+      }
 
       if (!final->empty())
         res->set_buchi();
 
-      for (sit = sets.begin(); sit != sets.end(); ++sit)
+      // For each transition in the initial automaton, add the
+      // corresponding transition in res.
+      for (hash_set* h: sets)
         {
-          hash_set* h = *sit;
-
           // Pick one state.
-          const state* src = *h->begin();
+          unsigned src = *h->begin();
           unsigned src_num = state_num[src];
           bool accepting = (final->find(src) != final->end());
 
           // Connect it to all destinations.
-          for (auto succit: a->succ(src))
+          for (auto& e: a->out(src))
             {
-              const state* dst = succit->dst();
-              hash_map::const_iterator i = state_num.find(dst);
-              dst->destroy();
-              if (i == state_num.end()) // Ignore useless destinations.
+              unsigned dn = state_num[e.dst];
+              if ((int)dn < 0)  // Ignore useless destinations.
                 continue;
-              res->new_acc_edge(src_num, i->second,
-                                succit->cond(), accepting);
+              res->new_acc_edge(src_num, dn, e.cond, accepting);
             }
         }
       res->merge_edges();
       if (res->num_states() > 0)
-        {
-          const state* init_state = a->get_init_state();
-          unsigned init_num = state_num[init_state];
-          init_state->destroy();
-          res->set_init_state(init_num);
-        }
+        res->set_init_state(state_num[a->get_init_state_number()]);
       else
-        {
-          res->set_init_state(res->new_state());
-        }
+        res->set_init_state(res->new_state());
       return res;
     }
 
@@ -275,7 +248,7 @@ namespace spot
       // The list of equivalent states.
       partition_t done;
 
-      hash_map state_set_map;
+      std::vector<unsigned> state_set_map(det_a->num_states(), -1U);
 
       // Size of det_a
       unsigned size = final->size() + non_final->size();
@@ -300,9 +273,8 @@ namespace spot
             cur_run.emplace_back(final);
           else
             done.emplace_back(final);
-          for (hash_set::const_iterator i = final->begin();
-               i != final->end(); ++i)
-            state_set_map[*i] = set_num;
+          for (auto i: *final)
+            state_set_map[i] = set_num;
 
           final_copy = new hash_set(*final);
         }
@@ -321,9 +293,8 @@ namespace spot
             cur_run.emplace_back(non_final);
           else
             done.emplace_back(non_final);
-          for (hash_set::const_iterator i = non_final->begin();
-               i != non_final->end(); ++i)
-            state_set_map[*i] = num;
+          for (auto i: *non_final)
+            state_set_map[i] = num;
         }
       else
         {
@@ -345,21 +316,17 @@ namespace spot
               hash_set* cur = cur_run.front();
               cur_run.pop_front();
 
-              trace << "processing " << format_hash_set(cur, det_a)
+              trace << "processing " << format_hash_set(cur)
                     << std::endl;
 
-              hash_set::iterator hi;
               bdd_states_map bdd_map;
-              for (hi = cur->begin(); hi != cur->end(); ++hi)
+              for (unsigned src: *cur)
                 {
-                  const state* src = *hi;
                   bdd f = bddfalse;
-                  for (auto si: det_a->succ(src))
+                  for (auto si: det_a->out(src))
                     {
-                      const state* dst = si->dst();
-                      hash_map::const_iterator i = state_set_map.find(dst);
-                      dst->destroy();
-                      if (i == state_set_map.end())
+                      unsigned i = state_set_map[si.dst];
+                      if ((int)i < 0)
                         // The destination state is not in our
                         // partition.  This can happen if the initial
                         // FINAL and NON_FINAL supplied to the algorithm
@@ -367,7 +334,7 @@ namespace spot
                         // want to ignore some useless states).  Simply
                         // ignore these states here.
                         continue;
-                      f |= (bdd_ithvar(i->second) & si->cond());
+                      f |= (bdd_ithvar(i) & si.cond);
                     }
 
                   // Have we already seen this formula ?
@@ -386,11 +353,11 @@ namespace spot
                     }
                 }
 
-              bdd_states_map::iterator bsi = bdd_map.begin();
+              auto bsi = bdd_map.begin();
               if (bdd_map.size() == 1)
                 {
                   // The set was not split.
-                  trace << "set " << format_hash_set(bsi->second, det_a)
+                  trace << "set " << format_hash_set(bsi->second)
                         << " was not split" << std::endl;
                   next_run.emplace_back(bsi->second);
                 }
@@ -417,19 +384,18 @@ namespace spot
                       num = *free_var.begin();
                       free_var.erase(free_var.begin());
                       used_var[num] = set->size();
-                      for (hash_set::iterator hit = set->begin();
-                           hit != set->end(); ++hit)
-                        state_set_map[*hit] = num;
-                      // Trivial sets can't be splitted any further.
+                      for (unsigned s: *set)
+                        state_set_map[s] = num;
+                      // Trivial sets can't be split any further.
                       if (set->size() == 1)
                         {
-                          trace << "set " << format_hash_set(set, det_a)
+                          trace << "set " << format_hash_set(set)
                                 << " is minimal" << std::endl;
                           done.emplace_back(set);
                         }
                       else
                         {
-                          trace << "set " << format_hash_set(set, det_a)
+                          trace << "set " << format_hash_set(set)
                                 << " should be processed further" << std::endl;
                           next_run.emplace_back(set);
                         }
@@ -448,8 +414,8 @@ namespace spot
 
 #ifdef TRACE
       trace << "Final partition: ";
-      for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i)
-        trace << format_hash_set(*i, det_a) << ' ';
+      for (hash_set* hs: done)
+        trace << format_hash_set(hs) << ' ';
       trace << std::endl;
 #endif
 
@@ -458,15 +424,9 @@ namespace spot
 
       // Free all the allocated memory.
       delete final_copy;
-      hash_map::iterator hit;
-      for (hit = state_set_map.begin(); hit != state_set_map.end();)
-        {
-          hash_map::iterator old = hit++;
-          old->first->destroy();
-        }
-      std::list<hash_set*>::iterator it;
-      for (it = done.begin(); it != done.end(); ++it)
-        delete *it;
+
+      for (hash_set* hs: done)
+        delete hs;
 
       return res;
     }
@@ -588,8 +548,8 @@ namespace spot
           if (!is_useless)
             {
               hash_set* dest_set = (d[m] & 1) ? non_final : final;
-              for (auto s: sm.states_of(m))
-                dest_set->insert(det_a->state_from_number(s));
+              auto& con = sm.states_of(m);
+              dest_set->insert(con.begin(), con.end());
             }
         }
     }
diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test
index 882e72a17..9c8e46d64 100644
--- a/tests/core/acc_word.test
+++ b/tests/core/acc_word.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement
+# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -99,13 +99,13 @@ cat >expected <<EOF
 HOA: v1.1
 name: "Fa & Fb"
 States: 4
-Start: 3
+Start: 2
 AP: 2 "a" "b"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete
 properties: deterministic stutter-invariant terminal
-spot.highlight.edges: 1 3 2 3 4 2 7 3 8 2 9 3
+spot.highlight.edges: 1 3 2 3 5 3 6 3 7 2 8 2
 --BODY--
 State: 0 {0}
 [t] 0
@@ -113,13 +113,13 @@ State: 1
 [1] 0
 [!1] 1
 State: 2
-[0] 0
-[!0] 2
-State: 3
 [0&1] 0
 [0&!1] 1
-[!0&1] 2
-[!0&!1] 3
+[!0&!1] 2
+[!0&1] 3
+State: 3
+[0] 0
+[!0] 3
 --END--
 EOF
 diff expected out
diff --git a/tests/core/readsave.test b/tests/core/readsave.test
index e0b073907..c1ab01cf2 100755
--- a/tests/core/readsave.test
+++ b/tests/core/readsave.test
@@ -557,7 +557,6 @@ digraph G {
   2 [label="1", peripheries=2]
   3 [label="2", peripheries=2]
   4 [label="3", peripheries=2]
-  u4 [label="...", shape=none, width=0, height=0]
 }
 EOF
 
diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb
index dec25e75f..841518fc9 100644
--- a/tests/python/automata.ipynb
+++ b/tests/python/automata.ipynb
@@ -15,10 +15,9 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.4.3+"
+   "version": "3.5.3"
   },
-  "name": "",
-  "signature": "sha256:4ddb9b8fc1c41bacd7e47f70861303cde0ad425f842ade8e1f23ee74738914b0"
+  "name": ""
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -178,7 +177,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe334de9900> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe56a0540> >"
        ]
       }
      ],
@@ -205,119 +204,119 @@
        "output_type": "pyout",
        "prompt_number": 3,
        "svg": [
-        "<svg height=\"351pt\" viewBox=\"0.00 0.00 226.36 351.00\" width=\"226pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<svg height=\"351pt\" viewBox=\"0.00 0.00 220.18 351.00\" width=\"220pt\" 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 347)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-347 222.356,-347 222.356,4 -4,4\" stroke=\"none\"/>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-347 216.176,-347 216.176,4 -4,4\" stroke=\"none\"/>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"120.356\" cy=\"-287\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"120.356\" y=\"-283.3\">0</text>\n",
+        "<ellipse cx=\"116.176\" cy=\"-287\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"116.176\" y=\"-283.3\">0</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M120.356,-341.845C120.356,-340.206 120.356,-325.846 120.356,-312.368\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"120.356,-305.058 123.506,-312.058 120.356,-308.558 120.356,-312.058 120.356,-312.058 120.356,-312.058 120.356,-308.558 117.206,-312.058 120.356,-305.058 120.356,-305.058\" stroke=\"black\"/>\n",
+        "<path d=\"M116.176,-341.845C116.176,-340.206 116.176,-325.846 116.176,-312.368\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"116.176,-305.058 119.326,-312.058 116.176,-308.558 116.176,-312.058 116.176,-312.058 116.176,-312.058 116.176,-308.558 113.026,-312.058 116.176,-305.058 116.176,-305.058\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M137.393,-293.379C147.214,-294.681 156.356,-292.555 156.356,-287 156.356,-282.834 151.214,-280.596 144.499,-280.287\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"137.393,-280.621 144.238,-277.146 140.89,-280.457 144.386,-280.292 144.386,-280.292 144.386,-280.292 140.89,-280.457 144.533,-283.439 137.393,-280.621 137.393,-280.621\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"174.856\" y=\"-283.3\">a &amp; !b</text>\n",
+        "<path d=\"M133.213,-293.379C143.033,-294.681 152.176,-292.555 152.176,-287 152.176,-282.834 147.033,-280.596 140.319,-280.287\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"133.213,-280.621 140.057,-277.146 136.709,-280.457 140.205,-280.292 140.205,-280.292 140.205,-280.292 136.709,-280.457 140.353,-283.439 133.213,-280.621 133.213,-280.621\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"168.676\" y=\"-283.3\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"67.3561\" cy=\"-196\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"67.3561\" y=\"-192.3\">1</text>\n",
+        "<ellipse cx=\"63.1755\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"63.1755\" cy=\"-196\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"63.1755\" y=\"-192.3\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
-        "<path d=\"M111.365,-270.902C103.283,-257.33 91.2671,-237.152 81.832,-221.309\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"78.2263,-215.254 84.5144,-219.656 80.0171,-218.261 81.808,-221.268 81.808,-221.268 81.808,-221.268 80.0171,-218.261 79.1015,-222.88 78.2263,-215.254 78.2263,-215.254\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"102.856\" y=\"-239.8\">b</text>\n",
+        "<path d=\"M107.185,-270.902C99.1023,-257.33 87.0865,-237.152 77.6514,-221.309\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"74.0458,-215.254 80.3339,-219.656 75.8366,-218.261 77.6274,-221.268 77.6274,-221.268 77.6274,-221.268 75.8366,-218.261 74.9209,-222.88 74.0458,-215.254 74.0458,-215.254\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"98.6755\" y=\"-239.8\">b</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g class=\"node\" id=\"node4\"><title>4</title>\n",
-        "<ellipse cx=\"175.356\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"175.356\" y=\"-192.3\">4</text>\n",
+        "<ellipse cx=\"169.176\" cy=\"-196\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169.176\" y=\"-192.3\">4</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
-        "<path d=\"M129.438,-271.303C138.435,-256.746 152.298,-234.312 162.439,-217.902\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"166.26,-211.718 165.26,-219.329 164.42,-214.696 162.581,-217.673 162.581,-217.673 162.581,-217.673 164.42,-214.696 159.901,-216.017 166.26,-211.718 166.26,-211.718\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170.856\" y=\"-239.8\">!a &amp; !b</text>\n",
+        "<path d=\"M125.166,-270.902C133.822,-256.367 146.99,-234.255 156.667,-218.005\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"160.318,-211.875 159.442,-219.501 158.527,-214.882 156.736,-217.889 156.736,-217.889 156.736,-217.889 158.527,-214.882 154.029,-216.277 160.318,-211.875 160.318,-211.875\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"163.176\" y=\"-239.8\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
-        "<path d=\"M87.9369,-204.37C98.2008,-205.528 107.356,-202.738 107.356,-196 107.356,-190.946 102.206,-188.113 95.3012,-187.501\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"87.9369,-187.63 94.8809,-184.358 91.4364,-187.569 94.9358,-187.508 94.9358,-187.508 94.9358,-187.508 91.4364,-187.569 94.9907,-190.657 87.9369,-187.63 87.9369,-187.63\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"123.356\" y=\"-192.3\">c &amp; d</text>\n",
+        "<path d=\"M83.7563,-204.37C94.0202,-205.528 103.176,-202.738 103.176,-196 103.176,-190.946 98.0257,-188.113 91.1207,-187.501\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"83.7563,-187.63 90.7003,-184.358 87.2558,-187.569 90.7553,-187.508 90.7553,-187.508 90.7553,-187.508 87.2558,-187.569 90.8102,-190.657 83.7563,-187.63 83.7563,-187.63\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"118.176\" y=\"-192.3\">c &amp; d</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node5\"><title>2</title>\n",
-        "<ellipse cx=\"68.3561\" cy=\"-18\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-14.3\">2</text>\n",
+        "<ellipse cx=\"64.1755\" cy=\"-18\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"64.1755\" y=\"-14.3\">2</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
-        "<path d=\"M50.199,-181.727C34.8703,-168.686 13.4697,-147.255 4.35608,-123 -1.27155,-108.022 -1.54226,-101.873 4.35608,-87 13.1144,-64.9152 32.818,-45.8318 48.0656,-33.5506\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"53.866,-29.0284 50.2823,-35.8166 51.1058,-31.1804 48.3455,-33.3324 48.3455,-33.3324 48.3455,-33.3324 51.1058,-31.1804 46.4087,-30.8481 53.866,-29.0284 53.866,-29.0284\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.8561\" y=\"-101.3\">!c &amp; d</text>\n",
+        "<path d=\"M46.8076,-181.236C32.4563,-168.007 12.6056,-146.588 4.17551,-123 -1.20916,-107.933 -1.48317,-101.966 4.17551,-87 12.2372,-65.6786 30.3712,-46.7242 44.6062,-34.2791\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"50.0362,-29.6769 46.7329,-36.6059 47.3662,-31.9399 44.6962,-34.2029 44.6962,-34.2029 44.6962,-34.2029 47.3662,-31.9399 42.6595,-31.7998 50.0362,-29.6769 50.0362,-29.6769\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"20.6755\" y=\"-101.3\">!c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node6\"><title>3</title>\n",
-        "<ellipse cx=\"68.3561\" cy=\"-105\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"68.3561\" y=\"-101.3\">3</text>\n",
+        "<ellipse cx=\"64.1755\" cy=\"-105\" fill=\"none\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"64.1755\" y=\"-101.3\">3</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
-        "<path d=\"M56.8135,-176.159C52.3073,-165.855 48.6383,-152.816 51.3561,-141 52.4094,-136.42 54.1455,-131.745 56.1156,-127.365\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"59.3394,-120.78 59.0906,-128.452 57.8004,-123.923 56.2615,-127.067 56.2615,-127.067 56.2615,-127.067 57.8004,-123.923 53.4323,-125.682 59.3394,-120.78 59.3394,-120.78\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"57.3561\" y=\"-144.8\">!d</text>\n",
+        "<path d=\"M53.2767,-176.138C49.0477,-165.827 45.6086,-152.789 48.1755,-141 49.1456,-136.544 50.7357,-131.977 52.5462,-127.674\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"55.5153,-121.184 55.4677,-128.86 54.0593,-124.366 52.6032,-127.549 52.6032,-127.549 52.6032,-127.549 54.0593,-124.366 49.7387,-126.239 55.5153,-121.184 55.5153,-121.184\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.1755\" y=\"-144.8\">!d</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
-        "<path d=\"M191.646,-204.016C201.745,-205.949 211.356,-203.277 211.356,-196 211.356,-190.542 205.95,-187.674 198.986,-187.397\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"191.646,-187.984 198.373,-184.286 195.135,-187.705 198.624,-187.426 198.624,-187.426 198.624,-187.426 195.135,-187.705 198.875,-190.566 191.646,-187.984 191.646,-187.984\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"214.856\" y=\"-192.3\">1</text>\n",
+        "<path d=\"M185.466,-204.016C195.565,-205.949 205.176,-203.277 205.176,-196 205.176,-190.542 199.769,-187.674 192.806,-187.397\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"185.466,-187.984 192.193,-184.286 188.955,-187.705 192.444,-187.426 192.444,-187.426 192.444,-187.426 188.955,-187.705 192.694,-190.566 185.466,-187.984 185.466,-187.984\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"208.676\" y=\"-192.3\">1</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
-        "<path d=\"M82.9697,-29.0929C91.4609,-35.4971 101.918,-44.3722 109.356,-54 128.603,-78.9113 134.158,-92.7751 125.356,-123 119.215,-144.088 103.068,-163.203 89.3663,-176.43\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"84.0682,-181.376 87.035,-174.297 86.6265,-178.988 89.1847,-176.599 89.1847,-176.599 89.1847,-176.599 86.6265,-178.988 91.3345,-178.901 84.0682,-181.376 84.0682,-181.376\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"132.856\" y=\"-101.3\">c</text>\n",
+        "<path d=\"M77.8501,-30.0814C85.3082,-36.5564 94.3776,-45.173 101.176,-54 120.513,-79.1097 128.036,-92.5709 119.176,-123 113.156,-143.671 97.7364,-162.693 84.5983,-175.987\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"79.5143,-180.969 82.3093,-173.82 82.0142,-178.52 84.514,-176.07 84.514,-176.07 84.514,-176.07 82.0142,-178.52 86.7187,-178.32 79.5143,-180.969 79.5143,-180.969\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"125.676\" y=\"-101.3\">c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
-        "<path d=\"M85.0201,-25.3828C94.9811,-27.0234 104.356,-24.5625 104.356,-18 104.356,-13.0781 99.0826,-10.4634 92.2436,-10.1558\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"85.0201,-10.6172 91.8051,-7.02727 88.513,-10.394 92.0059,-10.1709 92.0059,-10.1709 92.0059,-10.1709 88.513,-10.394 92.2067,-13.3145 85.0201,-10.6172 85.0201,-10.6172\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"109.856\" y=\"-14.3\">!c</text>\n",
+        "<path d=\"M80.8396,-25.3828C90.8005,-27.0234 100.176,-24.5625 100.176,-18 100.176,-13.0781 94.9021,-10.4634 88.0631,-10.1558\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"80.8396,-10.6172 87.6245,-7.02727 84.3325,-10.394 87.8253,-10.1709 87.8253,-10.1709 87.8253,-10.1709 84.3325,-10.394 88.0262,-13.3145 80.8396,-10.6172 80.8396,-10.6172\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"105.176\" y=\"-14.3\">!c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
-        "<path d=\"M68.1643,-123.066C68.0258,-135.398 67.8354,-152.339 67.6743,-166.682\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"67.5931,-173.908 64.522,-166.873 67.6324,-170.408 67.6718,-166.909 67.6718,-166.909 67.6718,-166.909 67.6324,-170.408 70.8216,-166.944 67.5931,-173.908 67.5931,-173.908\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"84.3561\" y=\"-144.8\">c &amp; d</text>\n",
+        "<path d=\"M63.9838,-123.066C63.8452,-135.398 63.6549,-152.339 63.4937,-166.682\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"63.4125,-173.908 60.3414,-166.873 63.4519,-170.408 63.4912,-166.909 63.4912,-166.909 63.4912,-166.909 63.4519,-170.408 66.641,-166.944 63.4125,-173.908 63.4125,-173.908\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"79.1755\" y=\"-144.8\">c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
-        "<path d=\"M68.3561,-86.799C68.3561,-74.3561 68.3561,-57.3644 68.3561,-43.5044\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"68.3561,-36.1754 71.5062,-43.1754 68.3561,-39.6754 68.3562,-43.1754 68.3562,-43.1754 68.3562,-43.1754 68.3561,-39.6754 65.2062,-43.1755 68.3561,-36.1754 68.3561,-36.1754\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"86.8561\" y=\"-57.8\">!c &amp; d</text>\n",
+        "<path d=\"M64.1755,-86.799C64.1755,-74.3561 64.1755,-57.3644 64.1755,-43.5044\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"64.1755,-36.1754 67.3256,-43.1754 64.1756,-39.6754 64.1756,-43.1754 64.1756,-43.1754 64.1756,-43.1754 64.1756,-39.6754 61.0256,-43.1755 64.1755,-36.1754 64.1755,-36.1754\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"80.6755\" y=\"-57.8\">!c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
-        "<path d=\"M85.0201,-112.383C94.9811,-114.023 104.356,-111.562 104.356,-105 104.356,-100.078 99.0826,-97.4634 92.2436,-97.1558\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"85.0201,-97.6172 91.8051,-94.0273 88.513,-97.394 92.0059,-97.1709 92.0059,-97.1709 92.0059,-97.1709 88.513,-97.394 92.2067,-100.314 85.0201,-97.6172 85.0201,-97.6172\" stroke=\"black\"/>\n",
-        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"110.356\" y=\"-101.3\">!d</text>\n",
+        "<path d=\"M80.8396,-112.383C90.8005,-114.023 100.176,-111.562 100.176,-105 100.176,-100.078 94.9021,-97.4634 88.0631,-97.1558\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"80.8396,-97.6172 87.6245,-94.0273 84.3325,-97.394 87.8253,-97.1709 87.8253,-97.1709 87.8253,-97.1709 84.3325,-97.394 88.0262,-100.314 80.8396,-97.6172 80.8396,-97.6172\" stroke=\"black\"/>\n",
+        "<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"105.176\" y=\"-101.3\">!d</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe335a6c0f0>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -372,7 +371,7 @@
         "<polygon fill=\"black\" points=\"37.9419,-49 30.9419,-52.1501 34.4419,-49 30.9419,-49.0001 30.9419,-49.0001 30.9419,-49.0001 34.4419,-49 30.9418,-45.8501 37.9419,-49 37.9419,-49\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
-        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
+        "<g class=\"edge\" id=\"edge11\"><title>0-&gt;0</title>\n",
         "<path d=\"M49.6208,-66.0373C48.3189,-75.8579 50.4453,-85 56,-85 60.166,-85 62.4036,-79.8576 62.7128,-73.1433\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"62.3792,-66.0373 65.8541,-72.8818 62.5434,-69.5335 62.7076,-73.0296 62.7076,-73.0296 62.7076,-73.0296 62.5434,-69.5335 59.561,-73.1774 62.3792,-66.0373 62.3792,-66.0373\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-88.8\">a &amp; !b</text>\n",
@@ -383,7 +382,7 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-189.3\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;1</title>\n",
+        "<g class=\"edge\" id=\"edge12\"><title>0-&gt;1</title>\n",
         "<path d=\"M67.6431,-62.8073C87.4829,-88.5454 130.165,-143.916 152.947,-173.472\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"157.226,-179.023 150.458,-175.402 155.089,-176.251 152.952,-173.479 152.952,-173.479 152.952,-173.479 155.089,-176.251 155.447,-171.556 157.226,-179.023 157.226,-179.023\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"108\" y=\"-150.8\">b</text>\n",
@@ -394,13 +393,13 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-30.3\">4</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;4</title>\n",
+        "<g class=\"edge\" id=\"edge13\"><title>0-&gt;4</title>\n",
         "<path d=\"M73.8585,-46.7218C92.5211,-44.1998 122.756,-40.114 143.912,-37.2551\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"150.983,-36.2996 144.468,-40.3588 147.514,-36.7684 144.046,-37.2371 144.046,-37.2371 144.046,-37.2371 147.514,-36.7684 143.624,-34.1155 150.983,-36.2996 150.983,-36.2996\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-48.8\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;1</title>\n",
+        "<g class=\"edge\" id=\"edge2\"><title>1-&gt;1</title>\n",
         "<path d=\"M160.021,-208.916C157.679,-219.15 160.672,-229 169,-229 175.376,-229 178.625,-223.226 178.746,-215.927\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"177.979,-208.916 181.872,-215.532 178.36,-212.395 178.741,-215.874 178.741,-215.874 178.741,-215.874 178.36,-212.395 175.61,-216.217 177.979,-208.916 177.979,-208.916\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"152\" y=\"-247.8\">c &amp; d</text>\n",
@@ -412,7 +411,7 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"385\" y=\"-189.3\">2</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;2</title>\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;2</title>\n",
         "<path d=\"M183.382,-181.807C199.601,-169.041 228.334,-148.914 257,-141 296.803,-130.011 340.921,-157.735 365.268,-176.79\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"371.017,-181.419 363.59,-179.483 368.291,-179.224 365.565,-177.029 365.565,-177.029 365.565,-177.029 368.291,-179.224 367.54,-174.576 371.017,-181.419 371.017,-181.419\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"257\" y=\"-159.8\">!c &amp; d</text>\n",
@@ -424,44 +423,44 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"275.5\" y=\"-240.3\">3</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;3</title>\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
         "<path d=\"M186.45,-197.514C200.79,-201.783 221.911,-208.888 239,-218 244.62,-220.997 250.345,-224.799 255.51,-228.565\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"261.277,-232.918 253.792,-231.215 258.484,-230.809 255.69,-228.701 255.69,-228.701 255.69,-228.701 258.484,-230.809 257.588,-226.187 261.277,-232.918 261.277,-232.918\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"215.5\" y=\"-236.8\">!d</text>\n",
         "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"214\" y=\"-221.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;1</title>\n",
+        "<g class=\"edge\" id=\"edge5\"><title>2-&gt;1</title>\n",
         "<path d=\"M366.768,-193C328.813,-193 237.915,-193 194.238,-193\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"187.151,-193 194.151,-189.85 190.651,-193 194.151,-193 194.151,-193 194.151,-193 190.651,-193 194.151,-196.15 187.151,-193 187.151,-193\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"272\" y=\"-196.8\">c</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;2</title>\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;2</title>\n",
         "<path d=\"M375.767,-208.541C373.169,-218.909 376.246,-229 385,-229 391.702,-229 395.077,-223.085 395.124,-215.659\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"394.233,-208.541 398.229,-215.095 394.668,-212.014 395.103,-215.487 395.103,-215.487 395.103,-215.487 394.668,-212.014 391.977,-215.879 394.233,-208.541 394.233,-208.541\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"379.5\" y=\"-232.8\">!c</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;1</title>\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;1</title>\n",
         "<path d=\"M258.25,-249.586C243.436,-253.647 221.422,-257.015 205,-248 192.725,-241.262 184.14,-228.191 178.545,-216.482\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"175.592,-209.803 181.304,-214.931 177.007,-213.004 178.423,-216.205 178.423,-216.205 178.423,-216.205 177.007,-213.004 175.542,-217.479 175.592,-209.803 175.592,-209.803\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"205\" y=\"-256.8\">c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge11\"><title>3-&gt;2</title>\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;2</title>\n",
         "<path d=\"M292.362,-236.475C310.807,-227.724 341.364,-213.227 362.073,-203.403\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"368.422,-200.39 363.448,-206.237 365.26,-201.891 362.098,-203.391 362.098,-203.391 362.098,-203.391 365.26,-201.891 360.748,-200.545 368.422,-200.39 368.422,-200.39\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"312\" y=\"-229.8\">!c &amp; d</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;3</title>\n",
         "<path d=\"M266.521,-259.916C264.179,-270.15 267.172,-280 275.5,-280 281.876,-280 285.125,-274.226 285.246,-266.927\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"284.479,-259.916 288.372,-266.532 284.86,-263.395 285.241,-266.874 285.241,-266.874 285.241,-266.874 284.86,-263.395 282.11,-267.217 284.479,-259.916 284.479,-259.916\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"269\" y=\"-283.8\">!d</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge13\"><title>4-&gt;4</title>\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;4</title>\n",
         "<path d=\"M160.021,-49.916C157.679,-60.1504 160.672,-70 169,-70 175.376,-70 178.625,-64.2263 178.746,-56.9268\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"177.979,-49.916 181.872,-56.5315 178.36,-53.3952 178.741,-56.8744 178.741,-56.8744 178.741,-56.8744 178.36,-53.3952 175.61,-57.2174 177.979,-49.916 177.979,-49.916\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169\" y=\"-73.8\">1</text>\n",
@@ -470,7 +469,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe3340e5588>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -570,7 +569,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c8331b0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4d87f90> >"
        ]
       }
      ],
@@ -640,7 +639,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833060> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da41b0> >"
        ]
       }
      ],
@@ -716,7 +715,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c8330f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4e0f330> >"
        ]
       }
      ],
@@ -839,7 +838,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe3340e56d8>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -919,30 +918,18 @@
         "</g>\n",
         "<!-- 3 -->\n",
         "<g class=\"node\" id=\"node6\"><title>3</title>\n",
-        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"432.883\" y=\"-113.3\">3</text>\n",
+        "<ellipse cx=\"478.883\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"478.883\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.883\" y=\"-18.3\">3</text>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;3 -->\n",
         "<g class=\"edge\" id=\"edge17\"><title>6-&gt;3</title>\n",
-        "<path d=\"M298.339,-199.782C325.793,-183.094 377.444,-151.699 408.145,-133.037\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"414.363,-129.258 410.017,-135.585 411.372,-131.076 408.381,-132.894 408.381,-132.894 408.381,-132.894 411.372,-131.076 406.745,-130.202 414.363,-129.258 414.363,-129.258\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.883\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
-        "</g>\n",
-        "<!-- 5 -->\n",
-        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
-        "<ellipse cx=\"478.883\" cy=\"-22\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<ellipse cx=\"478.883\" cy=\"-22\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"478.883\" y=\"-18.3\">5</text>\n",
-        "</g>\n",
-        "<!-- 6&#45;&gt;5 -->\n",
-        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
         "<path d=\"M301.69,-207.819C355.332,-199.487 491.143,-175.144 515.883,-139 535.586,-110.215 514.515,-70.3416 497.048,-45.6345\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"492.712,-39.6958 499.384,-43.4919 494.776,-42.5226 496.84,-45.3493 496.84,-45.3493 496.84,-45.3493 494.776,-42.5226 494.296,-47.2068 492.712,-39.6958 492.712,-39.6958\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"522.883\" y=\"-113.3\">a &amp; !b &amp; !c</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
-        "<g class=\"node\" id=\"node8\"><title>4</title>\n",
+        "<g class=\"node\" id=\"node7\"><title>4</title>\n",
         "<ellipse cx=\"218.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
         "<ellipse cx=\"218.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"218.883\" y=\"-113.3\">4</text>\n",
@@ -953,6 +940,18 @@
         "<polygon fill=\"black\" points=\"229.23,-136.54 235.461,-141.023 230.982,-139.57 232.734,-142.6 232.734,-142.6 232.734,-142.6 230.982,-139.57 230.007,-144.176 229.23,-136.54 229.23,-136.54\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"250.883\" y=\"-160.8\">a &amp; !b &amp; c</text>\n",
         "</g>\n",
+        "<!-- 5 -->\n",
+        "<g class=\"node\" id=\"node8\"><title>5</title>\n",
+        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<ellipse cx=\"432.883\" cy=\"-117\" fill=\"none\" rx=\"22\" ry=\"22\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"432.883\" y=\"-113.3\">5</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;5 -->\n",
+        "<g class=\"edge\" id=\"edge19\"><title>6-&gt;5</title>\n",
+        "<path d=\"M298.339,-199.782C325.793,-183.094 377.444,-151.699 408.145,-133.037\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"414.363,-129.258 410.017,-135.585 411.372,-131.076 408.381,-132.894 408.381,-132.894 408.381,-132.894 411.372,-131.076 406.745,-130.202 414.363,-129.258 414.363,-129.258\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.883\" y=\"-160.8\">a &amp; b &amp; !c</text>\n",
+        "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
         "<path d=\"M119.464,-30.3702C129.728,-31.5284 138.883,-28.7383 138.883,-22 138.883,-16.9463 133.734,-14.1134 126.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
@@ -983,53 +982,53 @@
         "<polygon fill=\"black\" points=\"347.464,-13.6298 354.408,-10.3582 350.964,-13.5688 354.463,-13.5077 354.463,-13.5077 354.463,-13.5077 350.964,-13.5688 354.518,-16.6573 347.464,-13.6298 347.464,-13.6298\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"366.883\" y=\"-18.3\">b</text>\n",
         "</g>\n",
-        "<!-- 3&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;2</title>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>3-&gt;3</title>\n",
+        "<path d=\"M499.464,-30.3702C509.728,-31.5284 518.883,-28.7383 518.883,-22 518.883,-16.9463 513.734,-14.1134 506.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"499.464,-13.6298 506.408,-10.3582 502.964,-13.5688 506.463,-13.5077 506.463,-13.5077 506.463,-13.5077 502.964,-13.5688 506.518,-16.6573 499.464,-13.6298 499.464,-13.6298\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"518.883\" y=\"-18.3\">a</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>4-&gt;0</title>\n",
+        "<path d=\"M214.631,-95.3163C211.41,-84.2043 205.939,-70.9826 196.883,-62 178.078,-43.3468 149.236,-33.3217 127.704,-28.1297\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"120.707,-26.5487 128.229,-25.019 124.121,-27.3201 127.534,-28.0915 127.534,-28.0915 127.534,-28.0915 124.121,-27.3201 126.84,-31.1641 120.707,-26.5487 120.707,-26.5487\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206.883\" y=\"-65.8\">!a &amp; c</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>4-&gt;3</title>\n",
+        "<path d=\"M238.845,-107.727C265.547,-96.7677 314.456,-77.0653 356.883,-62 388.924,-50.6228 426.214,-38.9231 451.051,-31.345\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"458.026,-29.2257 452.244,-34.2749 454.677,-30.2433 451.328,-31.261 451.328,-31.261 451.328,-31.261 454.677,-30.2433 450.412,-28.2471 458.026,-29.2257 458.026,-29.2257\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.883\" y=\"-65.8\">a &amp; !c</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;4</title>\n",
+        "<path d=\"M239.464,-125.37C249.728,-126.528 258.883,-123.738 258.883,-117 258.883,-111.946 253.734,-109.113 246.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"239.464,-108.63 246.408,-105.358 242.964,-108.569 246.463,-108.508 246.463,-108.508 246.463,-108.508 242.964,-108.569 246.518,-111.657 239.464,-108.63 239.464,-108.63\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258.883\" y=\"-113.3\">a &amp; c</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>5-&gt;2</title>\n",
         "<path d=\"M423.273,-97.1109C416.901,-85.9186 407.728,-72.013 396.883,-62 384.323,-50.4024 367.69,-40.9523 353.79,-34.2605\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"347.216,-31.1996 354.891,-31.2984 350.389,-32.6769 353.562,-34.1541 353.562,-34.1541 353.562,-34.1541 350.389,-32.6769 352.232,-37.0098 347.216,-31.1996 347.216,-31.1996\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.883\" y=\"-65.8\">!a &amp; b</text>\n",
         "</g>\n",
-        "<!-- 3&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;3</title>\n",
-        "<path d=\"M453.464,-125.37C463.728,-126.528 472.883,-123.738 472.883,-117 472.883,-111.946 467.734,-109.113 460.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"453.464,-108.63 460.408,-105.358 456.964,-108.569 460.463,-108.508 460.463,-108.508 460.463,-108.508 456.964,-108.569 460.518,-111.657 453.464,-108.63 453.464,-108.63\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"472.883\" y=\"-113.3\">a &amp; b</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;5 -->\n",
-        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;5</title>\n",
+        "<!-- 5&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;3</title>\n",
         "<path d=\"M444.753,-98.1028C448.839,-91.5928 453.288,-84.0908 456.883,-77 461.334,-68.2222 465.577,-58.3236 469.128,-49.4213\" fill=\"none\" stroke=\"black\"/>\n",
         "<polygon fill=\"black\" points=\"471.701,-42.843 472.085,-50.5095 470.426,-46.1025 469.152,-49.3621 469.152,-49.3621 469.152,-49.3621 470.426,-46.1025 466.218,-48.2147 471.701,-42.843 471.701,-42.843\" stroke=\"black\"/>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"462.883\" y=\"-65.8\">a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;5 -->\n",
         "<g class=\"edge\" id=\"edge13\"><title>5-&gt;5</title>\n",
-        "<path d=\"M499.464,-30.3702C509.728,-31.5284 518.883,-28.7383 518.883,-22 518.883,-16.9463 513.734,-14.1134 506.829,-13.5015\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"499.464,-13.6298 506.408,-10.3582 502.964,-13.5688 506.463,-13.5077 506.463,-13.5077 506.463,-13.5077 502.964,-13.5688 506.518,-16.6573 499.464,-13.6298 499.464,-13.6298\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"518.883\" y=\"-18.3\">a</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;0 -->\n",
-        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;0</title>\n",
-        "<path d=\"M214.631,-95.3163C211.41,-84.2043 205.939,-70.9826 196.883,-62 178.078,-43.3468 149.236,-33.3217 127.704,-28.1297\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"120.707,-26.5487 128.229,-25.019 124.121,-27.3201 127.534,-28.0915 127.534,-28.0915 127.534,-28.0915 124.121,-27.3201 126.84,-31.1641 120.707,-26.5487 120.707,-26.5487\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"206.883\" y=\"-65.8\">!a &amp; c</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;5 -->\n",
-        "<g class=\"edge\" id=\"edge12\"><title>4-&gt;5</title>\n",
-        "<path d=\"M238.845,-107.727C265.547,-96.7677 314.456,-77.0653 356.883,-62 388.924,-50.6228 426.214,-38.9231 451.051,-31.345\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"458.026,-29.2257 452.244,-34.2749 454.677,-30.2433 451.328,-31.261 451.328,-31.261 451.328,-31.261 454.677,-30.2433 450.412,-28.2471 458.026,-29.2257 458.026,-29.2257\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.883\" y=\"-65.8\">a &amp; !c</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;4</title>\n",
-        "<path d=\"M239.464,-125.37C249.728,-126.528 258.883,-123.738 258.883,-117 258.883,-111.946 253.734,-109.113 246.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"239.464,-108.63 246.408,-105.358 242.964,-108.569 246.463,-108.508 246.463,-108.508 246.463,-108.508 242.964,-108.569 246.518,-111.657 239.464,-108.63 239.464,-108.63\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"258.883\" y=\"-113.3\">a &amp; c</text>\n",
+        "<path d=\"M453.464,-125.37C463.728,-126.528 472.883,-123.738 472.883,-117 472.883,-111.946 467.734,-109.113 460.829,-108.501\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"453.464,-108.63 460.408,-105.358 456.964,-108.569 460.463,-108.508 460.463,-108.508 460.463,-108.508 456.964,-108.569 460.518,-111.657 453.464,-108.63 453.464,-108.63\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"472.883\" y=\"-113.3\">a &amp; b</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe3340aba20>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -1176,7 +1175,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833300> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4510> >"
        ]
       }
      ],
@@ -1277,7 +1276,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c8332d0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4540> >"
        ]
       }
      ],
@@ -1395,7 +1394,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833120> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4570> >"
        ]
       }
      ],
@@ -1494,7 +1493,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833330> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da43c0> >"
        ]
       }
      ],
@@ -1964,7 +1963,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c8332a0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4150> >"
        ]
       }
      ],
@@ -2161,7 +2160,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe334078400>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2286,7 +2285,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe33407f8d0>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2428,7 +2427,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe3340f9ba8>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2579,7 +2578,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe334d5cae0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4660> >"
        ]
       }
      ],
@@ -2735,7 +2734,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe334d5cfc0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4450> >"
        ]
       }
      ],
@@ -2805,7 +2804,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe334d5cae0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4e0f5a0> >"
        ]
       }
      ],
@@ -2877,7 +2876,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe33408fa58>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2930,7 +2929,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe3340b0828>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -3042,7 +3041,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe3340cf3c8>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -3154,7 +3153,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe3340a9cf8>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -3169,7 +3168,7 @@
     },
     {
      "cell_type": "code",
-     "collapsed": true,
+     "collapsed": false,
      "input": [
       "a = spot.translate('FGa')\n",
       "display(a)\n",
@@ -3232,7 +3231,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c833390> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da46f0> >"
        ]
       },
       {
@@ -3315,7 +3314,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7fe33406c7b8>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -3400,7 +3399,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c747540> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4090> >"
        ]
       }
      ],
@@ -3410,7 +3409,7 @@
      "cell_type": "markdown",
      "metadata": {},
      "source": [
-      "Adding an automatic proposition to all edges"
+      "Adding an atomic proposition to all edges"
      ]
     },
     {
@@ -3489,7 +3488,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c747540> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4090> >"
        ]
       }
      ],
@@ -3578,7 +3577,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe33c747540> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7fe4da4090> >"
        ]
       }
      ],
@@ -3588,4 +3587,4 @@
    "metadata": {}
   }
  ]
-}
\ No newline at end of file
+}