From abe2c08b789b59b1fe2ab56d7534bb964aaca9a4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 25 Jul 2017 17:38:24 +0200
Subject: [PATCH] acc: make &= and |= symmetrical

Operator &= used to always move Fin to the front, it does not anymore.
The only thing it does now is to merge Inf(x)&Inf(y) as Inf({x,y}).
Operator |= is now symmetrical and merges Fin()s.

Fixes #253.

* spot/twa/acc.cc, spot/twa/acc.hh: Simplify &= and make |= symmetrical.
* spot/twaalgos/cleanacc.cc: Fix conjunction order.
* tests/core/acc.test, tests/core/acc2.test, tests/core/parseaut.test,
tests/core/readsave.test, tests/core/satmin2.test,
tests/core/sccdot.test, tests/python/acc_cond.ipynb,
tests/python/accparse.ipynb, tests/python/automata.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
---
 NEWS                        |   6 +
 spot/twa/acc.cc             |  18 +--
 spot/twa/acc.hh             | 212 ++++++++++++++----------------------
 spot/twaalgos/cleanacc.cc   |   6 +-
 tests/core/acc.test         |  16 +--
 tests/core/acc2.test        |  10 +-
 tests/core/parseaut.test    |  10 +-
 tests/core/readsave.test    |   4 +-
 tests/core/satmin2.test     |   2 +-
 tests/core/sccdot.test      |   4 +-
 tests/python/acc_cond.ipynb |  12 +-
 tests/python/accparse.ipynb |  11 +-
 tests/python/automata.ipynb |  46 ++++----
 tests/python/product.ipynb  | 130 +++++++++++-----------
 tests/python/randaut.ipynb  |  62 ++++++-----
 15 files changed, 254 insertions(+), 295 deletions(-)

diff --git a/NEWS b/NEWS
index 2391f79ca..471136894 100644
--- a/NEWS
+++ b/NEWS
@@ -156,6 +156,12 @@ New in spot 2.3.5.dev (not yet released)
   - If the SPOT_BDD_TRACE envorinment variable is set, statistics
     about BDD garbage collection and table resizing are shown.
 
+  - The & and | operators for acceptannce conditions have been changed
+    slightly to be more symmetrical.  In older version, operator &
+    would move Fin() terms to the front, but that is not the case
+    anymore.  Also operator & was already grouping all Inf() terms
+    (for efficiency reasons), in this version operator | is
+    symmetrically grouping all Fin() terms.
 
   Python:
 
diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index 9bd502d0a..1c9d1bd2e 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -914,7 +914,7 @@ namespace spot
     while ((cube = isop.next()) != bddfalse)
       {
         mark_t i = 0U;
-        acc_code c;
+        acc_code f;
         while (cube != bddtrue)
           {
             // The acceptance set associated to this BDD variable
@@ -928,8 +928,7 @@ namespace spot
                 // The strange order here make sure we can smaller set
                 // numbers at the end of the acceptance code, i.e., at
                 // the front of the output.
-                auto a = fin(s) & std::move(c);
-                std::swap(a, c);
+                f = fin(s) & f;
               }
             else                // Positive variable? -> Inf
               {
@@ -937,10 +936,8 @@ namespace spot
                 cube = h;
               }
           }
-        c &= inf(i);
         // See comment above for the order.
-        c |= std::move(rescode);
-        std::swap(c, rescode);
+        rescode = (inf(i) & f) | rescode;
       }
 
     return rescode;
@@ -986,7 +983,7 @@ namespace spot
     while ((cube = isop.next()) != bddfalse)
       {
         mark_t m = 0U;
-        acc_code c = f();
+        acc_code i = f();
         while (cube != bddtrue)
           {
             // The acceptance set associated to this BDD variable
@@ -1000,8 +997,7 @@ namespace spot
                 // The strange order here make sure we can smaller set
                 // numbers at the end of the acceptance code, i.e., at
                 // the front of the output.
-                auto a = inf(s) | std::move(c);
-                std::swap(a, c);
+                i = inf(s) | i;
               }
             else                // Positive variable? -> Fin
               {
@@ -1009,10 +1005,8 @@ namespace spot
                 cube = h;
               }
           }
-        c |= fin(m);
         // See comment above for the order.
-        c &= std::move(rescode);
-        std::swap(c, rescode);
+        rescode = (fin(m) | i) & rescode;
       }
     return rescode;
   }
diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index eb1c0f67b..b552e907c 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -578,11 +578,11 @@ namespace spot
         unsigned n = 0;
         for (Iterator i = begin; i != end; ++i)
           {
-            acc_cond::acc_code pair = fin({n++});
+            unsigned f = n++;
             acc_cond::mark_t m = 0U;
             for (unsigned ni = *i; ni > 0; --ni)
               m.set(n++);
-            pair &= inf(m);
+            auto pair = inf(m) & fin({f});
             std::swap(pair, res);
             res |= std::move(pair);
           }
@@ -596,100 +596,6 @@ namespace spot
       // acceptance formula.
       static acc_code random(unsigned n, double reuse = 0.0);
 
