diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 32e581e11..b7e357f6f 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -466,10 +466,25 @@ namespace spot
                         bool max = false;
                         bool odd = false;
                         if (aut_->acc().is_parity(max, odd))
-                          os_ << nl << "[parity "
-                              << (max ? "max " : "min ")
-                              << (odd ? "odd " : "even ")
-                              << aut_->num_sets() << ']';
+                          {
+                            os_ << nl << "[parity "
+                                << (max ? "max " : "min ")
+                                << (odd ? "odd " : "even ")
+                                << aut_->num_sets() << ']';
+                          }
+                        else
+                          {
+                            std::vector<acc_cond::rs_pair> r_pairs;
+                            bool r_like = aut_->acc().is_rabin_like(r_pairs);
+                            unsigned rsz = r_pairs.size();
+                            std::vector<acc_cond::rs_pair> s_pairs;
+                            bool s_like = aut_->acc().is_streett_like(s_pairs);
+                            unsigned ssz = s_pairs.size();
+                            if (r_like && (!s_like || (rsz <= ssz)))
+                              os_ << nl << "[Rabin-like " << rsz << ']';
+                            else if (s_like && (!r_like || (ssz < rsz)))
+                              os_ << nl << "[Streett-like " << ssz << ']';
+                          }
                       }
                   }
               }
diff --git a/tests/core/alternating.test b/tests/core/alternating.test
index ab2a97a8b..bc74cacdc 100755
--- a/tests/core/alternating.test
+++ b/tests/core/alternating.test
@@ -559,10 +559,11 @@ EOF
 run 0 autfilt --dot='sbarf(Lato)' ex7 > ex7.dot
 
 color='<font color="#1F78B4">⓿</font>'
+color1='<font color="#FF4DA0">❶</font>'
 cat >expect7.dot<<EOF
 digraph G {
   rankdir=LR
-  label=<Fin(<font color="#FF4DA0">❶</font>) &amp; Fin($color)>
+  label=<Fin($color1) &amp; Fin($color)<br/>[Streett-like 2]>
   labelloc="t"
   fontname="Lato"
   node [fontname="Lato"]
@@ -658,7 +659,7 @@ run 0 autfilt --dot='sbarf(Lato)' ex8 > ex8.dot
 cat >expect8.dot<<EOF
 digraph G {
   rankdir=LR
-  label=<Fin(<font color="#FF4DA0">❶</font>) &amp; Fin($color)>
+  label=<Fin($color1) &amp; Fin($color)<br/>[Streett-like 2]>
   labelloc="t"
   fontname="Lato"
   node [fontname="Lato"]
diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test
index 38c7124bc..ff423059d 100755
--- a/tests/core/sccdot.test
+++ b/tests/core/sccdot.test
@@ -74,7 +74,7 @@ run 0 autfilt --dot=as in.hoa > out.dot
 cat <<EOF >expected
 digraph G {
   rankdir=LR
-  label="(Inf(0)&Inf(1)) & Fin(2)"
+  label="(Inf(0)&Inf(1)) & Fin(2)\n[Streett-like 3]"
   labelloc="t"
   node [shape="circle"]
   I [label="", style=invis, width=0]
diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb
index baba7e9bc..80ccdd004 100644
--- a/tests/python/decompose.ipynb
+++ b/tests/python/decompose.ipynb
@@ -212,7 +212,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f8a0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e720> >"
        ]
       }
      ],
@@ -330,7 +330,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f780> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e6f0> >"
        ]
       }
      ],
@@ -472,7 +472,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f600> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e5d0> >"
        ]
       }
      ],
@@ -563,7 +563,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c623810> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e600> >"
        ]
       }
      ],
@@ -641,7 +641,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f810> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062ef60> >"
        ]
       }
      ],
@@ -758,7 +758,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f8d0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e540> >"
        ]
       },
       {
@@ -883,7 +883,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c623900> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e5a0> >"
        ]
       },
       {
@@ -1027,7 +1027,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f6f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e450> >"
        ]
       }
      ],
@@ -1433,7 +1433,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd630> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d4b0> >"
        ]
       }
      ],
@@ -1759,7 +1759,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f8d0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d480> >"
        ]
       },
       {
@@ -1957,7 +1957,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f6f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062eed0> >"
        ]
       },
       {
@@ -2138,7 +2138,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f7b0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e450> >"
        ]
       }
      ],
@@ -2474,7 +2474,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd0f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e376f660> >"
        ]
       }
      ],
@@ -2619,7 +2619,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f7e0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d540> >"
        ]
       },
       {
@@ -2739,7 +2739,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd690> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062ef00> >"
        ]
       },
       {
@@ -2920,7 +2920,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f6f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e480> >"
        ]
       }
      ],
@@ -3278,7 +3278,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd6c0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d480> >"
        ]
       }
      ],
