From 6b516df34a28c1c4aa5e84eeec882ac954889beb Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 13 Nov 2015 23:16:39 +0100
Subject: [PATCH] dot: display pairs of states for products

* src/twaalgos/dot.cc: Here.
* wrap/python/tests/automata.ipynb: Test it.
* NEWS: Document this.
---
 NEWS                             |   5 +
 src/twaalgos/dot.cc              |  22 +-
 wrap/python/tests/automata.ipynb | 397 +++++++++++++++++++++++++++++--
 3 files changed, 401 insertions(+), 23 deletions(-)

diff --git a/NEWS b/NEWS
index e2a376583..9f4f3c85d 100644
--- a/NEWS
+++ b/NEWS
@@ -48,6 +48,11 @@ New in spot 1.99.5a (not yet released)
     automata already tagged as "deterministic", and "inherently-weak"
     or "weak" even for automata tagged "weak" or "terminal".
 
+  * The dot output will display pair of states when displaying an
+    automaton built as an explicit product.  This works in IPython
+    with spot.product() or spot.product_or() and in the shell with
+    autfilt's --product or --product-or options.
+
   * Renamings:
     is_guarantee_automaton() -> is_terminal_automaton()
     tgba_run -> twa_run
diff --git a/src/twaalgos/dot.cc b/src/twaalgos/dot.cc
index 3b7476c02..e9de09c3f 100644
--- a/src/twaalgos/dot.cc
+++ b/src/twaalgos/dot.cc
@@ -56,6 +56,7 @@ namespace spot
       bool opt_html_labels_ = false;
       const_twa_graph_ptr aut_;
       std::vector<std::string>* sn_ = nullptr;
+      std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
       std::string* name_ = nullptr;
       acc_cond::mark_t inf_sets_ = 0U;
       acc_cond::mark_t fin_sets_ = 0U;
@@ -385,6 +386,8 @@ namespace spot
 		os_ << '"';
 		if (has_name)
 		  escape_str(os_, (*sn_)[s]);
+		else if (sprod_)
+		  os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
 		else
 		  os_ << s;
 		if (acc)
@@ -399,6 +402,8 @@ namespace spot
 		os_ << '<';
 		if (has_name)
 		  escape_html(os_, (*sn_)[s]);
+		else if (sprod_)
+		  os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
 		else
 		  os_ << s;
 		if (acc)
@@ -416,6 +421,8 @@ namespace spot
 	    os_ << "  " << s << " [label=\"";
 	    if (sn_ && s < sn_->size() && !(*sn_)[s].empty())
 	      escape_str(os_, (*sn_)[s]);
+	    else if (sprod_)
+	      os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
 	    else
 	      os_ << s;
 	    os_ << '"';
@@ -466,13 +473,24 @@ namespace spot
       {
 	aut_ = aut;
 	if (opt_want_state_names_)
-	  sn_ = aut->get_named_prop<std::vector<std::string>>("state-names");
+	  {
+	    sn_ = aut->get_named_prop<std::vector<std::string>>("state-names");
+	    // We have no names.  Do we have product sources?
+	    if (!sn_)
+	      {
+		sprod_ = aut->get_named_prop
+		  <std::vector<std::pair<unsigned, unsigned>>>
+		  ("product-states");
+		if (sprod_ && aut->num_states() != sprod_->size())
+		  sprod_ = nullptr;
+	      }
+	  }
 	if (opt_name_)
 	  name_ = aut_->get_named_prop<std::string>("automaton-name");
 	mark_states_ = !opt_force_acc_trans_ && aut_->prop_state_acc();
 	if (opt_shape_ == ShapeAuto)
 	  {
-	    if (sn_ || aut->num_states() > 100)
+	    if (sn_ || sprod_ || aut->num_states() > 100)
 	      opt_shape_ = ShapeEllipse;
 	    else
 	      opt_shape_ = ShapeCircle;
diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb
index 80d4f1167..c576294be 100644
--- a/wrap/python/tests/automata.ipynb
+++ b/wrap/python/tests/automata.ipynb
@@ -17,8 +17,7 @@
    "pygments_lexer": "ipython3",
    "version": "3.4.3+"
   },
-  "name": "",
-  "signature": "sha256:d67ef646828999fe2beb805f3bb74087bbb30e12354c11fdfbe0f28c23bd7e5f"
+  "name": ""
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -178,7 +177,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d053f5d0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee805b4b0> >"
        ]
       }
      ],
