diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 103ab89d1..9d8c16d91 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -1196,11 +1196,6 @@ namespace spot
       {
         if (!circuit)
           return;
-        auto is_input = [nb_in = circuit->num_inputs()](unsigned val)
-        {
-          return (val & ~1) <= (2 * nb_in);
-        };
-
         const auto& in_names = circuit->input_names();
         const auto& out_names = circuit->output_names();
 
@@ -1212,133 +1207,99 @@ namespace spot
         auto num_gates = circuit->num_gates();
         auto gates = circuit->gates();
 
-        // If a circuit doesn't use an input, we need a special placement
-        bool uses_in = false;
-
         auto add_edge = [](std::ostream &stream, const unsigned src,
                            const unsigned dst) {
           auto src_gate = src & ~1;
-          stream << src_gate;
-          stream << " -> " << dst;
+          stream << "  " << src_gate << " -> " << dst;
           if (src & 1)
             stream << " [arrowhead=dot]";
           stream << '\n';
         };
 
         if (vertical)
-          os_ << "digraph \"\" {\nrankdir = BT;\n";
+          os_ << "digraph \"\" {\n  rankdir = BT\n";
         else
-          os_ << "digraph \"\" {\nrankdir = LR;\n";
+          os_ << "digraph \"\" {\n  rankdir = LR\n";
 
-        os_ << "# latches left\n";
+        os_ << "  {\n    rank = same\n"
+          "    node [shape=box,style=filled,fillcolor=\"#ffe6cc\"]\n";
         for (unsigned i = 0; i < num_latches; ++i)
-        {
-          auto first = circuit->latch_var(i);
-          auto first_m_mod = first & ~1;
-          os_ << "node[shape=box, label=\"L" << i << "_out\"] "
-              << first_m_mod << ";\n";
-        }
-
-        //Predefine all nodes
-
-        os_ << "# input nodes\n";
-        for (unsigned i = 0; i < num_inputs; ++i)
-          os_ << "node [shape=triangle, label=\""
-              << in_names[i] << "\"] "
-              << circuit->input_var(i) << ";\n";
-
-        os_ << "# latch nodes\n";
-        for (unsigned i = 0; i < num_latches; ++i)
-          os_ << "node[shape=box, label=\"L" << i << "\"] L" << i << ";\n";
-
-        os_ << "# gate nodes\n";
-        for (unsigned i = 0; i < num_gates; ++i)
-          if ((gates[i].first != 0) && (gates[i].second != 0))
           {
-            uses_in |= is_input(gates[i].first) | is_input(gates[i].second);
-            auto gate_var = circuit->gate_var(i);
-            os_ << "node [shape=circle, label=\"" << gate_var
-                << "\"] " << gate_var << ";\n";
+            auto first_m_mod = circuit->latch_var(i) & ~1;
+            os_ << "    " << first_m_mod << " [label=\"L" << i << "_out\"]\n";
           }
-
-        os_ << "# and ins\n";
-        for (unsigned i = 0; i < num_gates; ++i)
-          if ((gates[i].first != 0) && (gates[i].second != 0))
+        os_ << "  }\n";
+        if (num_gates)
           {
-            auto gate_var = circuit->gate_var(i);
-            add_edge(os_, gates[i].first, gate_var);
-            add_edge(os_, gates[i].second, gate_var);
+            os_ << "  node [shape=circle,style=solid]\n";
+            for (unsigned i = 0; i < num_gates; ++i)
+              if ((gates[i].first != 0) && (gates[i].second != 0))
+                os_ << "  " << circuit->gate_var(i) << '\n';
           }
-
-        bool has_alone_gate = false;
-
-        os_ << "# Latches\n";
-        for (unsigned i = 0; i < num_latches; ++i)
-        {
-          auto second = latches[i];
-          os_ << "node[shape=box, label=\"L" << i << "_in\"] L" << i << ";\n";
-          if (second <= 1 && !has_alone_gate)
+        bool has_false = false;
+        if (num_latches)
           {
-            os_ << "node[shape=box, label=\"Const\"] 0" << std::endl;
-            has_alone_gate = true;
+            os_ << "  {\n    rank=same\n"
+              "    node [shape=box,style=filled,"
+              "fillcolor=\"#ffe6cc\",label=\"\\N_in\"]\n";
+            for (unsigned i = 0; i < num_latches; ++i)
+              {
+                os_ << "    L" << i << '\n';
+                if (latches[i] <= 1)
+                  has_false = true;
+              }
+            os_ << "  }\n";
           }
-          os_ << (second & ~1) << " -> L" << i;
-          if (i & 1)
-            os_ << "[arrowhead=dot]";
-          os_ << '\n';
-        }
-
-        // Outs can be defined after everything else
-        os_ << "# Outs\n";
         const char* out_pos = vertical ? ":s" : ":w";
+        const char* rotate = vertical ? "" : ",orientation=-90";
+        if (num_outputs)
+          {
+            os_ << "  {\n    rank = sink\n    "
+              "node [shape=invtriangle,style=filled,fillcolor=\"#ffe5f1\""
+                << rotate << "]\n";
+            for (unsigned i = 0; i < num_outputs; ++i)
+              {
+                os_ << "    o" << i << " [label=\"" << out_names[i] << "\"]\n";
+                if (outputs[i] <= 1)
+                  has_false = true;
+              }
+            os_ << "  }\n";
+          }
+        if (num_inputs | has_false)
+          {
+            os_ << "  {\n    rank=source\n"
+              "    node [shape=triangle,style=filled,fillcolor=\"#e9f4fb\""
+                << rotate << "]\n";
+            for (unsigned i = 0; i < num_inputs; ++i)
+              os_ << "    " << circuit->input_var(i)
+                  << " [label=\"" << in_names[i] << "\"]\n";
+            if (has_false)
+              os_ <<
+                "    0 [shape=box,fillcolor=\"#ffe6cc\",label=\"False\"]\n";
+            os_ << "  }\n";
+          }
         for (unsigned i = 0; i < num_outputs; ++i)
-        {
-          os_ << "node [shape=triangle, orientation=180, label=\""
-             << out_names[i] << "\"] o" << i
-             << out_names[i] << ";\n";
-          auto z = outputs[i];
-          uses_in |= is_input(z);
-          if (z <= 1 && !has_alone_gate)
           {
-            os_ << "node[shape=box, label=\"Const\"] 0" << std::endl;
-            has_alone_gate = true;
+            auto z = outputs[i];
+            os_ << "  " << (z & ~1) << " -> o" << i << out_pos;
+            if (z & 1)
+              os_ << " [arrowhead=dot]";
+            os_ << '\n';
           }
-          os_ << (z & ~1) << "->" << 'o' << i << out_names[i] << out_pos;
-          if (outputs[i] & 1)
-            os_ << " [arrowhead=dot]";
-          os_ << '\n';
-        }
-
-        if (has_alone_gate || num_inputs > 0)
-        {
-          os_ << (uses_in ? "{rank = source; " : "{rank = same; ");
-          for (unsigned i = 0; i < num_inputs; ++i)
-            os_ << circuit->input_var(i) << "; ";
-          if (has_alone_gate)
-            os_ << "0; ";
-          os_ << "}\n";
-        }
-        if (num_outputs > 0)
-        {
-          os_ << "{rank = sink; ";
-          for (unsigned i = 0; i < num_outputs; ++i)
-            os_ << 'o' << i << out_names[i] << "; ";
-          os_ << "}\n";
-        }
-        if (num_latches > 0)
-        {
-          os_ << "{rank = same; ";
-          for (unsigned i = 0; i < num_latches; ++i)
-            os_ << 'L' << i << "; ";
-          os_ << "}\n{rank = same; ";
-          for (unsigned i = 0; i < num_latches; ++i)
+        for (unsigned i = 0; i < num_latches; ++i)
           {
-            auto first = circuit->latch_var(i);
-            auto first_m_mod = first & ~1;
-            os_ << first_m_mod << "; ";
+            os_ << "  " << (latches[i] & ~1) << " -> L" << i;
+            if (latches[i] & 1)
+              os_ << " [arrowhead=dot]";
+            os_ << '\n';
           }
-          os_ << "}\n";
-        }
+        for (unsigned i = 0; i < num_gates; ++i)
+          if ((gates[i].first != 0) && (gates[i].second != 0))
+            {
+              auto gate_var = circuit->gate_var(i);
+              add_edge(os_, gates[i].first, gate_var);
+              add_edge(os_, gates[i].second, gate_var);
+            }
         os_ << "}\n";
       }
     };
diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb
index 3ee2d3eb5..5e29b62e4 100644
--- a/tests/python/synthesis.ipynb
+++ b/tests/python/synthesis.ipynb
@@ -696,7 +696,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e7018b5a0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6c003de2a0> >"
       ]
      },
      "metadata": {},
@@ -2713,7 +2713,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e700b8150> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6c005968d0> >"
       ]
      },
      "execution_count": 5,
@@ -3039,7 +3039,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e700b87b0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6c003de630> >"
       ]
      },
      "execution_count": 6,
@@ -3060,7 +3060,7 @@
     "\n",
     "A strategy can be converted to a circuit in the [AIGER format](http://fmv.jku.at/aiger/FORMAT.aiger) using `strategy_to_aig()`.  This takes a second argument specifying what type of encoding to use (exactly like `ltlsynt`'s `--aiger=...` option).  \n",
     "\n",
-    "In this case, the circuit is quite simple: `o0` should be the negation of previous value of `i1`.  This is done by storing the value of `i1` in a latch.  And the value if `i0` can be ignored."
+    "In this case, the circuit is quite simple: `o0` should be the negation of previous value of `i1`.  This is done by storing the value of `i1` in a latch.  And the value of `i0` can be ignored."
    ]
   },
   {
@@ -3085,74 +3085,144 @@
        "<!-- 6 -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>6</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"76.7,-118 11.7,-118 11.7,-82 76.7,-82 76.7,-118\"/>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"76.7,-118 11.7,-118 11.7,-82 76.7,-82 76.7,-118\"/>\n",
        "<text text-anchor=\"middle\" x=\"44.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_out</text>\n",
        "</g>\n",
-       "<!-- o0o0 -->\n",
-       "<g id=\"node5\" class=\"node\">\n",
-       "<title>o0o0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"44.2,-154 88.59,-188.5 -0.2,-188.5 44.2,-154\"/>\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"44.2,-154 88.59,-188.5 -0.2,-188.5 44.2,-154\"/>\n",
        "<text text-anchor=\"middle\" x=\"44.2\" y=\"-173.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
        "</g>\n",
-       "<!-- 6&#45;&gt;o0o0 -->\n",
-       "<g id=\"edge2\" class=\"edge\">\n",
-       "<title>6&#45;&gt;o0o0:s</title>\n",
+       "<!-- 6&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>6&#45;&gt;o0:s</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M44.2,-118.19C44.2,-126.29 44.2,-136.29 44.2,-145.98\"/>\n",
        "<ellipse fill=\"black\" stroke=\"black\" cx=\"44.2\" cy=\"-150\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
-       "<!-- 2 -->\n",
+       "<!-- L0 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
+       "<title>L0</title>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"149.7,-118 94.7,-118 94.7,-82 149.7,-82 149.7,-118\"/>\n",
+       "<text text-anchor=\"middle\" x=\"122.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_in</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
        "<title>2</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"122.2,-46 83.2,-11.5 161.19,-11.5 122.2,-46\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"122.2,-46 83.2,-11.5 161.19,-11.5 122.2,-46\"/>\n",
        "<text text-anchor=\"middle\" x=\"122.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
        "</g>\n",
-       "<!-- L0 -->\n",
-       "<g id=\"node4\" class=\"node\">\n",
-       "<title>L0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"149.2,-118 95.2,-118 95.2,-82 149.2,-82 149.2,-118\"/>\n",
-       "<text text-anchor=\"middle\" x=\"122.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
-       "</g>\n",
        "<!-- 2&#45;&gt;L0 -->\n",
-       "<g id=\"edge1\" class=\"edge\">\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
        "<title>2&#45;&gt;L0</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M122.2,-46.1C122.2,-54.12 122.2,-63.28 122.2,-71.69\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"118.7,-71.82 122.2,-81.82 125.7,-71.82 118.7,-71.82\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M122.2,-46.1C122.2,-54.74 122.2,-64.71 122.2,-73.64\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"122.2\" cy=\"-77.82\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
        "<!-- 4 -->\n",
-       "<g id=\"node3\" class=\"node\">\n",
+       "<g id=\"node5\" class=\"node\">\n",
        "<title>4</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"218.2,-46 179.2,-11.5 257.19,-11.5 218.2,-46\"/>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"218.2,-46 179.2,-11.5 257.19,-11.5 218.2,-46\"/>\n",
        "<text text-anchor=\"middle\" x=\"218.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f4e700b8390> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f6c004d8870> >"
       ]
      },
      "metadata": {},
      "output_type": "display_data"
