From ac0503526752a8a3351cf3cea49e1a3906543cbc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 7 Nov 2023 17:17:58 +0100
Subject: [PATCH] product_susp: fix handling of unsatisfiable/universal
 acceptances
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Part of issue #546 reported by Rüdiger Ehlers

* spot/twaalgos/product.cc (product_susp): Fix detection and handling
of unsatisfiable/universal acceptances.
* tests/python/_product_susp.ipynb: Add test cases.
---
 NEWS                             |    4 +
 spot/twaalgos/product.cc         |   49 +-
 tests/python/_product_susp.ipynb | 1269 +++++++++++++++++++++++++++++-
 3 files changed, 1265 insertions(+), 57 deletions(-)

diff --git a/NEWS b/NEWS
index cc61c1236..df7bf8dd3 100644
--- a/NEWS
+++ b/NEWS
@@ -112,6 +112,10 @@ New in spot 2.11.6.dev  (not yet released)
     (Issue #541.)  This has been fixed by disabled the use_simulation
     optimization in this case.
 
+  - product_or_susp() and product_susp() would behave incorrectly in
+    presence of unsatisifable or universal acceptance conditions that
+    were not f or t.  (Part of issue #546.)
+
 New in spot 2.11.6  (2023-08-01)
 
   Bug fixes:
diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc
index 243f3768c..b337a5a43 100644
--- a/spot/twaalgos/product.cc
+++ b/spot/twaalgos/product.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2020, 2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2020, 2022, 2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -607,33 +607,36 @@ namespace spot
         throw std::runtime_error("product_susp(): left and right automata "
                                  "should share their bdd_dict");
 
-      auto false_or_left = [&] (bool ff)
-        {
-          if (ff)
-            {
-              auto res = make_twa_graph(left->get_dict());
-              res->new_state();
-              res->prop_terminal(true);
-              res->prop_stutter_invariant(true);
-              res->prop_universal(true);
-              res->prop_complete(false);
-              return res;
-            }
-          return make_twa_graph(left, twa::prop_set::all());
-        };
+      auto const_automaton = [&left] (bool is_true)
+      {
+        auto res = make_twa_graph(left->get_dict());
+        res->new_state();
+        res->prop_terminal(true);
+        res->prop_stutter_invariant(true);
+        res->prop_universal(true);
+        res->prop_complete(is_true);
+        if (is_true)
+          res->new_edge(0, 0, bddtrue);
+        return res;
+      };
 
       // We assume RIGHT is suspendable, but we want to deal with some
       // trivial true/false cases so we can later assume right has
       // more than one acceptance set.
       // Note: suspendable with "t" acceptance = universal language.
-      if (SPOT_UNLIKELY(right->num_sets() == 0))
+      if (SPOT_UNLIKELY(right->num_sets() == 0
+                        || right->num_edges() == 0
+                        || right->acc().is_t()
+                        || right->acc().is_f()))
         {
-          if (and_acc)
-            return false_or_left(right->is_empty());
-          else if (right->is_empty()) // left OR false = left
+        trivial:
+          if (and_acc && right->is_empty())
+            return const_automaton(false);
+          else if (!and_acc && !right->is_empty())
+            // suspendable with "t" acceptance = universal language.
+            return const_automaton(true);
+          else // left AND true = left; left OR false = left
             return make_twa_graph(left, twa::prop_set::all());
-          else // left OR true = true
-            return make_twa_graph(right, twa::prop_set::all());
         }
 
       auto res = make_twa_graph(left->get_dict());
@@ -644,8 +647,8 @@ namespace spot
       res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc());
 
       auto rightunsatmark = right->acc().unsat_mark();
-      if (SPOT_UNLIKELY(!rightunsatmark.first))
-        return false_or_left(and_acc);
+      if (SPOT_UNLIKELY(!rightunsatmark.first)) // right is universal
+        goto trivial;
       acc_cond::mark_t rejmark = rightunsatmark.second;
 
       if (leftweak)
diff --git a/tests/python/_product_susp.ipynb b/tests/python/_product_susp.ipynb
index a0de91f95..cba4d3bf6 100644
--- a/tests/python/_product_susp.ipynb
+++ b/tests/python/_product_susp.ipynb
@@ -607,13 +607,15 @@
    "source": [
     "left = spot.translate('(Ga | Gb | Gc)')\n",
     "right = spot.translate('GFa')\n",
-    "test(left, right)\n"
+    "test(left, right)"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": 3,
-   "metadata": {},
+   "metadata": {
+    "scrolled": false
+   },
    "outputs": [
     {
      "data": {
@@ -624,11 +626,11 @@
        "<!-- Generated by graphviz version 2.43.0 (0)\n",
        " -->\n",
        "<!-- Pages: 1 -->\n",
-       "<svg width=\"293pt\" height=\"360pt\"\n",
-       " viewBox=\"0.00 0.00 292.50 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.8 0.8) rotate(0) translate(4 446.46)\">\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-446.46 362,-446.46 362,4 -4,4\"/>\n",
-       "<text text-anchor=\"start\" x=\"157.5\" y=\"-412.26\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<svg width=\"304pt\" height=\"360pt\"\n",
+       " viewBox=\"0.00 0.00 303.83 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.8333333333333334 0.8333333333333334) rotate(0) translate(4 429.66)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-429.66 362,-429.66 362,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"157.5\" y=\"-410.46\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 6 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
@@ -1129,11 +1131,11 @@
        "<!-- Generated by graphviz version 2.43.0 (0)\n",
        " -->\n",
        "<!-- Pages: 1 -->\n",
-       "<svg width=\"293pt\" height=\"360pt\"\n",
-       " viewBox=\"0.00 0.00 292.50 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.8 0.8) rotate(0) translate(4 446.46)\">\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-446.46 362,-446.46 362,4 -4,4\"/>\n",
-       "<text text-anchor=\"start\" x=\"157.5\" y=\"-412.26\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<svg width=\"304pt\" height=\"360pt\"\n",
+       " viewBox=\"0.00 0.00 303.83 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.8333333333333334 0.8333333333333334) rotate(0) translate(4 429.66)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-429.66 362,-429.66 362,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"157.5\" y=\"-410.46\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 6 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
@@ -1717,11 +1719,11 @@
        "<!-- Generated by graphviz version 2.43.0 (0)\n",
        " -->\n",
        "<!-- Pages: 1 -->\n",
-       "<svg width=\"173pt\" height=\"220pt\"\n",
-       " viewBox=\"0.00 0.00 173.00 219.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 215.8)\">\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-215.8 169,-215.8 169,4 -4,4\"/>\n",
-       "<text text-anchor=\"start\" x=\"61\" y=\"-181.6\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<svg width=\"173pt\" height=\"203pt\"\n",
+       " viewBox=\"0.00 0.00 173.00 203.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 199)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-199 169,-199 169,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"61\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
@@ -1932,11 +1934,11 @@
        "<!-- Generated by graphviz version 2.43.0 (0)\n",
        " -->\n",
        "<!-- Pages: 1 -->\n",
-       "<svg width=\"173pt\" height=\"220pt\"\n",
-       " viewBox=\"0.00 0.00 173.00 219.80\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 215.8)\">\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-215.8 169,-215.8 169,4 -4,4\"/>\n",
-       "<text text-anchor=\"start\" x=\"61\" y=\"-181.6\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<svg width=\"173pt\" height=\"203pt\"\n",
+       " viewBox=\"0.00 0.00 173.00 203.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 199)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-199 169,-199 169,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"61\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
@@ -2719,7 +2721,8 @@
     }
    ],
    "source": [
-    "test(spot.translate('(Ga | GF!a)', 'det', 'gen'), spot.translate('GF(a <-> !Xa)'))"
+    "a = spot.translate('(Ga | GF!a)', 'det', 'gen')\n",
+    "test(a, spot.translate('GF(a <-> !Xa)'))"
    ]
   },
   {
@@ -3089,13 +3092,1218 @@
     }
    ],
    "source": [
-    "test(spot.translate('(Ga | GF!a)'), spot.translate('true', 'monitor'))"
+    "a = spot.translate('(Ga | GF!a)')\n",
+    "tt = spot.translate('true', 'monitor')\n",
+    "test(a, tt)"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": 7,
    "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"92pt\" height=\"115pt\"\n",
+       " viewBox=\"0.00 0.00 92.00 115.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 111)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 88,-111 88,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"39\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"8\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[Fin&#45;less 1]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M67,-36C67,-36 55,-36 55,-36 49,-36 43,-30 43,-24 43,-24 43,-12 43,-12 43,-6 49,0 55,0 55,0 67,0 67,0 73,0 79,-6 79,-12 79,-12 79,-24 79,-24 79,-30 73,-36 67,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"61\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M6.15,-18C7.79,-18 22.15,-18 35.63,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"42.94,-18 35.94,-21.15 39.44,-18 35.94,-18 35.94,-18 35.94,-18 39.44,-18 35.94,-14.85 42.94,-18 42.94,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M54.49,-36.15C53.49,-45.54 55.66,-54 61,-54 64.92,-54 67.14,-49.44 67.64,-43.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"67.51,-36.15 70.79,-43.1 67.57,-39.65 67.64,-43.15 67.64,-43.15 67.64,-43.15 67.57,-39.65 64.49,-43.21 67.51,-36.15 67.51,-36.15\"/>\n",
+       "<text text-anchor=\"start\" x=\"56.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"92pt\" height=\"115pt\"\n",
+       " viewBox=\"0.00 0.00 92.00 115.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 111)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 88,-111 88,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"39\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"8\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[Fin&#45;less 1]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M67,-36C67,-36 55,-36 55,-36 49,-36 43,-30 43,-24 43,-24 43,-12 43,-12 43,-6 49,0 55,0 55,0 67,0 67,0 73,0 79,-6 79,-12 79,-12 79,-24 79,-24 79,-30 73,-36 67,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"61\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M6.15,-18C7.79,-18 22.15,-18 35.63,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"42.94,-18 35.94,-21.15 39.44,-18 35.94,-18 35.94,-18 35.94,-18 39.44,-18 35.94,-14.85 42.94,-18 42.94,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M54.49,-36.15C53.49,-45.54 55.66,-54 61,-54 64.92,-54 67.14,-49.44 67.64,-43.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"67.51,-36.15 70.79,-43.1 67.57,-39.65 67.64,-43.15 67.64,-43.15 67.64,-43.15 67.57,-39.65 64.49,-43.21 67.51,-36.15 67.51,-36.15\"/>\n",
+       "<text text-anchor=\"start\" x=\"56.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"82pt\" height=\"115pt\"\n",
+       " viewBox=\"0.00 0.00 82.00 115.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 111)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 78,-111 78,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"34\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"26\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.62,-35.04C48.32,-44.86 50.45,-54 56,-54 60.17,-54 62.4,-48.86 62.71,-42.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-35.04 65.85,-41.88 62.54,-38.53 62.71,-42.03 62.71,-42.03 62.71,-42.03 62.54,-38.53 59.56,-42.18 62.38,-35.04 62.38,-35.04\"/>\n",
+       "<text text-anchor=\"start\" x=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "tt.set_acceptance(spot.acc_cond(1, \"t\"))  # issue 546\n",
+    "test(a, tt)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"119pt\" height=\"113pt\"\n",
+       " viewBox=\"0.00 0.00 119.00 113.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 109)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-109 115,-109 115,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"8\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+       "<text text-anchor=\"start\" x=\"31\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"47\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">) | Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"83\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"99\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"11\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[Streett&#45;like 1]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M80.5,-36C80.5,-36 68.5,-36 68.5,-36 62.5,-36 56.5,-30 56.5,-24 56.5,-24 56.5,-12 56.5,-12 56.5,-6 62.5,0 68.5,0 68.5,0 80.5,0 80.5,0 86.5,0 92.5,-6 92.5,-12 92.5,-12 92.5,-24 92.5,-24 92.5,-30 86.5,-36 80.5,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"74.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M19.65,-18C21.29,-18 35.65,-18 49.13,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"56.44,-18 49.44,-21.15 52.94,-18 49.44,-18 49.44,-18 49.44,-18 52.94,-18 49.44,-14.85 56.44,-18 56.44,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M67.99,-36.15C66.99,-45.54 69.16,-54 74.5,-54 78.42,-54 80.64,-49.44 81.14,-43.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"81.01,-36.15 84.29,-43.1 81.07,-39.65 81.14,-43.15 81.14,-43.15 81.14,-43.15 81.07,-39.65 77.99,-43.21 81.01,-36.15 81.01,-36.15\"/>\n",
+       "<text text-anchor=\"start\" x=\"70\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"119pt\" height=\"113pt\"\n",
+       " viewBox=\"0.00 0.00 119.00 113.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 109)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-109 115,-109 115,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"8\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+       "<text text-anchor=\"start\" x=\"31\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"47\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">) | Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"83\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"99\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"11\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[Streett&#45;like 1]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M80.5,-36C80.5,-36 68.5,-36 68.5,-36 62.5,-36 56.5,-30 56.5,-24 56.5,-24 56.5,-12 56.5,-12 56.5,-6 62.5,0 68.5,0 68.5,0 80.5,0 80.5,0 86.5,0 92.5,-6 92.5,-12 92.5,-12 92.5,-24 92.5,-24 92.5,-30 86.5,-36 80.5,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"74.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M19.65,-18C21.29,-18 35.65,-18 49.13,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"56.44,-18 49.44,-21.15 52.94,-18 49.44,-18 49.44,-18 49.44,-18 52.94,-18 49.44,-14.85 56.44,-18 56.44,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M67.99,-36.15C66.99,-45.54 69.16,-54 74.5,-54 78.42,-54 80.64,-49.44 81.14,-43.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"81.01,-36.15 84.29,-43.1 81.07,-39.65 81.14,-43.15 81.14,-43.15 81.14,-43.15 81.07,-39.65 77.99,-43.21 81.01,-36.15 81.01,-36.15\"/>\n",
+       "<text text-anchor=\"start\" x=\"70\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"82pt\" height=\"115pt\"\n",
+       " viewBox=\"0.00 0.00 82.00 115.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 111)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 78,-111 78,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"34\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"26\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.62,-35.04C48.32,-44.86 50.45,-54 56,-54 60.17,-54 62.4,-48.86 62.71,-42.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-35.04 65.85,-41.88 62.54,-38.53 62.71,-42.03 62.71,-42.03 62.71,-42.03 62.54,-38.53 59.56,-42.18 62.38,-35.04 62.38,-35.04\"/>\n",
+       "<text text-anchor=\"start\" x=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "tt.set_acceptance(spot.acc_cond(1, \"Fin(1) | Inf(1)\"))  # issue 546\n",
+    "test(a, tt)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"125pt\" height=\"113pt\"\n",
+       " viewBox=\"0.00 0.00 125.00 113.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 109)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-109 121,-109 121,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"8\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+       "<text text-anchor=\"start\" x=\"31\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"47\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"89\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"105\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"18\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[Rabin&#45;like 1]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M83.5,-36C83.5,-36 71.5,-36 71.5,-36 65.5,-36 59.5,-30 59.5,-24 59.5,-24 59.5,-12 59.5,-12 59.5,-6 65.5,0 71.5,0 71.5,0 83.5,0 83.5,0 89.5,0 95.5,-6 95.5,-12 95.5,-12 95.5,-24 95.5,-24 95.5,-30 89.5,-36 83.5,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"77.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M22.65,-18C24.29,-18 38.65,-18 52.13,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"59.44,-18 52.44,-21.15 55.94,-18 52.44,-18 52.44,-18 52.44,-18 55.94,-18 52.44,-14.85 59.44,-18 59.44,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.99,-36.15C69.99,-45.54 72.16,-54 77.5,-54 81.42,-54 83.64,-49.44 84.14,-43.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"84.01,-36.15 87.29,-43.1 84.07,-39.65 84.14,-43.15 84.14,-43.15 84.14,-43.15 84.07,-39.65 80.99,-43.21 84.01,-36.15 84.01,-36.15\"/>\n",
+       "<text text-anchor=\"start\" x=\"73\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"183pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 183.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 179,-259 179,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"8\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">(Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"33\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"49\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"83\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
+       "<text text-anchor=\"start\" x=\"99\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)) &amp; Fin(</text>\n",
+       "<text text-anchor=\"start\" x=\"147\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
+       "<text text-anchor=\"start\" x=\"163\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"43\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Streett&#45;like 3]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"66\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"66\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M11.15,-85C12.79,-85 27.15,-85 40.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"47.94,-85 40.94,-88.15 44.44,-85 40.94,-85 40.94,-85 40.94,-85 44.44,-85 40.94,-81.85 47.94,-85 47.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"147\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"147\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M80.4,-96.54C93.3,-107.64 112.93,-124.54 127.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"132.8,-141.64 125.44,-139.46 130.14,-139.35 127.49,-137.07 127.49,-137.07 127.49,-137.07 130.14,-139.35 129.55,-134.68 132.8,-141.64 132.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"103\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"147\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"147\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M80.4,-73.63C93.3,-62.69 112.93,-46.05 127.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"132.8,-29.2 129.5,-36.13 130.13,-31.46 127.46,-33.73 127.46,-33.73 127.46,-33.73 130.13,-31.46 125.42,-31.32 132.8,-29.2 132.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"106.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M139.97,-169.66C138.41,-179.62 140.75,-189 147,-189 151.69,-189 154.18,-183.73 154.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"154.03,-169.66 157.6,-176.46 154.24,-173.16 154.46,-176.65 154.46,-176.65 154.46,-176.65 154.24,-173.16 151.31,-176.84 154.03,-169.66 154.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"143.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"139\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M143.4,-35.78C142.79,-45.31 143.99,-54 147,-54 149.21,-54 150.44,-49.32 150.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"150.6,-35.78 153.85,-42.74 150.65,-39.28 150.7,-42.78 150.7,-42.78 150.7,-42.78 150.65,-39.28 147.55,-42.83 150.6,-35.78 150.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"143.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M141.15,-35.14C137.71,-52.58 139.66,-72 147,-72 153.37,-72 155.68,-57.4 153.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"152.85,-35.14 157.04,-41.58 153.39,-38.6 153.92,-42.06 153.92,-42.06 153.92,-42.06 153.39,-38.6 150.81,-42.54 152.85,-35.14 152.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"141.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"139\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/html": [
+       "<div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"163pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 163.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 159,-259 159,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"57\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"78\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"94\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"56\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-56.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"125pt\" height=\"113pt\"\n",
+       " viewBox=\"0.00 0.00 125.00 113.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 109)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-109 121,-109 121,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"8\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
+       "<text text-anchor=\"start\" x=\"31\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"47\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"89\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
+       "<text text-anchor=\"start\" x=\"105\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+       "<text text-anchor=\"start\" x=\"18\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[Rabin&#45;like 1]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<path fill=\"#ffffaa\" stroke=\"black\" d=\"M83.5,-36C83.5,-36 71.5,-36 71.5,-36 65.5,-36 59.5,-30 59.5,-24 59.5,-24 59.5,-12 59.5,-12 59.5,-6 65.5,0 71.5,0 71.5,0 83.5,0 83.5,0 89.5,0 95.5,-6 95.5,-12 95.5,-12 95.5,-24 95.5,-24 95.5,-30 89.5,-36 83.5,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"77.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M22.65,-18C24.29,-18 38.65,-18 52.13,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"59.44,-18 52.44,-21.15 55.94,-18 52.44,-18 52.44,-18 52.44,-18 55.94,-18 52.44,-14.85 59.44,-18 59.44,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.99,-36.15C69.99,-45.54 72.16,-54 77.5,-54 81.42,-54 83.64,-49.44 84.14,-43.3\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"84.01,-36.15 87.29,-43.1 84.07,-39.65 84.14,-43.15 84.14,-43.15 84.14,-43.15 84.07,-39.65 80.99,-43.21 84.01,-36.15 84.01,-36.15\"/>\n",
+       "<text text-anchor=\"start\" x=\"73\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div><div style='vertical-align:text-top;display:inline-block;'><?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"246pt\" height=\"263pt\"\n",
+       " viewBox=\"0.00 0.00 246.00 263.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 259)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-259 242,-259 242,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"38.5\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"59.5\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "<text text-anchor=\"start\" x=\"75.5\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">) | (Fin(</text>\n",
+       "<text text-anchor=\"start\" x=\"117.5\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; Inf(</text>\n",
+       "<text text-anchor=\"start\" x=\"175.5\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
+       "<text text-anchor=\"start\" x=\"191.5\" y=\"-240.8\" font-family=\"Lato\" font-size=\"14.00\">))</text>\n",
+       "<text text-anchor=\"start\" x=\"78.5\" y=\"-226.8\" font-family=\"Lato\" font-size=\"14.00\">[Rabin&#45;like 2]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-85\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-81.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-85C2.79,-85 17.15,-85 30.63,-85\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-85 30.94,-88.15 34.44,-85 30.94,-85 30.94,-85 30.94,-85 34.44,-85 30.94,-81.85 37.94,-85 37.94,-85\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-96.54C83.3,-107.64 102.93,-124.54 117.36,-136.95\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-141.64 115.44,-139.46 120.14,-139.35 117.49,-137.07 117.49,-137.07 117.49,-137.07 120.14,-139.35 119.55,-134.68 122.8,-141.64 122.8,-141.64\"/>\n",
+       "<text text-anchor=\"start\" x=\"93\" y=\"-125.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"137\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M70.4,-73.63C83.3,-62.69 102.93,-46.05 117.36,-33.81\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"122.8,-29.2 119.5,-36.13 120.13,-31.46 117.46,-33.73 117.46,-33.73 117.46,-33.73 120.13,-31.46 115.42,-31.32 122.8,-29.2 122.8,-29.2\"/>\n",
+       "<text text-anchor=\"middle\" x=\"96.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;1 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M129.97,-169.66C128.41,-179.62 130.75,-189 137,-189 141.69,-189 144.18,-183.73 144.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.03,-169.66 147.6,-176.46 144.24,-173.16 144.46,-176.65 144.46,-176.65 144.46,-176.65 144.24,-173.16 141.31,-176.84 144.03,-169.66 144.03,-169.66\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"220\" cy=\"-153\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"220\" y=\"-149.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;3 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>1&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M155.18,-153C166.67,-153 181.96,-153 194.69,-153\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"201.85,-153 194.85,-156.15 198.35,-153 194.85,-153 194.85,-153 194.85,-153 198.35,-153 194.85,-149.85 201.85,-153 201.85,-153\"/>\n",
+       "<text text-anchor=\"start\" x=\"173\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-35.78C132.79,-45.31 133.99,-54 137,-54 139.21,-54 140.44,-49.32 140.7,-43.05\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"140.6,-35.78 143.85,-42.74 140.65,-39.28 140.7,-42.78 140.7,-42.78 140.7,-42.78 140.65,-39.28 137.55,-42.83 140.6,-35.78 140.6,-35.78\"/>\n",
+       "<text text-anchor=\"start\" x=\"133.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;2 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>2&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M131.15,-35.14C127.71,-52.58 129.66,-72 137,-72 143.37,-72 145.68,-57.4 143.94,-42.15\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"142.85,-35.14 147.04,-41.58 143.39,-38.6 143.92,-42.06 143.92,-42.06 143.92,-42.06 143.39,-38.6 140.81,-42.54 142.85,-35.14 142.85,-35.14\"/>\n",
+       "<text text-anchor=\"start\" x=\"131.5\" y=\"-90.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+       "<text text-anchor=\"start\" x=\"129\" y=\"-75.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;3 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>3&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M212.97,-169.66C211.41,-179.62 213.75,-189 220,-189 224.69,-189 227.18,-183.73 227.47,-176.89\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"227.03,-169.66 230.6,-176.46 227.24,-173.16 227.46,-176.65 227.46,-176.65 227.46,-176.65 227.24,-173.16 224.31,-176.84 227.03,-169.66 227.03,-169.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"220\" y=\"-192.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n",
+       "</div>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.HTML object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "tt.set_acceptance(spot.acc_cond(1, \"Fin(1) & Inf(1)\"))\n",
+    "test(a, tt)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {
+    "scrolled": false
+   },
    "outputs": [
     {
      "data": {
@@ -3458,20 +4666,13 @@
     }
    ],
    "source": [
-    "test(spot.translate('(Ga | GF!a)'), spot.translate('false'))"
+    "test(a, spot.translate('false'))"
    ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": []
   }
  ],
  "metadata": {
   "kernelspec": {
-   "display_name": "Python 3",
+   "display_name": "Python 3 (ipykernel)",
    "language": "python",
    "name": "python3"
   },
@@ -3485,7 +4686,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.9.1+"
+   "version": "3.11.6"
   }
  },
  "nbformat": 4,