diff --git a/NEWS b/NEWS
index d3e21ebb2..f86d8aa3d 100644
--- a/NEWS
+++ b/NEWS
@@ -30,6 +30,11 @@ New in spot 2.5.3.dev  (not yet released)
     "exiting transitions".  This can be used to display alternating
     automata in a way many people expect.
 
+  - print_dot() has a new option "K" to cancel the effect of "k"
+    (which uses state labels whenever possible).  This is most useful
+    when one want to force transition-labeling of a Kripke structure,
+    where "k" is usually the default.
+
   - cleanup_parity() and cleanup_parity_here() are smarter and now
     remove from the acceptance condition the parity colors that are
     not used in the automaton.
diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc
index 1a1eafadb..b844b3d18 100644
--- a/bin/common_aoutput.cc
+++ b/bin/common_aoutput.cc
@@ -88,7 +88,7 @@ static const argp_option options[] =
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Output format:", 3 },
     { "dot", 'd',
-      "1|a|A|b|B|c|C(COLOR)|e|f(FONT)|h|k|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#",
+      "1|a|A|b|B|c|C(COLOR)|e|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#",
       OPTION_ARG_OPTIONAL,
       "GraphViz's format.  Add letters for "
       "(1) force numbered states, "
@@ -103,6 +103,7 @@ static const argp_option options[] =
       "(f(FONT)) use FONT, "
       "(h) horizontal layout, "
       "(k) use state labels when possible, "
+      "(K) use transition labels (default), "
       "(n) show name, "
       "(N) hide name, "
       "(o) ordered transitions, "
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 8387ec388..a3bebd26d 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -97,6 +97,7 @@ namespace spot
       bool opt_html_labels_ = false;
       bool opt_color_sets_ = false;
       bool opt_state_labels_ = false;
+      bool uppercase_k_seen_ = false;
       bool opt_rainbow = false;
       bool opt_bullet = false;
       bool opt_bullet_but_buchi = false;
@@ -271,6 +272,10 @@ namespace spot
             case 'k':
               opt_state_labels_ = true;
               break;
+            case 'K':
+              opt_state_labels_ = false;
+              uppercase_k_seen_ = true;
+              break;
             case 'n':
               opt_name_ = true;
               break;
@@ -333,6 +338,11 @@ namespace spot
         parse_opts(options ? options : ".");
       }
 
+      bool uppercase_k_seen() const
+      {
+        return uppercase_k_seen_;
+      }
+
       const char*
       html_set_color(int v) const
       {
@@ -944,8 +954,9 @@ namespace spot
                   const char* options)
   {
     dotty_output d(os, options);
-    // Enable automatic state labels for Kripke structure.
-    if (std::dynamic_pointer_cast<const fair_kripke>(g))
+    // Enable state labels for Kripke structure.
+    if (std::dynamic_pointer_cast<const fair_kripke>(g)
+        && !d.uppercase_k_seen())
       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()))
diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py
index 3f3bab32f..dc05fce22 100755
--- a/tests/python/ipnbdoctest.py
+++ b/tests/python/ipnbdoctest.py
@@ -115,12 +115,16 @@ def canonicalize(s, type, ignores):
     s = re.sub(r' fill="black"', '', s)
     s = re.sub(r' stroke="transparent"', ' stroke="none"', s)
     s = re.sub(r'><title>', '>\n<title>', s)
+    # tooltips with a ", " are likely to have \n which was not
+    # well supported by 2.38.
+    s = re.sub(r'<a xlink:title=".*?, .*?">\n', '<a xlink:title="...">\n', s,
+               flags=re.DOTALL)
     # Different Pandas versions produce different CSS styles (when there is a
     # style).
     s = re.sub(r'<style[ a-z]*>.*</style>\n', '', s, flags=re.DOTALL)
     # Table that contains enc.user are log from the SAT-solver.  They contain
     # timing result we cannot compare between runs.
-    s = re.sub(r'<table.*dataframe.*enc.user.*</table>', '<table></table>', s,
+    s = re.sub(r'<table.*dataframe.*?enc.user.*?</table>', '<table></table>', s,
                flags=re.DOTALL)
 
     for n, p in enumerate(ignores):
diff --git a/tests/python/ltsmin-pml.ipynb b/tests/python/ltsmin-pml.ipynb
index 91d1d87bb..67dba3ed2 100644
--- a/tests/python/ltsmin-pml.ipynb
+++ b/tests/python/ltsmin-pml.ipynb
@@ -38,8 +38,8 @@
       "SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n",
       "(C) University of Twente, Formal Methods and Tools group\n",
       "\n",
-      "Parsing tmpqado0fcz.pml...\n",
-      "Parsing tmpqado0fcz.pml done (0.0 sec)\n",
+      "Parsing tmp_kk6cvzf.pml...\n",
+      "Parsing tmp_kk6cvzf.pml done (0.0 sec)\n",
       "\n",
       "Optimizing graphs...\n",
       "   StateMerging changed 0 states/transitions.\n",
@@ -225,8 +225,8 @@
       "   Found          2 /          2 (100.0%) Commuting actions               \n",
       "Generating guard dependency matrices done (0.0 sec)\n",
       "\n",
-      "Written C code to /home/adl/git/spot/tests/python/tmpqado0fcz.pml.spins.c\n",
-      "Compiled C code to PINS library tmpqado0fcz.pml.spins\n",
+      "Written C code to /home/adl/git/spot/tests/python/tmp_kk6cvzf.pml.spins.c\n",
+      "Compiled C code to PINS library tmp_kk6cvzf.pml.spins\n",
       "\n"
      ]
     }
@@ -560,7 +560,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f0cd1edc630> >"
+       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fa8d4065b40> >"
       ]
      },
      "execution_count": 4,