@@ -3569,7 +3569,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f7e0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d540> >"
        ]
       },
       {
@@ -3722,7 +3722,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f5a0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e3f0> >"
        ]
       },
       {
@@ -3860,7 +3860,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f6f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062ef00> >"
        ]
       }
      ],
@@ -4164,7 +4164,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd5d0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d5d0> >"
        ]
       }
      ],
@@ -4276,7 +4276,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bdab0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d810> >"
        ]
       }
      ],
@@ -4369,7 +4369,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f750> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064da20> >"
        ]
       },
       {
@@ -4436,7 +4436,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f750> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e3f0> >"
        ]
       }
      ],
@@ -4523,7 +4523,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd750> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064da80> >"
        ]
       }
      ],
@@ -4585,16 +4585,17 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"352pt\" height=\"149pt\"\n",
-        " viewBox=\"0.00 0.00 352.00 149.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 145)\">\n",
+        "<svg width=\"352pt\" height=\"162pt\"\n",
+        " viewBox=\"0.00 0.00 352.00 162.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 158)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-145 348,-145 348,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"123\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
-        "<text text-anchor=\"start\" x=\"145\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"161\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
-        "<text text-anchor=\"start\" x=\"201\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"217\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-158 348,-158 348,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"123\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+        "<text text-anchor=\"start\" x=\"145\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"161\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
+        "<text text-anchor=\"start\" x=\"201\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"217\" y=\"-139.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<text text-anchor=\"start\" x=\"126.5\" y=\"-125.8\" font-family=\"Lato\" font-size=\"14.00\">[Streett&#45;like 1]</text>\n",
         "<g id=\"clust1\" class=\"cluster\"><title>cluster_0</title>\n",
         "<polygon fill=\"none\" stroke=\"green\" points=\"284,-9 284,-109 336,-109 336,-9 284,-9\"/>\n",
         "</g>\n",
@@ -4678,7 +4679,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd600> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064db40> >"
        ]
       }
      ],
@@ -4808,7 +4809,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c59f5a0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064dc00> >"
        ]
       },
       {
@@ -4897,7 +4898,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd120> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e062e3f0> >"
        ]
       },
       {
@@ -5015,7 +5016,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bddb0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064dcc0> >"
        ]
       }
      ],
@@ -5199,7 +5200,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5570f0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e05e74b0> >"
        ]
       },
       {
@@ -5310,7 +5311,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bd9c0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d780> >"
        ]
       }
      ],
@@ -5401,7 +5402,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f132c5bdbd0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f71e064d420> >"
        ]
       }
      ],
diff --git a/tests/python/randaut.ipynb b/tests/python/randaut.ipynb
index 5ad351bdf..9e1ac5953 100644
--- a/tests/python/randaut.ipynb
+++ b/tests/python/randaut.ipynb
@@ -35,7 +35,7 @@
      "language": "python",
      "metadata": {},
      "outputs": [],