@@ -317,7 +316,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f48d04f8470>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -470,7 +469,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f48d005f518>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -570,7 +569,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05238d0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042780> >"
        ]
       }
      ],
@@ -640,7 +639,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05237e0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042600> >"
        ]
       }
      ],
@@ -716,7 +715,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523750> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042660> >"
        ]
       }
      ],
@@ -839,7 +838,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f48d005f5c0>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -1029,7 +1028,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f48d0027710>"
+        "<IPython.core.display.SVG object>"
        ]
       }
      ],
@@ -1176,7 +1175,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523ab0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042d80> >"
        ]
       }
      ],
@@ -1277,7 +1276,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523870> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042e40> >"
        ]
       }
      ],
@@ -1395,7 +1394,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05237b0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee80425a0> >"
        ]
       }
      ],
@@ -1494,7 +1493,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d04c2120> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042630> >"
        ]
       }
      ],
@@ -1964,7 +1963,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523f30> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee80423c0> >"
        ]
       }
      ],
@@ -2161,7 +2160,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f48d00277b8>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2286,7 +2285,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f48c1bcb668>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2428,7 +2427,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f48d002b8d0>"
+        "<IPython.core.display.SVG object>"
        ]
       },
       {
@@ -2579,7 +2578,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523780> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee8042ed0> >"
        ]
       }
      ],
@@ -2735,7 +2734,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d05236f0> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faee80426c0> >"
        ]
       }
      ],