-    },
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "aag 3 2 1 1 0\n",
-      "2\n",
-      "4\n",
-      "6 3\n",
-      "7\n",
-      "i0 i1\n",
-      "i1 i0\n",
-      "o0 o0\n"
-     ]
     }
    ],
    "source": [
     "aig = spot.strategy_to_aig(strat, \"isop\")\n",
-    "display(aig)\n",
-    "print(aig.to_str())"
+    "display(aig)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "a7100505",
+   "metadata": {},
+   "source": [
+    "While we are at it, let us mention that you can render those circuits horizontally as follows:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "id": "8272357d",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?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=\"311pt\" height=\"172pt\"\n",
+       " viewBox=\"0.00 0.00 311.39 172.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 168)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-168 307.39,-168 307.39,4 -4,4\"/>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"178.99,-41 113.99,-41 113.99,-5 178.99,-5 178.99,-41\"/>\n",
+       "<text text-anchor=\"middle\" x=\"146.49\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_out</text>\n",
+       "</g>\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"214.8,-23 281.39,0 281.39,-46 214.8,-23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"259.19\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>6&#45;&gt;o0:w</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M179.09,-23C187.85,-23 197.52,-23 206.88,-23\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"210.99\" cy=\"-23\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- L0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>L0</title>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"173.99,-95 118.99,-95 118.99,-59 173.99,-59 173.99,-95\"/>\n",
+       "<text text-anchor=\"middle\" x=\"146.49\" y=\"-73.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_in</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"77.99,-77 19.5,-100 19.5,-54 77.99,-77\"/>\n",
+       "<text text-anchor=\"middle\" x=\"39\" y=\"-73.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;L0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>2&#45;&gt;L0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M78.08,-77C88.7,-77 100.18,-77 110.6,-77\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"114.7\" cy=\"-77\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"77.99,-141 19.5,-164 19.5,-118 77.99,-141\"/>\n",
+       "<text text-anchor=\"middle\" x=\"39\" y=\"-137.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.jupyter.SVG object>"
+      ]
+     },
+     "execution_count": 8,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "aig.show('h')"
    ]
   },
   {
@@ -3176,7 +3246,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 9,
    "id": "efc7c557",
    "metadata": {},
    "outputs": [
@@ -3346,7 +3416,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e700b8cc0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6c003dec90> >"
       ]
      },
      "metadata": {},