-      acc_code& operator&=(acc_code&& r)
-      {
-        if (is_t() || r.is_f())
-          {
-            *this = std::move(r);
-            return *this;
-          }
-        if (is_f() || r.is_t())
-          return *this;
-        unsigned s = size() - 1;
-        unsigned rs = r.size() - 1;
-        // We want to group all Inf(x) operators:
-        //   Inf(a) & Inf(b) = Inf(a & b)
-        if (((*this)[s].sub.op == acc_op::Inf
-             && r[rs].sub.op == acc_op::Inf)
-            || ((*this)[s].sub.op == acc_op::InfNeg
-                && r[rs].sub.op == acc_op::InfNeg))
-          {
-            (*this)[s - 1].mark |= r[rs - 1].mark;
-            return *this;
-          }
-
-        // In the more complex scenarios, left and right may both
-        // be conjunctions, and Inf(x) might be a member of each
-        // side.  Find it if it exists.
-        // left_inf points to the left Inf mark if any.
-        // right_inf points to the right Inf mark if any.
-        acc_word* left_inf = nullptr;
-        if ((*this)[s].sub.op == acc_op::And)
-          {
-            auto start = &(*this)[s] - (*this)[s].sub.size;
-            auto pos = &(*this)[s] - 1;
-            pop_back();
-            while (pos > start)
-              {
-                if (pos->sub.op == acc_op::Inf)
-                  {
-                    left_inf = pos - 1;
-                    break;
-                  }
-                pos -= pos->sub.size + 1;
-              }
-          }
-        else if ((*this)[s].sub.op == acc_op::Inf)
-          {
-            left_inf = &(*this)[s - 1];
-          }
-
-        acc_word* right_inf = nullptr;
-        auto right_end = &r.back();
-        if (right_end->sub.op == acc_op::And)
-          {
-            auto start = &r[0];
-            auto pos = --right_end;
-            while (pos > start)
-            {
-              if (pos->sub.op == acc_op::Inf)
-                {
-                  right_inf = pos - 1;
-                  break;
-                }
-              pos -= pos->sub.size + 1;
-            }
-          }
-        else if (right_end->sub.op == acc_op::Inf)
-          {
-            right_inf = right_end - 1;
-          }
-
-        if (left_inf && right_inf)
-          {
-            left_inf->mark |= right_inf->mark;
-            insert(this->end(), &r[0], right_inf);
-            insert(this->end(), right_inf + 2, right_end + 1);
-          }
-        else if (right_inf)
-          {
-            // Always insert Inf() at the very first entry.
-            insert(this->begin(), right_inf, right_inf + 2);
-            insert(this->end(), &r[0], right_inf);
-            insert(this->end(), right_inf + 2, right_end + 1);
-          }
-        else
-          {
-            insert(this->end(), &r[0], right_end + 1);
-          }
-
-        acc_word w;
-        w.sub.op = acc_op::And;
-        w.sub.size = size();
-        emplace_back(w);
-        return *this;
-      }
-
       acc_code& operator&=(const acc_code& r)
       {
         if (is_t() || r.is_f())
@@ -701,7 +607,8 @@ namespace spot
           return *this;
         unsigned s = size() - 1;
         unsigned rs = r.size() - 1;
-        // Inf(a) & Inf(b) = Inf(a & b)
+        // We want to group all Inf(x) operators:
+        //   Inf(a) & Inf(b) = Inf(a & b)
         if (((*this)[s].sub.op == acc_op::Inf
              && r[rs].sub.op == acc_op::Inf)
             || ((*this)[s].sub.op == acc_op::InfNeg
@@ -758,23 +665,17 @@ namespace spot
             right_inf = right_end - 1;
           }
 
+        acc_cond::mark_t carry = 0U;
         if (left_inf && right_inf)
           {
-            left_inf->mark |= right_inf->mark;
-            insert(this->end(), &r[0], right_inf);
-            insert(this->end(), right_inf + 2, right_end + 1);
-          }
-        else if (right_inf)
-          {
-            // Always insert Inf() at the very first entry.
-            insert(this->begin(), right_inf, right_inf + 2);
-            insert(this->end(), &r[0], right_inf);
-            insert(this->end(), right_inf + 2, right_end + 1);
-          }
-        else
-          {
-            insert(this->end(), &r[0], right_end + 1);
+            carry = left_inf->mark;
+            auto pos = left_inf - &(*this)[0];
+            erase(begin() + pos, begin() + pos + 2);
           }
+        auto sz = size();
+        insert(end(), &r[0], right_end + 1);
+        if (carry)
+          (*this)[sz + (right_inf - &r[0])].mark |= carry;
 
         acc_word w;
         w.sub.op = acc_op::And;
@@ -783,6 +684,11 @@ namespace spot
         return *this;
       }
 
+      acc_code operator&(const acc_code& r)
+      {
+        return *this &= r;
+      }
+
       acc_code operator&(acc_code&& r)
       {
         acc_code res = *this;
@@ -790,20 +696,13 @@ namespace spot
         return res;
       }
 
-      acc_code operator&(const acc_code& r)
-      {
-        acc_code res = *this;
-        res &= r;
-        return res;
-      }
-
-      acc_code& operator|=(acc_code&& r)
+      acc_code& operator|=(const acc_code& r)
       {
         if (is_t() || r.is_f())
           return *this;
         if (is_f() || r.is_t())
           {
-            *this = std::move(r);
+            *this = r;
             return *this;
           }
         unsigned s = size() - 1;
@@ -817,11 +716,65 @@ namespace spot
             (*this)[s - 1].mark |= r[rs - 1].mark;
             return *this;
           }
+
+        // In the more complex scenarios, left and right may both
+        // be disjunctions, and Fin(x) might be a member of each
+        // side.  Find it if it exists.
+        // left_inf points to the left Inf mark if any.
+        // right_inf points to the right Inf mark if any.
+        acc_word* left_fin = nullptr;
         if ((*this)[s].sub.op == acc_op::Or)
-          pop_back();
-        if (r.back().sub.op == acc_op::Or)
-          r.pop_back();
-        insert(this->end(), r.begin(), r.end());
+          {
+            auto start = &(*this)[s] - (*this)[s].sub.size;
+            auto pos = &(*this)[s] - 1;
+            pop_back();
+            while (pos > start)
+              {
+                if (pos->sub.op == acc_op::Fin)
+                  {
+                    left_fin = pos - 1;
+                    break;
+                  }
+                pos -= pos->sub.size + 1;
+              }
+          }
+        else if ((*this)[s].sub.op == acc_op::Fin)
+          {
+            left_fin = &(*this)[s - 1];
+          }
+
+        const acc_word* right_fin = nullptr;
+        auto right_end = &r.back();
+        if (right_end->sub.op == acc_op::Or)
+          {
+            auto start = &r[0];
+            auto pos = --right_end;
+            while (pos > start)
+            {
+              if (pos->sub.op == acc_op::Fin)
+                {
+                  right_fin = pos - 1;
+                  break;
+                }
+              pos -= pos->sub.size + 1;
+            }
+          }
+        else if (right_end->sub.op == acc_op::Fin)
+          {
+            right_fin = right_end - 1;
+          }
+
+        acc_cond::mark_t carry = 0U;
+        if (left_fin && right_fin)
+          {
+            carry = left_fin->mark;
+            auto pos = (left_fin - &(*this)[0]);
+            this->erase(begin() + pos, begin() + pos + 2);
+          }
+        auto sz = size();
+        insert(end(), &r[0], right_end + 1);
+        if (carry)
+          (*this)[sz + (right_fin - &r[0])].mark |= carry;
         acc_word w;
         w.sub.op = acc_op::Or;
         w.sub.size = size();
@@ -829,11 +782,6 @@ namespace spot
         return *this;
       }
 