@@ -576,8 +576,696 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "And then from this Kripke structure you can do some model checking using the same functions as illustrated in `ltsmin-dve.ipynb`.\n",
-    "\n",
+    "And then from this Kripke structure you can do some model checking using the same functions as illustrated in `ltsmin-dve.ipynb`."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "For displaying Kripke structures more compactly, it can be useful to use option `1` to move all state labels in tooltips (mouse over the state to see them):"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<svg height=\"280pt\" viewBox=\"0.00 0.00 454.79 280.00\" width=\"455pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 276)\">\n",
+       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-276 450.7924,-276 450.7924,4 -4,4\" stroke=\"transparent\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.3962\" y=\"-256.8\">t</text>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"212.3962\" y=\"-241.8\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g class=\"node\" id=\"node2\">\n",
+       "<title>0</title>\n",
+       "<g id=\"a_node2\"><a xlink:title=\"P_0._pc=1, P_0.a=0, P_0.b=0\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"55\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"55\" y=\"-113.3\">0</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g class=\"edge\" id=\"edge1\">\n",
+       "<title>I-&gt;0</title>\n",
+       "<path d=\"M1.1121,-117C4.0448,-117 17.0329,-117 29.5224,-117\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"36.7386,-117 29.7386,-120.1501 33.2386,-117 29.7386,-117.0001 29.7386,-117.0001 29.7386,-117.0001 33.2386,-117 29.7386,-113.8501 36.7386,-117 36.7386,-117\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g class=\"node\" id=\"node3\">\n",
+       "<title>1</title>\n",
+       "<g id=\"a_node3\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=0\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"127\" cy=\"-144\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"127\" y=\"-140.3\">1</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g class=\"edge\" id=\"edge2\">\n",
+       "<title>0-&gt;1</title>\n",
+       "<path d=\"M72.063,-123.3986C81.3884,-126.8956 93.0837,-131.2814 103.284,-135.1065\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"110.0595,-137.6473 102.3991,-138.1388 106.7823,-136.4183 103.5052,-135.1894 103.5052,-135.1894 103.5052,-135.1894 106.7823,-136.4183 104.6112,-132.2399 110.0595,-137.6473 110.0595,-137.6473\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g class=\"node\" id=\"node4\">\n",
+       "<title>2</title>\n",
+       "<g id=\"a_node4\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=1\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"127\" cy=\"-90\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"127\" y=\"-86.3\">2</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g class=\"edge\" id=\"edge3\">\n",
+       "<title>0-&gt;2</title>\n",
+       "<path d=\"M72.063,-110.6014C81.3884,-107.1044 93.0837,-102.7186 103.284,-98.8935\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"110.0595,-96.3527 104.6112,-101.7601 106.7823,-97.5817 103.5052,-98.8106 103.5052,-98.8106 103.5052,-98.8106 106.7823,-97.5817 102.3991,-95.8612 110.0595,-96.3527 110.0595,-96.3527\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g class=\"node\" id=\"node5\">\n",
+       "<title>3</title>\n",
+       "<g id=\"a_node5\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=0\n",
+       "!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"199\" cy=\"-171\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"199\" y=\"-167.3\">3</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;3 -->\n",
+       "<g class=\"edge\" id=\"edge4\">\n",
+       "<title>1-&gt;3</title>\n",
+       "<path d=\"M144.063,-150.3986C153.3884,-153.8956 165.0837,-158.2814 175.284,-162.1065\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"182.0595,-164.6473 174.3991,-165.1388 178.7823,-163.4183 175.5052,-162.1894 175.5052,-162.1894 175.5052,-162.1894 178.7823,-163.4183 176.6112,-159.2399 182.0595,-164.6473 182.0595,-164.6473\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g class=\"node\" id=\"node6\">\n",
+       "<title>4</title>\n",
+       "<g id=\"a_node6\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=1\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"199\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"199\" y=\"-113.3\">4</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;4 -->\n",
+       "<g class=\"edge\" id=\"edge5\">\n",
+       "<title>1-&gt;4</title>\n",
+       "<path d=\"M144.063,-137.6014C153.3884,-134.1044 165.0837,-129.7186 175.284,-125.8935\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"182.0595,-123.3527 176.6112,-128.7601 178.7823,-124.5817 175.5052,-125.8106 175.5052,-125.8106 175.5052,-125.8106 178.7823,-124.5817 174.3991,-122.8612 182.0595,-123.3527 182.0595,-123.3527\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;4 -->\n",
+       "<g class=\"edge\" id=\"edge6\">\n",
+       "<title>2-&gt;4</title>\n",
+       "<path d=\"M144.063,-96.3986C153.3884,-99.8956 165.0837,-104.2814 175.284,-108.1065\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"182.0595,-110.6473 174.3991,-111.1388 178.7823,-109.4183 175.5052,-108.1894 175.5052,-108.1894 175.5052,-108.1894 178.7823,-109.4183 176.6112,-105.2399 182.0595,-110.6473 182.0595,-110.6473\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g class=\"node\" id=\"node7\">\n",
+       "<title>5</title>\n",
+       "<g id=\"a_node7\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=2\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"199\" cy=\"-63\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"199\" y=\"-59.3\">5</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;5 -->\n",
+       "<g class=\"edge\" id=\"edge7\">\n",
+       "<title>2-&gt;5</title>\n",
+       "<path d=\"M144.063,-83.6014C153.3884,-80.1044 165.0837,-75.7186 175.284,-71.8935\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"182.0595,-69.3527 176.6112,-74.7601 178.7823,-70.5817 175.5052,-71.8106 175.5052,-71.8106 175.5052,-71.8106 178.7823,-70.5817 174.3991,-68.8612 182.0595,-69.3527 182.0595,-69.3527\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g class=\"node\" id=\"node8\">\n",
+       "<title>6</title>\n",
+       "<g id=\"a_node8\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=0\n",
+       "!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; dead\">\n",
+       "<ellipse cx=\"271\" cy=\"-198\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"271\" y=\"-194.3\">6</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;6 -->\n",
+       "<g class=\"edge\" id=\"edge8\">\n",
+       "<title>3-&gt;6</title>\n",
+       "<path d=\"M216.063,-177.3986C225.3884,-180.8956 237.0837,-185.2814 247.284,-189.1065\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"254.0595,-191.6473 246.3991,-192.1388 250.7823,-190.4183 247.5052,-189.1894 247.5052,-189.1894 247.5052,-189.1894 250.7823,-190.4183 248.6112,-186.2399 254.0595,-191.6473 254.0595,-191.6473\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g class=\"node\" id=\"node9\">\n",
+       "<title>7</title>\n",
+       "<g id=\"a_node9\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=1\n",
+       "!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"271\" cy=\"-144\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"271\" y=\"-140.3\">7</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;7 -->\n",
+       "<g class=\"edge\" id=\"edge9\">\n",
+       "<title>3-&gt;7</title>\n",
+       "<path d=\"M216.063,-164.6014C225.3884,-161.1044 237.0837,-156.7186 247.284,-152.8935\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"254.0595,-150.3527 248.6112,-155.7601 250.7823,-151.5817 247.5052,-152.8106 247.5052,-152.8106 247.5052,-152.8106 250.7823,-151.5817 246.3991,-149.8612 254.0595,-150.3527 254.0595,-150.3527\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;7 -->\n",
+       "<g class=\"edge\" id=\"edge10\">\n",
+       "<title>4-&gt;7</title>\n",
+       "<path d=\"M216.063,-123.3986C225.3884,-126.8956 237.0837,-131.2814 247.284,-135.1065\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"254.0595,-137.6473 246.3991,-138.1388 250.7823,-136.4183 247.5052,-135.1894 247.5052,-135.1894 247.5052,-135.1894 250.7823,-136.4183 248.6112,-132.2399 254.0595,-137.6473 254.0595,-137.6473\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g class=\"node\" id=\"node10\">\n",
+       "<title>8</title>\n",
+       "<g id=\"a_node10\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=2\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"271\" cy=\"-90\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"271\" y=\"-86.3\">8</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;8 -->\n",
+       "<g class=\"edge\" id=\"edge11\">\n",
+       "<title>4-&gt;8</title>\n",
+       "<path d=\"M216.063,-110.6014C225.3884,-107.1044 237.0837,-102.7186 247.284,-98.8935\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"254.0595,-96.3527 248.6112,-101.7601 250.7823,-97.5817 247.5052,-98.8106 247.5052,-98.8106 247.5052,-98.8106 250.7823,-97.5817 246.3991,-95.8612 254.0595,-96.3527 254.0595,-96.3527\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;8 -->\n",
+       "<g class=\"edge\" id=\"edge12\">\n",
+       "<title>5-&gt;8</title>\n",
+       "<path d=\"M216.063,-69.3986C225.3884,-72.8956 237.0837,-77.2814 247.284,-81.1065\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"254.0595,-83.6473 246.3991,-84.1388 250.7823,-82.4183 247.5052,-81.1894 247.5052,-81.1894 247.5052,-81.1894 250.7823,-82.4183 248.6112,-78.2399 254.0595,-83.6473 254.0595,-83.6473\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 9 -->\n",
+       "<g class=\"node\" id=\"node11\">\n",
+       "<title>9</title>\n",
+       "<g id=\"a_node11\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=3\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead\">\n",
+       "<ellipse cx=\"271\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"271\" y=\"-14.3\">9</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;9 -->\n",
+       "<g class=\"edge\" id=\"edge13\">\n",
+       "<title>5-&gt;9</title>\n",
+       "<path d=\"M214.2693,-53.4567C224.4395,-47.1003 237.9581,-38.6512 249.2477,-31.5952\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"255.2549,-27.8407 250.9884,-34.2219 252.2869,-29.6957 249.3189,-31.5507 249.3189,-31.5507 249.3189,-31.5507 252.2869,-29.6957 247.6494,-28.8795 255.2549,-27.8407 255.2549,-27.8407\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;6 -->\n",
+       "<g class=\"edge\" id=\"edge14\">\n",
+       "<title>6-&gt;6</title>\n",
+       "<path d=\"M259.2435,-212.0417C254.8468,-222.9126 258.7656,-234 271,-234 280.5581,-234 285.0408,-227.2328 284.4481,-219.0885\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"282.7565,-212.0417 287.4535,-218.1131 283.5735,-215.4451 284.3905,-218.8484 284.3905,-218.8484 284.3905,-218.8484 283.5735,-215.4451 281.3275,-219.5837 282.7565,-212.0417 282.7565,-212.0417\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g class=\"node\" id=\"node12\">\n",
+       "<title>10</title>\n",
+       "<g id=\"a_node12\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=1\n",
+       "!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; dead\">\n",
+       "<ellipse cx=\"346.4481\" cy=\"-178\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"346.4481\" y=\"-174.3\">10</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;10 -->\n",
+       "<g class=\"edge\" id=\"edge15\">\n",
+       "<title>7-&gt;10</title>\n",
+       "<path d=\"M287.7444,-151.5457C297.3075,-155.8552 309.5081,-161.3533 320.3065,-166.2195\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"326.8127,-169.1515 319.1366,-169.1474 323.6218,-167.7135 320.4308,-166.2755 320.4308,-166.2755 320.4308,-166.2755 323.6218,-167.7135 321.725,-163.4036 326.8127,-169.1515 326.8127,-169.1515\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 11 -->\n",
+       "<g class=\"node\" id=\"node13\">\n",
+       "<title>11</title>\n",
+       "<g id=\"a_node13\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=2\n",
+       "!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
+       "<ellipse cx=\"346.4481\" cy=\"-117\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"346.4481\" y=\"-113.3\">11</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;11 -->\n",
+       "<g class=\"edge\" id=\"edge16\">\n",
+       "<title>7-&gt;11</title>\n",
+       "<path d=\"M288.1203,-137.8733C297.3932,-134.5549 309.062,-130.3791 319.5215,-126.636\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"326.1829,-124.2521 320.6536,-129.5766 322.8875,-125.4315 319.5922,-126.6108 319.5922,-126.6108 319.5922,-126.6108 322.8875,-125.4315 318.5308,-123.645 326.1829,-124.2521 326.1829,-124.2521\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;11 -->\n",
+       "<g class=\"edge\" id=\"edge17\">\n",
+       "<title>8-&gt;11</title>\n",
+       "<path d=\"M288.1203,-96.1267C297.3932,-99.4451 309.062,-103.6209 319.5215,-107.364\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"326.1829,-109.7479 318.5308,-110.355 322.8875,-108.5685 319.5922,-107.3892 319.5922,-107.3892 319.5922,-107.3892 322.8875,-108.5685 320.6536,-104.4234 326.1829,-109.7479 326.1829,-109.7479\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 12 -->\n",
+       "<g class=\"node\" id=\"node14\">\n",
+       "<title>12</title>\n",
+       "<g id=\"a_node14\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=3\n",
+       "&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead\">\n",
+       "<ellipse cx=\"346.4481\" cy=\"-38\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"346.4481\" y=\"-34.3\">12</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;12 -->\n",
+       "<g class=\"edge\" id=\"edge18\">\n",
+       "<title>8-&gt;12</title>\n",
+       "<path d=\"M285.9061,-79.7265C296.3653,-72.5179 310.5728,-62.7258 322.5961,-54.4391\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"328.653,-50.2646 324.677,-56.8307 325.7712,-52.2509 322.8894,-54.2371 322.8894,-54.2371 322.8894,-54.2371 325.7712,-52.2509 321.1018,-51.6434 328.653,-50.2646 328.653,-50.2646\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 9&#45;&gt;9 -->\n",
+       "<g class=\"edge\" id=\"edge19\">\n",
+       "<title>9-&gt;9</title>\n",
+       "<path d=\"M259.2435,-32.0417C254.8468,-42.9126 258.7656,-54 271,-54 280.5581,-54 285.0408,-47.2328 284.4481,-39.0885\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"282.7565,-32.0417 287.4535,-38.1131 283.5735,-35.4451 284.3905,-38.8484 284.3905,-38.8484 284.3905,-38.8484 283.5735,-35.4451 281.3275,-39.5837 282.7565,-32.0417 282.7565,-32.0417\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;10 -->\n",
+       "<g class=\"edge\" id=\"edge20\">\n",
+       "<title>10-&gt;10</title>\n",
+       "<path d=\"M333.6706,-195.4405C330.3374,-206.6551 334.5965,-217.4481 346.4481,-217.4481 355.7071,-217.4481 360.3321,-210.8606 360.3231,-202.631\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"359.2256,-195.4405 363.3958,-201.885 359.7537,-198.9004 360.2819,-202.3603 360.2819,-202.3603 360.2819,-202.3603 359.7537,-198.9004 357.1679,-202.8357 359.2256,-195.4405 359.2256,-195.4405\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 13 -->\n",
+       "<g class=\"node\" id=\"node15\">\n",
+       "<title>13</title>\n",
+       "<g id=\"a_node15\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=2\n",
+       "!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead\">\n",
+       "<ellipse cx=\"425.3443\" cy=\"-157\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"425.3443\" y=\"-153.3\">13</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 11&#45;&gt;13 -->\n",
+       "<g class=\"edge\" id=\"edge21\">\n",
+       "<title>11-&gt;13</title>\n",
+       "<path d=\"M365.9505,-126.8876C376.1735,-132.0706 388.8216,-138.4832 399.8153,-144.0569\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"406.0662,-147.2261 398.3983,-146.8702 402.9445,-145.6434 399.8228,-144.0607 399.8228,-144.0607 399.8228,-144.0607 402.9445,-145.6434 401.2472,-141.2511 406.0662,-147.2261 406.0662,-147.2261\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 14 -->\n",
+       "<g class=\"node\" id=\"node16\">\n",
+       "<title>14</title>\n",
+       "<g id=\"a_node16\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=3\n",
+       "!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead\">\n",
+       "<ellipse cx=\"425.3443\" cy=\"-78\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"425.3443\" y=\"-74.3\">14</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 11&#45;&gt;14 -->\n",
+       "<g class=\"edge\" id=\"edge22\">\n",
+       "<title>11-&gt;14</title>\n",
+       "<path d=\"M365.9505,-107.3595C376.0779,-102.3534 388.5854,-96.1707 399.5066,-90.7721\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"406.0662,-87.5296 401.1869,-93.4554 402.9286,-89.0806 399.791,-90.6316 399.791,-90.6316 399.791,-90.6316 402.9286,-89.0806 398.3951,-87.8077 406.0662,-87.5296 406.0662,-87.5296\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;12 -->\n",
+       "<g class=\"edge\" id=\"edge23\">\n",
+       "<title>12-&gt;12</title>\n",
+       "<path d=\"M333.6706,-55.4405C330.3374,-66.6551 334.5965,-77.4481 346.4481,-77.4481 355.7071,-77.4481 360.3321,-70.8606 360.3231,-62.631\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"359.2256,-55.4405 363.3958,-61.885 359.7537,-58.9004 360.2819,-62.3603 360.2819,-62.3603 360.2819,-62.3603 359.7537,-58.9004 357.1679,-62.8357 359.2256,-55.4405 359.2256,-55.4405\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 13&#45;&gt;13 -->\n",
+       "<g class=\"edge\" id=\"edge24\">\n",
+       "<title>13-&gt;13</title>\n",
+       "<path d=\"M412.0083,-174.03C408.2544,-185.3902 412.6998,-196.4481 425.3443,-196.4481 435.3216,-196.4481 440.194,-189.5633 439.9613,-181.0776\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"438.6803,-174.03 443.0315,-180.3538 439.3063,-177.4736 439.9323,-180.9172 439.9323,-180.9172 439.9323,-180.9172 439.3063,-177.4736 436.833,-181.4805 438.6803,-174.03 438.6803,-174.03\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;14 -->\n",
+       "<g class=\"edge\" id=\"edge25\">\n",
+       "<title>14-&gt;14</title>\n",
+       "<path d=\"M412.0083,-95.03C408.2544,-106.3902 412.6998,-117.4481 425.3443,-117.4481 435.3216,-117.4481 440.194,-110.5633 439.9613,-102.0776\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"438.6803,-95.03 443.0315,-101.3538 439.3063,-98.4736 439.9323,-101.9172 439.9323,-101.9172 439.9323,-101.9172 439.3063,-98.4736 436.833,-102.4805 438.6803,-95.03 438.6803,-95.03\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.SVG object>"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "k.show('.1')"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Another option is to use option `K` to disable to state-labeling (that is enabled by default for Kripke structure) and use transition-labeling instead.  Combining with `1`, this will preserve the state's data as a tooltip."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<svg height=\"145pt\" viewBox=\"0.00 0.00 734.00 144.84\" 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(.4584 .4584) rotate(0) translate(4 312)\">\n",
+       "<polygon fill=\"#ffffff\" points=\"-4,4 -4,-312 1597.3443,-312 1597.3443,4 -4,4\" stroke=\"transparent\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"793.6721\" y=\"-292.8\">t</text>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"785.6721\" y=\"-277.8\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g class=\"node\" id=\"node2\">\n",
+       "<title>0</title>\n",
+       "<g id=\"a_node2\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=0\">\n",
+       "<ellipse cx=\"56\" cy=\"-124\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-120.3\">0</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g class=\"edge\" id=\"edge1\">\n",
+       "<title>I-&gt;0</title>\n",
+       "<path d=\"M1.1233,-124C4.178,-124 17.9448,-124 30.9241,-124\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"37.9807,-124 30.9808,-127.1501 34.4807,-124 30.9807,-124.0001 30.9807,-124.0001 30.9807,-124.0001 34.4807,-124 30.9807,-120.8501 37.9807,-124 37.9807,-124\" stroke=\"#000000\"/>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g class=\"node\" id=\"node3\">\n",
+       "<title>1</title>\n",
+       "<g id=\"a_node3\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=0\">\n",
+       "<ellipse cx=\"339\" cy=\"-151\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"339\" y=\"-147.3\">1</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;1 -->\n",
+       "<g class=\"edge\" id=\"edge2\">\n",
+       "<title>0-&gt;1</title>\n",
+       "<path d=\"M74.1334,-125.73C123.0527,-130.3973 257.8131,-143.2543 313.9471,-148.6098\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"321.0176,-149.2844 313.75,-151.7552 317.5334,-148.9519 314.0492,-148.6194 314.0492,-148.6194 314.0492,-148.6194 317.5334,-148.9519 314.3484,-145.4837 321.0176,-149.2844 321.0176,-149.2844\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-150.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g class=\"node\" id=\"node4\">\n",
+       "<title>2</title>\n",
+       "<g id=\"a_node4\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=1\">\n",
+       "<ellipse cx=\"339\" cy=\"-97\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"339\" y=\"-93.3\">2</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g class=\"edge\" id=\"edge3\">\n",
+       "<title>0-&gt;2</title>\n",
+       "<path d=\"M72.0948,-115.8947C78.1791,-113.2081 85.2627,-110.5184 92,-109 171.3469,-91.1175 268.5282,-93.1308 313.6908,-95.3859\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"320.7377,-95.7614 313.58,-98.5344 317.2426,-95.5751 313.7476,-95.3889 313.7476,-95.3889 313.7476,-95.3889 317.2426,-95.5751 313.9152,-92.2433 320.7377,-95.7614 320.7377,-95.7614\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-112.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g class=\"node\" id=\"node5\">\n",
+       "<title>3</title>\n",
+       "<g id=\"a_node5\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=0\">\n",
+       "<ellipse cx=\"622\" cy=\"-181\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"622\" y=\"-177.3\">3</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;3 -->\n",
+       "<g class=\"edge\" id=\"edge4\">\n",
+       "<title>1-&gt;3</title>\n",
+       "<path d=\"M356.4916,-155.3657C362.3452,-156.6984 368.9261,-158.0587 375,-159 455.4345,-171.4653 551.7818,-177.518 596.6674,-179.8309\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"603.9277,-180.1953 596.7785,-182.9904 600.4321,-180.0199 596.9365,-179.8444 596.9365,-179.8444 596.9365,-179.8444 600.4321,-180.0199 597.0944,-176.6983 603.9277,-180.1953 603.9277,-180.1953\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"375\" y=\"-182.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g class=\"node\" id=\"node6\">\n",
+       "<title>4</title>\n",
+       "<g id=\"a_node6\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=1\">\n",
+       "<ellipse cx=\"622\" cy=\"-124\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"622\" y=\"-120.3\">4</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;4 -->\n",
+       "<g class=\"edge\" id=\"edge5\">\n",
+       "<title>1-&gt;4</title>\n",
+       "<path d=\"M356.8799,-147.1161C362.6418,-145.974 369.0706,-144.814 375,-144 455.5833,-132.938 551.8597,-127.3067 596.6979,-125.1182\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"603.9503,-124.7725 597.1082,-128.2523 600.4543,-124.9392 596.9582,-125.1059 596.9582,-125.1059 596.9582,-125.1059 600.4543,-124.9392 596.8082,-121.9594 603.9503,-124.7725 603.9503,-124.7725\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"375\" y=\"-147.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;4 -->\n",
+       "<g class=\"edge\" id=\"edge6\">\n",
+       "<title>2-&gt;4</title>\n",
+       "<path d=\"M357.011,-95.3125C398.2549,-91.9674 502.4344,-86.4773 586,-107 590.6903,-108.1519 595.5022,-109.9415 600.0199,-111.9348\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"606.3799,-114.9506 598.7053,-114.7976 603.2174,-113.451 600.0549,-111.9514 600.0549,-111.9514 600.0549,-111.9514 603.2174,-113.451 601.4046,-109.1051 606.3799,-114.9506 606.3799,-114.9506\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"375\" y=\"-110.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 5 -->\n",
+       "<g class=\"node\" id=\"node7\">\n",
+       "<title>5</title>\n",
+       "<g id=\"a_node7\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=2\">\n",
+       "<ellipse cx=\"622\" cy=\"-67\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"622\" y=\"-63.3\">5</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;5 -->\n",
+       "<g class=\"edge\" id=\"edge7\">\n",
+       "<title>2-&gt;5</title>\n",
+       "<path d=\"M353.1631,-85.4308C359.459,-80.9825 367.2023,-76.3987 375,-74 453.0699,-49.9845 551.6427,-57.82 597.0346,-63.4126\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"604.1083,-64.3198 596.7644,-66.5536 600.6368,-63.8745 597.1652,-63.4292 597.1652,-63.4292 597.1652,-63.4292 600.6368,-63.8745 597.566,-60.3048 604.1083,-64.3198 604.1083,-64.3198\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"375\" y=\"-77.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g class=\"node\" id=\"node8\">\n",
+       "<title>6</title>\n",
+       "<g id=\"a_node8\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=0\">\n",
+       "<ellipse cx=\"909\" cy=\"-219\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"909\" y=\"-215.3\">6</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;6 -->\n",
+       "<g class=\"edge\" id=\"edge8\">\n",
+       "<title>3-&gt;6</title>\n",
+       "<path d=\"M638.076,-189.5095C644.1584,-192.3605 651.2455,-195.255 658,-197 738.4394,-217.7818 837.6774,-219.8367 883.5454,-219.513\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"890.6971,-219.4397 883.7298,-222.6614 887.1973,-219.4756 883.6975,-219.5116 883.6975,-219.5116 883.6975,-219.5116 887.1973,-219.4756 883.6651,-216.3618 890.6971,-219.4397 890.6971,-219.4397\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"658\" y=\"-222.8\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g class=\"node\" id=\"node9\">\n",
+       "<title>7</title>\n",
+       "<g id=\"a_node9\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=1\">\n",
+       "<ellipse cx=\"909\" cy=\"-162\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"909\" y=\"-158.3\">7</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;7 -->\n",
+       "<g class=\"edge\" id=\"edge9\">\n",
+       "<title>3-&gt;7</title>\n",
+       "<path d=\"M640.3897,-179.7826C690.0004,-176.4982 826.6656,-167.4507 883.593,-163.682\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"890.7634,-163.2073 883.9868,-166.8129 887.2711,-163.4385 883.7787,-163.6698 883.7787,-163.6698 883.7787,-163.6698 887.2711,-163.4385 883.5706,-160.5267 890.7634,-163.2073 890.7634,-163.2073\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"658\" y=\"-181.8\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;7 -->\n",
+       "<g class=\"edge\" id=\"edge10\">\n",
+       "<title>4-&gt;7</title>\n",
+       "<path d=\"M640.024,-123.3352C681.7908,-122.2601 788.1123,-122.2066 873,-145 877.6644,-146.2525 882.4646,-148.0877 886.9789,-150.0943\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"893.3392,-153.1089 885.6646,-152.9573 890.1765,-151.6099 887.0137,-150.1108 887.0137,-150.1108 887.0137,-150.1108 890.1765,-151.6099 888.3629,-147.2643 893.3392,-153.1089 893.3392,-153.1089\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"660\" y=\"-148.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g class=\"node\" id=\"node10\">\n",
+       "<title>8</title>\n",
+       "<g id=\"a_node10\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=2\">\n",
+       "<ellipse cx=\"909\" cy=\"-105\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"909\" y=\"-101.3\">8</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;8 -->\n",
+       "<g class=\"edge\" id=\"edge11\">\n",
+       "<title>4-&gt;8</title>\n",
+       "<path d=\"M637.5264,-114.2792C643.6636,-110.9702 650.9305,-107.6838 658,-106 738.7126,-86.7765 838.2097,-95.5949 883.9018,-101.3765\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"891.0201,-102.3085 883.6704,-104.523 887.5497,-101.8541 884.0793,-101.3997 884.0793,-101.3997 884.0793,-101.3997 887.5497,-101.8541 884.4883,-98.2763 891.0201,-102.3085 891.0201,-102.3085\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"660\" y=\"-109.8\">&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;8 -->\n",
+       "<g class=\"edge\" id=\"edge12\">\n",
+       "<title>5-&gt;8</title>\n",
+       "<path d=\"M639.7767,-63.9238C681.906,-57.4113 790.4721,-45.2204 873,-76 879.5163,-78.4303 885.746,-82.5382 891.1365,-86.9095\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"896.6303,-91.6892 889.2816,-89.471 893.9898,-89.3919 891.3492,-87.0945 891.3492,-87.0945 891.3492,-87.0945 893.9898,-89.3919 893.4168,-84.7181 896.6303,-91.6892 896.6303,-91.6892\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"661.5\" y=\"-79.8\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 9 -->\n",
+       "<g class=\"node\" id=\"node11\">\n",
+       "<title>9</title>\n",
+       "<g id=\"a_node11\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=3\">\n",
+       "<ellipse cx=\"909\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"909\" y=\"-14.3\">9</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;9 -->\n",
+       "<g class=\"edge\" id=\"edge13\">\n",
+       "<title>5-&gt;9</title>\n",
+       "<path d=\"M634.3491,-53.39C640.7594,-47.2624 649.1032,-40.6067 658,-37 735.4952,-5.5841 837.3723,-10.5169 883.8873,-15.0122\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"891.1273,-15.7526 883.8432,-18.1741 887.6455,-15.3965 884.1637,-15.0404 884.1637,-15.0404 884.1637,-15.0404 887.6455,-15.3965 884.4841,-11.9067 891.1273,-15.7526 891.1273,-15.7526\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"661.5\" y=\"-40.8\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;6 -->\n",
+       "<g class=\"edge\" id=\"edge14\">\n",
+       "<title>6-&gt;6</title>\n",
+       "<path d=\"M892.517,-226.9571C874.8006,-239.3082 880.2949,-255 909,-255 934.1169,-255 941.4632,-242.986 931.0386,-231.7082\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"925.483,-226.9571 932.8503,-229.1127 928.143,-229.2319 930.803,-231.5066 930.803,-231.5066 930.803,-231.5066 928.143,-229.2319 928.7557,-233.9006 925.483,-226.9571 925.483,-226.9571\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"803.5\" y=\"-258.8\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g class=\"node\" id=\"node12\">\n",
+       "<title>10</title>\n",
+       "<g id=\"a_node12\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=1\">\n",
+       "<ellipse cx=\"1199.4481\" cy=\"-209\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1199.4481\" y=\"-205.3\">10</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;10 -->\n",
+       "<g class=\"edge\" id=\"edge15\">\n",
+       "<title>7-&gt;10</title>\n",
+       "<path d=\"M925.1091,-170.3858C931.1951,-173.2234 938.276,-176.141 945,-178 1024.8004,-200.0622 1123.0007,-206.4301 1170.7095,-208.2629\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1177.9224,-208.5198 1170.8147,-211.4186 1174.4246,-208.3952 1170.9268,-208.2705 1170.9268,-208.2705 1170.9268,-208.2705 1174.4246,-208.3952 1171.039,-205.1225 1177.9224,-208.5198 1177.9224,-208.5198\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"945\" y=\"-210.8\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 11 -->\n",
+       "<g class=\"node\" id=\"node13\">\n",
+       "<title>11</title>\n",
+       "<g id=\"a_node13\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=2\">\n",
+       "<ellipse cx=\"1199.4481\" cy=\"-148\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1199.4481\" y=\"-144.3\">11</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 7&#45;&gt;11 -->\n",
+       "<g class=\"edge\" id=\"edge16\">\n",
+       "<title>7-&gt;11</title>\n",
+       "<path d=\"M927.1688,-161.1242C976.1181,-158.7648 1111.0587,-152.2605 1170.5891,-149.391\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1177.8009,-149.0434 1170.9607,-152.5269 1174.305,-149.212 1170.809,-149.3805 1170.809,-149.3805 1170.809,-149.3805 1174.305,-149.212 1170.6573,-146.2342 1177.8009,-149.0434 1177.8009,-149.0434\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"945\" y=\"-162.8\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;11 -->\n",
+       "<g class=\"edge\" id=\"edge17\">\n",
+       "<title>8-&gt;11</title>\n",
+       "<path d=\"M927.2917,-105.0114C969.1809,-105.4423 1075.0035,-108.8384 1160,-131 1164.4515,-132.1607 1169.0483,-133.7491 1173.4618,-135.4917\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1180.1992,-138.3177 1172.5256,-138.5149 1176.9716,-136.9639 1173.744,-135.61 1173.744,-135.61 1173.744,-135.61 1176.9716,-136.9639 1174.9625,-132.7052 1180.1992,-138.3177 1180.1992,-138.3177\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"948.5\" y=\"-134.8\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 12 -->\n",
+       "<g class=\"node\" id=\"node14\">\n",
+       "<title>12</title>\n",
+       "<g id=\"a_node14\"><a xlink:title=\"P_0._pc=0, P_0.a=1, P_0.b=3\">\n",
+       "<ellipse cx=\"1199.4481\" cy=\"-54\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1199.4481\" y=\"-50.3\">12</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;12 -->\n",
+       "<g class=\"edge\" id=\"edge18\">\n",
+       "<title>8-&gt;12</title>\n",
+       "<path d=\"M924.6522,-95.7427C930.8049,-92.4906 938.0495,-89.122 945,-87 1024.2629,-62.8012 1122.707,-56.3459 1170.5891,-54.6249\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1177.8291,-54.3873 1170.9362,-57.7653 1174.331,-54.5022 1170.8329,-54.617 1170.8329,-54.617 1170.8329,-54.617 1174.331,-54.5022 1170.7295,-51.4687 1177.8291,-54.3873 1177.8291,-54.3873\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"948.5\" y=\"-90.8\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 9&#45;&gt;9 -->\n",
+       "<g class=\"edge\" id=\"edge19\">\n",
+       "<title>9-&gt;9</title>\n",
+       "<path d=\"M892.517,-25.9571C874.8006,-38.3082 880.2949,-54 909,-54 934.1169,-54 941.4632,-41.986 931.0386,-30.7082\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"925.483,-25.9571 932.8503,-28.1127 928.143,-28.2319 930.803,-30.5066 930.803,-30.5066 930.803,-30.5066 928.143,-28.2319 928.7557,-32.9006 925.483,-25.9571 925.483,-25.9571\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"807\" y=\"-57.8\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;10 -->\n",
+       "<g class=\"edge\" id=\"edge20\">\n",
+       "<title>10-&gt;10</title>\n",
+       "<path d=\"M1180.523,-219.5036C1165.296,-232.716 1171.6043,-248.4481 1199.4481,-248.4481 1223.5938,-248.4481 1231.5447,-236.6174 1223.3006,-224.8585\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1218.3731,-219.5036 1225.431,-222.5217 1220.7431,-222.0791 1223.113,-224.6547 1223.113,-224.6547 1223.113,-224.6547 1220.7431,-222.0791 1220.795,-226.7876 1218.3731,-219.5036 1218.3731,-219.5036\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1093.9481\" y=\"-252.2481\">!&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
+       "</g>\n",
+       "<!-- 13 -->\n",
+       "<g class=\"node\" id=\"node15\">\n",
+       "<title>13</title>\n",
+       "<g id=\"a_node15\"><a xlink:title=\"P_0._pc=0, P_0.a=3, P_0.b=2\">\n",
+       "<ellipse cx=\"1489.3443\" cy=\"-188\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1489.3443\" y=\"-184.3\">13</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 11&#45;&gt;13 -->\n",
+       "<g class=\"edge\" id=\"edge21\">\n",
+       "<title>11-&gt;13</title>\n",
+       "<path d=\"M1220.7649,-150.9413C1272.1766,-158.0351 1403.0149,-176.0882 1460.9717,-184.0851\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1467.9963,-185.0544 1460.6314,-187.2179 1464.5291,-184.576 1461.062,-184.0975 1461.062,-184.0975 1461.062,-184.0975 1464.5291,-184.576 1461.4926,-180.9771 1467.9963,-185.0544 1467.9963,-185.0544\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1238.8962\" y=\"-185.8\">!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 14 -->\n",
+       "<g class=\"node\" id=\"node16\">\n",
+       "<title>14</title>\n",
+       "<g id=\"a_node16\"><a xlink:title=\"P_0._pc=0, P_0.a=2, P_0.b=3\">\n",
+       "<ellipse cx=\"1489.3443\" cy=\"-94\" fill=\"#ffffaa\" rx=\"21.3963\" ry=\"21.3963\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1489.3443\" y=\"-90.3\">14</text>\n",
+       "</a>\n",
+       "</g>\n",
+       "</g>\n",
+       "<!-- 11&#45;&gt;14 -->\n",
+       "<g class=\"edge\" id=\"edge22\">\n",
+       "<title>11-&gt;14</title>\n",
+       "<path d=\"M1219.7032,-140.0131C1225.8015,-137.8264 1232.5586,-135.6162 1238.8962,-134 1318.0725,-113.808 1414.0628,-101.8713 1460.8858,-96.8318\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1467.9683,-96.082 1461.3389,-99.9515 1464.4878,-96.4505 1461.0072,-96.819 1461.0072,-96.819 1461.0072,-96.819 1464.4878,-96.4505 1460.6756,-93.6865 1467.9683,-96.082 1467.9683,-96.082\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1238.8962\" y=\"-137.8\">!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; !dead</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;12 -->\n",
+       "<g class=\"edge\" id=\"edge23\">\n",
+       "<title>12-&gt;12</title>\n",
+       "<path d=\"M1180.523,-64.5036C1165.296,-77.716 1171.6043,-93.4481 1199.4481,-93.4481 1223.5938,-93.4481 1231.5447,-81.6174 1223.3006,-69.8585\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1218.3731,-64.5036 1225.431,-67.5217 1220.7431,-67.0791 1223.113,-69.6547 1223.113,-69.6547 1223.113,-69.6547 1220.7431,-67.0791 1220.795,-71.7876 1218.3731,-64.5036 1218.3731,-64.5036\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1097.4481\" y=\"-97.2481\">&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
+       "</g>\n",
+       "<!-- 13&#45;&gt;13 -->\n",
+       "<g class=\"edge\" id=\"edge24\">\n",
+       "<title>13-&gt;13</title>\n",
+       "<path d=\"M1470.4192,-198.5036C1455.1922,-211.716 1461.5005,-227.4481 1489.3443,-227.4481 1513.49,-227.4481 1521.4409,-215.6174 1513.1968,-203.8585\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1508.2693,-198.5036 1515.3272,-201.5217 1510.6393,-201.0791 1513.0092,-203.6547 1513.0092,-203.6547 1513.0092,-203.6547 1510.6393,-201.0791 1510.6912,-205.7876 1508.2693,-198.5036 1508.2693,-198.5036\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1385.3443\" y=\"-231.2481\">!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;14 -->\n",
+       "<g class=\"edge\" id=\"edge25\">\n",
+       "<title>14-&gt;14</title>\n",
+       "<path d=\"M1470.4192,-104.5036C1455.1922,-117.716 1461.5005,-133.4481 1489.3443,-133.4481 1513.49,-133.4481 1521.4409,-121.6174 1513.1968,-109.8585\" fill=\"none\" stroke=\"#000000\"/>\n",
+       "<polygon fill=\"#000000\" points=\"1508.2693,-104.5036 1515.3272,-107.5217 1510.6393,-107.0791 1513.0092,-109.6547 1513.0092,-109.6547 1513.0092,-109.6547 1510.6393,-107.0791 1510.6912,-111.7876 1508.2693,-104.5036 1508.2693,-104.5036\" stroke=\"#000000\"/>\n",
+       "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1385.3443\" y=\"-137.2481\">!&quot;P_0.a &lt; 2&quot; &amp; &quot;P_0.b &gt; 1&quot; &amp; dead</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>"
+      ],
+      "text/plain": [
+       "<IPython.core.display.SVG object>"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "k.show('.1K')"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
     "Loading from a `*.pml` file\n",
     "---------------------------\n",
     "\n",
@@ -586,7 +1274,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -595,7 +1283,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 8,
    "metadata": {},
    "outputs": [
     {
@@ -627,7 +1315,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 9,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -636,7 +1324,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 10,
    "metadata": {},
    "outputs": [
     {
@@ -648,7 +1336,7 @@
        "  P_0.b: int"
       ]
      },
-     "execution_count": 8,
+     "execution_count": 10,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -659,7 +1347,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 11,
    "metadata": {},
    "outputs": [],
    "source": [