@@ -3368,62 +3438,62 @@
        "<!-- 4 -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>4</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"65,-118 0,-118 0,-82 65,-82 65,-118\"/>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"65,-118 0,-118 0,-82 65,-82 65,-118\"/>\n",
        "<text text-anchor=\"middle\" x=\"32.5\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_out</text>\n",
        "</g>\n",
        "<!-- 6 -->\n",
-       "<g id=\"node4\" class=\"node\">\n",
+       "<g id=\"node2\" class=\"node\">\n",
        "<title>6</title>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"62.5\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"62.5\" y=\"-168.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;6 -->\n",
-       "<g id=\"edge2\" class=\"edge\">\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
        "<title>4&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M39.92,-118.3C43.66,-127.03 48.25,-137.76 52.32,-147.25\"/>\n",
        "<ellipse fill=\"black\" stroke=\"black\" cx=\"54.01\" cy=\"-151.18\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
-       "<!-- 2 -->\n",
-       "<g id=\"node2\" class=\"node\">\n",
-       "<title>2</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"93.5,-46 54.51,-11.5 132.49,-11.5 93.5,-46\"/>\n",
-       "<text text-anchor=\"middle\" x=\"93.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
-       "</g>\n",
-       "<!-- 2&#45;&gt;6 -->\n",
-       "<g id=\"edge1\" class=\"edge\">\n",
-       "<title>2&#45;&gt;6</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M89.77,-43.11C86.03,-62.12 80.05,-92.11 74.5,-118 72.67,-126.56 70.58,-135.88 68.68,-144.29\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"65.2,-143.78 66.38,-154.31 72.02,-145.34 65.2,-143.78\"/>\n",
-       "</g>\n",
        "<!-- L0 -->\n",
        "<g id=\"node3\" class=\"node\">\n",
        "<title>L0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"62.5,-262 8.5,-262 8.5,-226 62.5,-226 62.5,-262\"/>\n",