-      acc_code& operator|=(const acc_code& r)
-      {
-        return *this |= acc_code(r);
-      }
-
       acc_code operator|(acc_code&& r)
       {
         acc_code res = *this;
@@ -841,11 +789,9 @@ namespace spot
         return res;
       }
 
-      acc_code operator|(const acc_code& r)
+      acc_code& operator|(const acc_code& r)
       {
-        acc_code res = *this;
-        res |= r;
-        return res;
+        return *this |= r;
       }
 
       acc_code& operator<<=(unsigned sets)
diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc
index 44018de30..2d9233a31 100644
--- a/spot/twaalgos/cleanacc.cc
+++ b/spot/twaalgos/cleanacc.cc
@@ -193,8 +193,7 @@ namespace spot
               for (auto m: seen_fin.sets())
                 inf.front().mark -= complement[m];
 
-              res &= inf;
-              return res;
+              return inf & res;
             }
           case acc_cond::acc_op::Or:
             {
@@ -225,8 +224,7 @@ namespace spot
               for (auto m: seen_inf.sets())
                 fin.front().mark -= complement[m];
 
-              res |= fin;
-              return res;
+              return res | fin;
             }
           case acc_cond::acc_op::Fin:
             return acc_cond::acc_code::fin(pos[-1].mark);
diff --git a/tests/core/acc.test b/tests/core/acc.test
index 634244dcf..223675ba2 100755
--- a/tests/core/acc.test
+++ b/tests/core/acc.test
@@ -64,12 +64,12 @@ stripping
 #1: {2}
 2 Inf(0)&Inf(1)&Inf(3) 1
 5 Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
-7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
-7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
-7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
-10 (Fin(0)|Fin(1)) & (Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))) 0
+5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
+5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
+5 (Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
+8 (Fin(0)|Fin(1)) & ((Fin(0)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3))) 0
 2 f 1
-9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
+5 (Fin(0)|Fin(1)|Fin(2)) | (Inf(0)&Inf(1)&Inf(3)) 1
 5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0
 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) {0} true
 {1}
@@ -82,9 +82,9 @@ f
 Fin(2)
 Inf(2)
 Fin(2) | Inf(2)
-Fin(2) & Inf(2)
-Fin(0) | (Fin(2) & Inf(1)) | Fin(3)
-Fin(0) | (Fin(2) & Inf(1)) | Fin(3)
+Inf(2) & Fin(2)
+(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))
+(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))
 EOF
 
 run 0 ../acc | tee stdout
diff --git a/tests/core/acc2.test b/tests/core/acc2.test
index ba5c2ae67..95116bce5 100755
--- a/tests/core/acc2.test
+++ b/tests/core/acc2.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -71,13 +71,13 @@ diff acceptances output
 
 #------------- CNF -------------
 
