From b11c07b3516865ed806596e1bb1202b1186eeddb Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 28 Jan 2016 17:45:50 +0100
Subject: [PATCH] dot: add a <N option

* spot/twaalgos/dot.cc: Implement it.
* spot/taalgos/dot.cc: Ignore it.
* spot/twaalgos/copy.cc, spot/twaalgos/copy.hh: Add option
to limit the number of states.
* tests/python/ltsmin.ipynb: Improve test case.
* tests/Makefile.am: Cleanup the files generated by ltsmin.ipynb.
* python/spot/__init__.py (setup): Add a max_states argument
that default to 50.
* bin/common_aoutput.cc: Mention the <INT option.
* NEWS: Likewise.
---
 NEWS                      |   12 +
 bin/common_aoutput.cc     |    5 +-
 python/spot/__init__.py   |    5 +-
 spot/taalgos/dot.cc       |   15 +-
 spot/twaalgos/copy.cc     |   28 +-
 spot/twaalgos/copy.hh     |    3 +-
 spot/twaalgos/dot.cc      |   43 +-
 tests/Makefile.am         |    2 +-
 tests/python/ltsmin.ipynb | 1396 +++++++++++++++++++++++++++----------
 9 files changed, 1145 insertions(+), 364 deletions(-)

diff --git a/NEWS b/NEWS
index 25682d60c..e1ed299a7 100644
--- a/NEWS
+++ b/NEWS
@@ -12,11 +12,23 @@ New in spot 1.99.7a (not yet released)
     object can be queried about the supported variables and their
     types.
 
+  * print_dot() now accepts an option of the form "<N" to specify
+    a maximum number of states to output.  Incomplete states are
+    then marked appropriately.  For a quick example, compare
+       ltl2tgba -D 'Ga | Gb | Gc' -d'<3'
+    with
+       ltl2tgba -D 'Ga | Gb | Gc' -d
+
   Python:
 
   * The ltsmin interface has been binded in Python.  See
     https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example.
 