-       "<text text-anchor=\"middle\" x=\"35.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"62,-262 7,-262 7,-226 62,-226 62,-262\"/>\n",
+       "<text text-anchor=\"middle\" x=\"34.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_in</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;L0 -->\n",
-       "<g id=\"edge3\" class=\"edge\">\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
        "<title>6&#45;&gt;L0</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M56.24,-189.24C53.13,-197.3 49.29,-207.26 45.76,-216.4\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"42.44,-215.29 42.1,-225.88 48.97,-217.81 42.44,-215.29\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M56.15,-188.88C52.68,-197.54 48.32,-208.45 44.42,-218.2\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"42.9\" cy=\"-221.99\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
-       "<!-- o0o0 -->\n",
-       "<g id=\"node5\" class=\"node\">\n",
-       "<title>o0o0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"90.5,-298 134.89,-332.5 46.11,-332.5 90.5,-298\"/>\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"90.5,-298 134.89,-332.5 46.11,-332.5 90.5,-298\"/>\n",
        "<text text-anchor=\"middle\" x=\"90.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
        "</g>\n",
-       "<!-- 6&#45;&gt;o0o0 -->\n",
-       "<g id=\"edge4\" class=\"edge\">\n",
-       "<title>6&#45;&gt;o0o0:s</title>\n",
+       "<!-- 6&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>6&#45;&gt;o0:s</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M68.58,-189.32C76.1,-210.91 88.19,-250.57 90.21,-287.63\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"86.72,-288.1 90.5,-298 93.72,-287.91 86.72,-288.1\"/>\n",
        "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"93.5,-46 54.51,-11.5 132.49,-11.5 93.5,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"93.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;6 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>2&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M89.77,-43.11C86.03,-62.12 80.05,-92.11 74.5,-118 72.67,-126.56 70.58,-135.88 68.68,-144.29\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"65.2,-143.78 66.38,-154.31 72.02,-145.34 65.2,-143.78\"/>\n",
+       "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f4e7124ccf0> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f6c0059b570> >"
       ]
      },
      "metadata": {},