-res="(Fin(2) | Inf(1)) & (Fin(1) | Inf(3)) & Inf(0)"
+res="Inf(0) & (Inf(1) | Fin(2)) & (Inf(3) | Fin(1))"
 cat >acceptances<<EOF
 2 Inf(0)&Inf(1), 2 Inf(0)&Inf(1)
 2 Fin(0) & Inf(1), 2 Fin(0) & Inf(1)
 2 t, 2 t
 2 f, 2 f
-3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(2) | Inf(1)) & Inf(0)
+3 (Inf(1) | Fin(2)) & Inf(0), 3 Inf(0) & (Inf(1) | Fin(2))
 4 (Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3)), 4 $res
 4 $res, 4 $res
 3 (Fin(0) & Fin(2)) | (Fin(1) & Fin(2)), 3 (Fin(0)|Fin(1)) & Fin(2)
@@ -94,7 +94,7 @@ diff acceptances output
 #------------- COMP -------------
 
 a="(Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)"
-b="(Fin(1) & Inf(2)) | (Fin(3) & Inf(1)) | Fin(0)"
+b="(Fin(1) & Inf(2)) | (Inf(1) & Fin(3)) | Fin(0)"
 cat >acceptances<<EOF
 2 Inf(0)&Inf(1), 2 Fin(0)|Fin(1)
 2 Fin(0) & Inf(1), 2 Inf(0) | Fin(1)
@@ -102,7 +102,7 @@ cat >acceptances<<EOF
 2 f, 2 t
 3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(1) & Inf(2)) | Fin(0)
 4 $a, 4 $b
-4 $b, 4 (Inf(1) | Fin(2)) & (Inf(3) | Fin(1)) & Inf(0)
+4 $b, 4 (Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)
 3 (Fin(0)|Fin(1)) & Fin(2), 3 (Inf(0)&Inf(1)) | Inf(2)
 EOF
 
diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test
index ae39ed017..1aa5114e4 100755
--- a/tests/core/parseaut.test
+++ b/tests/core/parseaut.test
@@ -2508,7 +2508,7 @@ HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 4 (Fin(1) & Inf(0)) | (Fin(3) & Inf(2))
+Acceptance: 4 (Inf(0) & Fin(1)) | (Inf(2) & Fin(3))
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic
 --BODY--
@@ -2522,7 +2522,7 @@ HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 4 (Fin(3) & Inf(2)) | (Fin(1) & Inf(0))
+Acceptance: 4 (Fin(3) & Inf(2)) | (Inf(0) & Fin(1))
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic
 --BODY--
@@ -2536,7 +2536,7 @@ HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 6 (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5)) & Inf(0)
+Acceptance: 6 Inf(0) & (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5))
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic
 --BODY--
@@ -2550,7 +2550,7 @@ HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 6 (Inf(4) | Fin(5)) & (Inf(1) | (Fin(2)|Fin(3))) & Inf(0)
+Acceptance: 6 (Fin(5) | Inf(4)) & Inf(0) & ((Fin(2)|Fin(3)) | Inf(1))
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic
 --BODY--
@@ -2624,7 +2624,7 @@ HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 4 Fin(0) & ((Fin(2) & Inf(3)) | Inf(1))
+Acceptance: 4 Fin(0) & ((Inf(3) & Fin(2)) | Inf(1))
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic
 --BODY--
diff --git a/tests/core/readsave.test b/tests/core/readsave.test
index cb2465fd2..1478d65c4 100755
--- a/tests/core/readsave.test
+++ b/tests/core/readsave.test
@@ -470,7 +470,7 @@ EOF
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)"
+  label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))"
   labelloc="t"
   I [label="", style=invis, width=0]
   I -> 0
@@ -524,7 +524,7 @@ diff out expected
 cat >expected2 <<EOF
 digraph G {
   rankdir=LR
-  label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)"
+  label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))"
   labelloc="t"
   node [shape="circle"]
   I [label="", style=invis, width=0]
diff --git a/tests/core/satmin2.test b/tests/core/satmin2.test
index dd24c90a9..3a5cbe150 100755
--- a/tests/core/satmin2.test
+++ b/tests/core/satmin2.test
@@ -335,7 +335,7 @@ HOA: v1
 States: 1
 Start: 0
 AP: 1 "a"
-Acceptance: 2 (Fin(1) & Inf(0)) | (Fin(0) & Inf(1))
+Acceptance: 2 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))
 properties: trans-labels explicit-labels trans-acc colored complete
 properties: deterministic
 --BODY--
diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test
index b35415186..38c7124bc 100755
--- a/tests/core/sccdot.test
+++ b/tests/core/sccdot.test
@@ -74,7 +74,7 @@ run 0 autfilt --dot=as in.hoa > out.dot
 cat <<EOF >expected
 digraph G {
   rankdir=LR
-  label="Fin(2) & (Inf(0)&Inf(1))"
+  label="(Inf(0)&Inf(1)) & Fin(2)"
   labelloc="t"
   node [shape="circle"]
   I [label="", style=invis, width=0]
@@ -156,7 +156,7 @@ HOA: v1
 States: 8
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 3 Fin(2) & (Inf(0)&Inf(1))
+Acceptance: 3 (Inf(0)&Inf(1)) & Fin(2)
 properties: trans-labels explicit-labels trans-acc
 --BODY--
 State: 0
diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb
index c371ba95b..759b8fa99 100644
--- a/tests/python/acc_cond.ipynb
+++ b/tests/python/acc_cond.ipynb
@@ -15,7 +15,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.5.3"
+   "version": "3.5.3+"
   },
   "name": ""
  },