-     "prompt_number": 1
+     "prompt_number": 2
     },
     {
      "cell_type": "markdown",
@@ -1201,19 +1201,20 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"459.5\" y=\"-101.849\">p0 &amp; p1</text>\n",
         "</g>\n",
         "</g>\n",
-        "</svg></TD></TR><TR><TD><svg height=\"105pt\" viewBox=\"0.00 0.00 389.00 105.29\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.63047 0.63047) rotate(0) translate(4 163)\">\n",
+        "</svg></TD></TR><TR><TD><svg height=\"113pt\" viewBox=\"0.00 0.00 389.00 113.48\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.63047 0.63047) rotate(0) translate(4 176)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-163 613,-163 613,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"192.5\" y=\"-144.8\">(Fin(</text>\n",
-        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.5\" y=\"-144.8\">\u2777</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.5\" y=\"-144.8\">) | Inf(</text>\n",
-        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"273.5\" y=\"-144.8\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289.5\" y=\"-144.8\">)) &amp; (Inf(</text>\n",
-        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"340.5\" y=\"-144.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.5\" y=\"-144.8\">)&amp;Inf(</text>\n",
-        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"392.5\" y=\"-144.8\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.5\" y=\"-144.8\">))</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-176 613,-176 613,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"192.5\" y=\"-157.8\">(Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.5\" y=\"-157.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.5\" y=\"-157.8\">) | Inf(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"273.5\" y=\"-157.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289.5\" y=\"-157.8\">)) &amp; (Inf(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"340.5\" y=\"-157.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.5\" y=\"-157.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"392.5\" y=\"-157.8\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.5\" y=\"-157.8\">))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259\" y=\"-143.8\">[Streett-like 3]</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
@@ -1305,19 +1306,20 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"500\" y=\"-46.8\">!p0 &amp; p1</text>\n",
         "</g>\n",
         "</g>\n",
-        "</svg></TD><TD><svg height=\"105pt\" viewBox=\"0.00 0.00 389.00 105.29\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.63047 0.63047) rotate(0) translate(4 163)\">\n",
+        "</svg></TD><TD><svg height=\"113pt\" viewBox=\"0.00 0.00 389.00 113.48\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.63047 0.63047) rotate(0) translate(4 176)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-163 613,-163 613,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"192.5\" y=\"-144.8\">(Fin(</text>\n",
-        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.5\" y=\"-144.8\">\u2777</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.5\" y=\"-144.8\">) | Inf(</text>\n",
-        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"273.5\" y=\"-144.8\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289.5\" y=\"-144.8\">)) &amp; (Inf(</text>\n",
-        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"340.5\" y=\"-144.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.5\" y=\"-144.8\">)&amp;Inf(</text>\n",
-        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"392.5\" y=\"-144.8\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.5\" y=\"-144.8\">))</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-176 613,-176 613,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"192.5\" y=\"-157.8\">(Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"220.5\" y=\"-157.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"236.5\" y=\"-157.8\">) | Inf(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"273.5\" y=\"-157.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"289.5\" y=\"-157.8\">)) &amp; (Inf(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"340.5\" y=\"-157.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"356.5\" y=\"-157.8\">)&amp;Inf(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"392.5\" y=\"-157.8\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"408.5\" y=\"-157.8\">))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259\" y=\"-143.8\">[Streett-like 3]</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
@@ -2085,19 +2087,20 @@
         "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"553.5\" y=\"-39.0475\">\u2777</text>\n",
         "</g>\n",
         "</g>\n",
-        "</svg></TD></TR><TR><TD><svg height=\"102pt\" viewBox=\"0.00 0.00 389.00 101.87\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.636661 0.636661) rotate(0) translate(4 156)\">\n",
+        "</svg></TD></TR><TR><TD><svg height=\"110pt\" viewBox=\"0.00 0.00 389.00 110.14\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.636661 0.636661) rotate(0) translate(4 169)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-156 607,-156 607,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-137.8\">(Fin(</text>\n",
-        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-137.8\">\u2777</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-137.8\">)|Fin(</text>\n",
-        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-137.8\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Inf(</text>\n",
-        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-137.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-137.8\">) &amp; Fin(</text>\n",
-        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-137.8\">))</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-169 607,-169 607,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-150.8\">(Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-150.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-150.8\">)|Fin(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-150.8\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-150.8\">)) | (Inf(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-150.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-150.8\">) &amp; Fin(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-150.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-150.8\">))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-136.8\">[Rabin-like 3]</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
@@ -2177,19 +2180,20 @@
         "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"368\" y=\"-26.8\">p0 &amp; !p1</text>\n",
         "</g>\n",
         "</g>\n",
-        "</svg></TD><TD><svg height=\"102pt\" viewBox=\"0.00 0.00 389.00 101.87\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.636661 0.636661) rotate(0) translate(4 156)\">\n",
+        "</svg></TD><TD><svg height=\"110pt\" viewBox=\"0.00 0.00 389.00 110.14\" width=\"389pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+        "<g class=\"graph\" id=\"graph0\" transform=\"scale(0.636661 0.636661) rotate(0) translate(4 169)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" points=\"-4,4 -4,-156 607,-156 607,4 -4,4\" stroke=\"none\"/>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-137.8\">(Fin(</text>\n",
-        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-137.8\">\u2777</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-137.8\">)|Fin(</text>\n",
-        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-137.8\">\u2778</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-137.8\">)) | (Inf(</text>\n",
-        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-137.8\">\u24ff</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-137.8\">) &amp; Fin(</text>\n",
-        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-137.8\">\u2776</text>\n",
-        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-137.8\">))</text>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-169 607,-169 607,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"190.5\" y=\"-150.8\">(Fin(</text>\n",
+        "<text fill=\"#ff7f00\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"218.5\" y=\"-150.8\">\u2777</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"234.5\" y=\"-150.8\">)|Fin(</text>\n",
+        "<text fill=\"#6a3d9a\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.5\" y=\"-150.8\">\u2778</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"282.5\" y=\"-150.8\">)) | (Inf(</text>\n",
+        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"326.5\" y=\"-150.8\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"342.5\" y=\"-150.8\">) &amp; Fin(</text>\n",
+        "<text fill=\"#ff4da0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"388.5\" y=\"-150.8\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"404.5\" y=\"-150.8\">))</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"259.5\" y=\"-136.8\">[Rabin-like 3]</text>\n",
         "<!-- I -->\n",
         "<!-- 0 -->\n",
         "<g class=\"node\" id=\"node2\"><title>0</title>\n",
@@ -2273,22 +2277,13 @@
        ],
        "metadata": {},
        "output_type": "pyout",
-       "prompt_number": 2,
+       "prompt_number": 3,
        "text": [
         "<IPython.core.display.HTML object>"
        ]
       }
      ],
-     "prompt_number": 2
-    },
-    {
-     "cell_type": "code",
-     "collapsed": false,
-     "input": [],
-     "language": "python",
-     "metadata": {},
-     "outputs": [],
-     "prompt_number": null
+     "prompt_number": 3
     }
    ],
    "metadata": {}