@@ -3450,7 +3520,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 10,
    "id": "f9f8d0e3",
    "metadata": {},
    "outputs": [
@@ -3463,93 +3533,93 @@
        "<!-- Generated by graphviz version 2.43.0 (0)\n",
        " -->\n",
        "<!-- Pages: 1 -->\n",
-       "<svg width=\"328pt\" height=\"352pt\"\n",
-       " viewBox=\"0.00 0.00 327.70 352.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<svg width=\"332pt\" height=\"352pt\"\n",
+       " viewBox=\"0.00 0.00 332.50 352.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 348)\">\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-348 323.7,-348 323.7,4 -4,4\"/>\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-348 328.5,-348 328.5,4 -4,4\"/>\n",
        "<!-- 6 -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>6</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"65,-118 0,-118 0,-82 65,-82 65,-118\"/>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"65,-118 0,-118 0,-82 65,-82 65,-118\"/>\n",
        "<text text-anchor=\"middle\" x=\"32.5\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_out</text>\n",
        "</g>\n",
        "<!-- 8 -->\n",
-       "<g id=\"node5\" class=\"node\">\n",
+       "<g id=\"node2\" class=\"node\">\n",
        "<title>8</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"63.5\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"63.5\" y=\"-168.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"62.5\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"62.5\" y=\"-168.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;8 -->\n",
-       "<g id=\"edge2\" class=\"edge\">\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
        "<title>6&#45;&gt;8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M40.16,-118.3C44.12,-127.25 49.01,-138.29 53.29,-147.94\"/>\n",
-       "<ellipse fill=\"black\" stroke=\"black\" cx=\"54.94\" cy=\"-151.67\" rx=\"4\" ry=\"4\"/>\n",
-       "</g>\n",
-       "<!-- 2 -->\n",
-       "<g id=\"node2\" class=\"node\">\n",
-       "<title>2</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"93.5,-46 54.51,-11.5 132.49,-11.5 93.5,-46\"/>\n",
-       "<text text-anchor=\"middle\" x=\"93.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
-       "</g>\n",
-       "<!-- 2&#45;&gt;8 -->\n",
-       "<g id=\"edge1\" class=\"edge\">\n",
-       "<title>2&#45;&gt;8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M89.64,-42.92C84.4,-68.61 74.99,-114.68 69.01,-144\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"65.54,-143.48 66.97,-153.98 72.4,-144.88 65.54,-143.48\"/>\n",
-       "</g>\n",
-       "<!-- 4 -->\n",
-       "<g id=\"node3\" class=\"node\">\n",
-       "<title>4</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"189.5,-46 150.51,-11.5 228.49,-11.5 189.5,-46\"/>\n",
-       "<text text-anchor=\"middle\" x=\"189.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M39.92,-118.3C43.66,-127.03 48.25,-137.76 52.32,-147.25\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"54.01\" cy=\"-151.18\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
        "<!-- L0 -->\n",
-       "<g id=\"node4\" class=\"node\">\n",
+       "<g id=\"node3\" class=\"node\">\n",
        "<title>L0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"63.5,-262 9.5,-262 9.5,-226 63.5,-226 63.5,-262\"/>\n",
-       "<text text-anchor=\"middle\" x=\"36.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"67,-262 12,-262 12,-226 67,-226 67,-262\"/>\n",
+       "<text text-anchor=\"middle\" x=\"39.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_in</text>\n",
        "</g>\n",
        "<!-- 8&#45;&gt;L0 -->\n",
        "<g id=\"edge3\" class=\"edge\">\n",
        "<title>8&#45;&gt;L0</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M57.24,-189.24C54.13,-197.3 50.29,-207.26 46.76,-216.4\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"43.44,-215.29 43.1,-225.88 49.97,-217.81 43.44,-215.29\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.17,-189.24C54.35,-197.82 50.82,-208.54 47.67,-218.14\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"46.38\" cy=\"-222.08\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
-       "<!-- o0o0 -->\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"95.5,-298 139.89,-332.5 51.11,-332.5 95.5,-298\"/>\n",
+       "<text text-anchor=\"middle\" x=\"95.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>8&#45;&gt;o0:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M69.5,-188.83C78.39,-210.3 92.87,-250.3 95.18,-287.97\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"91.69,-288.12 95.5,-298 98.68,-287.89 91.69,-288.12\"/>\n",
+       "</g>\n",
+       "<!-- o1 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>o1</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"201.5,-298 245.89,-332.5 157.11,-332.5 201.5,-298\"/>\n",
+       "<text text-anchor=\"middle\" x=\"201.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
        "<g id=\"node6\" class=\"node\">\n",
-       "<title>o0o0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"91.5,-298 135.89,-332.5 47.11,-332.5 91.5,-298\"/>\n",
-       "<text text-anchor=\"middle\" x=\"91.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"93.5,-46 54.51,-11.5 132.49,-11.5 93.5,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"93.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
        "</g>\n",
-       "<!-- 8&#45;&gt;o0o0 -->\n",
+       "<!-- 2&#45;&gt;8 -->\n",
        "<g id=\"edge4\" class=\"edge\">\n",
-       "<title>8&#45;&gt;o0o0:s</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M69.58,-189.32C77.1,-210.91 89.19,-250.57 91.21,-287.63\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"87.72,-288.1 91.5,-298 94.72,-287.91 87.72,-288.1\"/>\n",
+       "<title>2&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M89.57,-42.62C84.15,-68.35 74.32,-114.94 68.12,-144.35\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"64.65,-143.84 66.01,-154.35 71.5,-145.28 64.65,-143.84\"/>\n",
        "</g>\n",
-       "<!-- o1o1 -->\n",
+       "<!-- 4 -->\n",
        "<g id=\"node7\" class=\"node\">\n",
-       "<title>o1o1</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"275.5,-298 319.89,-332.5 231.11,-332.5 275.5,-298\"/>\n",
-       "<text text-anchor=\"middle\" x=\"275.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"285.5,-46 246.51,-11.5 324.49,-11.5 285.5,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"285.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node8\" class=\"node\">\n",
        "<title>0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"246.5,-5 304.5,-5 304.5,-41 246.5,-41 246.5,-5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"275.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">Const</text>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"228.5,-41 174.5,-41 174.5,-5 228.5,-5 228.5,-41\"/>\n",
+       "<text text-anchor=\"middle\" x=\"201.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">False</text>\n",
        "</g>\n",
-       "<!-- 0&#45;&gt;o1o1 -->\n",
-       "<g id=\"edge5\" class=\"edge\">\n",
-       "<title>0&#45;&gt;o1o1:s</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M275.5,-41.31C275.5,-83.11 275.5,-193.09 275.5,-287.99\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"272,-288 275.5,-298 279,-288 272,-288\"/>\n",
+       "<!-- 0&#45;&gt;o1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;o1:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M201.5,-41.31C201.5,-83.11 201.5,-193.09 201.5,-287.99\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"198,-288 201.5,-298 205,-288 198,-288\"/>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f4e700b85a0> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f6c003dee40> >"
       ]
      },
      "metadata": {},