@@ -489,7 +489,7 @@
        "output_type": "pyout",
        "prompt_number": 17,
        "text": [
-        "(Fin(1) & Inf(0)) | Inf(2)"
+        "(Inf(0) & Fin(1)) | Inf(2)"
        ]
       }
      ],
@@ -571,7 +571,7 @@
        "output_type": "pyout",
        "prompt_number": 20,
        "text": [
-        "(Fin(3) | Inf(1)) & (Fin(0)|Fin(2)) & Inf(4)"
+        "(Fin(3) | Inf(1)) & Inf(4) & (Fin(0)|Fin(2))"
        ]
       }
      ],
@@ -619,7 +619,7 @@
        "output_type": "pyout",
        "prompt_number": 22,
        "text": [
-        "Fin(0) & (Fin(2) | Inf(1)) & (Fin(4) | Inf(1) | Inf(3))"
+        "Fin(0) & (Inf(1) | Fin(2)) & (Inf(1) | Inf(3) | Fin(4))"
        ]
       }
      ],
@@ -720,8 +720,8 @@
        "output_type": "stream",
        "stream": "stdout",
        "text": [
-        "(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\n",
-        "(Inf(0) | Fin(1)) & (Inf(2) | Fin(3))\n"
+        "((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) & ((Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n",
+        "((Inf(4) | Fin(5)) & (Inf(6) | Fin(7))) | ((Inf(0) | Fin(1)) & (Inf(2) | Fin(3)))\n"
        ]
       }
      ],
diff --git a/tests/python/accparse.ipynb b/tests/python/accparse.ipynb
index 3b6c6ca63..734e3e848 100644
--- a/tests/python/accparse.ipynb
+++ b/tests/python/accparse.ipynb
@@ -15,10 +15,9 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.4.3+"
+   "version": "3.5.3+"
   },
-  "name": "",
-  "signature": "sha256:1ee7951bed30652ae110a14b210541829221552eb944ff01f25236179673dd5b"
+  "name": ""
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -51,7 +50,7 @@
        "output_type": "pyout",
        "prompt_number": 2,
        "text": [
-        "(Fin(1) & Inf(0)) | (Fin(3) & Inf(2))"
+        "(Inf(0) & Fin(1)) | (Inf(2) & Fin(3))"
        ]
       }
      ],
@@ -91,7 +90,7 @@
        "output_type": "pyout",
        "prompt_number": 4,
        "text": [
-        "(Inf(0) | Inf(2)) & (Fin(3) | Inf(0)) & (Fin(1) | Inf(2)) & (Fin(1)|Fin(3))"
+        "(Inf(0) | Inf(2)) & (Inf(0) | Fin(3)) & (Inf(2) | Fin(1)) & (Fin(1)|Fin(3))"
        ]
       }
      ],
@@ -174,4 +173,4 @@
    "metadata": {}
   }
  ]
-}
\ No newline at end of file
+}
diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb
index d3e5cc8f0..336f0f3ee 100644
--- a/tests/python/automata.ipynb
+++ b/tests/python/automata.ipynb
@@ -15,7 +15,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.5.3"
+   "version": "3.5.3+"
   },
   "name": ""
  },
@@ -177,7 +177,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae817a8d0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1ff810> >"
        ]
       }
      ],
@@ -569,7 +569,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816aa20> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1ff720> >"
        ]
       }
      ],
@@ -639,7 +639,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a4b0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18dbd0> >"
        ]
       }
      ],
@@ -715,7 +715,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a300> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d150> >"
        ]
       }
      ],
@@ -1175,7 +1175,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a9f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18df00> >"
        ]
       }
      ],
@@ -1276,7 +1276,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a870> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18df30> >"
        ]
       }
      ],
@@ -1394,7 +1394,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a690> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d660> >"
        ]
       }
      ],
@@ -1493,7 +1493,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a6f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d870> >"
        ]
       }
      ],
@@ -1963,7 +1963,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816a3f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18ddb0> >"
        ]
       }
      ],
@@ -2056,12 +2056,12 @@
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 174.462)\">\n",
         "<title>G</title>\n",
         "<polygon fill=\"white\" points=\"-4,4 -4,-174.462 357,-174.462 357,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-156.262\">(Fin(</text>\n",
-        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"36\" y=\"-156.262\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"52\" y=\"-156.262\">) &amp; Fin(</text>\n",
-        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-156.262\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"114\" y=\"-156.262\">) &amp; Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157\" y=\"-156.262\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-156.262\">(Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"33\" y=\"-156.262\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"49\" y=\"-156.262\">) &amp; Fin(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"95\" y=\"-156.262\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"111\" y=\"-156.262\">) &amp; Fin(</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"157\" y=\"-156.262\">\u2778</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"173\" y=\"-156.262\">)) | (Inf(</text>\n",
         "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"217\" y=\"-156.262\">\u2777</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"233\" y=\"-156.262\">)&amp;Inf(</text>\n",
@@ -2578,7 +2578,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae817a3f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18de10> >"
        ]
       }
      ],
@@ -2734,7 +2734,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816aab0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18d7b0> >"
        ]
       }
      ],