+  * spot.setup() sets de maximum number of states to display in
+    automata to 50 by default, as more states is likely to be
+    unreadable (and slow to process by GraphViz).  This can be
+    overridden by calling spot.setup(max_states=N).
+
   Documentation:
 
   * There is a new page giving informal illustrations (and extra
diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc
index 482126d40..ccca94d21 100644
--- a/bin/common_aoutput.cc
+++ b/bin/common_aoutput.cc
@@ -80,7 +80,7 @@ static const argp_option options[] =
   {
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Output format:", 3 },
-    { "dot", 'd', "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT",
+    { "dot", 'd', "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT|<INT",
       OPTION_ARG_OPTIONAL,
       "GraphViz's format.  Add letters for "
       "(1) force numbered states, "
@@ -93,7 +93,8 @@ static const argp_option options[] =
       "(r) rainbow colors for acceptance sets, "
       "(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
       "(t) force transition-based acceptance, "
-      "(+INT) add INT to all set numbers", 0 },
+      "(+INT) add INT to all set numbers, "
+      "(<INT) display at most INT states", 0 },
     { "hoaf", 'H', "i|l|m|s|t|v", OPTION_ARG_OPTIONAL,
       "Output the automaton in HOA format (default).  Add letters to select "
       "(i) use implicit labels for complete deterministic automata, "
diff --git a/python/spot/__init__.py b/python/spot/__init__.py
index dbab62b50..29f9e3509 100644
--- a/python/spot/__init__.py
+++ b/python/spot/__init__.py
@@ -71,6 +71,8 @@ def setup(**kwargs):
         the font to use in the GraphViz output (default: 'Lato')
     show_default : str
         default options for show()
+    max_states : int
+        maximum number of states in GraphViz output (default: 50)
     """
     import os
 
@@ -80,7 +82,8 @@ def setup(**kwargs):
                                            kwargs.get('fillcolor', '#ffffaa'))
 
     bullets = 'B' if kwargs.get('bullets', True) else ''
-    d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets
+    max_states = '<' + str(kwargs.get('max_states', 50))
+    d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets + max_states
     global _show_default
     _show_default = kwargs.get('show_default', None)
     os.environ['SPOT_DOTDEFAULT'] = d
diff --git a/spot/taalgos/dot.cc b/spot/taalgos/dot.cc
index d2931e19c..5e2e4d9a0 100644
--- a/spot/taalgos/dot.cc
+++ b/spot/taalgos/dot.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et
-// Developpement de l Epita (LRDE).
+// Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche
+// et Developpement de l Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -84,7 +84,16 @@ namespace spot
 	    case 'v':
 	      opt_horizontal_ = false;
 	      break;
+	    case '0':
 	    case '1':
+	    case '2':
+	    case '3':
+	    case '4':
+	    case '5':
+	    case '6':
+	    case '7':
+	    case '8':
+	    case '9':
 	    case 'a':
 	    case 'b':
 	    case 'B':
@@ -96,6 +105,8 @@ namespace spot
 	    case 'R':
 	    case 's':
 	    case 't':
+	    case '+':
+	    case '<':
 	      // All these options are implemented by dotty() on TGBA,
 	      // but are not implemented here.  We simply ignore them,
 	      // because raising an exception if they are in
diff --git a/spot/twaalgos/copy.cc b/spot/twaalgos/copy.cc
index 9e9934e70..3b33e1a58 100644
--- a/spot/twaalgos/copy.cc
+++ b/spot/twaalgos/copy.cc
@@ -27,13 +27,15 @@
 namespace spot
 {
   twa_graph_ptr
-  copy(const const_twa_ptr& aut, twa::prop_set p, bool preserve_names)
+  copy(const const_twa_ptr& aut, twa::prop_set p,
+       bool preserve_names, unsigned max_states)
   {
     twa_graph_ptr out = make_twa_graph(aut->get_dict());
     out->copy_acceptance_of(aut);
     out->copy_ap_of(aut);
     out->prop_copy(aut, p);
     std::vector<std::string>* names = nullptr;
+    std::set<unsigned>* incomplete = nullptr;
     if (preserve_names)
       {
 	names = new std::vector<std::string>;
@@ -69,9 +71,27 @@ namespace spot
 	unsigned src2;
 	std::tie(src1, src2) = *todo.front();
 	todo.pop_front();
-
 	for (auto* t: aut->succ(src1))
-	  out->new_edge(src2, new_state(t->dst()), t->cond(), t->acc());
+	  {
+	    if (SPOT_UNLIKELY(max_states < out->num_states()))
+	      {
+		// If we have reached the max number of state, never try
+		// to create a new one.
+		auto i = seen.find(t->dst());
+		if (i == seen.end())
+		  {
+		    if (!incomplete)
+		      incomplete = new std::set<unsigned>;
+		    incomplete->insert(src2);
+		    continue;
+		  }
+		out->new_edge(src2, i->second, t->cond(), t->acc());
+	      }
+	    else
+	      {
+		out->new_edge(src2, new_state(t->dst()), t->cond(), t->acc());
+	      }
+	  }
       }
 
 
@@ -84,6 +104,8 @@ namespace spot
 	ptr->destroy();
       }
 
+    if (incomplete)
+      out->set_named_prop("incomplete-states", incomplete);
     return out;
   }
 }
diff --git a/spot/twaalgos/copy.hh b/spot/twaalgos/copy.hh
index b4a6a0296..c718e3519 100644
--- a/spot/twaalgos/copy.hh
+++ b/spot/twaalgos/copy.hh
@@ -33,5 +33,6 @@ namespace spot
   ///
   /// This works for using the abstract interface for automata
   SPOT_API twa_graph_ptr
-  copy(const const_twa_ptr& aut, twa::prop_set p, bool preserve_names = false);
+  copy(const const_twa_ptr& aut, twa::prop_set p,
+       bool preserve_names = false, unsigned max_states = -1U);
 }
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 1265cc579..daa2e62e1 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -57,6 +57,7 @@ namespace spot
       const_twa_graph_ptr aut_;
       std::vector<std::string>* sn_ = nullptr;
       std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
+      std::set<unsigned>* incomplete_;
       std::string* name_ = nullptr;
       acc_cond::mark_t inf_sets_ = 0U;
       acc_cond::mark_t fin_sets_ = 0U;
@@ -83,9 +84,21 @@ namespace spot
 	};
       const char*const* palette = palette9;
       int palette_mod = 9;
+      unsigned max_states_ = -1U;
+      bool max_states_given_ = false;
 
     public:
 
+      unsigned max_states()
+      {
+	return max_states_;
+      }
+
+      bool max_states_given()
+      {
+	return max_states_given_;
+      }
+
       void
       parse_opts(const char* options)
       {
@@ -95,7 +108,7 @@ namespace spot
 	    {
 	    case '.':
 	      {
-	        // Copy the value in a string, so future calls to
+		// Copy the value in a string, so future calls to
 		// parse_opts do not fail if the environment has
 		// changed.  (This matters particularly in an ipython
 		// notebook, where it is tempting to redefine
@@ -123,6 +136,25 @@ namespace spot
 		options = end;
 		break;
 	      }
+	    case '<':
+	      {
+		char* end;
+		max_states_ = strtoul(options, &end, 10);
+		if (options == end)
+		  throw std::runtime_error
+		    ("missing number after '<' in print_dot() options");
+		if (max_states_ == 0)
+		  {
+		    max_states_ = -1U;
+		    max_states_given_ = false;
+		  }
+		else
+		  {
+		    max_states_given_ = true;
+		  }
+		options = end;
+		break;
+	      }
 	    case '1':
 	      opt_want_state_names_ = false;
 	      break;
@@ -445,6 +477,9 @@ namespace spot
 	      os_ << ", peripheries=2";
 	    os_ << "]\n";
 	  }
+	if (incomplete_ && incomplete_->find(s) != incomplete_->end())
+	  os_ << "  u" << s << " [label=\"...\", shape=none, width=0, height=0"
+	    "]\n  " << s << " -> u" << s << " [style=dashed]\n";
       }
 
       void
@@ -497,6 +532,8 @@ namespace spot
 		  sprod_ = nullptr;
 	      }
 	  }
+	incomplete_ =
+	  aut->get_named_prop<std::set<unsigned>>("incomplete-states");
 	if (opt_name_)
 	  name_ = aut_->get_named_prop<std::string>("automaton-name");
 	mark_states_ = (!opt_force_acc_trans_
@@ -566,8 +603,8 @@ namespace spot
   {
     dotty_output d(os, options);
     auto aut = std::dynamic_pointer_cast<const twa_graph>(g);
-    if (!aut)
-      aut = copy(g, twa::prop_set::all(), true);
+    if (!aut || (d.max_states_given() && aut->num_states() >= d.max_states()))
+      aut = copy(g, twa::prop_set::all(), true, d.max_states() - 1);
     d.print(aut);
     return os;
   }
diff --git a/tests/Makefile.am b/tests/Makefile.am
index a69507cb4..1e22ade06 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -316,7 +316,7 @@ TESTS_python = \
   python/trival.py
 endif
 
-CLEANFILES = python/finite.dve2C python/finite.dve.cpp
+CLEANFILES = python/test1.dve python/test1.dve2C python/test1.dve.cpp
 
 SUFFIXES = .ipynb .html
 .ipynb.html:
diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb
index de6a7d238..e96a57a35 100644
--- a/tests/python/ltsmin.ipynb
+++ b/tests/python/ltsmin.ipynb
@@ -1,7 +1,7 @@
 {
  "metadata": {
   "name": "",
-  "signature": "sha256:83724638edf025d8183ef0d5193234734b94f7e3470d9034bea411e730c834c6"
+  "signature": "sha256:5cb288dca975d2e3b9a45bf32740468542c11fbd89d5a3df2155fe7e53ce9834"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -12,15 +12,14 @@
      "cell_type": "markdown",
      "metadata": {},
      "source": [
-      "This first chunk just makes sure the version of divine instaled accepts the `--LTSmin` option.  If that is not the case, this notebook should be skipped by the test suite: `sys.exit(77)` does that."
+      "This first chunk just makes sure the version of DiVinE installed accepts the `--LTSmin` option.  If that is not the case, this notebook should be skipped by the test suite: `sys.exit(77)` does that."
      ]
     },
     {
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "import os, sys\n",
-      "srcdir = os.environ.get('srcdir', '.')\n",
+      "import sys\n",
       "# Make sure we have divine and that it is patched to accept the --LTSmin option.\n",
       "import shutil\n",
       "if shutil.which(\"divine\") == None:\n",
@@ -48,42 +47,75 @@
      "input": [
       "import spot\n",
       "import spot.ltsmin\n",
-      "spot.setup()"
+      "# This is notebook also tests the limitation of the number of states in the GraphViz output\n",
+      "spot.setup(max_states=10)"
      ],
      "language": "python",
      "metadata": {},
      "outputs": [],
      "prompt_number": 2
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Write an example DiVinE model. "
+     ]
+    },
     {
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "m = spot.ltsmin.load(srcdir + '/../ltsmin/finite.dve')\n",
-      "m"
+      "%%file test1.dve\n",
+      "int a = 0, b = 0;\n",
+      "\n",
+      "process P {\n",
+      " state x;\n",
+      " init x;\n",
+      "\n",
+      " trans\n",
+      "   x -> x { guard a < 3 && b < 3; effect a = a + 1; },\n",
+      "   x -> x { guard a < 3 && b < 3; effect b = b + 1; };\n",
+      "}\n",
+      "\n",
+      "process Q {\n",
+      "  state wait, work;\n",
+      "  init wait;\n",
+      "  trans\n",
+      "    wait -> work { guard b > 1; },\n",
+      "    work -> wait { guard a > 1; };\n",
+      "}\n",
+      "\n",
+      "system async;"
      ],
      "language": "python",
      "metadata": {},
      "outputs": [
       {
-       "metadata": {},
-       "output_type": "pyout",
-       "prompt_number": 3,
+       "output_type": "stream",
+       "stream": "stdout",
        "text": [
-        "ltsmin model with the following variables:\n",
-        "  P: ['x']\n",
-        "  P.a: int\n",
-        "  P.b: int"
+        "Overwriting test1.dve\n"
        ]
       }
      ],
      "prompt_number": 3
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Compile the model using the `ltlmin` interface and load it.  This should work with DiVinE models if `divine --LTSmin` works, and with Promela models if `spins` is installed.\n",
+      "\n",
+      "Printing an ltsmin model shows some information about the variables it contains and their types."
+     ]
+    },
     {
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "m.info()"
+      "m = spot.ltsmin.load('test1.dve')\n",
+      "m"
      ],
      "language": "python",
      "metadata": {},
@@ -93,9 +125,11 @@
        "output_type": "pyout",
        "prompt_number": 4,
        "text": [
-        "{'state_size': 3,\n",
-        " 'variables': [('P', 0), ('P.a', 1), ('P.b', 1)],\n",
-        " 'types': [('P', ['x']), ('int', [])]}"
+        "ltsmin model with the following variables:\n",
+        "  a: int\n",
+        "  b: int\n",
+        "  P: ['x']\n",
+        "  Q: ['wait', 'work']"
        ]
       }
      ],
@@ -105,8 +139,7 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "k = m.kripke([\"P.a<1\", \"P.b>2\"])\n",
-      "k"
+      "sorted(m.info().items())"
      ],
      "language": "python",
      "metadata": {},
@@ -115,248 +148,10 @@
        "metadata": {},
        "output_type": "pyout",
        "prompt_number": 5,
-       "svg": [
-        "<?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=\"114pt\"\n",
-        " viewBox=\"0.00 0.00 734.00 114.05\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.410264 0.410264) rotate(0) translate(4 274)\">\n",
-        "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-274 1785.09,-274 1785.09,4 -4,4\"/>\n",
-        "<!-- I -->\n",
-        "<!-- 0 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"97.1448\" cy=\"-126\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"97.1448\" y=\"-122.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=0</text>\n",
-        "</g>\n",
-        "<!-- I&#45;&gt;0 -->\n",
-        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.06896,-126C2.11771,-126 15.0011,-126 30.9641,-126\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9685,-126 30.9685,-129.15 34.4685,-126 30.9685,-126 30.9685,-126 30.9685,-126 34.4685,-126 30.9684,-122.85 37.9685,-126 37.9685,-126\"/>\n",
-        "</g>\n",
-        "<!-- 1 -->\n",
-        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"414.434\" cy=\"-151\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"414.434\" y=\"-147.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=1, P.b=0</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;1 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M154.512,-130.469C209.377,-134.82 292.624,-141.421 349.831,-145.957\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"357.024,-146.527 349.797,-149.114 353.535,-146.25 350.046,-145.974 350.046,-145.974 350.046,-145.974 353.535,-146.25 350.295,-142.834 357.024,-146.527 357.024,-146.527\"/>\n",
-        "<text text-anchor=\"start\" x=\"174.29\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 2 -->\n",
-        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"414.434\" cy=\"-97\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"414.434\" y=\"-93.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=1</text>\n",
-        "</g>\n",
-        "<!-- 0&#45;&gt;2 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M149.262,-117.331C157.61,-116.092 166.179,-114.926 174.29,-114 233.096,-107.288 300.359,-102.788 348.54,-100.113\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"355.805,-99.715 348.988,-103.243 352.31,-99.9063 348.816,-100.098 348.816,-100.098 348.816,-100.098 352.31,-99.9063 348.643,-96.9523 355.805,-99.715 355.805,-99.715\"/>\n",
-        "<text text-anchor=\"start\" x=\"174.29\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 3 -->\n",
-        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"735.724\" cy=\"-181\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"735.724\" y=\"-177.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=2, P.b=0</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;3 -->\n",
-        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M470.738,-156.905C477.751,-157.626 484.832,-158.34 491.579,-159 552.693,-164.975 622.506,-171.233 671.6,-175.54\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"678.69,-176.161 671.441,-178.688 675.203,-175.856 671.716,-175.55 671.716,-175.55 671.716,-175.55 675.203,-175.856 671.991,-172.412 678.69,-176.161 678.69,-176.161\"/>\n",
-        "<text text-anchor=\"start\" x=\"491.579\" y=\"-176.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 4 -->\n",
-        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"735.724\" cy=\"-124\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"735.724\" y=\"-120.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=1, P.b=1</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;4 -->\n",
-        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M471.154,-145.816C478.032,-145.194 484.966,-144.576 491.579,-144 552.509,-138.694 622.062,-133.01 671.124,-129.063\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"678.211,-128.494 671.486,-132.195 674.722,-128.774 671.234,-129.055 671.234,-129.055 671.234,-129.055 674.722,-128.774 670.981,-125.915 678.211,-128.494 678.211,-128.494\"/>\n",
-        "<text text-anchor=\"start\" x=\"491.579\" y=\"-147.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;4 -->\n",
-        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M473.536,-99.0371C522.878,-101.137 595.516,-105.101 658.579,-112 664.412,-112.638 670.48,-113.41 676.532,-114.25\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"683.614,-115.265 676.238,-117.39 680.149,-114.768 676.685,-114.272 676.685,-114.272 676.685,-114.272 680.149,-114.768 677.132,-111.154 683.614,-115.265 683.614,-115.265\"/>\n",
-        "<text text-anchor=\"start\" x=\"493.579\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 5 -->\n",
-        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"735.724\" cy=\"-67\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"735.724\" y=\"-63.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=2</text>\n",
-        "</g>\n",
-        "<!-- 2&#45;&gt;5 -->\n",
-        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M463.206,-86.5822C472.576,-84.8242 482.358,-83.1873 491.579,-82 551.55,-74.278 620.371,-70.5027 669.453,-68.6743\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"676.548,-68.4184 669.666,-71.8187 673.05,-68.5446 669.553,-68.6708 669.553,-68.6708 669.553,-68.6708 673.05,-68.5446 669.439,-65.5228 676.548,-68.4184 676.548,-68.4184\"/>\n",
-        "<text text-anchor=\"start\" x=\"493.579\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 6 -->\n",
-        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1057.01\" cy=\"-219\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1057.01\" y=\"-215.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=3, P.b=0</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;6 -->\n",
-        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M785.779,-190.641C794.768,-192.231 804.084,-193.761 812.869,-195 873.519,-203.554 943.108,-210.094 992.255,-214.17\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"999.354,-214.754 992.12,-217.32 995.866,-214.467 992.378,-214.18 992.378,-214.18 992.378,-214.18 995.866,-214.467 992.636,-211.041 999.354,-214.754 999.354,-214.754\"/>\n",
-        "<text text-anchor=\"start\" x=\"812.869\" y=\"-216.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 7 -->\n",
-        "<g id=\"node9\" class=\"node\"><title>7</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1057.01\" cy=\"-162\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1057.01\" y=\"-158.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=2, P.b=1</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;7 -->\n",
-        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M793.806,-177.603C849.367,-174.297 933.671,-169.28 991.603,-165.833\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"998.888,-165.399 992.087,-168.96 995.394,-165.607 991.9,-165.815 991.9,-165.815 991.9,-165.815 995.394,-165.607 991.713,-162.671 998.888,-165.399 998.888,-165.399\"/>\n",
-        "<text text-anchor=\"start\" x=\"812.869\" y=\"-179.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;7 -->\n",
-        "<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M793.383,-128.246C842.763,-132.268 916.235,-139.026 979.869,-148 986.319,-148.91 993.057,-149.977 999.742,-151.109\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1006.96,-152.359 999.524,-154.268 1003.51,-151.762 1000.06,-151.164 1000.06,-151.164 1000.06,-151.164 1003.51,-151.762 1000.6,-148.061 1006.96,-152.359 1006.96,-152.359\"/>\n",
-        "<text text-anchor=\"start\" x=\"812.869\" y=\"-151.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 8 -->\n",
-        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1057.01\" cy=\"-105\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1057.01\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=1, P.b=2</text>\n",
-        "</g>\n",
-        "<!-- 4&#45;&gt;8 -->\n",
-        "<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M779.906,-111.991C790.594,-109.519 802.077,-107.281 812.869,-106 873.199,-98.8403 942.543,-99.4149 991.699,-101.29\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"998.801,-101.576 991.68,-104.442 995.304,-101.435 991.807,-101.294 991.807,-101.294 991.807,-101.294 995.304,-101.435 991.933,-98.147 998.801,-101.576 998.801,-101.576\"/>\n",
-        "<text text-anchor=\"start\" x=\"812.869\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;8 -->\n",
-        "<g id=\"edge12\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M795.145,-66.8248C844.681,-67.5751 917.426,-70.7999 979.869,-82 990.029,-83.8224 1000.75,-86.5416 1010.83,-89.4783\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1017.7,-91.5379 1010.09,-92.5438 1014.35,-90.5323 1010.99,-89.5266 1010.99,-89.5266 1010.99,-89.5266 1014.35,-90.5323 1011.9,-86.5094 1017.7,-91.5379 1017.7,-91.5379\"/>\n",
-        "<text text-anchor=\"start\" x=\"814.869\" y=\"-85.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 9 -->\n",
-        "<g id=\"node11\" class=\"node\"><title>9</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1057.01\" cy=\"-18\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1057.01\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=3</text>\n",
-        "</g>\n",
-        "<!-- 5&#45;&gt;9 -->\n",
-        "<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;9</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M781.654,-55.5506C791.873,-53.178 802.711,-50.8429 812.869,-49 873.728,-37.9586 943.862,-29.4618 993.118,-24.1795\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1000.23,-23.4235 993.603,-27.2958 996.75,-23.7935 993.27,-24.1635 993.27,-24.1635 993.27,-24.1635 996.75,-23.7935 992.937,-21.0311 1000.23,-23.4235 1000.23,-23.4235\"/>\n",
-        "<text text-anchor=\"start\" x=\"814.869\" y=\"-52.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 6&#45;&gt;6 -->\n",
-        "<g id=\"edge14\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1029.39,-234.916C1022.18,-245.15 1031.39,-255 1057.01,-255 1076.63,-255 1086.63,-249.226 1087,-241.927\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1084.64,-234.916 1089.86,-240.544 1085.76,-238.233 1086.88,-241.55 1086.88,-241.55 1086.88,-241.55 1085.76,-238.233 1083.89,-242.555 1084.64,-234.916 1084.64,-234.916\"/>\n",
-        "<text text-anchor=\"start\" x=\"975.513\" y=\"-258.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 10 -->\n",
-        "<g id=\"node12\" class=\"node\"><title>10</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1378.3\" cy=\"-208\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1378.3\" y=\"-204.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=3, P.b=1</text>\n",
-        "</g>\n",
-        "<!-- 7&#45;&gt;10 -->\n",
-        "<g id=\"edge15\" class=\"edge\"><title>7&#45;&gt;10</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1102.93,-173.541C1113.15,-175.909 1123.99,-178.219 1134.16,-180 1194.79,-190.621 1264.67,-198.188 1313.91,-202.756\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1321.02,-203.408 1313.76,-205.906 1317.54,-203.089 1314.05,-202.769 1314.05,-202.769 1314.05,-202.769 1317.54,-203.089 1314.34,-199.632 1321.02,-203.408 1321.02,-203.408\"/>\n",
-        "<text text-anchor=\"start\" x=\"1134.16\" y=\"-204.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 11 -->\n",
-        "<g id=\"node13\" class=\"node\"><title>11</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1378.3\" cy=\"-154\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1378.3\" y=\"-150.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=2, P.b=2</text>\n",
-        "</g>\n",
-        "<!-- 7&#45;&gt;11 -->\n",
-        "<g id=\"edge16\" class=\"edge\"><title>7&#45;&gt;11</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1116.2,-160.542C1171.49,-159.157 1254.49,-157.077 1312.01,-155.636\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1319.24,-155.455 1312.32,-158.779 1315.74,-155.542 1312.24,-155.63 1312.24,-155.63 1312.24,-155.63 1315.74,-155.542 1312.17,-152.481 1319.24,-155.455 1319.24,-155.455\"/>\n",
-        "<text text-anchor=\"start\" x=\"1134.16\" y=\"-164.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;11 -->\n",
-        "<g id=\"edge17\" class=\"edge\"><title>8&#45;&gt;11</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1113.27,-110.856C1162.69,-116.43 1237.01,-125.642 1301.16,-137 1308.61,-138.32 1316.44,-139.874 1324.13,-141.497\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1331.13,-143.002 1323.62,-144.61 1327.71,-142.266 1324.28,-141.531 1324.28,-141.531 1324.28,-141.531 1327.71,-142.266 1324.95,-138.451 1331.13,-143.002 1331.13,-143.002\"/>\n",
-        "<text text-anchor=\"start\" x=\"1134.16\" y=\"-140.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 12 -->\n",
-        "<g id=\"node14\" class=\"node\"><title>12</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1378.3\" cy=\"-67\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1378.3\" y=\"-63.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=1, P.b=3</text>\n",
-        "</g>\n",
-        "<!-- 8&#45;&gt;12 -->\n",
-        "<g id=\"edge18\" class=\"edge\"><title>8&#45;&gt;12</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1090.3,-90.0264C1103.59,-84.5744 1119.32,-79.0137 1134.16,-76 1193.74,-63.8954 1263.17,-62.5565 1312.56,-63.7043\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1319.69,-63.8907 1312.61,-66.8568 1316.19,-63.7993 1312.69,-63.7078 1312.69,-63.7078 1312.69,-63.7078 1316.19,-63.7993 1312.78,-60.5589 1319.69,-63.8907 1319.69,-63.8907\"/>\n",
-        "<text text-anchor=\"start\" x=\"1134.16\" y=\"-79.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 9&#45;&gt;9 -->\n",
-        "<g id=\"edge19\" class=\"edge\"><title>9&#45;&gt;9</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1029.39,-33.916C1022.18,-44.1504 1031.39,-54 1057.01,-54 1076.63,-54 1086.63,-48.2263 1087,-40.9268\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1084.64,-33.916 1089.86,-39.5438 1085.76,-37.2328 1086.88,-40.5496 1086.88,-40.5496 1086.88,-40.5496 1085.76,-37.2328 1083.89,-41.5554 1084.64,-33.916 1084.64,-33.916\"/>\n",
-        "<text text-anchor=\"start\" x=\"979.013\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; &quot;P.b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 10&#45;&gt;10 -->\n",
-        "<g id=\"edge20\" class=\"edge\"><title>10&#45;&gt;10</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1350.68,-223.916C1343.47,-234.15 1352.68,-244 1378.3,-244 1397.92,-244 1407.92,-238.226 1408.29,-230.927\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1405.93,-223.916 1411.15,-229.544 1407.05,-227.233 1408.16,-230.55 1408.16,-230.55 1408.16,-230.55 1407.05,-227.233 1405.18,-231.555 1405.93,-223.916 1405.93,-223.916\"/>\n",
-        "<text text-anchor=\"start\" x=\"1296.8\" y=\"-247.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 13 -->\n",
-        "<g id=\"node15\" class=\"node\"><title>13</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1699.59\" cy=\"-186\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1699.59\" y=\"-182.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=3, P.b=2</text>\n",
-        "</g>\n",
-        "<!-- 11&#45;&gt;13 -->\n",
-        "<g id=\"edge21\" class=\"edge\"><title>11&#45;&gt;13</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1434.92,-159.574C1491.06,-165.201 1577.61,-173.874 1636.09,-179.736\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1643.08,-180.436 1635.8,-182.872 1639.6,-180.087 1636.11,-179.738 1636.11,-179.738 1636.11,-179.738 1639.6,-180.087 1636.43,-176.604 1643.08,-180.436 1643.08,-180.436\"/>\n",
-        "<text text-anchor=\"start\" x=\"1455.45\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 14 -->\n",
-        "<g id=\"node16\" class=\"node\"><title>14</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1699.59\" cy=\"-99\" rx=\"59.2899\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1699.59\" y=\"-95.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=2, P.b=3</text>\n",
-        "</g>\n",
-        "<!-- 11&#45;&gt;14 -->\n",
-        "<g id=\"edge22\" class=\"edge\"><title>11&#45;&gt;14</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1430.25,-145.224C1487.6,-135.345 1580.6,-119.325 1640.67,-108.977\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1647.83,-107.744 1641.46,-112.037 1644.38,-108.339 1640.93,-108.933 1640.93,-108.933 1640.93,-108.933 1644.38,-108.339 1640.4,-105.829 1647.83,-107.744 1647.83,-107.744\"/>\n",
-        "<text text-anchor=\"start\" x=\"1455.45\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
-        "</g>\n",
-        "<!-- 12&#45;&gt;12 -->\n",
-        "<g id=\"edge23\" class=\"edge\"><title>12&#45;&gt;12</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1350.68,-82.916C1343.47,-93.1504 1352.68,-103 1378.3,-103 1397.92,-103 1407.92,-97.2263 1408.29,-89.9268\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1405.93,-82.916 1411.15,-88.5438 1407.05,-86.2328 1408.16,-89.5496 1408.16,-89.5496 1408.16,-89.5496 1407.05,-86.2328 1405.18,-90.5554 1405.93,-82.916 1405.93,-82.916\"/>\n",
-        "<text text-anchor=\"start\" x=\"1298.3\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; &quot;P.b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 13&#45;&gt;13 -->\n",
-        "<g id=\"edge24\" class=\"edge\"><title>13&#45;&gt;13</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1671.97,-201.916C1664.76,-212.15 1673.97,-222 1699.59,-222 1719.21,-222 1729.21,-216.226 1729.58,-208.927\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1727.22,-201.916 1732.44,-207.544 1728.34,-205.233 1729.45,-208.55 1729.45,-208.55 1729.45,-208.55 1728.34,-205.233 1726.47,-209.555 1727.22,-201.916 1727.22,-201.916\"/>\n",
-        "<text text-anchor=\"start\" x=\"1618.09\" y=\"-225.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "<!-- 14&#45;&gt;14 -->\n",
-        "<g id=\"edge25\" class=\"edge\"><title>14&#45;&gt;14</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1671.97,-114.916C1664.76,-125.15 1673.97,-135 1699.59,-135 1719.21,-135 1729.21,-129.226 1729.58,-121.927\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1727.22,-114.916 1732.44,-120.544 1728.34,-118.233 1729.45,-121.55 1729.45,-121.55 1729.45,-121.55 1728.34,-118.233 1726.47,-122.555 1727.22,-114.916 1727.22,-114.916\"/>\n",
-        "<text text-anchor=\"start\" x=\"1619.59\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;P.a&lt;1&quot; &amp; &quot;P.b&gt;2&quot; &amp; dead</text>\n",
-        "</g>\n",
-        "</g>\n",
-        "</svg>\n"
-       ],
        "text": [
-        "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f95344639c0> >"
+        "[('state_size', 4),\n",
+        " ('types', [('int', []), ('P', ['x']), ('Q', ['wait', 'work'])]),\n",
+        " ('variables', [('a', 0), ('b', 0), ('P', 1), ('Q', 2)])]"
        ]
       }
      ],
@@ -366,7 +161,8 @@
      "cell_type": "code",
      "collapsed": false,
      "input": [
-      "a = spot.translate('\"P.a<1\" U \"P.b>2\"'); a"
+      "k = m.kripke([\"a<1\", \"b>2\"])\n",
+      "k"
      ],
      "language": "python",
      "metadata": {},
@@ -382,56 +178,922 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"208pt\" height=\"85pt\"\n",
-        " viewBox=\"0.00 0.00 208.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
+        "<svg width=\"734pt\" height=\"188pt\"\n",
+        " viewBox=\"0.00 0.00 734.00 188.34\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.60754 0.60754) rotate(0) translate(4 306)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 204,-81 204,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-306 1204.15,-306 1204.15,4 -4,4\"/>\n",
         "<!-- I -->\n",
-        "<!-- 1 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
-        "</g>\n",
-        "<!-- I&#45;&gt;1 -->\n",
-        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-22C2.79388,-22 17.1543,-22 30.6317,-22\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-22 30.9419,-25.1501 34.4419,-22 30.9419,-22.0001 30.9419,-22.0001 30.9419,-22.0001 34.4419,-22 30.9418,-18.8501 37.9419,-22 37.9419,-22\"/>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-39.0373C48.3189,-48.8579 50.4453,-58 56,-58 60.166,-58 62.4036,-52.8576 62.7128,-46.1433\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-39.0373 65.8541,-45.8818 62.5434,-42.5335 62.7076,-46.0296 62.7076,-46.0296 62.7076,-46.0296 62.5434,-42.5335 59.561,-46.1774 62.3792,-39.0373 62.3792,-39.0373\"/>\n",
-        "<text text-anchor=\"start\" x=\"0.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot;</text>\n",
-        "</g>\n",
         "<!-- 0 -->\n",
-        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"178\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
-        "<ellipse fill=\"none\" stroke=\"black\" cx=\"178\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
-        "<text text-anchor=\"middle\" x=\"178\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"106.894\" cy=\"-152\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"106.894\" y=\"-148.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0</text>\n",
         "</g>\n",
-        "<!-- 1&#45;&gt;0 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.1931,-22C93.6078,-22 125.5,-22 148.621,-22\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"155.792,-22 148.793,-25.1501 152.292,-22 148.792,-22.0001 148.792,-22.0001 148.792,-22.0001 152.292,-22 148.792,-18.8501 155.792,-22 155.792,-22\"/>\n",
-        "<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.b&gt;2&quot;</text>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.07603,-152C2.16168,-152 14.7505,-152 30.8523,-152\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9448,-152 30.9448,-155.15 34.4448,-152 30.9448,-152 30.9448,-152 30.9448,-152 34.4448,-152 30.9447,-148.85 37.9448,-152 37.9448,-152\"/>\n",
         "</g>\n",
-        "<!-- 0&#45;&gt;0 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M166.931,-41.3443C164.865,-52.0977 168.555,-62 178,-62 185.232,-62 189.089,-56.1954 189.573,-48.6485\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"189.069,-41.3443 192.693,-48.1107 189.31,-44.836 189.551,-48.3277 189.551,-48.3277 189.551,-48.3277 189.31,-44.836 186.408,-48.5447 189.069,-41.3443 189.069,-41.3443\"/>\n",
-        "<text text-anchor=\"middle\" x=\"178\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"424.682\" cy=\"-177\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"424.682\" y=\"-173.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M172.942,-157.15C224.867,-161.26 297.569,-167.016 351.324,-171.272\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"358.447,-171.836 351.22,-174.423 354.958,-171.559 351.468,-171.283 351.468,-171.283 351.468,-171.283 354.958,-171.559 351.717,-168.143 358.447,-171.836 358.447,-171.836\"/>\n",
+        "<text text-anchor=\"start\" x=\"193.788\" y=\"-173.8\" 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 -->\n",
+        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"424.682\" cy=\"-123\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"424.682\" y=\"-119.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M168.386,-143.874C176.907,-142.84 185.563,-141.848 193.788,-141 246.142,-135.601 305.353,-131.001 350.571,-127.802\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"357.705,-127.301 350.943,-130.934 354.213,-127.546 350.722,-127.791 350.722,-127.791 350.722,-127.791 354.213,-127.546 350.501,-124.649 357.705,-127.301 357.705,-127.301\"/>\n",
+        "<text text-anchor=\"start\" x=\"193.788\" y=\"-144.8\" 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 -->\n",
+        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"746.469\" cy=\"-213\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"746.469\" y=\"-209.3\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M486.662,-184.969C495.029,-186.016 503.513,-187.053 511.576,-188 566.357,-194.435 628.441,-201.039 674.872,-205.842\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"681.896,-206.567 674.609,-208.982 678.414,-206.208 674.933,-205.848 674.933,-205.848 674.933,-205.848 678.414,-206.208 675.256,-202.715 681.896,-206.567 681.896,-206.567\"/>\n",
+        "<text text-anchor=\"start\" x=\"511.576\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"746.469\" cy=\"-148\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"746.469\" y=\"-144.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M490.011,-171.166C543.249,-166.338 618.814,-159.486 673.945,-154.486\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"681.243,-153.824 674.556,-157.594 677.757,-154.141 674.272,-154.457 674.272,-154.457 674.272,-154.457 677.757,-154.141 673.987,-151.32 681.243,-153.824 681.243,-153.824\"/>\n",
+        "<text text-anchor=\"start\" x=\"511.576\" y=\"-172.8\" 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;4 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M493.643,-124.142C540.404,-125.43 603.882,-128.171 659.576,-134 666.939,-134.771 674.63,-135.759 682.254,-136.854\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"689.225,-137.886 681.84,-139.977 685.763,-137.373 682.301,-136.861 682.301,-136.861 682.301,-136.861 685.763,-137.373 682.762,-133.745 689.225,-137.886 689.225,-137.886\"/>\n",
+        "<text text-anchor=\"start\" x=\"513.576\" y=\"-137.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g id=\"node7\" class=\"node\"><title>5</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"746.469\" cy=\"-74\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"746.469\" y=\"-70.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;5 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M479.2,-111.897C489.903,-109.821 501.08,-107.755 511.576,-106 566.751,-96.7739 629.581,-88.2892 676.217,-82.3781\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"683.268,-81.4883 676.718,-85.49 679.796,-81.9265 676.323,-82.3648 676.323,-82.3648 676.323,-82.3648 679.796,-81.9265 675.929,-79.2396 683.268,-81.4883 683.268,-81.4883\"/>\n",
+        "<text text-anchor=\"start\" x=\"513.576\" y=\"-109.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g id=\"node8\" class=\"node\"><title>6</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1068.26\" cy=\"-251\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1068.26\" y=\"-247.3\" font-family=\"Lato\" font-size=\"14.00\">a=3, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;6 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M806.101,-222.223C815.219,-223.557 824.538,-224.861 833.363,-226 887.875,-233.035 949.719,-239.583 996.117,-244.212\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1003.14,-244.909 995.86,-247.351 999.654,-244.563 996.172,-244.217 996.172,-244.217 996.172,-244.217 999.654,-244.563 996.483,-241.082 1003.14,-244.909 1003.14,-244.909\"/>\n",
+        "<text text-anchor=\"start\" x=\"833.363\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g id=\"node9\" class=\"node\"><title>7</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1068.26\" cy=\"-190\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1068.26\" y=\"-186.3\" font-family=\"Lato\" font-size=\"14.00\">a=2, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;7 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>3&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M813.342,-208.262C866.099,-204.468 940.037,-199.15 994.526,-195.231\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1001.74,-194.712 994.988,-198.356 998.253,-194.963 994.762,-195.214 994.762,-195.214 994.762,-195.214 998.253,-194.963 994.536,-192.072 1001.74,-194.712 1001.74,-194.712\"/>\n",
+        "<text text-anchor=\"start\" x=\"833.363\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M809.051,-155.707C856.231,-161.658 922.933,-170.171 981.363,-178 987.37,-178.805 993.611,-179.653 999.865,-180.511\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1007.2,-181.522 999.834,-183.687 1003.73,-181.044 1000.26,-180.566 1000.26,-180.566 1000.26,-180.566 1003.73,-181.044 1000.69,-177.446 1007.2,-181.522 1007.2,-181.522\"/>\n",
+        "<text text-anchor=\"start\" x=\"833.363\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1068.26\" cy=\"-129\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1068.26\" y=\"-125.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;8 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>4&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M808.878,-140.266C817.1,-139.402 825.43,-138.614 833.363,-138 886.34,-133.903 946.217,-131.643 992.125,-130.413\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"999.37,-130.224 992.455,-133.556 995.872,-130.315 992.373,-130.407 992.373,-130.407 992.373,-130.407 995.872,-130.315 992.291,-127.258 999.37,-130.224 999.37,-130.224\"/>\n",
+        "<text text-anchor=\"start\" x=\"833.363\" y=\"-141.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;8 -->\n",
+        "<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M806.684,-83.045C854.025,-90.415 922.049,-101.315 981.363,-112 989.428,-113.453 997.905,-115.047 1006.26,-116.66\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1013.24,-118.016 1005.77,-119.773 1009.81,-117.349 1006.37,-116.681 1006.37,-116.681 1006.37,-116.681 1009.81,-117.349 1006.97,-113.589 1013.24,-118.016 1013.24,-118.016\"/>\n",
+        "<text text-anchor=\"start\" x=\"835.363\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- u5 -->\n",
+        "<g id=\"node11\" class=\"node\"><title>u5</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1081.26,-77.5 1055.26,-77.5 1055.26,-54.5 1081.26,-54.5 1081.26,-77.5\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1068.26\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;u5 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>5&#45;&gt;u5</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M815.288,-72.3034C889.294,-70.452 1003.22,-67.602 1048.12,-66.4787\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1055.2,-66.3016 1048.28,-69.6257 1051.7,-66.3892 1048.2,-66.4767 1048.2,-66.4767 1048.2,-66.4767 1051.7,-66.3892 1048.13,-63.3277 1055.2,-66.3016 1055.2,-66.3016\"/>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g id=\"node12\" class=\"node\"><title>9</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1068.26\" cy=\"-18\" rx=\"68.7879\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1068.26\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;9 -->\n",
+        "<g id=\"edge14\" class=\"edge\"><title>5&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M791.767,-60.378C805.051,-56.6313 819.718,-52.826 833.363,-50 887.57,-38.7736 949.685,-30.4857 996.275,-25.1606\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1003.32,-24.3639 996.722,-28.2802 999.846,-24.757 996.368,-25.1501 996.368,-25.1501 996.368,-25.1501 999.846,-24.757 996.014,-22.02 1003.32,-24.3639 1003.32,-24.3639\"/>\n",
+        "<text text-anchor=\"start\" x=\"835.363\" y=\"-53.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g id=\"edge15\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1052.8,-268.782C1050.17,-278.315 1055.32,-287 1068.26,-287 1077.76,-287 1083.06,-282.316 1084.16,-276.052\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1083.72,-268.782 1087.29,-275.575 1083.93,-272.275 1084.15,-275.769 1084.15,-275.769 1084.15,-275.769 1083.93,-272.275 1081,-275.962 1083.72,-268.782 1083.72,-268.782\"/>\n",
+        "<text text-anchor=\"start\" x=\"996.257\" y=\"-290.8\" font-family=\"Lato\" font-size=\"14.00\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- u7 -->\n",
+        "<g id=\"node13\" class=\"node\"><title>u7</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1200.15,-201.5 1174.15,-201.5 1174.15,-178.5 1200.15,-178.5 1200.15,-201.5\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1187.15\" y=\"-186.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;u7 -->\n",
+        "<g id=\"edge16\" class=\"edge\"><title>7&#45;&gt;u7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1137.25,-190C1148.02,-190 1158.34,-190 1166.71,-190\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1173.79,-190 1166.79,-193.15 1170.29,-190 1166.79,-190 1166.79,-190 1166.79,-190 1170.29,-190 1166.79,-186.85 1173.79,-190 1173.79,-190\"/>\n",
+        "</g>\n",
+        "<!-- u8 -->\n",
+        "<g id=\"node14\" class=\"node\"><title>u8</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1200.15,-140.5 1174.15,-140.5 1174.15,-117.5 1200.15,-117.5 1200.15,-140.5\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1187.15\" y=\"-125.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;u8 -->\n",
+        "<g id=\"edge17\" class=\"edge\"><title>8&#45;&gt;u8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1137.25,-129C1148.02,-129 1158.34,-129 1166.71,-129\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1173.79,-129 1166.79,-132.15 1170.29,-129 1166.79,-129 1166.79,-129 1166.79,-129 1170.29,-129 1166.79,-125.85 1173.79,-129 1173.79,-129\"/>\n",
+        "</g>\n",
+        "<!-- u9 -->\n",
+        "<g id=\"node15\" class=\"node\"><title>u9</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1200.15,-29.5 1174.15,-29.5 1174.15,-6.5 1200.15,-6.5 1200.15,-29.5\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1187.15\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;u9 -->\n",
+        "<g id=\"edge18\" class=\"edge\"><title>9&#45;&gt;u9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1137.25,-18C1148.02,-18 1158.34,-18 1166.71,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1173.79,-18 1166.79,-21.1501 1170.29,-18 1166.79,-18.0001 1166.79,-18.0001 1166.79,-18.0001 1170.29,-18 1166.79,-14.8501 1173.79,-18 1173.79,-18\"/>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f9534463de0> >"
+        "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f7f00239600> >"
        ]
       }
      ],
      "prompt_number": 6
     },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "k.show('.<15')"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 7,
+       "svg": [
+        "<svg height=\"168pt\" viewBox=\"0.00 0.00 734.00 168.16\" 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.479758 0.479758) rotate(0) translate(4 346.5)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-346.5 1525.94,-346.5 1525.94,4 -4,4\" stroke=\"none\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"106.894\" cy=\"-168.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"106.894\" y=\"-164.8\">a=0, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.07603,-168.5C2.16168,-168.5 14.7505,-168.5 30.8523,-168.5\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9448,-168.5 30.9448,-171.65 34.4448,-168.5 30.9448,-168.5 30.9448,-168.5 30.9448,-168.5 34.4448,-168.5 30.9447,-165.35 37.9448,-168.5 37.9448,-168.5\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"424.682\" cy=\"-193.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"424.682\" y=\"-189.8\">a=1, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M172.942,-173.65C224.867,-177.76 297.569,-183.516 351.324,-187.772\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"358.447,-188.336 351.22,-190.923 354.958,-188.059 351.468,-187.783 351.468,-187.783 351.468,-187.783 354.958,-188.059 351.717,-184.643 358.447,-188.336 358.447,-188.336\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"193.788\" y=\"-190.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"424.682\" cy=\"-139.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"424.682\" y=\"-135.8\">a=0, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
+        "<path d=\"M168.386,-160.374C176.907,-159.34 185.563,-158.348 193.788,-157.5 246.142,-152.101 305.353,-147.501 350.571,-144.302\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"357.705,-143.801 350.943,-147.434 354.213,-144.046 350.722,-144.291 350.722,-144.291 350.722,-144.291 354.213,-144.046 350.501,-141.149 357.705,-143.801 357.705,-143.801\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"193.788\" y=\"-161.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"746.469\" cy=\"-237.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"746.469\" y=\"-233.8\">a=2, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M485.749,-201.914C494.415,-203.121 503.223,-204.345 511.576,-205.5 567.569,-213.242 631.118,-221.93 677.828,-228.297\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"684.886,-229.259 677.524,-231.435 681.418,-228.787 677.95,-228.314 677.95,-228.314 677.95,-228.314 681.418,-228.787 678.375,-225.193 684.886,-229.259 684.886,-229.259\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"511.576\" y=\"-229.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"746.469\" cy=\"-166.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"746.469\" y=\"-162.8\">a=1, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
+        "<path d=\"M490.395,-188.036C543.406,-183.56 618.361,-177.232 673.303,-172.593\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"680.578,-171.979 673.868,-175.707 677.09,-172.273 673.603,-172.568 673.603,-172.568 673.603,-172.568 677.09,-172.273 673.338,-169.429 680.578,-171.979 680.578,-171.979\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"511.576\" y=\"-190.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M492.308,-143.008C539.154,-145.732 603.271,-149.974 659.576,-155.5 665.49,-156.081 671.626,-156.744 677.775,-157.451\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"684.985,-158.299 677.665,-160.61 681.509,-157.89 678.033,-157.481 678.033,-157.481 678.033,-157.481 681.509,-157.89 678.401,-154.353 684.985,-158.299 684.985,-158.299\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"513.576\" y=\"-159.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
+        "<ellipse cx=\"746.469\" cy=\"-97.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"746.469\" y=\"-93.8\">a=0, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;5 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;5</title>\n",
+        "<path d=\"M482.922,-129.824C492.479,-128.307 502.3,-126.81 511.576,-125.5 566.462,-117.745 628.796,-110.353 675.304,-105.113\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"682.338,-104.323 675.733,-108.235 678.86,-104.714 675.381,-105.105 675.381,-105.105 675.381,-105.105 678.86,-104.714 675.03,-101.974 682.338,-104.323 682.338,-104.323\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"513.576\" y=\"-129.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g class=\"node\" id=\"node8\"><title>6</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-291.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-287.8\">a=3, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;6</title>\n",
+        "<path d=\"M798.675,-249.435C810.064,-251.92 822.1,-254.414 833.363,-256.5 888.853,-266.776 952.179,-276.107 998.932,-282.545\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1006,-283.513 998.635,-285.684 1002.53,-283.038 999.063,-282.563 999.063,-282.563 999.063,-282.563 1002.53,-283.038 999.491,-279.442 1006,-283.513 1006,-283.513\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-284.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g class=\"node\" id=\"node9\"><title>7</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-237.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-233.8\">a=2, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;7</title>\n",
+        "<path d=\"M815.68,-237.5C867.468,-237.5 938.636,-237.5 992.066,-237.5\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"999.152,-237.5 992.152,-240.65 995.652,-237.5 992.152,-237.5 992.152,-237.5 992.152,-237.5 995.652,-237.5 992.152,-234.35 999.152,-237.5 999.152,-237.5\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-241.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;7</title>\n",
+        "<path d=\"M799.561,-178.065C856.704,-190.753 948.233,-211.074 1008.05,-224.356\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1015.19,-225.94 1007.67,-227.497 1011.77,-225.181 1008.35,-224.422 1008.35,-224.422 1008.35,-224.422 1011.77,-225.181 1009.04,-221.347 1015.19,-225.94 1015.19,-225.94\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-222.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g class=\"node\" id=\"node10\"><title>8</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-161.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-157.8\">a=1, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;8</title>\n",
+        "<path d=\"M814.512,-163.104C820.883,-162.864 827.245,-162.655 833.363,-162.5 886.345,-161.154 946.1,-160.92 991.949,-161.015\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"999.185,-161.033 992.177,-164.165 995.685,-161.024 992.185,-161.015 992.185,-161.015 992.185,-161.015 995.685,-161.024 992.193,-157.865 999.185,-161.033 999.185,-161.033\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-166.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;8</title>\n",
+        "<path d=\"M803.321,-107.797C850.76,-116.65 920.621,-129.941 981.363,-142.5 990.183,-144.324 999.497,-146.315 1008.61,-148.301\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1015.53,-149.815 1008.02,-151.395 1012.11,-149.066 1008.69,-148.318 1008.69,-148.318 1008.69,-148.318 1012.11,-149.066 1009.36,-145.241 1015.53,-149.815 1015.53,-149.815\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"835.363\" y=\"-146.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g class=\"node\" id=\"node11\"><title>9</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-20.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-16.8\">a=0, b=3, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;9 -->\n",
+        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;9</title>\n",
+        "<path d=\"M782.92,-82.2213C798.222,-76.0621 816.458,-69.295 833.363,-64.5 888.566,-48.8426 952.705,-37.2246 999.841,-29.871\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1006.96,-28.7722 1000.52,-32.9529 1003.5,-29.306 1000.04,-29.8397 1000.04,-29.8397 1000.04,-29.8397 1003.5,-29.306 999.564,-26.7266 1006.96,-28.7722 1006.96,-28.7722\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"835.363\" y=\"-68.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 10 -->\n",
+        "<g class=\"node\" id=\"node12\"><title>10</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-85.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-81.8\">a=0, b=2, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;10 -->\n",
+        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;10</title>\n",
+        "<path d=\"M807.449,-88.8628C816.127,-87.8916 824.963,-87.0538 833.363,-86.5 886.44,-83.0012 946.439,-82.8212 992.378,-83.4797\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"999.628,-83.5921 992.579,-86.6331 996.128,-83.5378 992.628,-83.4834 992.628,-83.4834 992.628,-83.4834 996.128,-83.5378 992.677,-80.3338 999.628,-83.5921 999.628,-83.5921\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"835.363\" y=\"-90.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;6</title>\n",
+        "<path d=\"M1040.13,-308.164C1033.88,-318.125 1043.26,-327.5 1068.26,-327.5 1087.4,-327.5 1097.38,-322.005 1098.2,-314.958\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1096.38,-308.164 1101.24,-314.111 1097.29,-311.545 1098.19,-314.926 1098.19,-314.926 1098.19,-314.926 1097.29,-311.545 1095.15,-315.741 1096.38,-308.164 1096.38,-308.164\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"996.257\" y=\"-331.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 11 -->\n",
+        "<g class=\"node\" id=\"node13\"><title>11</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-275.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-271.8\">a=3, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge16\"><title>7-&gt;11</title>\n",
+        "<path d=\"M1126.48,-247.312C1136.04,-248.811 1145.86,-250.268 1155.15,-251.5 1209.42,-258.701 1271.02,-264.944 1317.38,-269.256\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1324.39,-269.905 1317.13,-272.397 1320.91,-269.583 1317.42,-269.26 1317.42,-269.26 1317.42,-269.26 1320.91,-269.583 1317.71,-266.124 1324.39,-269.905 1324.39,-269.905\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-272.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 12 -->\n",
+        "<g class=\"node\" id=\"node14\"><title>12</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-218.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-214.8\">a=2, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge17\"><title>7-&gt;12</title>\n",
+        "<path d=\"M1135.52,-233.563C1187.96,-230.448 1261.14,-226.1 1315.4,-222.875\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1322.6,-222.448 1315.79,-226.008 1319.1,-222.656 1315.61,-222.863 1315.61,-222.863 1315.61,-222.863 1319.1,-222.656 1315.42,-219.719 1322.6,-222.448 1322.6,-222.448\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-236.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge18\"><title>8-&gt;12</title>\n",
+        "<path d=\"M1124.69,-171.915C1134.82,-173.793 1145.3,-175.719 1155.15,-177.5 1212.45,-187.859 1277.73,-199.269 1324.73,-207.416\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1331.82,-208.644 1324.39,-210.553 1328.37,-208.047 1324.92,-207.449 1324.92,-207.449 1324.92,-207.449 1328.37,-208.047 1325.46,-204.345 1331.82,-208.644 1331.82,-208.644\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-207.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 13 -->\n",
+        "<g class=\"node\" id=\"node15\"><title>13</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-161.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-157.8\">a=1, b=3, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;13 -->\n",
+        "<g class=\"edge\" id=\"edge19\"><title>8-&gt;13</title>\n",
+        "<path d=\"M1137.47,-161.5C1189.26,-161.5 1260.42,-161.5 1313.85,-161.5\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1320.94,-161.5 1313.94,-164.65 1317.44,-161.5 1313.94,-161.5 1313.94,-161.5 1313.94,-161.5 1317.44,-161.5 1313.94,-158.35 1320.94,-161.5 1320.94,-161.5\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-165.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 14 -->\n",
+        "<g class=\"node\" id=\"node16\"><title>14</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-104.5\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-100.8\">a=1, b=2, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge20\"><title>8-&gt;14</title>\n",
+        "<path d=\"M1120.48,-149.671C1131.87,-147.18 1143.9,-144.656 1155.15,-142.5 1211.26,-131.745 1275.32,-121.477 1322.2,-114.331\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1329.28,-113.256 1322.83,-117.421 1325.82,-113.781 1322.36,-114.307 1322.36,-114.307 1322.36,-114.307 1325.82,-113.781 1321.88,-111.193 1329.28,-113.256 1329.28,-113.256\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-146.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- u9 -->\n",
+        "<g class=\"node\" id=\"node17\"><title>u9</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1403.04,-23 1377.04,-23 1377.04,-0 1403.04,-0 1403.04,-23\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-7.8\">...</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;u9 -->\n",
+        "<g class=\"edge\" id=\"edge21\"><title>9-&gt;u9</title>\n",
+        "<path d=\"M1137.08,-18.5913C1211.08,-16.5085 1325.01,-13.3023 1369.91,-12.0385\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1376.99,-11.8393 1370.08,-15.185 1373.49,-11.9378 1369.99,-12.0363 1369.99,-12.0363 1369.99,-12.0363 1373.49,-11.9378 1369.9,-8.88754 1376.99,-11.8393 1376.99,-11.8393\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge23\"><title>10-&gt;14</title>\n",
+        "<path d=\"M1136.25,-82.2061C1183.12,-80.7754 1247.12,-80.5712 1303.15,-86.5 1312.66,-87.5063 1322.67,-89.1012 1332.36,-90.9355\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1339.35,-92.3085 1331.88,-94.0503 1335.92,-91.6339 1332.49,-90.9593 1332.49,-90.9593 1332.49,-90.9593 1335.92,-91.6339 1333.09,-87.8684 1339.35,-92.3085 1339.35,-92.3085\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1157.15\" y=\"-90.3\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- u10 -->\n",
+        "<g class=\"node\" id=\"node18\"><title>u10</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1403.04,-64 1377.04,-64 1377.04,-41 1403.04,-41 1403.04,-64\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-48.8\">...</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;u10 -->\n",
+        "<g class=\"edge\" id=\"edge22\"><title>10-&gt;u10</title>\n",
+        "<path d=\"M1132.82,-78.9408C1206.52,-71.3359 1323.74,-59.2391 1369.68,-54.4985\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1376.91,-53.7519 1370.27,-57.6039 1373.43,-54.1112 1369.95,-54.4706 1369.95,-54.4706 1369.95,-54.4706 1373.43,-54.1112 1369.63,-51.3372 1376.91,-53.7519 1376.91,-53.7519\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge24\"><title>11-&gt;11</title>\n",
+        "<path d=\"M1374.59,-293.282C1371.96,-302.815 1377.11,-311.5 1390.04,-311.5 1399.54,-311.5 1404.85,-306.816 1405.95,-300.552\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1405.5,-293.282 1409.08,-300.075 1405.72,-296.775 1405.93,-300.269 1405.93,-300.269 1405.93,-300.269 1405.72,-296.775 1402.79,-300.462 1405.5,-293.282 1405.5,-293.282\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1318.04\" y=\"-315.3\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- u12 -->\n",
+        "<g class=\"node\" id=\"node19\"><title>u12</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1521.94,-230 1495.94,-230 1495.94,-207 1521.94,-207 1521.94,-230\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1508.94\" y=\"-214.8\">...</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;u12 -->\n",
+        "<g class=\"edge\" id=\"edge25\"><title>12-&gt;u12</title>\n",
+        "<path d=\"M1459.04,-218.5C1469.81,-218.5 1480.13,-218.5 1488.5,-218.5\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1495.58,-218.5 1488.58,-221.65 1492.08,-218.5 1488.58,-218.5 1488.58,-218.5 1488.58,-218.5 1492.08,-218.5 1488.58,-215.35 1495.58,-218.5 1495.58,-218.5\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- u13 -->\n",
+        "<g class=\"node\" id=\"node20\"><title>u13</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1521.94,-173 1495.94,-173 1495.94,-150 1521.94,-150 1521.94,-173\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1508.94\" y=\"-157.8\">...</text>\n",
+        "</g>\n",
+        "<!-- 13&#45;&gt;u13 -->\n",
+        "<g class=\"edge\" id=\"edge26\"><title>13-&gt;u13</title>\n",
+        "<path d=\"M1459.04,-161.5C1469.81,-161.5 1480.13,-161.5 1488.5,-161.5\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1495.58,-161.5 1488.58,-164.65 1492.08,-161.5 1488.58,-161.5 1488.58,-161.5 1488.58,-161.5 1492.08,-161.5 1488.58,-158.35 1495.58,-161.5 1495.58,-161.5\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- u14 -->\n",
+        "<g class=\"node\" id=\"node21\"><title>u14</title>\n",
+        "<polygon fill=\"#ffffaa\" points=\"1521.94,-116 1495.94,-116 1495.94,-93 1521.94,-93 1521.94,-116\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1508.94\" y=\"-100.8\">...</text>\n",
+        "</g>\n",
+        "<!-- 14&#45;&gt;u14 -->\n",
+        "<g class=\"edge\" id=\"edge27\"><title>14-&gt;u14</title>\n",
+        "<path d=\"M1459.04,-104.5C1469.81,-104.5 1480.13,-104.5 1488.5,-104.5\" fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\"/>\n",
+        "<polygon fill=\"black\" points=\"1495.58,-104.5 1488.58,-107.65 1492.08,-104.5 1488.58,-104.5 1488.58,-104.5 1488.58,-104.5 1492.08,-104.5 1488.58,-101.35 1495.58,-104.5 1495.58,-104.5\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG at 0x7f7f001d13c8>"
+       ]
+      }
+     ],
+     "prompt_number": 7
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "k.show('.<0')  # unlimited output"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 8,
+       "svg": [
+        "<svg height=\"125pt\" viewBox=\"0.00 0.00 734.00 124.51\" 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.347783 0.347783) rotate(0) translate(4 354)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-354 2106.51,-354 2106.51,4 -4,4\" stroke=\"none\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"106.894\" cy=\"-176\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"106.894\" y=\"-172.3\">a=0, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.07603,-176C2.16168,-176 14.7505,-176 30.8523,-176\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9448,-176 30.9448,-179.15 34.4448,-176 30.9448,-176 30.9448,-176 30.9448,-176 34.4448,-176 30.9447,-172.85 37.9448,-176 37.9448,-176\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"424.682\" cy=\"-201\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"424.682\" y=\"-197.3\">a=1, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M172.942,-181.15C224.867,-185.26 297.569,-191.016 351.324,-195.272\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"358.447,-195.836 351.22,-198.423 354.958,-195.559 351.468,-195.283 351.468,-195.283 351.468,-195.283 354.958,-195.559 351.717,-192.143 358.447,-195.836 358.447,-195.836\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"193.788\" y=\"-196.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"424.682\" cy=\"-147\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"424.682\" y=\"-143.3\">a=0, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
+        "<path d=\"M167.439,-167.171C176.262,-166.011 185.254,-164.911 193.788,-164 245.916,-158.437 304.89,-154.116 350.054,-151.223\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"357.181,-150.771 350.395,-154.358 353.688,-150.992 350.195,-151.214 350.195,-151.214 350.195,-151.214 353.688,-150.992 349.996,-148.07 357.181,-150.771 357.181,-150.771\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"193.788\" y=\"-167.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"746.469\" cy=\"-245\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"746.469\" y=\"-241.3\">a=2, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;3</title>\n",
+        "<path d=\"M485.749,-209.414C494.415,-210.621 503.223,-211.845 511.576,-213 567.569,-220.742 631.118,-229.43 677.828,-235.797\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"684.886,-236.759 677.524,-238.935 681.418,-236.287 677.95,-235.814 677.95,-235.814 677.95,-235.814 681.418,-236.287 678.375,-232.693 684.886,-236.759 684.886,-236.759\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"511.576\" y=\"-235.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4 -->\n",
+        "<g class=\"node\" id=\"node6\"><title>4</title>\n",
+        "<ellipse cx=\"746.469\" cy=\"-178\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"746.469\" y=\"-174.3\">a=1, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;4</title>\n",
+        "<path d=\"M491.554,-196.262C544.311,-192.468 618.249,-187.15 672.738,-183.231\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"679.956,-182.712 673.2,-186.356 676.465,-182.963 672.974,-183.214 672.974,-183.214 672.974,-183.214 676.465,-182.963 672.748,-180.072 679.956,-182.712 679.956,-182.712\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"511.576\" y=\"-197.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;4 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>2-&gt;4</title>\n",
+        "<path d=\"M492.092,-150.809C538.977,-153.815 603.229,-158.577 659.576,-165 666.319,-165.769 673.345,-166.669 680.347,-167.63\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"687.33,-168.61 679.96,-170.757 683.864,-168.124 680.398,-167.637 680.398,-167.637 680.398,-167.637 683.864,-168.124 680.835,-164.518 687.33,-168.61 687.33,-168.61\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"513.576\" y=\"-168.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5 -->\n",
+        "<g class=\"node\" id=\"node7\"><title>5</title>\n",
+        "<ellipse cx=\"746.469\" cy=\"-96\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"746.469\" y=\"-92.3\">a=0, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;5 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;5</title>\n",
+        "<path d=\"M483.964,-137.705C539.334,-128.875 622.464,-115.617 680.071,-106.43\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"687.318,-105.274 680.902,-109.487 683.862,-105.825 680.406,-106.377 680.406,-106.377 680.406,-106.377 683.862,-105.825 679.909,-103.266 687.318,-105.274 687.318,-105.274\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"513.576\" y=\"-135.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 6 -->\n",
+        "<g class=\"node\" id=\"node8\"><title>6</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-299\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-295.3\">a=3, b=0, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>3-&gt;6</title>\n",
+        "<path d=\"M798.675,-256.935C810.064,-259.42 822.1,-261.914 833.363,-264 888.853,-274.276 952.179,-283.607 998.932,-290.045\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1006,-291.013 998.635,-293.184 1002.53,-290.538 999.063,-290.063 999.063,-290.063 999.063,-290.063 1002.53,-290.538 999.491,-286.942 1006,-291.013 1006,-291.013\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-290.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 7 -->\n",
+        "<g class=\"node\" id=\"node9\"><title>7</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-245\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-241.3\">a=2, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;7</title>\n",
+        "<path d=\"M815.68,-245C867.468,-245 938.636,-245 992.066,-245\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"999.152,-245 992.152,-248.15 995.652,-245 992.152,-245 992.152,-245 992.152,-245 995.652,-245 992.152,-241.85 999.152,-245 999.152,-245\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-248.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>4-&gt;7</title>\n",
+        "<path d=\"M801.869,-188.919C849.304,-198.499 919.943,-212.905 981.363,-226 990.171,-227.878 999.479,-229.899 1008.59,-231.897\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1015.51,-233.418 1007.99,-234.991 1012.09,-232.666 1008.67,-231.915 1008.67,-231.915 1008.67,-231.915 1012.09,-232.666 1009.35,-228.838 1015.51,-233.418 1015.51,-233.418\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-229.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8 -->\n",
+        "<g class=\"node\" id=\"node10\"><title>8</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-169\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-165.3\">a=1, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 4&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge11\"><title>4-&gt;8</title>\n",
+        "<path d=\"M810.75,-171.466C818.363,-170.869 826.033,-170.356 833.363,-170 886.396,-167.422 946.272,-167.217 992.166,-167.633\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"999.409,-167.705 992.378,-170.785 995.909,-167.67 992.409,-167.635 992.409,-167.635 992.409,-167.635 995.909,-167.67 992.44,-164.485 999.409,-167.705 999.409,-167.705\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"833.363\" y=\"-173.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;8 -->\n",
+        "<g class=\"edge\" id=\"edge12\"><title>5-&gt;8</title>\n",
+        "<path d=\"M800.026,-107.354C847.477,-117.683 919.181,-133.488 981.363,-148 990.867,-150.218 1000.95,-152.629 1010.73,-155.001\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1017.79,-156.718 1010.25,-158.125 1014.39,-155.891 1010.99,-155.064 1010.99,-155.064 1010.99,-155.064 1014.39,-155.891 1011.73,-152.003 1017.79,-156.718 1017.79,-156.718\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"835.363\" y=\"-151.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g class=\"node\" id=\"node11\"><title>9</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-28\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-24.3\">a=0, b=3, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;9 -->\n",
+        "<g class=\"edge\" id=\"edge13\"><title>5-&gt;9</title>\n",
+        "<path d=\"M795.508,-83.1854C807.815,-80.0431 821.052,-76.785 833.363,-74 890.762,-61.0159 956.561,-48.2632 1003.72,-39.491\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1010.83,-38.1721 1004.52,-42.5459 1007.39,-38.8104 1003.95,-39.4487 1003.95,-39.4487 1003.95,-39.4487 1007.39,-38.8104 1003.37,-36.3515 1010.83,-38.1721 1010.83,-38.1721\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"835.363\" y=\"-77.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 10 -->\n",
+        "<g class=\"node\" id=\"node12\"><title>10</title>\n",
+        "<ellipse cx=\"1068.26\" cy=\"-93\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1068.26\" y=\"-89.3\">a=0, b=2, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 5&#45;&gt;10 -->\n",
+        "<g class=\"edge\" id=\"edge14\"><title>5-&gt;10</title>\n",
+        "<path d=\"M815.452,-94.2979C821.509,-94.1823 827.547,-94.0801 833.363,-94 886.357,-93.2698 946.111,-93.0242 991.958,-92.9589\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"999.193,-92.95 992.197,-96.1087 995.693,-92.9543 992.193,-92.9587 992.193,-92.9587 992.193,-92.9587 995.693,-92.9543 992.189,-89.8087 999.193,-92.95 999.193,-92.95\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"835.363\" y=\"-97.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;6 -->\n",
+        "<g class=\"edge\" id=\"edge15\"><title>6-&gt;6</title>\n",
+        "<path d=\"M1040.13,-315.664C1033.88,-325.625 1043.26,-335 1068.26,-335 1087.4,-335 1097.38,-329.505 1098.2,-322.458\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1096.38,-315.664 1101.24,-321.611 1097.29,-319.045 1098.19,-322.426 1098.19,-322.426 1098.19,-322.426 1097.29,-319.045 1095.15,-323.241 1096.38,-315.664 1096.38,-315.664\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"996.257\" y=\"-338.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 11 -->\n",
+        "<g class=\"node\" id=\"node13\"><title>11</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-298\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-294.3\">a=3, b=1, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge16\"><title>7-&gt;11</title>\n",
+        "<path d=\"M1121.86,-256.527C1132.84,-258.791 1144.35,-261.062 1155.15,-263 1210.89,-273.002 1274.46,-282.386 1321.24,-288.914\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1328.31,-289.897 1320.94,-292.053 1324.84,-289.415 1321.38,-288.933 1321.38,-288.933 1321.38,-288.933 1324.84,-289.415 1321.81,-285.813 1328.31,-289.897 1328.31,-289.897\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-288.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 12 -->\n",
+        "<g class=\"node\" id=\"node14\"><title>12</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-244\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-240.3\">a=2, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge17\"><title>7-&gt;12</title>\n",
+        "<path d=\"M1137.47,-244.787C1189.26,-244.625 1260.42,-244.402 1313.85,-244.235\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1320.94,-244.213 1313.95,-247.385 1317.44,-244.224 1313.94,-244.235 1313.94,-244.235 1313.94,-244.235 1317.44,-244.224 1313.93,-241.085 1320.94,-244.213 1320.94,-244.213\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-247.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge18\"><title>8-&gt;12</title>\n",
+        "<path d=\"M1120.28,-180.967C1177.73,-194.439 1270.87,-216.284 1331.03,-230.394\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1338.2,-232.076 1330.67,-233.544 1334.79,-231.277 1331.39,-230.477 1331.39,-230.477 1331.39,-230.477 1334.79,-231.277 1332.11,-227.411 1338.2,-232.076 1338.2,-232.076\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-226.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 13 -->\n",
+        "<g class=\"node\" id=\"node15\"><title>13</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-108\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-104.3\">a=1, b=3, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;13 -->\n",
+        "<g class=\"edge\" id=\"edge19\"><title>8-&gt;13</title>\n",
+        "<path d=\"M1118.18,-156.408C1130.23,-153.481 1143.13,-150.495 1155.15,-148 1211.36,-136.338 1275.68,-125.52 1322.62,-118.083\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1329.71,-116.965 1323.29,-121.167 1326.25,-117.51 1322.8,-118.055 1322.8,-118.055 1322.8,-118.055 1326.25,-117.51 1322.3,-114.944 1329.71,-116.965 1329.71,-116.965\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-151.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 14 -->\n",
+        "<g class=\"node\" id=\"node16\"><title>14</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-167\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-163.3\">a=1, b=2, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge20\"><title>8-&gt;14</title>\n",
+        "<path d=\"M1137.47,-168.573C1189.26,-168.25 1260.42,-167.804 1313.85,-167.47\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1320.94,-167.426 1313.96,-170.62 1317.44,-167.448 1313.94,-167.47 1313.94,-167.47 1313.94,-167.47 1317.44,-167.448 1313.92,-164.32 1320.94,-167.426 1320.94,-167.426\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1155.15\" y=\"-171.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 15 -->\n",
+        "<g class=\"node\" id=\"node17\"><title>15</title>\n",
+        "<ellipse cx=\"1390.04\" cy=\"-18\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1390.04\" y=\"-14.3\">a=0, b=3, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 9&#45;&gt;15 -->\n",
+        "<g class=\"edge\" id=\"edge21\"><title>9-&gt;15</title>\n",
+        "<path d=\"M1130.18,-20.0242C1138.56,-19.1859 1147.06,-18.4695 1155.15,-18 1208.25,-14.9193 1268.25,-14.9913 1314.18,-15.7962\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1321.43,-15.9313 1314.37,-18.9502 1317.93,-15.866 1314.43,-15.8008 1314.43,-15.8008 1314.43,-15.8008 1317.93,-15.866 1314.49,-12.6513 1321.43,-15.9313 1321.43,-15.9313\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1159.15\" y=\"-21.8\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;14 -->\n",
+        "<g class=\"edge\" id=\"edge22\"><title>10-&gt;14</title>\n",
+        "<path d=\"M1121.78,-81.5041C1172.16,-73.4685 1248.42,-69.4035 1303.15,-103 1317.06,-111.537 1309.21,-123.884 1321.15,-135 1327.19,-140.617 1334.39,-145.413 1341.81,-149.45\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1348.07,-152.664 1340.41,-152.271 1344.96,-151.066 1341.85,-149.468 1341.85,-149.468 1341.85,-149.468 1344.96,-151.066 1343.28,-146.665 1348.07,-152.664 1348.07,-152.664\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1157.15\" y=\"-106.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 10&#45;&gt;15 -->\n",
+        "<g class=\"edge\" id=\"edge23\"><title>10-&gt;15</title>\n",
+        "<path d=\"M1102.05,-77.1077C1117.79,-70.0376 1137.12,-62.1621 1155.15,-57 1219.21,-38.6599 1237.44,-44.0653 1303.15,-33 1310.2,-31.8123 1317.58,-30.552 1324.92,-29.2864\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1332.23,-28.0215 1325.87,-32.3185 1328.78,-28.6181 1325.33,-29.2146 1325.33,-29.2146 1325.33,-29.2146 1328.78,-28.6181 1324.8,-26.1107 1332.23,-28.0215 1332.23,-28.0215\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1157.15\" y=\"-60.8\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 11&#45;&gt;11 -->\n",
+        "<g class=\"edge\" id=\"edge24\"><title>11-&gt;11</title>\n",
+        "<path d=\"M1361.92,-314.664C1355.67,-324.625 1365.04,-334 1390.04,-334 1409.19,-334 1419.17,-328.505 1419.99,-321.458\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1418.17,-314.664 1423.02,-320.611 1419.08,-318.045 1419.98,-321.426 1419.98,-321.426 1419.98,-321.426 1419.08,-318.045 1416.94,-322.241 1418.17,-314.664 1418.17,-314.664\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1318.04\" y=\"-337.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 16 -->\n",
+        "<g class=\"node\" id=\"node18\"><title>16</title>\n",
+        "<ellipse cx=\"1711.83\" cy=\"-198\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1711.83\" y=\"-194.3\">a=3, b=2, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;16 -->\n",
+        "<g class=\"edge\" id=\"edge25\"><title>12-&gt;16</title>\n",
+        "<path d=\"M1433.47,-229.887C1447.2,-225.795 1462.59,-221.705 1476.94,-219 1529.81,-209.029 1590.33,-203.758 1636.56,-200.99\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1643.57,-200.583 1636.76,-204.134 1640.07,-200.786 1636.58,-200.989 1636.58,-200.989 1636.58,-200.989 1640.07,-200.786 1636.4,-197.845 1643.57,-200.583 1643.57,-200.583\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1476.94\" y=\"-222.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 17 -->\n",
+        "<g class=\"node\" id=\"node19\"><title>17</title>\n",
+        "<ellipse cx=\"1711.83\" cy=\"-320\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1711.83\" y=\"-316.3\">a=2, b=3, Q=0</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;17 -->\n",
+        "<g class=\"edge\" id=\"edge26\"><title>12-&gt;17</title>\n",
+        "<path d=\"M1430.55,-258.715C1439.95,-262.491 1449.88,-266.706 1458.94,-271 1467.21,-274.921 1468.3,-277.981 1476.94,-281 1529.24,-299.277 1591.2,-309.116 1638.2,-314.337\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1645.32,-315.105 1638.02,-317.486 1641.84,-314.73 1638.36,-314.354 1638.36,-314.354 1638.36,-314.354 1641.84,-314.73 1638.7,-311.222 1645.32,-315.105 1645.32,-315.105\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1476.94\" y=\"-315.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 18 -->\n",
+        "<g class=\"node\" id=\"node20\"><title>18</title>\n",
+        "<ellipse cx=\"1711.83\" cy=\"-252\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1711.83\" y=\"-248.3\">a=2, b=2, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 12&#45;&gt;18 -->\n",
+        "<g class=\"edge\" id=\"edge27\"><title>12-&gt;18</title>\n",
+        "<path d=\"M1443.52,-255.359C1454.51,-257.291 1466.06,-258.996 1476.94,-260 1531.58,-265.046 1593.68,-262.541 1640.14,-259.047\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1647.17,-258.502 1640.44,-262.184 1643.68,-258.773 1640.19,-259.044 1640.19,-259.044 1640.19,-259.044 1643.68,-258.773 1639.95,-255.903 1647.17,-258.502 1647.17,-258.502\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1476.94\" y=\"-265.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 19 -->\n",
+        "<g class=\"node\" id=\"node21\"><title>19</title>\n",
+        "<ellipse cx=\"1711.83\" cy=\"-97\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"1711.83\" y=\"-93.3\">a=1, b=3, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 13&#45;&gt;19 -->\n",
+        "<g class=\"edge\" id=\"edge28\"><title>13-&gt;19</title>\n",
+        "<path d=\"M1445.39,-97.0507C1455.82,-95.3637 1466.68,-93.8887 1476.94,-93 1530.82,-88.3307 1591.93,-89.6014 1638.17,-91.8959\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1645.17,-92.2567 1638.02,-95.0422 1641.68,-92.0765 1638.18,-91.8963 1638.18,-91.8963 1638.18,-91.8963 1641.68,-92.0765 1638.35,-88.7505 1645.17,-92.2567 1645.17,-92.2567\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1478.94\" y=\"-96.8\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 14&#45;&gt;18 -->\n",
+        "<g class=\"edge\" id=\"edge29\"><title>14-&gt;18</title>\n",
+        "<path d=\"M1443.65,-155.656C1494.79,-147.758 1572.25,-144.451 1624.94,-182 1641.81,-194.024 1628.16,-210.482 1642.94,-225 1647.17,-229.153 1652.11,-232.689 1657.37,-235.695\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1663.67,-238.987 1656.01,-238.536 1660.57,-237.365 1657.47,-235.744 1657.47,-235.744 1657.47,-235.744 1660.57,-237.365 1658.93,-232.952 1663.67,-238.987 1663.67,-238.987\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1476.94\" y=\"-185.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 14&#45;&gt;19 -->\n",
+        "<g class=\"edge\" id=\"edge30\"><title>14-&gt;19</title>\n",
+        "<path d=\"M1423.39,-151.158C1439.2,-144.011 1458.71,-136.057 1476.94,-131 1492.69,-126.63 1579.47,-114.526 1642.74,-106.009\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1649.94,-105.041 1643.42,-109.096 1646.47,-105.508 1643,-105.974 1643,-105.974 1643,-105.974 1646.47,-105.508 1642.58,-102.852 1649.94,-105.041 1649.94,-105.041\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1476.94\" y=\"-134.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 15&#45;&gt;15 -->\n",
+        "<g class=\"edge\" id=\"edge31\"><title>15-&gt;15</title>\n",
+        "<path d=\"M1361.92,-34.6641C1355.67,-44.625 1365.04,-54 1390.04,-54 1409.19,-54 1419.17,-48.5045 1419.99,-41.4581\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1418.17,-34.6641 1423.02,-40.6108 1419.08,-38.0449 1419.98,-41.4258 1419.98,-41.4258 1419.98,-41.4258 1419.08,-38.0449 1416.94,-42.2407 1418.17,-34.6641 1418.17,-34.6641\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1322.04\" y=\"-57.8\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 20 -->\n",
+        "<g class=\"node\" id=\"node22\"><title>20</title>\n",
+        "<ellipse cx=\"2033.62\" cy=\"-202\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"2033.62\" y=\"-198.3\">a=3, b=2, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 16&#45;&gt;20 -->\n",
+        "<g class=\"edge\" id=\"edge32\"><title>16-&gt;20</title>\n",
+        "<path d=\"M1780.65,-198.848C1832.5,-199.497 1903.95,-200.39 1957.52,-201.061\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1964.62,-201.149 1957.59,-204.212 1961.12,-201.106 1957.63,-201.062 1957.63,-201.062 1957.63,-201.062 1961.12,-201.106 1957.66,-197.912 1964.62,-201.149 1964.62,-201.149\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1798.73\" y=\"-203.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 21 -->\n",
+        "<g class=\"node\" id=\"node23\"><title>21</title>\n",
+        "<ellipse cx=\"2033.62\" cy=\"-316\" fill=\"#ffffaa\" rx=\"68.7879\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"2033.62\" y=\"-312.3\">a=2, b=3, Q=1</text>\n",
+        "</g>\n",
+        "<!-- 17&#45;&gt;21 -->\n",
+        "<g class=\"edge\" id=\"edge33\"><title>17-&gt;21</title>\n",
+        "<path d=\"M1780.35,-317.447C1786.56,-317.271 1792.76,-317.117 1798.73,-317 1851.72,-315.962 1911.47,-315.722 1957.32,-315.737\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1964.55,-315.741 1957.55,-318.887 1961.05,-315.739 1957.55,-315.737 1957.55,-315.737 1957.55,-315.737 1961.05,-315.739 1957.55,-312.587 1964.55,-315.741 1964.55,-315.741\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1800.73\" y=\"-320.8\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 18&#45;&gt;12 -->\n",
+        "<g class=\"edge\" id=\"edge36\"><title>18-&gt;12</title>\n",
+        "<path d=\"M1651.32,-243.382C1642.49,-242.393 1633.49,-241.545 1624.94,-241 1571.47,-237.59 1510.98,-238.492 1464.92,-240.167\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1457.65,-240.442 1464.53,-237.029 1461.15,-240.309 1464.65,-240.177 1464.65,-240.177 1464.65,-240.177 1461.15,-240.309 1464.77,-243.325 1457.65,-240.442 1457.65,-240.442\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1476.94\" y=\"-244.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 18&#45;&gt;20 -->\n",
+        "<g class=\"edge\" id=\"edge34\"><title>18-&gt;20</title>\n",
+        "<path d=\"M1773.51,-243.854C1820.79,-237.345 1888.03,-227.729 1946.73,-218 1954.4,-216.728 1962.45,-215.323 1970.42,-213.89\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1977.69,-212.568 1971.37,-216.918 1974.25,-213.194 1970.8,-213.819 1970.8,-213.819 1970.8,-213.819 1974.25,-213.194 1970.24,-210.72 1977.69,-212.568 1977.69,-212.568\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1798.73\" y=\"-242.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 18&#45;&gt;21 -->\n",
+        "<g class=\"edge\" id=\"edge35\"><title>18-&gt;21</title>\n",
+        "<path d=\"M1769.68,-261.992C1817.13,-270.499 1886.48,-283.325 1946.73,-296 1956.01,-297.953 1965.83,-300.132 1975.39,-302.314\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1982.29,-303.9 1974.76,-305.402 1978.87,-303.116 1975.46,-302.332 1975.46,-302.332 1975.46,-302.332 1978.87,-303.116 1976.17,-299.262 1982.29,-303.9 1982.29,-303.9\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1798.73\" y=\"-299.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 19&#45;&gt;19 -->\n",
+        "<g class=\"edge\" id=\"edge37\"><title>19-&gt;19</title>\n",
+        "<path d=\"M1683.71,-113.664C1677.46,-123.625 1686.83,-133 1711.83,-133 1730.97,-133 1740.95,-127.505 1741.78,-120.458\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1739.96,-113.664 1744.81,-119.611 1740.86,-117.045 1741.77,-120.426 1741.77,-120.426 1741.77,-120.426 1740.86,-117.045 1738.73,-121.241 1739.96,-113.664 1739.96,-113.664\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1641.83\" y=\"-136.8\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
+        "</g>\n",
+        "<!-- 20&#45;&gt;16 -->\n",
+        "<g class=\"edge\" id=\"edge38\"><title>20-&gt;16</title>\n",
+        "<path d=\"M1988.01,-188.315C1974.84,-184.894 1960.32,-181.713 1946.73,-180 1881.47,-171.775 1864.15,-173.218 1798.73,-180 1789.21,-180.986 1779.2,-182.57 1769.51,-184.401\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1762.52,-185.772 1768.78,-181.333 1765.95,-185.098 1769.39,-184.425 1769.39,-184.425 1769.39,-184.425 1765.95,-185.098 1769.99,-187.516 1762.52,-185.772 1762.52,-185.772\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1798.73\" y=\"-183.8\">!&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 21&#45;&gt;17 -->\n",
+        "<g class=\"edge\" id=\"edge39\"><title>21-&gt;17</title>\n",
+        "<path d=\"M1980.14,-327.359C1969.15,-329.291 1957.6,-330.996 1946.73,-332 1881.23,-338.048 1864.35,-336.562 1798.73,-332 1792.22,-331.548 1785.45,-330.905 1778.7,-330.148\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"1771.4,-329.287 1778.72,-326.979 1774.87,-329.697 1778.35,-330.107 1778.35,-330.107 1778.35,-330.107 1774.87,-329.697 1777.98,-333.235 1771.4,-329.287 1771.4,-329.287\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"1800.73\" y=\"-338.8\">!&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG at 0x7f7f06a48e80>"
+       ]
+      }
+     ],
+     "prompt_number": 8
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "a = spot.translate('\"a<1\" U \"b>2\"'); a"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 9,
+       "svg": [
+        "<?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=\"234pt\" height=\"85pt\"\n",
+        " viewBox=\"0.00 0.00 234.00 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 81)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-81 230,-81 230,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"65\" cy=\"-22\" rx=\"27\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"65\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.04566,-22C1.94863,-22 16.101,-22 30.7579,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9378,-22 30.9378,-25.1501 34.4378,-22 30.9378,-22.0001 30.9378,-22.0001 30.9378,-22.0001 34.4378,-22 30.9378,-18.8501 37.9378,-22 37.9378,-22\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M57.1448,-39.4099C55.6785,-49.0879 58.2969,-58 65,-58 69.9226,-58 72.6423,-53.1936 73.1591,-46.8073\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"72.8552,-39.4099 76.2899,-46.2747 72.9989,-42.9069 73.1426,-46.404 73.1426,-46.404 73.1426,-46.404 72.9989,-42.9069 69.9953,-46.5333 72.8552,-39.4099 72.8552,-39.4099\"/>\n",
+        "<text text-anchor=\"start\" x=\"19.5\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot;</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"195\" cy=\"-22\" rx=\"27\" ry=\"18\"/>\n",
+        "<ellipse fill=\"none\" stroke=\"black\" cx=\"195\" cy=\"-22\" rx=\"31\" ry=\"22\"/>\n",
+        "<text text-anchor=\"middle\" x=\"195\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M92.2116,-22C110.793,-22 135.995,-22 156.673,-22\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"163.78,-22 156.78,-25.1501 160.28,-22 156.78,-22.0001 156.78,-22.0001 156.78,-22.0001 160.28,-22 156.78,-18.8501 163.78,-22 163.78,-22\"/>\n",
+        "<text text-anchor=\"start\" x=\"110\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;b&gt;2&quot;</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M182.991,-42.5808C181.329,-52.8447 185.332,-62 195,-62 202.251,-62 206.315,-56.8502 207.194,-49.9451\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"207.009,-42.5808 210.333,-49.4999 207.097,-46.0797 207.184,-49.5786 207.184,-49.5786 207.184,-49.5786 207.097,-46.0797 204.035,-49.6574 207.009,-42.5808 207.009,-42.5808\"/>\n",
+        "<text text-anchor=\"middle\" x=\"195\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>\n"
+       ],
+       "text": [
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7f00198690> >"
+       ]
+      }
+     ],
+     "prompt_number": 9
+    },
     {
      "cell_type": "code",
      "collapsed": false,
@@ -444,7 +1106,7 @@
       {
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 7,
+       "prompt_number": 10,
        "svg": [
         "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
         "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
@@ -452,115 +1114,147 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"734pt\" height=\"75pt\"\n",
-        " viewBox=\"0.00 0.00 734.00 74.61\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.46633 0.46633) rotate(0) translate(4 156)\">\n",
+        "<svg width=\"734pt\" height=\"105pt\"\n",
+        " viewBox=\"0.00 0.00 734.00 104.73\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.459345 0.459345) rotate(0) translate(4 224)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-156 1569.99,-156 1569.99,4 -4,4\"/>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-224 1593.93,-224 1593.93,4 -4,4\"/>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"111.443\" cy=\"-111\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"111.443\" y=\"-107.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"121.193\" cy=\"-179\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"121.193\" y=\"-175.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=0, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- I&#45;&gt;0 -->\n",
         "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.07932,-111C2.17808,-111 14.5697,-111 30.6452,-111\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.738,-111 30.7381,-114.15 34.238,-111 30.738,-111 30.738,-111 30.738,-111 34.238,-111 30.738,-107.85 37.738,-111 37.738,-111\"/>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.08639,-179C2.22134,-179 14.4198,-179 30.6117,-179\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.775,-179 30.775,-182.15 34.275,-179 30.775,-179 30.775,-179 30.775,-179 34.275,-179 30.7749,-175.85 37.775,-179 37.775,-179\"/>\n",
         "</g>\n",
         "<!-- 1 -->\n",
         "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"457.33\" cy=\"-134\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"457.33\" y=\"-130.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=1, P.b=0 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"467.578\" cy=\"-202\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"467.578\" y=\"-198.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=0, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;1 -->\n",
         "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M182.449,-115.682C239.534,-119.5 320.08,-124.887 379.048,-128.831\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"386.129,-129.305 378.934,-131.98 382.636,-129.071 379.144,-128.838 379.144,-128.838 379.144,-128.838 382.636,-129.071 379.355,-125.695 386.129,-129.305 386.129,-129.305\"/>\n",
-        "<text text-anchor=\"start\" x=\"202.887\" y=\"-130.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M201.202,-184.277C254.796,-187.856 325.624,-192.586 380.627,-196.26\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"387.937,-196.748 380.742,-199.424 384.444,-196.515 380.952,-196.281 380.952,-196.281 380.952,-196.281 384.444,-196.515 381.162,-193.138 387.937,-196.748 387.937,-196.748\"/>\n",
+        "<text text-anchor=\"start\" x=\"222.385\" y=\"-198.8\" 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 -->\n",
         "<g id=\"node4\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"457.33\" cy=\"-80\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"457.33\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=1 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"467.578\" cy=\"-148\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"467.578\" y=\"-144.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=1, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 0&#45;&gt;2 -->\n",
         "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M174.157,-101.526C183.76,-100.226 193.581,-98.998 202.887,-98 261.413,-91.7238 327.785,-87.1 377.923,-84.1111\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"385.2,-83.682 378.397,-87.2387 381.706,-83.8881 378.212,-84.0942 378.212,-84.0942 378.212,-84.0942 381.706,-83.8881 378.026,-80.9496 385.2,-83.682 385.2,-83.682\"/>\n",
-        "<text text-anchor=\"start\" x=\"202.887\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M191.935,-169.446C202.138,-168.195 212.526,-167.002 222.385,-166 274.68,-160.684 333.428,-156.304 380.194,-153.196\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"387.299,-152.727 380.521,-156.331 383.806,-152.958 380.314,-153.188 380.314,-153.188 380.314,-153.188 383.806,-152.958 380.107,-150.045 387.299,-152.727 387.299,-152.727\"/>\n",
+        "<text text-anchor=\"start\" x=\"222.385\" y=\"-169.8\" 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 -->\n",
         "<g id=\"node5\" class=\"node\"><title>3</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"803.217\" cy=\"-103\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"803.217\" y=\"-99.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=1, P.b=1 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"813.963\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"813.963\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=1, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;3 -->\n",
         "<g id=\"edge4\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M528.336,-84.6821C585.421,-88.5001 665.967,-93.8872 724.934,-97.8311\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"732.016,-98.3047 724.821,-100.98 728.523,-98.0711 725.031,-97.8375 725.031,-97.8375 725.031,-97.8375 728.523,-98.0711 725.242,-94.6945 732.016,-98.3047 732.016,-98.3047\"/>\n",
-        "<text text-anchor=\"start\" x=\"548.774\" y=\"-99.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M547.587,-153.277C601.181,-156.856 672.009,-161.586 727.012,-165.26\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"734.322,-165.748 727.127,-168.424 730.83,-165.515 727.337,-165.281 727.337,-165.281 727.337,-165.281 730.83,-165.515 727.547,-162.138 734.322,-165.748 734.322,-165.748\"/>\n",
+        "<text text-anchor=\"start\" x=\"568.77\" y=\"-167.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 4 -->\n",
         "<g id=\"node6\" class=\"node\"><title>4</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"803.217\" cy=\"-49\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"803.217\" y=\"-45.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=2 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"813.963\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"813.963\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;4 -->\n",
         "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M520.044,-70.5262C529.647,-69.2264 539.468,-67.998 548.774,-67 607.3,-60.7238 673.672,-56.1 723.81,-53.1111\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"731.087,-52.682 724.284,-56.2387 727.593,-52.8881 724.099,-53.0942 724.099,-53.0942 724.099,-53.0942 727.593,-52.8881 723.913,-49.9496 731.087,-52.682 731.087,-52.682\"/>\n",
-        "<text text-anchor=\"start\" x=\"548.774\" y=\"-70.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M538.32,-138.446C548.523,-137.195 558.911,-136.002 568.77,-135 621.065,-129.684 679.813,-125.304 726.579,-122.196\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"733.684,-121.727 726.907,-125.331 730.192,-121.958 726.699,-122.188 726.699,-122.188 726.699,-122.188 730.192,-121.958 726.492,-119.045 733.684,-121.727 733.684,-121.727\"/>\n",
+        "<text text-anchor=\"start\" x=\"568.77\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 5 -->\n",
         "<g id=\"node7\" class=\"node\"><title>5</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1149.1\" cy=\"-72\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1149.1\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=1, P.b=2 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1160.35\" cy=\"-171\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1160.35\" y=\"-167.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;5 -->\n",
         "<g id=\"edge6\" class=\"edge\"><title>4&#45;&gt;5</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M874.223,-53.6821C931.308,-57.5001 1011.85,-62.8872 1070.82,-66.8311\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1077.9,-67.3047 1070.71,-69.9805 1074.41,-67.0711 1070.92,-66.8375 1070.92,-66.8375 1070.92,-66.8375 1074.41,-67.0711 1071.13,-63.6945 1077.9,-67.3047 1077.9,-67.3047\"/>\n",
-        "<text text-anchor=\"start\" x=\"894.661\" y=\"-68.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M876.083,-129.044C888.968,-131.456 902.494,-133.893 915.156,-136 970.724,-145.246 1033.65,-154.231 1081.71,-160.781\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1088.69,-161.73 1081.33,-163.908 1085.22,-161.259 1081.76,-160.787 1081.76,-160.787 1081.76,-160.787 1085.22,-161.259 1082.18,-157.666 1088.69,-161.73 1088.69,-161.73\"/>\n",
+        "<text text-anchor=\"start\" x=\"915.156\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 6 -->\n",
         "<g id=\"node8\" class=\"node\"><title>6</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1149.1\" cy=\"-18\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1149.1\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=3 * 1</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1160.35\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1160.35\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=0 * 1</text>\n",
         "</g>\n",
         "<!-- 4&#45;&gt;6 -->\n",
         "<g id=\"edge7\" class=\"edge\"><title>4&#45;&gt;6</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M865.931,-39.5262C875.534,-38.2264 885.355,-36.998 894.661,-36 953.187,-29.7238 1019.56,-25.1 1069.7,-22.1111\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1076.97,-21.682 1070.17,-25.2387 1073.48,-21.8881 1069.99,-22.0942 1069.99,-22.0942 1069.99,-22.0942 1073.48,-21.8881 1069.8,-18.9496 1076.97,-21.682 1076.97,-21.682\"/>\n",
-        "<text text-anchor=\"start\" x=\"894.661\" y=\"-39.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; !&quot;P.b&gt;2&quot; &amp; !dead</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M897.452,-117C949.442,-117 1016.57,-117 1069.85,-117\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1076.94,-117 1069.94,-120.15 1073.44,-117 1069.94,-117 1069.94,-117 1069.94,-117 1073.44,-117 1069.94,-113.85 1076.94,-117 1076.94,-117\"/>\n",
+        "<text text-anchor=\"start\" x=\"915.156\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
         "<!-- 7 -->\n",
         "<g id=\"node9\" class=\"node\"><title>7</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1487.99\" cy=\"-18\" rx=\"73.387\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"1487.99\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">P.a=0, P.b=3 * 0</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1160.35\" cy=\"-63\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1160.35\" y=\"-59.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=2, Q=1 * 1</text>\n",
         "</g>\n",
-        "<!-- 6&#45;&gt;7 -->\n",
-        "<g id=\"edge8\" class=\"edge\"><title>6&#45;&gt;7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1222.79,-18C1277.14,-18 1351.41,-18 1407.36,-18\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1414.44,-18 1407.44,-21.1501 1410.94,-18 1407.44,-18.0001 1407.44,-18.0001 1407.44,-18.0001 1410.94,-18 1407.44,-14.8501 1414.44,-18 1414.44,-18\"/>\n",
-        "<text text-anchor=\"start\" x=\"1240.55\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; &quot;P.b&gt;2&quot; &amp; dead</text>\n",
+        "<!-- 4&#45;&gt;7 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M876.083,-104.956C888.968,-102.544 902.494,-100.107 915.156,-98 970.724,-88.7538 1033.65,-79.7694 1081.71,-73.2187\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1088.69,-72.2701 1082.18,-76.3341 1085.22,-72.7414 1081.76,-73.2128 1081.76,-73.2128 1081.76,-73.2128 1085.22,-72.7414 1081.33,-70.0915 1088.69,-72.2701 1088.69,-72.2701\"/>\n",
+        "<text text-anchor=\"start\" x=\"915.156\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
         "</g>\n",
-        "<!-- 7&#45;&gt;7 -->\n",
-        "<g id=\"edge9\" class=\"edge\"><title>7&#45;&gt;7</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1458.46,-34.6641C1451.9,-44.625 1461.74,-54 1487.99,-54 1508.09,-54 1518.57,-48.5045 1519.43,-41.4581\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"1517.52,-34.6641 1522.45,-40.5499 1518.47,-38.0334 1519.42,-41.4027 1519.42,-41.4027 1519.42,-41.4027 1518.47,-38.0334 1516.39,-42.2555 1517.52,-34.6641 1517.52,-34.6641\"/>\n",
-        "<text text-anchor=\"start\" x=\"1409.99\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;P.a&lt;1&quot; &amp; &quot;P.b&gt;2&quot; &amp; dead</text>\n",
-        "<text text-anchor=\"start\" x=\"1479.99\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<!-- 8 -->\n",
+        "<g id=\"node10\" class=\"node\"><title>8</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1506.73\" cy=\"-117\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1506.73\" y=\"-113.3\" font-family=\"Lato\" font-size=\"14.00\">a=0, b=3, Q=1 * 0</text>\n",
+        "</g>\n",
+        "<!-- 6&#45;&gt;8 -->\n",
+        "<g id=\"edge9\" class=\"edge\"><title>6&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1243.84,-117C1295.83,-117 1362.95,-117 1416.23,-117\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1423.32,-117 1416.32,-120.15 1419.82,-117 1416.32,-117 1416.32,-117 1416.32,-117 1419.82,-117 1416.32,-113.85 1423.32,-117 1423.32,-117\"/>\n",
+        "<text text-anchor=\"start\" x=\"1263.54\" y=\"-120.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- u7 -->\n",
+        "<g id=\"node11\" class=\"node\"><title>u7</title>\n",
+        "<polygon fill=\"#ffffaa\" stroke=\"none\" points=\"1519.73,-77.5 1493.73,-77.5 1493.73,-54.5 1519.73,-54.5 1519.73,-77.5\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1506.73\" y=\"-62.3\" font-family=\"Lato\" font-size=\"14.00\">...</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;u7 -->\n",
+        "<g id=\"edge10\" class=\"edge\"><title>7&#45;&gt;u7</title>\n",
+        "<path fill=\"none\" stroke=\"black\" stroke-dasharray=\"5,2\" d=\"M1243.84,-63.7186C1324.16,-64.4183 1440.61,-65.4327 1486.3,-65.8307\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1493.5,-65.8934 1486.47,-68.9823 1490,-65.8629 1486.5,-65.8324 1486.5,-65.8324 1486.5,-65.8324 1490,-65.8629 1486.53,-62.6825 1493.5,-65.8934 1493.5,-65.8934\"/>\n",
+        "</g>\n",
+        "<!-- 9 -->\n",
+        "<g id=\"node12\" class=\"node\"><title>9</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"1506.73\" cy=\"-18\" rx=\"83.3857\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"1506.73\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">a=1, b=2, Q=1 * 1</text>\n",
+        "</g>\n",
+        "<!-- 7&#45;&gt;9 -->\n",
+        "<g id=\"edge11\" class=\"edge\"><title>7&#45;&gt;9</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1223.24,-51.2056C1235.89,-48.986 1249.12,-46.7999 1261.54,-45 1315.04,-37.2455 1375.42,-30.5512 1422.76,-25.7681\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1429.94,-25.0468 1423.29,-28.8805 1426.46,-25.3965 1422.98,-25.7463 1422.98,-25.7463 1422.98,-25.7463 1426.46,-25.3965 1422.66,-22.612 1429.94,-25.0468 1429.94,-25.0468\"/>\n",
+        "<text text-anchor=\"start\" x=\"1261.54\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; !&quot;b&gt;2&quot; &amp; !dead</text>\n",
+        "</g>\n",
+        "<!-- 8&#45;&gt;8 -->\n",
+        "<g id=\"edge12\" class=\"edge\"><title>8&#45;&gt;8</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1476.26,-134.037C1470.04,-143.858 1480.19,-153 1506.73,-153 1526.64,-153 1537.33,-147.858 1538.81,-141.143\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"1537.21,-134.037 1541.82,-140.178 1537.98,-137.452 1538.74,-140.868 1538.74,-140.868 1538.74,-140.868 1537.98,-137.452 1535.67,-141.557 1537.21,-134.037 1537.21,-134.037\"/>\n",
+        "<text text-anchor=\"start\" x=\"1438.73\" y=\"-171.8\" font-family=\"Lato\" font-size=\"14.00\">&quot;a&lt;1&quot; &amp; &quot;b&gt;2&quot; &amp; dead</text>\n",
+        "<text text-anchor=\"start\" x=\"1498.73\" y=\"-156.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f95344637e0> >"
+        "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f7f00239cc0> >"
        ]
       }
      ],
-     "prompt_number": 7
+     "prompt_number": 10
     }
    ],
    "metadata": {}