diff --git a/NEWS b/NEWS
index fb9e30850..3bfcd22b7 100644
--- a/NEWS
+++ b/NEWS
@@ -6,7 +6,7 @@ New in spot 1.99.7a (not yet released)
     exception instead of using an assertion that could be disabled.
 
   * The load_ltsmin() function has been split in two.  Now you should
-    first call ltsmin_model::load(filename) to create an ltlmin_model,
+    first call ltsmin_model::load(filename) to create an ltsmin_model,
     and then call the ltsmin_model::kripke(...) method to create an
     automaton that can be iterated on the fly.  The intermediate
     object can be queried about the supported variables and their
@@ -23,6 +23,9 @@ New in spot 1.99.7a (not yet released)
     possible.  This is similar to the "k" option already supported
     by print_hoa(), and is useful when printing Kripke structures.
 
+  * Option "k" is automatically passed used by print_dot() and
+    print_hoa() when printing Kripke structures.
+
   Python:
 
   * The ltsmin interface has been binded in Python.  See
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 5d0f98b0d..44d30f2eb 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -31,6 +31,7 @@
 #include <spot/twa/formula2bdd.hh>
 #include <spot/twaalgos/copy.hh>
 #include <spot/twaalgos/sccinfo.hh>
+#include <spot/kripke/kripke.hh>
 #include <cstdlib>
 #include <cstring>
 #include <algorithm>
@@ -663,6 +664,9 @@ namespace spot
 		  const char* options)
   {
     dotty_output d(os, options);
+    // Enable automatic state labels for Kripke structure.
+    if (std::dynamic_pointer_cast<const kripke>(g))
+      d.parse_opts("k");
     auto aut = std::dynamic_pointer_cast<const twa_graph>(g);
     if (!aut || (d.max_states_given() && aut->num_states() >= d.max_states()))
       aut = copy(g, twa::prop_set::all(), true, d.max_states() - 1);
diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc
index b2e7e7c77..ac5eafe99 100644
--- a/spot/twaalgos/hoa.cc
+++ b/spot/twaalgos/hoa.cc
@@ -33,6 +33,7 @@
 #include <spot/misc/minato.hh>
 #include <spot/twa/formula2bdd.hh>
 #include <spot/tl/formula.hh>
+#include <spot/kripke/kripke.hh>
 
 namespace spot
 {
@@ -575,15 +576,28 @@ namespace spot
 
   std::ostream&
   print_hoa(std::ostream& os,
-		const const_twa_ptr& aut,
-		const char* opt)
+	    const const_twa_ptr& aut,
+	    const char* opt)
   {
 
     auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
     if (!a)
       a = make_twa_graph(aut, twa::prop_set::all());
 
-    return print_hoa(os, a, opt);
+    // for Kripke structures, automatically append "k" to the options.
+    char* tmpopt = nullptr;
+    if (std::dynamic_pointer_cast<const kripke>(aut))
+      {
+	unsigned n = opt ? strlen(opt) : 0;
+	tmpopt = new char[n + 2];
+	if (opt)
+	  strcpy(tmpopt, opt);
+	tmpopt[n] = 'k';
+	tmpopt[n + 1] = 0;
+      }
+    print_hoa(os, a, tmpopt ? tmpopt : opt);
+    delete[] tmpopt;
+    return os;
   }
 
 }
diff --git a/tests/core/parse_print_test.cc b/tests/core/parse_print_test.cc
index 5b6dcb1c0..272451bd9 100644
--- a/tests/core/parse_print_test.cc
+++ b/tests/core/parse_print_test.cc
@@ -44,7 +44,7 @@ int main(int argc, char** argv)
 	}
       if (!paut->ks)
 	break;
-      print_hoa(std::cout, paut->ks, "k");
+      print_hoa(std::cout, paut->ks);
     }
   return return_value;
 }
diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc
index ed81b09e7..69b315cc9 100644
--- a/tests/ltsmin/modelcheck.cc
+++ b/tests/ltsmin/modelcheck.cc
@@ -243,7 +243,7 @@ checked_main(int argc, char **argv)
       if (output == Kripke)
       {
         tm.start("kripke output");
-	spot::print_hoa(std::cout, model, "k");
+	spot::print_hoa(std::cout, model);
         tm.stop("kripke output");
         goto safe_exit;
       }
diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb
index 79ea17038..a4b291568 100644
--- a/tests/python/ltsmin.ipynb
+++ b/tests/python/ltsmin.ipynb
@@ -1,7 +1,7 @@
 {
  "metadata": {
   "name": "",
-  "signature": "sha256:984524909cc32e22143f3480e43c1951947d6885bf691c3b694cf0fd1b6b81d9"
+  "signature": "sha256:fa0fbee36e16c4615d30141ace5f7aa76009d478e4a4e2b088b6093b25f8bc69"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -162,7 +162,7 @@
      "collapsed": false,
      "input": [
       "k = m.kripke([\"a<1\", \"b>2\"])\n",
-      "k.show('.k')"
+      "k"
      ],
      "language": "python",
      "metadata": {},
@@ -172,186 +172,193 @@
        "output_type": "pyout",
        "prompt_number": 6,
        "svg": [
-        "<svg height=\"218pt\" viewBox=\"0.00 0.00 734.00 217.81\" width=\"734pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.648748 0.648748) rotate(0) translate(4 331.74)\">\n",
+        "<?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.38.0 (20140413.2041)\n",
+        " -->\n",
+        "<!-- Title: G Pages: 1 -->\n",
+        "<svg width=\"734pt\" height=\"218pt\"\n",
+        " viewBox=\"0.00 0.00 734.00 217.81\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.648748 0.648748) rotate(0) translate(4 331.74)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-331.74 1127.41,-331.74 1127.41,4 -4,4\" stroke=\"none\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-331.74 1127.41,-331.74 1127.41,4 -4,4\"/>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
-        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
-        "<ellipse cx=\"150.137\" cy=\"-154.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"150.137\" y=\"-158.67\">a=0, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"150.137\" y=\"-143.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"150.137\" cy=\"-154.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"150.137\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"150.137\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
-        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
-        "<path d=\"M1.10737,-154.87C2.31861,-154.87 13.6687,-154.87 29.5939,-154.87\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"36.6828,-154.87 29.6829,-158.02 33.1828,-154.87 29.6828,-154.87 29.6828,-154.87 29.6828,-154.87 33.1828,-154.87 29.6828,-151.72 36.6828,-154.87 36.6828,-154.87\" stroke=\"black\"/>\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.10737,-154.87C2.31861,-154.87 13.6687,-154.87 29.5939,-154.87\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"36.6828,-154.87 29.6829,-158.02 33.1828,-154.87 29.6828,-154.87 29.6828,-154.87 29.6828,-154.87 33.1828,-154.87 29.6828,-151.72 36.6828,-154.87 36.6828,-154.87\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
-        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
-        "<ellipse cx=\"415.24\" cy=\"-190.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-194.67\">a=1, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-179.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"415.24\" cy=\"-190.87\" rx=\"115.931\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-194.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-179.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
-        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
-        "<path d=\"M248.733,-168.224C268.01,-170.862 288.33,-173.642 307.88,-176.317\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"315.044,-177.297 307.682,-179.469 311.577,-176.823 308.109,-176.348 308.109,-176.348 308.109,-176.348 311.577,-176.823 308.536,-173.227 315.044,-177.297 315.044,-177.297\" stroke=\"black\"/>\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M248.733,-168.224C268.01,-170.862 288.33,-173.642 307.88,-176.317\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"315.044,-177.297 307.682,-179.469 311.577,-176.823 308.109,-176.348 308.109,-176.348 308.109,-176.348 311.577,-176.823 308.536,-173.227 315.044,-177.297 315.044,-177.297\"/>\n",
         "</g>\n",
         "<!-- 2 -->\n",
-        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
-        "<ellipse cx=\"415.24\" cy=\"-118.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-122.67\">a=0, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"415.24\" y=\"-107.67\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"415.24\" cy=\"-118.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-122.67\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"415.24\" y=\"-107.67\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
-        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
-        "<path d=\"M248.733,-141.516C268.617,-138.795 289.613,-135.923 309.727,-133.17\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"316.802,-132.202 310.293,-136.272 313.334,-132.677 309.866,-133.151 309.866,-133.151 309.866,-133.151 313.334,-132.677 309.439,-130.031 316.802,-132.202 316.802,-132.202\" stroke=\"black\"/>\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M248.733,-141.516C268.617,-138.795 289.613,-135.923 309.727,-133.17\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"316.802,-132.202 310.293,-136.272 313.334,-132.677 309.866,-133.151 309.866,-133.151 309.866,-133.151 313.334,-132.677 309.439,-130.031 316.802,-132.202 316.802,-132.202\"/>\n",
         "</g>\n",
         "<!-- 3 -->\n",
-        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-226.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-230.67\">a=2, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-215.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"683.171\" cy=\"-226.87\" rx=\"115.931\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-230.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-215.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;3 -->\n",
-        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
-        "<path d=\"M515.641,-204.326C535.172,-206.97 555.737,-209.754 575.495,-212.429\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.447,-213.37 575.088,-215.553 578.979,-212.901 575.511,-212.431 575.511,-212.431 575.511,-212.431 578.979,-212.901 575.933,-209.31 582.447,-213.37 582.447,-213.37\" stroke=\"black\"/>\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M515.641,-204.326C535.172,-206.97 555.737,-209.754 575.495,-212.429\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"582.447,-213.37 575.088,-215.553 578.979,-212.901 575.511,-212.431 575.511,-212.431 575.511,-212.431 578.979,-212.901 575.933,-209.31 582.447,-213.37 582.447,-213.37\"/>\n",
         "</g>\n",
         "<!-- 4 -->\n",
-        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-154.87\" fill=\"#ffffaa\" rx=\"115.931\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-158.67\">a=1, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-143.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"683.171\" cy=\"-154.87\" rx=\"115.931\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-158.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-143.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 1&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
-        "<path d=\"M515.641,-177.414C535.172,-174.77 555.737,-171.986 575.495,-169.311\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.447,-168.37 575.933,-172.431 578.979,-168.84 575.511,-169.309 575.511,-169.309 575.511,-169.309 578.979,-168.84 575.088,-166.188 582.447,-168.37 582.447,-168.37\" stroke=\"black\"/>\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M515.641,-177.414C535.172,-174.77 555.737,-171.986 575.495,-169.311\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"582.447,-168.37 575.933,-172.431 578.979,-168.84 575.511,-169.309 575.511,-169.309 575.511,-169.309 578.979,-168.84 575.088,-166.188 582.447,-168.37 582.447,-168.37\"/>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;4 -->\n",
-        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
-        "<path d=\"M514.13,-132.122C534.134,-134.83 555.279,-137.692 575.57,-140.439\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"582.708,-141.405 575.349,-143.588 579.24,-140.936 575.772,-140.466 575.772,-140.466 575.772,-140.466 579.24,-140.936 576.194,-137.345 582.708,-141.405 582.708,-141.405\" stroke=\"black\"/>\n",
+        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M514.13,-132.122C534.134,-134.83 555.279,-137.692 575.57,-140.439\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"582.708,-141.405 575.349,-143.588 579.24,-140.936 575.772,-140.466 575.772,-140.466 575.772,-140.466 579.24,-140.936 576.194,-137.345 582.708,-141.405 582.708,-141.405\"/>\n",
         "</g>\n",
         "<!-- 5 -->\n",
-        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
-        "<ellipse cx=\"683.171\" cy=\"-82.8701\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-86.6701\">a=0, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"683.171\" y=\"-71.6701\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"683.171\" cy=\"-82.8701\" rx=\"113.274\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-86.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"683.171\" y=\"-71.6701\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;5 -->\n",
-        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;5</title>\n",
-        "<path d=\"M514.13,-105.618C534.753,-102.826 556.589,-99.8704 577.453,-97.0461\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"584.488,-96.0937 577.974,-100.154 581.019,-96.5633 577.551,-97.0329 577.551,-97.0329 577.551,-97.0329 581.019,-96.5633 577.128,-93.9113 584.488,-96.0937 584.488,-96.0937\" stroke=\"black\"/>\n",
+        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M514.13,-105.618C534.753,-102.826 556.589,-99.8704 577.453,-97.0461\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"584.488,-96.0937 577.974,-100.154 581.019,-96.5633 577.551,-97.0329 577.551,-97.0329 577.551,-97.0329 581.019,-96.5633 577.128,-93.9113 584.488,-96.0937 584.488,-96.0937\"/>\n",
         "</g>\n",
         "<!-- 6 -->\n",
-        "<g class=\"node\" id=\"node8\"><title>6</title>\n",
-        "<ellipse cx=\"948.273\" cy=\"-282.87\" fill=\"#ffffaa\" rx=\"113.274\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-286.67\">a=3, b=0, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-271.67\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-282.87\" rx=\"113.274\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-286.67\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-271.67\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;6 -->\n",
-        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;6</title>\n",
-        "<path d=\"M769.229,-244.974C797.049,-250.896 828.052,-257.494 856.29,-263.505\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"863.407,-265.019 855.904,-266.643 859.983,-264.291 856.56,-263.562 856.56,-263.562 856.56,-263.562 859.983,-264.291 857.216,-260.481 863.407,-265.019 863.407,-265.019\" stroke=\"black\"/>\n",
+        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M769.229,-244.974C797.049,-250.896 828.052,-257.494 856.29,-263.505\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"863.407,-265.019 855.904,-266.643 859.983,-264.291 856.56,-263.562 856.56,-263.562 856.56,-263.562 859.983,-264.291 857.216,-260.481 863.407,-265.019 863.407,-265.019\"/>\n",
         "</g>\n",
         "<!-- 7 -->\n",
-        "<g class=\"node\" id=\"node9\"><title>7</title>\n",
-        "<ellipse cx=\"948.273\" cy=\"-210.87\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-214.67\">a=2, b=1, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-199.67\">...</text>\n",
+        "<g id=\"node9\" class=\"node\"><title>7</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-210.87\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-214.67\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-199.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 3&#45;&gt;7 -->\n",
-        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;7</title>\n",
-        "<path d=\"M795.75,-220.085C819.635,-218.632 844.42,-217.125 866.855,-215.76\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"874.053,-215.323 867.257,-218.892 870.559,-215.535 867.066,-215.748 867.066,-215.748 867.066,-215.748 870.559,-215.535 866.874,-212.604 874.053,-215.323 874.053,-215.323\" stroke=\"black\"/>\n",
+        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M795.75,-220.085C819.635,-218.632 844.42,-217.125 866.855,-215.76\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"874.053,-215.323 867.257,-218.892 870.559,-215.535 867.066,-215.748 867.066,-215.748 867.066,-215.748 870.559,-215.535 866.874,-212.604 874.053,-215.323 874.053,-215.323\"/>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;7 -->\n",
-        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;7</title>\n",
-        "<path d=\"M769.229,-172.974C803.85,-180.343 843.401,-188.761 876.419,-195.789\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"883.361,-197.267 875.859,-198.89 879.938,-196.538 876.515,-195.809 876.515,-195.809 876.515,-195.809 879.938,-196.538 877.17,-192.728 883.361,-197.267 883.361,-197.267\" stroke=\"black\"/>\n",
+        "<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M769.229,-172.974C803.85,-180.343 843.401,-188.761 876.419,-195.789\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"883.361,-197.267 875.859,-198.89 879.938,-196.538 876.515,-195.809 876.515,-195.809 876.515,-195.809 879.938,-196.538 877.17,-192.728 883.361,-197.267 883.361,-197.267\"/>\n",
         "</g>\n",
         "<!-- 8 -->\n",
-        "<g class=\"node\" id=\"node10\"><title>8</title>\n",
-        "<ellipse cx=\"948.273\" cy=\"-138.87\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-142.67\">a=1, b=2, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-127.67\">...</text>\n",
+        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-138.87\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-142.67\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-127.67\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;8 -->\n",
-        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;8</title>\n",
-        "<path d=\"M795.75,-148.085C819.635,-146.632 844.42,-145.125 866.855,-143.76\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"874.053,-143.323 867.257,-146.892 870.559,-143.535 867.066,-143.748 867.066,-143.748 867.066,-143.748 870.559,-143.535 866.874,-140.604 874.053,-143.323 874.053,-143.323\" stroke=\"black\"/>\n",
+        "<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M795.75,-148.085C819.635,-146.632 844.42,-145.125 866.855,-143.76\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"874.053,-143.323 867.257,-146.892 870.559,-143.535 867.066,-143.748 867.066,-143.748 867.066,-143.748 870.559,-143.535 866.874,-140.604 874.053,-143.323 874.053,-143.323\"/>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;8 -->\n",
-        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;8</title>\n",
-        "<path d=\"M768.141,-100.743C802.961,-108.154 842.92,-116.659 876.251,-123.753\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"883.258,-125.245 875.756,-126.868 879.835,-124.516 876.411,-123.787 876.411,-123.787 876.411,-123.787 879.835,-124.516 877.067,-120.706 883.258,-125.245 883.258,-125.245\" stroke=\"black\"/>\n",
+        "<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M768.141,-100.743C802.961,-108.154 842.92,-116.659 876.251,-123.753\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"883.258,-125.245 875.756,-126.868 879.835,-124.516 876.411,-123.787 876.411,-123.787 876.411,-123.787 879.835,-124.516 877.067,-120.706 883.258,-125.245 883.258,-125.245\"/>\n",
         "</g>\n",
         "<!-- u5 -->\n",
-        "<g class=\"node\" id=\"node11\"><title>u5</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"961.273,-94.3701 935.273,-94.3701 935.273,-71.3701 961.273,-71.3701 961.273,-94.3701\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-79.1701\">...</text>\n",
+        "<g id=\"node11\" class=\"node\"><title>u5</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"961.273,-94.3701 935.273,-94.3701 935.273,-71.3701 961.273,-71.3701 961.273,-94.3701\"/>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-79.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;u5 -->\n",
-        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;u5</title>\n",
-        "<path d=\"M796.513,-82.8701C846.303,-82.8701 899.844,-82.8701 927.777,-82.8701\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"934.951,-82.8701 927.951,-86.0202 931.451,-82.8701 927.951,-82.8702 927.951,-82.8702 927.951,-82.8702 931.451,-82.8701 927.951,-79.7202 934.951,-82.8701 934.951,-82.8701\" stroke=\"black\"/>\n",
+        "<g id=\"edge12\" class=\"edge\"><title>5&#45;&gt;u5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M796.513,-82.8701C846.303,-82.8701 899.844,-82.8701 927.777,-82.8701\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"934.951,-82.8701 927.951,-86.0202 931.451,-82.8701 927.951,-82.8702 927.951,-82.8702 927.951,-82.8702 931.451,-82.8701 927.951,-79.7202 934.951,-82.8701 934.951,-82.8701\"/>\n",
         "</g>\n",
         "<!-- 9 -->\n",
-        "<g class=\"node\" id=\"node12\"><title>9</title>\n",
-        "<ellipse cx=\"948.273\" cy=\"-26.8701\" fill=\"#ffffaa\" rx=\"74.9067\" ry=\"26.7407\" stroke=\"black\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-30.6701\">a=0, b=3, Q=0</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"948.273\" y=\"-15.6701\">...</text>\n",
+        "<g id=\"node12\" class=\"node\"><title>9</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"948.273\" cy=\"-26.8701\" rx=\"74.9067\" ry=\"26.7407\"/>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-30.6701\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n",
+        "<text text-anchor=\"middle\" x=\"948.273\" y=\"-15.6701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 5&#45;&gt;9 -->\n",
-        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;9</title>\n",
-        "<path d=\"M768.141,-64.9973C802.961,-57.5862 842.92,-49.081 876.251,-41.9869\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"883.258,-40.4954 877.067,-45.0337 879.835,-41.224 876.411,-41.9527 876.411,-41.9527 876.411,-41.9527 879.835,-41.224 875.756,-38.8717 883.258,-40.4954 883.258,-40.4954\" stroke=\"black\"/>\n",
+        "<g id=\"edge14\" class=\"edge\"><title>5&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M768.141,-64.9973C802.961,-57.5862 842.92,-49.081 876.251,-41.9869\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"883.258,-40.4954 877.067,-45.0337 879.835,-41.224 876.411,-41.9527 876.411,-41.9527 876.411,-41.9527 879.835,-41.224 875.756,-38.8717 883.258,-40.4954 883.258,-40.4954\"/>\n",
         "</g>\n",
         "<!-- 6&#45;&gt;6 -->\n",
-        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;6</title>\n",
-        "<path d=\"M918.017,-309.141C916.672,-319.298 926.758,-327.74 948.273,-327.74 964.41,-327.74 974.117,-322.991 977.395,-316.332\" fill=\"none\" stroke=\"black\"/>\n",
-        "<polygon fill=\"black\" points=\"978.53,-309.141 980.55,-316.546 977.984,-312.598 977.439,-316.055 977.439,-316.055 977.439,-316.055 977.984,-312.598 974.327,-315.564 978.53,-309.141 978.53,-309.141\" stroke=\"black\"/>\n",
+        "<g id=\"edge15\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M918.017,-309.141C916.672,-319.298 926.758,-327.74 948.273,-327.74 964.41,-327.74 974.117,-322.991 977.395,-316.332\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"978.53,-309.141 980.55,-316.546 977.984,-312.598 977.439,-316.055 977.439,-316.055 977.439,-316.055 977.984,-312.598 974.327,-315.564 978.53,-309.141 978.53,-309.141\"/>\n",
         "</g>\n",
         "<!-- u7 -->\n",
-        "<g class=\"node\" id=\"node13\"><title>u7</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1123.41,-222.37 1097.41,-222.37 1097.41,-199.37 1123.41,-199.37 1123.41,-222.37\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1110.41\" y=\"-207.17\">...</text>\n",
+        "<g id=\"node13\" class=\"node\"><title>u7</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1123.41,-222.37 1097.41,-222.37 1097.41,-199.37 1123.41,-199.37 1123.41,-222.37\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1110.41\" y=\"-207.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 7&#45;&gt;u7 -->\n",
-        "<g class=\"edge\" id=\"edge16\"><title>7-&gt;u7</title>\n",
-        "<path d=\"M1023.25,-210.87C1047.98,-210.87 1073.49,-210.87 1090.27,-210.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1097.33,-210.87 1090.33,-214.02 1093.83,-210.87 1090.33,-210.87 1090.33,-210.87 1090.33,-210.87 1093.83,-210.87 1090.33,-207.72 1097.33,-210.87 1097.33,-210.87\" stroke=\"black\"/>\n",
+        "<g id=\"edge16\" class=\"edge\"><title>7&#45;&gt;u7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1023.25,-210.87C1047.98,-210.87 1073.49,-210.87 1090.27,-210.87\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1097.33,-210.87 1090.33,-214.02 1093.83,-210.87 1090.33,-210.87 1090.33,-210.87 1090.33,-210.87 1093.83,-210.87 1090.33,-207.72 1097.33,-210.87 1097.33,-210.87\"/>\n",
         "</g>\n",
         "<!-- u8 -->\n",
-        "<g class=\"node\" id=\"node14\"><title>u8</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1123.41,-150.37 1097.41,-150.37 1097.41,-127.37 1123.41,-127.37 1123.41,-150.37\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1110.41\" y=\"-135.17\">...</text>\n",
+        "<g id=\"node14\" class=\"node\"><title>u8</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1123.41,-150.37 1097.41,-150.37 1097.41,-127.37 1123.41,-127.37 1123.41,-150.37\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1110.41\" y=\"-135.17\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 8&#45;&gt;u8 -->\n",
-        "<g class=\"edge\" id=\"edge17\"><title>8-&gt;u8</title>\n",
-        "<path d=\"M1023.25,-138.87C1047.98,-138.87 1073.49,-138.87 1090.27,-138.87\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1097.33,-138.87 1090.33,-142.02 1093.83,-138.87 1090.33,-138.87 1090.33,-138.87 1090.33,-138.87 1093.83,-138.87 1090.33,-135.72 1097.33,-138.87 1097.33,-138.87\" stroke=\"black\"/>\n",
+        "<g id=\"edge17\" class=\"edge\"><title>8&#45;&gt;u8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1023.25,-138.87C1047.98,-138.87 1073.49,-138.87 1090.27,-138.87\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1097.33,-138.87 1090.33,-142.02 1093.83,-138.87 1090.33,-138.87 1090.33,-138.87 1090.33,-138.87 1093.83,-138.87 1090.33,-135.72 1097.33,-138.87 1097.33,-138.87\"/>\n",
         "</g>\n",
         "<!-- u9 -->\n",
-        "<g class=\"node\" id=\"node15\"><title>u9</title>\n",
-        "<polygon fill=\"#ffffaa\" points=\"1123.41,-38.3701 1097.41,-38.3701 1097.41,-15.3701 1123.41,-15.3701 1123.41,-38.3701\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1110.41\" y=\"-23.1701\">...</text>\n",
+        "<g id=\"node15\" class=\"node\"><title>u9</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1123.41,-38.3701 1097.41,-38.3701 1097.41,-15.3701 1123.41,-15.3701 1123.41,-38.3701\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1110.41\" y=\"-23.1701\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
         "</g>\n",
         "<!-- 9&#45;&gt;u9 -->\n",
-        "<g class=\"edge\" id=\"edge18\"><title>9-&gt;u9</title>\n",
-        "<path d=\"M1023.25,-26.8701C1047.98,-26.8701 1073.49,-26.8701 1090.27,-26.8701\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
-        "<polygon fill=\"black\" points=\"1097.33,-26.8701 1090.33,-30.0202 1093.83,-26.8701 1090.33,-26.8702 1090.33,-26.8702 1090.33,-26.8702 1093.83,-26.8701 1090.33,-23.7202 1097.33,-26.8701 1097.33,-26.8701\" stroke=\"black\"/>\n",
+        "<g id=\"edge18\" class=\"edge\"><title>9&#45;&gt;u9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1023.25,-26.8701C1047.98,-26.8701 1073.49,-26.8701 1090.27,-26.8701\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1097.33,-26.8701 1090.33,-30.0202 1093.83,-26.8701 1090.33,-26.8702 1090.33,-26.8702 1090.33,-26.8702 1093.83,-26.8701 1090.33,-23.7202 1097.33,-26.8701 1097.33,-26.8701\"/>\n",
         "</g>\n",
         "</g>\n",
-        "</svg>"
+        "</svg>\n"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f9dfed68d30>"
+        "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f6211db0600> >"
        ]
       }
      ],
@@ -361,7 +368,7 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "k.show('.k<15')"
+      "k.show('.<15')"
      ],
      "language": "python",
      "metadata": {},
@@ -630,7 +637,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f9dfed5d438>"
+        "<IPython.core.display.SVG at 0x7f6211d5b400>"
        ]
       }
      ],
@@ -640,7 +647,7 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "k.show('.k<0')  # unlimited output"
+      "k.show('.<0')  # unlimited output"
      ],
      "language": "python",
      "metadata": {},
@@ -986,7 +993,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f9dfc4567b8>"
+        "<IPython.core.display.SVG at 0x7f621dda1400>"
        ]
       }
      ],
@@ -1056,7 +1063,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9e12e0b060> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f621de1c2d0> >"
        ]
       }
      ],
@@ -1218,7 +1225,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f9dfed0bf30> >"
+        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f6211db0cc0> >"
        ]
       }
      ],
@@ -1230,7 +1237,8 @@
      "input": [],
      "language": "python",
      "metadata": {},
-     "outputs": []
+     "outputs": [],
+     "prompt_number": 10
     }
    ],
    "metadata": {}