@@ -2804,7 +2804,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816ae10> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c18de10> >"
        ]
       }
      ],
@@ -3231,7 +3231,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae816af60> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a9450> >"
        ]
       },
       {
@@ -3399,7 +3399,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae81250f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a90c0> >"
        ]
       }
      ],
@@ -3488,7 +3488,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae81250f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a90c0> >"
        ]
       }
      ],
@@ -3577,7 +3577,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9ae81250f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f364c1a90c0> >"
        ]
       }
      ],
diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb
index 083b7212f..f3ea42b02 100644
--- a/tests/python/product.ipynb
+++ b/tests/python/product.ipynb
@@ -15,7 +15,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.5.3"
+   "version": "3.5.3+"
   },
   "name": ""
  },
@@ -1191,60 +1191,64 @@
      "outputs": [
       {
        "html": [
-        "<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 99.00 294.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 170.00 294.00\" width=\"170pt\" 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 290)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-290 95,-290 95,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-271.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-271.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-271.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-290 166,-290 166,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-271.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30\" y=\"-271.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46\" y=\"-271.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"82\" y=\"-271.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-271.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"134\" y=\"-271.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"150\" y=\"-271.8\">)</text>\n",
         "<!-- I -->\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node2\"><title>1</title>\n",
-        "<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
+        "<ellipse cx=\"53.5\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-203.3\">1</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;1</title>\n",
-        "<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
+        "<path d=\"M53.5,-261.845C53.5,-260.206 53.5,-245.846 53.5,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"53.5,-225.058 56.6501,-232.058 53.5,-228.558 53.5001,-232.058 53.5001,-232.058 53.5001,-232.058 53.5,-228.558 50.3501,-232.058 53.5,-225.058 53.5,-225.058\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node3\"><title>0</title>\n",
-        "<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
+        "<ellipse cx=\"53.5\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-116.3\">0</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
-        "<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
+        "<path d=\"M53.5,-188.799C53.5,-176.356 53.5,-159.364 53.5,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"53.5,-138.175 56.6501,-145.175 53.5,-141.675 53.5001,-145.175 53.5001,-145.175 53.5001,-145.175 53.5,-141.675 50.3501,-145.175 53.5,-138.175 53.5,-138.175\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"58\" y=\"-159.8\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a &amp; !b</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
+        "<path d=\"M70.1641,-127.383C80.125,-129.023 89.5,-126.562 89.5,-120 89.5,-115.078 84.2266,-112.463 77.3876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"70.1641,-112.617 76.949,-109.027 73.6569,-112.394 77.1498,-112.171 77.1498,-112.171 77.1498,-112.171 73.6569,-112.394 77.3507,-115.314 70.1641,-112.617 70.1641,-112.617\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-123.8\">a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-108.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node4\"><title>2</title>\n",
-        "<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
+        "<ellipse cx=\"53.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-14.3\">2</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
+        "<path d=\"M53.5,-101.581C53.5,-85.5213 53.5,-61.5179 53.5,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"53.5,-36.2191 56.6501,-43.219 53.5,-39.7191 53.5001,-43.2191 53.5001,-43.2191 53.5001,-43.2191 53.5,-39.7191 50.3501,-43.2191 53.5,-36.2191 53.5,-36.2191\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57\" y=\"-72.8\">b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.5\" y=\"-57.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>2-&gt;2</title>\n",
-        "<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
+        "<path d=\"M69.416,-26.6334C79.6504,-28.8856 89.5,-26.0078 89.5,-18 89.5,-11.869 83.7263,-8.74515 76.4268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"69.416,-9.36658 76.0477,-5.50081 72.8968,-9.00004 76.3775,-8.6335 76.3775,-8.6335 76.3775,-8.6335 72.8968,-9.00004 76.7074,-11.7662 69.416,-9.36658 69.416,-9.36658\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93\" y=\"-21.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-6.8\">\u24ff</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg></td><td style=\"vertical-align: top;\"><svg height=\"207pt\" viewBox=\"0.00 0.00 208.07 207.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
@@ -1698,60 +1702,64 @@
      "outputs": [
       {
        "html": [
-        "<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 99.00 294.00\" width=\"99pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<table><tr><td style=\"vertical-align: top;\"><svg height=\"294pt\" viewBox=\"0.00 0.00 170.00 294.00\" width=\"170pt\" 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 290)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-290 95,-290 95,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"24.5\" y=\"-271.8\">Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46.5\" y=\"-271.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"62.5\" y=\"-271.8\">)</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-290 166,-290 166,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"8\" y=\"-271.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"30\" y=\"-271.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"46\" y=\"-271.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"82\" y=\"-271.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-271.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"134\" y=\"-271.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"150\" y=\"-271.8\">)</text>\n",
         "<!-- I -->\n",
         "<!-- 1 -->\n",
         "<g class=\"node\" id=\"node2\"><title>1</title>\n",
-        "<ellipse cx=\"18\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-203.3\">1</text>\n",
+        "<ellipse cx=\"53.5\" cy=\"-207\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-203.3\">1</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;1 -->\n",
         "<g class=\"edge\" id=\"edge1\"><title>I-&gt;1</title>\n",
-        "<path d=\"M18,-261.845C18,-260.206 18,-245.846 18,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"18,-225.058 21.1501,-232.058 18,-228.558 18.0001,-232.058 18.0001,-232.058 18.0001,-232.058 18,-228.558 14.8501,-232.058 18,-225.058 18,-225.058\" stroke=\"black\"/>\n",
+        "<path d=\"M53.5,-261.845C53.5,-260.206 53.5,-245.846 53.5,-232.368\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"53.5,-225.058 56.6501,-232.058 53.5,-228.558 53.5001,-232.058 53.5001,-232.058 53.5001,-232.058 53.5,-228.558 50.3501,-232.058 53.5,-225.058 53.5,-225.058\" stroke=\"black\"/>\n",
         "</g>\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node3\"><title>0</title>\n",
-        "<ellipse cx=\"18\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-116.3\">0</text>\n",
+        "<ellipse cx=\"53.5\" cy=\"-120\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-116.3\">0</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge4\"><title>1-&gt;0</title>\n",
-        "<path d=\"M18,-188.799C18,-176.356 18,-159.364 18,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"18,-138.175 21.1501,-145.175 18,-141.675 18.0001,-145.175 18.0001,-145.175 18.0001,-145.175 18,-141.675 14.8501,-145.175 18,-138.175 18,-138.175\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"22.5\" y=\"-159.8\">1</text>\n",
+        "<path d=\"M53.5,-188.799C53.5,-176.356 53.5,-159.364 53.5,-145.504\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"53.5,-138.175 56.6501,-145.175 53.5,-141.675 53.5001,-145.175 53.5001,-145.175 53.5001,-145.175 53.5,-141.675 50.3501,-145.175 53.5,-138.175 53.5,-138.175\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"58\" y=\"-159.8\">1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;0 -->\n",
         "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
-        "<path d=\"M34.6641,-127.383C44.625,-129.023 54,-126.562 54,-120 54,-115.078 48.7266,-112.463 41.8876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"34.6641,-112.617 41.449,-109.027 38.1569,-112.394 41.6498,-112.171 41.6498,-112.171 41.6498,-112.171 38.1569,-112.394 41.8507,-115.314 34.6641,-112.617 34.6641,-112.617\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-123.8\">a &amp; !b</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"64.5\" y=\"-108.8\">\u24ff</text>\n",
+        "<path d=\"M70.1641,-127.383C80.125,-129.023 89.5,-126.562 89.5,-120 89.5,-115.078 84.2266,-112.463 77.3876,-112.156\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"70.1641,-112.617 76.949,-109.027 73.6569,-112.394 77.1498,-112.171 77.1498,-112.171 77.1498,-112.171 73.6569,-112.394 77.3507,-115.314 70.1641,-112.617 70.1641,-112.617\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-123.8\">a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"100\" y=\"-108.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g class=\"node\" id=\"node4\"><title>2</title>\n",
-        "<ellipse cx=\"18\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"18\" y=\"-14.3\">2</text>\n",
+        "<ellipse cx=\"53.5\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"53.5\" y=\"-14.3\">2</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M18,-101.581C18,-85.5213 18,-61.5179 18,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"18,-36.2191 21.1501,-43.219 18,-39.7191 18.0001,-43.2191 18.0001,-43.2191 18.0001,-43.2191 18,-39.7191 14.8501,-43.2191 18,-36.2191 18,-36.2191\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"21.5\" y=\"-72.8\">b</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"18\" y=\"-57.8\">\u24ff</text>\n",
+        "<path d=\"M53.5,-101.581C53.5,-85.5213 53.5,-61.5179 53.5,-43.5228\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"53.5,-36.2191 56.6501,-43.219 53.5,-39.7191 53.5001,-43.2191 53.5001,-43.2191 53.5001,-43.2191 53.5,-39.7191 50.3501,-43.2191 53.5,-36.2191 53.5,-36.2191\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57\" y=\"-72.8\">b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"53.5\" y=\"-57.8\">\u24ff</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g class=\"edge\" id=\"edge5\"><title>2-&gt;2</title>\n",
-        "<path d=\"M33.916,-26.6334C44.1504,-28.8856 54,-26.0078 54,-18 54,-11.869 48.2263,-8.74515 40.9268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"33.916,-9.36658 40.5477,-5.50081 37.3968,-9.00004 40.8775,-8.6335 40.8775,-8.6335 40.8775,-8.6335 37.3968,-9.00004 41.2074,-11.7662 33.916,-9.36658 33.916,-9.36658\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57.5\" y=\"-21.8\">1</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-6.8\">\u24ff</text>\n",
+        "<path d=\"M69.416,-26.6334C79.6504,-28.8856 89.5,-26.0078 89.5,-18 89.5,-11.869 83.7263,-8.74515 76.4268,-8.6284\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"69.416,-9.36658 76.0477,-5.50081 72.8968,-9.00004 76.3775,-8.6335 76.3775,-8.6335 76.3775,-8.6335 72.8968,-9.00004 76.7074,-11.7662 69.416,-9.36658 69.416,-9.36658\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"93\" y=\"-21.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"89.5\" y=\"-6.8\">\u24ff</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg></td><td style=\"vertical-align: top;\"><svg height=\"207pt\" viewBox=\"0.00 0.00 208.07 207.00\" width=\"208pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
@@ -2021,7 +2029,7 @@
        ]
       }
      ],
-     "prompt_number": 14
+     "prompt_number": 9
     },
     {
      "cell_type": "markdown",
@@ -2045,7 +2053,7 @@
        "output_type": "stream",
        "stream": "stdout",
        "text": [
-        "1000 loops, best of 3: 202 \u00b5s per loop\n"
+        "1000 loops, best of 3: 209 \u00b5s per loop\n"
        ]
       }
      ],
@@ -2064,8 +2072,8 @@
        "output_type": "stream",
        "stream": "stdout",
        "text": [
-        "The slowest run took 5.71 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
-        "100000 loops, best of 3: 4.39 \u00b5s per loop\n"
+        "The slowest run took 5.67 times longer than the fastest. This could mean that an intermediate result is being cached.\n",
+        "100000 loops, best of 3: 4.62 \u00b5s per loop\n"
        ]
       }
      ],