@@ -3576,7 +3646,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 10,
+   "execution_count": 11,
    "id": "57d7875d",
    "metadata": {},
    "outputs": [],
@@ -3597,7 +3667,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 12,
    "id": "4796e7d7",
    "metadata": {},
    "outputs": [
@@ -3614,101 +3684,101 @@
        " viewBox=\"0.00 0.00 202.39 289.50\" 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 285.5)\">\n",
        "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-285.5 198.39,-285.5 198.39,4 -4,4\"/>\n",
-       "<!-- 2 -->\n",
-       "<g id=\"node1\" class=\"node\">\n",
-       "<title>2</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"44.2,-46 5.2,-11.5 83.19,-11.5 44.2,-46\"/>\n",
-       "<text text-anchor=\"middle\" x=\"44.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
-       "</g>\n",
        "<!-- 6 -->\n",
-       "<g id=\"node3\" class=\"node\">\n",
+       "<g id=\"node1\" class=\"node\">\n",
        "<title>6</title>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"129.2\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"129.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
        "</g>\n",
-       "<!-- 2&#45;&gt;6 -->\n",
-       "<g id=\"edge1\" class=\"edge\">\n",
-       "<title>2&#45;&gt;6</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M56.74,-35.07C70.27,-47 92.03,-66.21 108.18,-80.46\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"106.23,-83.4 116.04,-87.39 110.86,-78.15 106.23,-83.4\"/>\n",
-       "</g>\n",
-       "<!-- 8 -->\n",
-       "<g id=\"node4\" class=\"node\">\n",
-       "<title>8</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"65.2\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"65.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
-       "</g>\n",
-       "<!-- 2&#45;&gt;8 -->\n",
-       "<g id=\"edge3\" class=\"edge\">\n",
-       "<title>2&#45;&gt;8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M49.17,-41.77C51.92,-51.58 55.37,-63.89 58.36,-74.59\"/>\n",
-       "<ellipse fill=\"black\" stroke=\"black\" cx=\"59.46\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
-       "</g>\n",
-       "<!-- 4 -->\n",
-       "<g id=\"node2\" class=\"node\">\n",
-       "<title>4</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"140.2,-46 101.2,-11.5 179.19,-11.5 140.2,-46\"/>\n",
-       "<text text-anchor=\"middle\" x=\"140.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
-       "</g>\n",
-       "<!-- 4&#45;&gt;6 -->\n",
-       "<g id=\"edge2\" class=\"edge\">\n",
-       "<title>4&#45;&gt;6</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M137.31,-43.71C136.05,-52.28 134.55,-62.48 133.19,-71.76\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"129.72,-71.32 131.73,-81.72 136.64,-72.34 129.72,-71.32\"/>\n",
-       "</g>\n",
-       "<!-- 4&#45;&gt;8 -->\n",
-       "<g id=\"edge4\" class=\"edge\">\n",
-       "<title>4&#45;&gt;8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M128.48,-35.72C116.36,-47.83 97.3,-66.9 83.26,-80.94\"/>\n",
-       "<ellipse fill=\"black\" stroke=\"black\" cx=\"80.41\" cy=\"-83.79\" rx=\"4\" ry=\"4\"/>\n",
-       "</g>\n",
        "<!-- 10 -->\n",
-       "<g id=\"node5\" class=\"node\">\n",
+       "<g id=\"node3\" class=\"node\">\n",
        "<title>10</title>\n",
        "<ellipse fill=\"none\" stroke=\"black\" cx=\"65.2\" cy=\"-176.75\" rx=\"23\" ry=\"23\"/>\n",
        "<text text-anchor=\"middle\" x=\"65.2\" y=\"-173.05\" font-family=\"Times,serif\" font-size=\"14.00\">10</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;10 -->\n",
-       "<g id=\"edge5\" class=\"edge\">\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
        "<title>6&#45;&gt;10</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M117.75,-114.36C108.69,-124.95 95.81,-139.99 85.07,-152.53\"/>\n",
        "<ellipse fill=\"black\" stroke=\"black\" cx=\"82.29\" cy=\"-155.79\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
-       "<!-- o1o1 -->\n",
-       "<g id=\"node7\" class=\"node\">\n",
-       "<title>o1o1</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"150.2,-235.5 194.59,-270 105.8,-270 150.2,-235.5\"/>\n",
+       "<!-- o1 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>o1</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"150.2,-235.5 194.59,-270 105.8,-270 150.2,-235.5\"/>\n",
        "<text text-anchor=\"middle\" x=\"150.2\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
        "</g>\n",
-       "<!-- 6&#45;&gt;o1o1 -->\n",
-       "<g id=\"edge8\" class=\"edge\">\n",
-       "<title>6&#45;&gt;o1o1:s</title>\n",
+       "<!-- 6&#45;&gt;o1 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>6&#45;&gt;o1:s</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M133.55,-117.85C139.22,-141.22 148.58,-185.13 150.01,-225.36\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"146.51,-225.56 150.2,-235.5 153.51,-225.43 146.51,-225.56\"/>\n",
        "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"65.2\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"65.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
        "<!-- 8&#45;&gt;10 -->\n",
-       "<g id=\"edge6\" class=\"edge\">\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
        "<title>8&#45;&gt;10</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M65.2,-118.34C65.2,-126.54 65.2,-136.58 65.2,-145.95\"/>\n",
        "<ellipse fill=\"black\" stroke=\"black\" cx=\"65.2\" cy=\"-149.95\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
-       "<!-- o0o0 -->\n",
-       "<g id=\"node6\" class=\"node\">\n",
-       "<title>o0o0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"44.2,-235.5 88.59,-270 -0.2,-270 44.2,-235.5\"/>\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"44.2,-235.5 88.59,-270 -0.2,-270 44.2,-235.5\"/>\n",
        "<text text-anchor=\"middle\" x=\"44.2\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
        "</g>\n",
-       "<!-- 10&#45;&gt;o0o0 -->\n",
-       "<g id=\"edge7\" class=\"edge\">\n",
-       "<title>10&#45;&gt;o0o0:s</title>\n",
+       "<!-- 10&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>10&#45;&gt;o0:s</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M54.45,-196.9C50.57,-205.12 46.74,-215.16 45.07,-225.34\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"41.57,-225.23 44.2,-235.5 48.54,-225.83 41.57,-225.23\"/>\n",
        "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"44.2,-46 5.2,-11.5 83.19,-11.5 44.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"44.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;6 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>2&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M56.74,-35.07C70.27,-47 92.03,-66.21 108.18,-80.46\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"106.23,-83.4 116.04,-87.39 110.86,-78.15 106.23,-83.4\"/>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;8 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.17,-41.77C51.92,-51.58 55.37,-63.89 58.36,-74.59\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"59.46\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"140.2,-46 101.2,-11.5 179.19,-11.5 140.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"140.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;6 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>4&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M137.31,-43.71C136.05,-52.28 134.55,-62.48 133.19,-71.76\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"129.72,-71.32 131.73,-81.72 136.64,-72.34 129.72,-71.32\"/>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;8 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>4&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M128.48,-35.72C116.36,-47.83 97.3,-66.9 83.26,-80.94\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"80.41\" cy=\"-83.79\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f4e700b8e40> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f6c00530750> >"
       ]
      },
      "metadata": {},
@@ -3722,7 +3792,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 13,
    "id": "000f3948",
    "metadata": {},
    "outputs": [
@@ -3751,7 +3821,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 14,
    "id": "60e8b21a",
    "metadata": {},
    "outputs": [
@@ -3777,7 +3847,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 15,
    "id": "f5d49a9e",
    "metadata": {},
    "outputs": [
@@ -3820,10 +3890,10 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f4e700b8cf0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6c003c2300> >"
       ]
      },
-     "execution_count": 14,
+     "execution_count": 15,
      "metadata": {},
      "output_type": "execute_result"
     }