@@ -2805,11 +2804,367 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f48d0523510> >"
+        "<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faedb3750f0> >"
        ]
       }
      ],
      "prompt_number": 22
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "a1 = spot.translate('a W c'); display(a1.show('.bat'))\n",
+      "a2 = spot.translate('a U b'); display(a2.show('.bat'))\n",
+      "# the product should display pairs of states, unless asked not to\n",
+      "p = spot.product(a1, a2); display(p.show('.bat')); display(p.show('.bat1'))"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"115pt\" viewBox=\"0.00 0.00 170.00 115.00\" width=\"170pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 111)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-111 166,-111 166,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"60\" y=\"-92.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"82\" y=\"-92.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"98\" y=\"-92.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>1</title>\n",
+        "<ellipse cx=\"56\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-14.3\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;1</title>\n",
+        "<path d=\"M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
+        "<path d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"38\" y=\"-72.8\">a &amp; !c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-57.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
+        "<ellipse cx=\"144\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"144\" y=\"-14.3\">0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
+        "<path d=\"M74.4034,-18C87.1928,-18 104.732,-18 118.874,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"125.916,-18 118.916,-21.1501 122.416,-18 118.916,-18.0001 118.916,-18.0001 118.916,-18.0001 122.416,-18 118.916,-14.8501 125.916,-18 125.916,-18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"96.5\" y=\"-36.8\">c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-21.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
+        "<path d=\"M136.332,-34.2903C134.483,-44.3892 137.039,-54 144,-54 149.221,-54 151.964,-48.5939 152.229,-41.6304\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"151.668,-34.2903 155.342,-41.0299 151.935,-37.7801 152.201,-41.2699 152.201,-41.2699 152.201,-41.2699 151.935,-37.7801 149.06,-41.5099 151.668,-34.2903 151.668,-34.2903\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"139.5\" y=\"-72.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136\" y=\"-57.8\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"115pt\" viewBox=\"0.00 0.00 163.00 115.00\" width=\"163pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 111)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-111 159,-111 159,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"56.5\" y=\"-92.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"78.5\" y=\"-92.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.5\" y=\"-92.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>1</title>\n",
+        "<ellipse cx=\"56\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-14.3\">1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;1</title>\n",
+        "<path d=\"M1.15491,-18C2.79388,-18 17.1543,-18 30.6317,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-18 30.9419,-21.1501 34.4419,-18 30.9419,-18.0001 30.9419,-18.0001 30.9419,-18.0001 34.4419,-18 30.9418,-14.8501 37.9419,-18 37.9419,-18\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
+        "<path d=\"M49.6208,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-35.0373 65.8541,-41.8818 62.5434,-38.5335 62.7076,-42.0296 62.7076,-42.0296 62.7076,-42.0296 62.5434,-38.5335 59.561,-42.1774 62.3792,-35.0373 62.3792,-35.0373\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"37.5\" y=\"-57.8\">a &amp; !b</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>0</title>\n",
+        "<ellipse cx=\"137\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"137\" y=\"-14.3\">0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>1-&gt;0</title>\n",
+        "<path d=\"M74.1418,-18C85.1153,-18 99.5214,-18 111.67,-18\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"118.892,-18 111.892,-21.1501 115.392,-18 111.892,-18.0001 111.892,-18.0001 111.892,-18.0001 115.392,-18 111.892,-14.8501 118.892,-18 118.892,-18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-21.8\">b</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;0</title>\n",
+        "<path d=\"M129.969,-34.6641C128.406,-44.625 130.75,-54 137,-54 141.688,-54 144.178,-48.7266 144.471,-41.8876\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"144.031,-34.6641 147.601,-41.4598 144.244,-38.1576 144.456,-41.6511 144.456,-41.6511 144.456,-41.6511 144.244,-38.1576 141.312,-41.8425 144.031,-34.6641 144.031,-34.6641\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"132.5\" y=\"-72.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"129\" y=\"-57.8\">\u24ff</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"258pt\" viewBox=\"0.00 0.00 374.00 258.00\" width=\"374pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 254)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-254 370,-254 370,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136\" y=\"-235.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"158\" y=\"-235.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174\" y=\"-235.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"210\" y=\"-235.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226\" y=\"-235.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"65\" cy=\"-118\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"65\" y=\"-114.3\">1,1</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.04566,-118C1.94863,-118 16.101,-118 30.7579,-118\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9378,-118 30.9378,-121.15 34.4378,-118 30.9378,-118 30.9378,-118 30.9378,-118 34.4378,-118 30.9378,-114.85 37.9378,-118 37.9378,-118\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>0-&gt;0</title>\n",
+        "<path d=\"M57.1448,-135.41C55.6785,-145.088 58.2969,-154 65,-154 69.9226,-154 72.6423,-149.194 73.1591,-142.807\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"72.8552,-135.41 76.2899,-142.275 72.9989,-138.907 73.1426,-142.404 73.1426,-142.404 73.1426,-142.404 72.9989,-138.907 69.9953,-142.533 72.8552,-135.41 72.8552,-135.41\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"32\" y=\"-172.8\">a &amp; !b &amp; !c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"57\" y=\"-157.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"339\" cy=\"-118\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"339\" y=\"-114.3\">0,0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M81.4599,-132.849C112.036,-160.34 182.598,-214.494 244,-193 274.537,-182.311 302.549,-157.079 319.902,-138.829\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"324.937,-133.413 322.478,-140.685 322.554,-135.977 320.171,-138.54 320.171,-138.54 320.171,-138.54 322.554,-135.977 317.864,-136.396 324.937,-133.413 324.937,-133.413\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"200\" y=\"-215.8\">b &amp; c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"209\" y=\"-200.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"217\" cy=\"-118\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"217\" y=\"-114.3\">0,1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
+        "<path d=\"M92.128,-118C117.324,-118 155.554,-118 182.874,-118\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"189.92,-118 182.92,-121.15 186.42,-118 182.92,-118 182.92,-118 182.92,-118 186.42,-118 182.92,-114.85 189.92,-118 189.92,-118\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110\" y=\"-136.8\">a &amp; !b &amp; c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"133\" y=\"-121.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"217\" cy=\"-18\" fill=\"#ffffaa\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"217\" y=\"-14.3\">1,0</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
+        "<path d=\"M82.8344,-104.351C90.9083,-97.9714 100.805,-90.3913 110,-84 136.571,-65.532 168.193,-46.1623 189.943,-33.2209\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"196.081,-29.5834 191.665,-35.8621 193.07,-31.3678 190.059,-33.1522 190.059,-33.1522 190.059,-33.1522 193.07,-31.3678 188.453,-30.4423 196.081,-29.5834 196.081,-29.5834\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"110\" y=\"-102.8\">a &amp; b &amp; !c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"133\" y=\"-87.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;1</title>\n",
+        "<path d=\"M328.453,-134.664C326.109,-144.625 329.625,-154 339,-154 346.031,-154 349.767,-148.727 350.206,-141.888\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"349.547,-134.664 353.32,-141.349 349.865,-138.15 350.183,-141.635 350.183,-141.635 350.183,-141.635 349.865,-138.15 347.046,-141.921 349.547,-134.664 349.547,-134.664\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"334.5\" y=\"-171.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"323\" y=\"-157.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"339\" y=\"-157.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;1</title>\n",
+        "<path d=\"M244.038,-118C261.764,-118 285.386,-118 304.51,-118\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"311.598,-118 304.598,-121.15 308.098,-118 304.598,-118 304.598,-118 304.598,-118 308.098,-118 304.598,-114.85 311.598,-118 311.598,-118\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"273.5\" y=\"-136.8\">b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"270\" y=\"-121.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;2</title>\n",
+        "<path d=\"M206.453,-134.664C204.109,-144.625 207.625,-154 217,-154 224.031,-154 227.767,-148.727 228.206,-141.888\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"227.547,-134.664 231.32,-141.349 227.865,-138.15 228.183,-141.635 228.183,-141.635 228.183,-141.635 227.865,-138.15 225.046,-141.921 227.547,-134.664 227.547,-134.664\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"198.5\" y=\"-172.8\">a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"209\" y=\"-157.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;1</title>\n",
+        "<path d=\"M234.685,-31.9046C255.821,-49.5173 292.31,-79.9248 315.785,-99.4879\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"321.456,-104.214 314.062,-102.152 318.767,-101.973 316.079,-99.7322 316.079,-99.7322 316.079,-99.7322 318.767,-101.973 318.095,-97.3123 321.456,-104.214 321.456,-104.214\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"274.5\" y=\"-96.8\">c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"262\" y=\"-82.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"278\" y=\"-82.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;3</title>\n",
+        "<path d=\"M206.453,-34.6641C204.109,-44.625 207.625,-54 217,-54 224.031,-54 227.767,-48.7266 228.206,-41.8876\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"227.547,-34.6641 231.32,-41.3488 227.865,-38.1496 228.183,-41.6351 228.183,-41.6351 228.183,-41.6351 227.865,-38.1496 225.046,-41.9214 227.547,-34.6641 227.547,-34.6641\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"199\" y=\"-71.8\">a &amp; !c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"201\" y=\"-57.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"217\" y=\"-57.8\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "svg": [
+        "<svg height=\"258pt\" viewBox=\"0.00 0.00 320.00 258.00\" width=\"320pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 254)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-254 316,-254 316,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"109\" y=\"-235.8\">Inf(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"131\" y=\"-235.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"147\" y=\"-235.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"183\" y=\"-235.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"199\" y=\"-235.8\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-118\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-114.3\">0</text>\n",
+        "</g>\n",
+        "<!-- I&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;0</title>\n",
+        "<path d=\"M1.15491,-118C2.79388,-118 17.1543,-118 30.6317,-118\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-118 30.9419,-121.15 34.4419,-118 30.9419,-118 30.9419,-118 30.9419,-118 34.4419,-118 30.9418,-114.85 37.9419,-118 37.9419,-118\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>0-&gt;0</title>\n",
+        "<path d=\"M49.6208,-135.037C48.3189,-144.858 50.4453,-154 56,-154 60.166,-154 62.4036,-148.858 62.7128,-142.143\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-135.037 65.8541,-141.882 62.5434,-138.533 62.7076,-142.03 62.7076,-142.03 62.7076,-142.03 62.5434,-138.533 59.561,-142.177 62.3792,-135.037 62.3792,-135.037\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"23\" y=\"-172.8\">a &amp; !b &amp; !c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"48\" y=\"-157.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"294\" cy=\"-118\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"294\" y=\"-114.3\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M68.7125,-131.209C93.5537,-157.536 153.703,-212.415 208,-193 237.136,-182.582 262.545,-156.671 277.815,-138.227\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"282.596,-132.291 280.658,-139.719 280.401,-135.017 278.205,-137.743 278.205,-137.743 278.205,-137.743 280.401,-135.017 275.752,-135.767 282.596,-132.291 282.596,-132.291\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"173\" y=\"-215.8\">b &amp; c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"182\" y=\"-200.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2 -->\n",
+        "<g class=\"node\" id=\"node4\"><title>2</title>\n",
+        "<ellipse cx=\"190\" cy=\"-118\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"190\" y=\"-114.3\">2</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
+        "<path d=\"M74.2567,-118C97.2816,-118 138.189,-118 164.429,-118\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"171.739,-118 164.739,-121.15 168.239,-118 164.739,-118 164.739,-118 164.739,-118 168.239,-118 164.739,-114.85 171.739,-118 171.739,-118\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-136.8\">a &amp; !b &amp; c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"115\" y=\"-121.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3 -->\n",
+        "<g class=\"node\" id=\"node5\"><title>3</title>\n",
+        "<ellipse cx=\"190\" cy=\"-18\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"190\" y=\"-14.3\">3</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
+        "<path d=\"M69.1464,-105.175C75.6666,-98.5602 83.9909,-90.5322 92,-84 116.925,-63.6708 148.008,-43.309 168.168,-30.6899\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"174.309,-26.8747 170.025,-33.2447 171.336,-28.7219 168.363,-30.5691 168.363,-30.5691 168.363,-30.5691 171.336,-28.7219 166.7,-27.8936 174.309,-26.8747 174.309,-26.8747\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-102.8\">a &amp; b &amp; !c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"115\" y=\"-87.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;1</title>\n",
+        "<path d=\"M285.021,-133.916C282.679,-144.15 285.672,-154 294,-154 300.376,-154 303.625,-148.226 303.746,-140.927\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"302.979,-133.916 306.872,-140.532 303.36,-137.395 303.741,-140.874 303.741,-140.874 303.741,-140.874 303.36,-137.395 300.61,-141.217 302.979,-133.916 302.979,-133.916\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289.5\" y=\"-171.8\">1</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"278\" y=\"-157.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"294\" y=\"-157.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge7\"><title>2-&gt;1</title>\n",
+        "<path d=\"M208.303,-118C224.962,-118 250.303,-118 268.927,-118\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"275.953,-118 268.953,-121.15 272.453,-118 268.953,-118 268.953,-118 268.953,-118 272.453,-118 268.953,-114.85 275.953,-118 275.953,-118\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"237.5\" y=\"-136.8\">b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234\" y=\"-121.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g class=\"edge\" id=\"edge8\"><title>2-&gt;2</title>\n",
+        "<path d=\"M181.021,-133.916C178.679,-144.15 181.672,-154 190,-154 196.376,-154 199.625,-148.226 199.746,-140.927\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"198.979,-133.916 202.872,-140.532 199.36,-137.395 199.741,-140.874 199.741,-140.874 199.741,-140.874 199.36,-137.395 196.61,-141.217 198.979,-133.916 198.979,-133.916\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"171.5\" y=\"-172.8\">a &amp; !b</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"182\" y=\"-157.8\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge9\"><title>3-&gt;1</title>\n",
+        "<path d=\"M203.507,-30.262C221.478,-47.8803 254.693,-80.4442 275.213,-100.562\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"280.39,-105.638 273.187,-102.987 277.891,-103.187 275.392,-100.737 275.392,-100.737 275.392,-100.737 277.891,-103.187 277.597,-98.4879 280.39,-105.638 280.39,-105.638\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"238.5\" y=\"-99.8\">c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226\" y=\"-85.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"242\" y=\"-85.8\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 3&#45;&gt;3 -->\n",
+        "<g class=\"edge\" id=\"edge10\"><title>3-&gt;3</title>\n",
+        "<path d=\"M181.021,-33.916C178.679,-44.1504 181.672,-54 190,-54 196.376,-54 199.625,-48.2263 199.746,-40.9268\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"198.979,-33.916 202.872,-40.5315 199.36,-37.3952 199.741,-40.8744 199.741,-40.8744 199.741,-40.8744 199.36,-37.3952 196.61,-41.2174 198.979,-33.916 198.979,-33.916\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"172\" y=\"-71.8\">a &amp; !c</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"174\" y=\"-57.8\">\u24ff</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190\" y=\"-57.8\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG object>"
+       ]
+      }
+     ],
+     "prompt_number": 23
+    },
+    {
+     "cell_type": "code",
+     "collapsed": true,
+     "input": [],
+     "language": "python",
+     "metadata": {},
+     "outputs": [],
+     "prompt_number": null
     }
    ],
    "metadata": {}