diff --git a/tests/python/randaut.ipynb b/tests/python/randaut.ipynb
index 4e24bd65b..03ef404bc 100644
--- a/tests/python/randaut.ipynb
+++ b/tests/python/randaut.ipynb
@@ -15,10 +15,9 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.4.3+"
+   "version": "3.5.3+"
   },
-  "name": "",
-  "signature": "sha256:3e27359f7131b7b08ba2b01c8501a8f9c7c39c11a83133150d0a75de7bff2ef2"
+  "name": ""
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -38,6 +37,13 @@
      "outputs": [],
      "prompt_number": 1
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "This shows the effect of running `cleanup_acceptance()` on 10 randomly generated automata."
+     ]
+    },
     {
      "cell_type": "code",
      "collapsed": false,
@@ -49,7 +55,9 @@
       "HTML(txt)"
      ],
      "language": "python",
-     "metadata": {},
+     "metadata": {
+      "scrolled": false
+     },
      "outputs": [
       {
        "html": [
@@ -462,10 +470,10 @@
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.625905 0.625905) rotate(0) translate(4 172)\">\n",
         "<title>G</title>\n",
         "<polygon fill=\"white\" points=\"-4,4 -4,-172 617.5,-172 617.5,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"195.25\" y=\"-153.8\">(Fin(</text>\n",
-        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"223.25\" y=\"-153.8\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"239.25\" y=\"-153.8\">) &amp; Inf(</text>\n",
-        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.25\" y=\"-153.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"195.25\" y=\"-153.8\">(Inf(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.25\" y=\"-153.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.25\" y=\"-153.8\">) &amp; Fin(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.25\" y=\"-153.8\">\u2776</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"298.25\" y=\"-153.8\">)) | (Inf(</text>\n",
         "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.25\" y=\"-153.8\">\u24ff</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"358.25\" y=\"-153.8\">)&amp;Inf(</text>\n",
@@ -952,15 +960,15 @@
         "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.596626 0.596626) rotate(0) translate(4 295.049)\">\n",
         "<title>G</title>\n",
         "<polygon fill=\"white\" points=\"-4,4 -4,-295.049 648,-295.049 648,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212\" y=\"-276.849\">(Fin(</text>\n",
-        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"240\" y=\"-276.849\">\u2777</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"256\" y=\"-276.849\">) | Inf(</text>\n",
-        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"293\" y=\"-276.849\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"309\" y=\"-276.849\">) | Fin(</text>\n",
-        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"349\" y=\"-276.849\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"365\" y=\"-276.849\">)) &amp; Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"412\" y=\"-276.849\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"428\" y=\"-276.849\">)</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212.5\" y=\"-276.849\">((Fin(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"244.5\" y=\"-276.849\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"260.5\" y=\"-276.849\">)|Fin(</text>\n",
+        "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292.5\" y=\"-276.849\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"308.5\" y=\"-276.849\">)) | Inf(</text>\n",
+        "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"348.5\" y=\"-276.849\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"364.5\" y=\"-276.849\">)) &amp; Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"411.5\" y=\"-276.849\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"427.5\" y=\"-276.849\">)</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
@@ -2081,10 +2089,10 @@
         "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-137.8\">\u2777</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-137.8\">)|Fin(</text>\n",
         "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-137.8\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Fin(</text>\n",
-        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329.5\" y=\"-137.8\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"345.5\" y=\"-137.8\">) &amp; Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-137.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-137.8\">) &amp; Fin(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u2776</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-137.8\">))</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
@@ -2173,10 +2181,10 @@
         "<text fill=\"#faa43a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-137.8\">\u2777</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-137.8\">)|Fin(</text>\n",
         "<text fill=\"#b276b2\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-137.8\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Fin(</text>\n",
-        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"329.5\" y=\"-137.8\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"345.5\" y=\"-137.8\">) &amp; Inf(</text>\n",
-        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-137.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-137.8\">) &amp; Fin(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u2776</text>\n",
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-137.8\">))</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
@@ -2263,7 +2271,7 @@
        "output_type": "pyout",
        "prompt_number": 2,
        "text": [
-        "<IPython.core.display.HTML at 0x7f74a8298ac8>"
+        "<IPython.core.display.HTML object>"
        ]
       }
      ],
@@ -2282,4 +2290,4 @@
    "metadata": {}
   }
  ]
-}
\ No newline at end of file
+}