From 33391798a39b6232a50340f15af951d0ca6a9c79 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 22 Apr 2016 18:48:03 +0200
Subject: [PATCH] python: export tgba_determinize

* python/spot/impl.i: Here.
* tests/python/automata.ipynb: Use it.
* NEWS: Mention it.
---
 NEWS                        |   4 +
 python/spot/impl.i          |   2 +
 tests/python/automata.ipynb | 291 ++++++++++++++++++++++++++++++++----
 3 files changed, 270 insertions(+), 27 deletions(-)

diff --git a/NEWS b/NEWS
index b89c16983..2b0472c9a 100644
--- a/NEWS
+++ b/NEWS
@@ -24,6 +24,10 @@ New in spot 2.0a (not yet released)
   * Add missing documentation for the option string passed to
     spot::make_emptiness_check_instantiator().
 
+  Python:
+
+  * The tgba_determinize() function is now accessible in Python.
+
   Bug fixes:
 
   * Typo in documentation of the -H option in --help output.
diff --git a/python/spot/impl.i b/python/spot/impl.i
index 2a1db01ff..cd895afbd 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -123,6 +123,7 @@
 #include <spot/twaalgos/ltl2taa.hh>
 #include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/twaalgos/compsusp.hh>
+#include <spot/twaalgos/determinize.hh>
 #include <spot/twaalgos/magic.hh>
 #include <spot/twaalgos/minimize.hh>
 #include <spot/twaalgos/neverclaim.hh>
@@ -428,6 +429,7 @@ namespace std {
 %include <spot/twaalgos/ltl2taa.hh>
 %include <spot/twaalgos/ltl2tgba_fm.hh>
 %include <spot/twaalgos/compsusp.hh>
+%include <spot/twaalgos/determinize.hh>
 %include <spot/twaalgos/magic.hh>
 %include <spot/twaalgos/minimize.hh>
 %include <spot/twaalgos/neverclaim.hh>
diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb
index 8fda68e28..e470761ee 100644
--- a/tests/python/automata.ipynb
+++ b/tests/python/automata.ipynb
@@ -18,7 +18,7 @@
    "version": "3.4.3+"
   },
   "name": "",
-  "signature": "sha256:93ecf5f37287bb2a03dcd63d41faa06f0ed9d8bcc403c73b24d1bf10404b3b1c"
+  "signature": "sha256:29d335e40a65f0ca04a3b2b07bfcbf92f794407b413644546d957487dcbf4bb1"
  },
  "nbformat": 3,
  "nbformat_minor": 0,
@@ -178,7 +178,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cfc093810> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8369240> >"
        ]
       }
      ],
@@ -317,7 +317,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7cff347ef0>"
+        "<IPython.core.display.SVG at 0x7f09a13dd5f8>"
        ]
       }
      ],
@@ -470,7 +470,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7d034410f0>"
+        "<IPython.core.display.SVG at 0x7f09a074abe0>"
        ]
       }
      ],
@@ -570,7 +570,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ee10> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323fc0> >"
        ]
       }
      ],
@@ -640,7 +640,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ecc0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323e70> >"
        ]
       }
      ],
@@ -716,7 +716,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ed50> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323f00> >"
        ]
       }
      ],
@@ -839,7 +839,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced200cc0>"
+        "<IPython.core.display.SVG at 0x7f09a0773da0>"
        ]
       }
      ],
@@ -1029,7 +1029,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced19d7f0>"
+        "<IPython.core.display.SVG at 0x7f098bfe96d8>"
        ]
       }
      ],
@@ -1176,7 +1176,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef60> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323f30> >"
        ]
       }
      ],
@@ -1277,7 +1277,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef30> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3210> >"
        ]
       }
      ],
@@ -1395,7 +1395,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef00> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3240> >"
        ]
       }
      ],
@@ -1494,7 +1494,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ed20> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff3270> >"
        ]
       }
      ],
@@ -1964,7 +1964,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ef90> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323ed0> >"
        ]
       }
      ],
@@ -2161,7 +2161,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced19d5c0>"
+        "<IPython.core.display.SVG at 0x7f09a0703dd8>"
        ]
       },
       {
@@ -2286,7 +2286,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7d03411e10>"
+        "<IPython.core.display.SVG at 0x7f09a0734198>"
        ]
       },
       {
@@ -2428,7 +2428,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced1fa710>"
+        "<IPython.core.display.SVG at 0x7f09a06db400>"
        ]
       },
       {
@@ -2579,7 +2579,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ecf0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff33f0> >"
        ]
       }
      ],
@@ -2735,7 +2735,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37eed0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f09a8323c60> >"
        ]
       }
      ],
@@ -2805,7 +2805,7 @@
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7cef37ecf0> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f098bff31b0> >"
        ]
       }
      ],
@@ -2877,7 +2877,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced1863c8>"
+        "<IPython.core.display.SVG at 0x7f09a06980f0>"
        ]
       },
       {
@@ -2930,7 +2930,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced1913c8>"
+        "<IPython.core.display.SVG at 0x7f09a0682358>"
        ]
       },
       {
@@ -3042,7 +3042,7 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced18d160>"
+        "<IPython.core.display.SVG at 0x7f09a0742908>"
        ]
       },
       {
@@ -3154,20 +3154,257 @@
         "</svg>"
        ],
        "text": [
-        "<IPython.core.display.SVG at 0x7f7ced1b7668>"
+        "<IPython.core.display.SVG at 0x7f09a0742828>"
        ]
       }
      ],
      "prompt_number": 23
     },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Explicit determinization after translation:"
+     ]
+    },
     {
      "cell_type": "code",
      "collapsed": true,
-     "input": [],
+     "input": [
+      "a = spot.translate('FGa')\n",
+      "display(a)\n",
+      "display(a.is_deterministic())"
+     ],
      "language": "python",
      "metadata": {},
-     "outputs": [],
-     "prompt_number": 23
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "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=\"161pt\" height=\"92pt\"\n",
+        " viewBox=\"0.00 0.00 161.00 92.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 88)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-88 157,-88 157,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=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-14.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,-18C2.79388,-18 17.1543,-18 30.6317,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"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\"/>\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,-35.0373C48.3189,-44.8579 50.4453,-54 56,-54 60.166,-54 62.4036,-48.8576 62.7128,-42.1433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"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\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"135\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">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.0888,-18C84.5562,-18 98.1196,-18 109.693,-18\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"116.959,-18 109.959,-21.1501 113.459,-18 109.959,-18.0001 109.959,-18.0001 109.959,-18.0001 113.459,-18 109.959,-14.8501 116.959,-18 116.959,-18\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\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=\"M128.266,-35.0373C126.892,-44.8579 129.137,-54 135,-54 139.397,-54 141.759,-48.8576 142.086,-42.1433\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"141.734,-35.0373 145.226,-41.8728 141.907,-38.533 142.08,-42.0287 142.08,-42.0287 142.08,-42.0287 141.907,-38.533 138.934,-42.1847 141.734,-35.0373 141.734,-35.0373\"/>\n",
+        "<text text-anchor=\"start\" x=\"131.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"127\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</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 0x7f09a82ac5d0> >"
+       ]
+      },
+      {
+       "metadata": {},
+       "output_type": "display_data",
+       "text": [
+        "False"
+       ]
+      }
+     ],
+     "prompt_number": 24
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "spot.tgba_determinize(a).show('.ba')"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 25,
+       "svg": [
+        "<svg height=\"127pt\" viewBox=\"0.00 0.00 170.00 127.47\" 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 123.465)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" points=\"-4,4 -4,-123.465 166,-123.465 166,4 -4,4\" stroke=\"none\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"29\" y=\"-105.265\">Fin(</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"54\" y=\"-105.265\">\u24ff</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"70\" y=\"-105.265\">) &amp; Inf(</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"113\" y=\"-105.265\">\u2776</text>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"129\" y=\"-105.265\">)</text>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g class=\"node\" id=\"node2\"><title>0</title>\n",
+        "<ellipse cx=\"56\" cy=\"-30.4654\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-26.7654\">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,-30.4654C2.79388,-30.4654 17.1543,-30.4654 30.6317,-30.4654\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"37.9419,-30.4654 30.9419,-33.6155 34.4419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 34.4419,-30.4655 30.9418,-27.3155 37.9419,-30.4654 37.9419,-30.4654\" stroke=\"black\"/>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;0</title>\n",
+        "<path d=\"M49.6208,-47.5027C48.3189,-57.3234 50.4453,-66.4654 56,-66.4654 60.166,-66.4654 62.4036,-61.323 62.7128,-54.6087\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"62.3792,-47.5027 65.8541,-54.3473 62.5434,-50.9989 62.7076,-54.495 62.7076,-54.495 62.7076,-54.495 62.5434,-50.9989 59.561,-54.6428 62.3792,-47.5027 62.3792,-47.5027\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"50.5\" y=\"-70.2654\">!a</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g class=\"node\" id=\"node3\"><title>1</title>\n",
+        "<ellipse cx=\"144\" cy=\"-30.4654\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"144\" y=\"-26.7654\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
+        "<path d=\"M74.0378,-33.3939C79.731,-34.2402 86.1223,-35.0477 92,-35.4654 99.0932,-35.9695 100.907,-35.9695 108,-35.4654 111.49,-35.2174 115.161,-34.832 118.759,-34.3826\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"125.962,-33.3939 119.456,-37.4666 122.495,-33.8699 119.027,-34.3459 119.027,-34.3459 119.027,-34.3459 122.495,-33.8699 118.599,-31.2251 125.962,-33.3939 125.962,-33.3939\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"96.5\" y=\"-54.2654\">a</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-39.2654\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g class=\"edge\" id=\"edge5\"><title>1-&gt;0</title>\n",
+        "<path d=\"M131.404,-17.3266C125.156,-11.2493 116.908,-4.67653 108,-1.46544 95.985,2.86544 83.5046,-4.00369 73.8973,-12.1402\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"68.5978,-17.0022 71.6264,-9.94872 71.1769,-14.636 73.7559,-12.2699 73.7559,-12.2699 73.7559,-12.2699 71.1769,-14.636 75.8855,-14.591 68.5978,-17.0022 68.5978,-17.0022\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"94.5\" y=\"-20.2654\">!a</text>\n",
+        "<text fill=\"#5da5da\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-5.26544\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g class=\"edge\" id=\"edge4\"><title>1-&gt;1</title>\n",
+        "<path d=\"M136.332,-46.7557C134.483,-56.8546 137.039,-66.4654 144,-66.4654 149.221,-66.4654 151.964,-61.0593 152.229,-54.0958\" fill=\"none\" stroke=\"black\"/>\n",
+        "<polygon fill=\"black\" points=\"151.668,-46.7557 155.342,-53.4954 151.935,-50.2455 152.201,-53.7354 152.201,-53.7354 152.201,-53.7354 151.935,-50.2455 149.06,-53.9754 151.668,-46.7557 151.668,-46.7557\" stroke=\"black\"/>\n",
+        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"140.5\" y=\"-85.2654\">a</text>\n",
+        "<text fill=\"#f17cb0\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"136\" y=\"-70.2654\">\u2776</text>\n",
+        "</g>\n",
+        "</g>\n",
+        "</svg>"
+       ],
+       "text": [
+        "<IPython.core.display.SVG at 0x7f09a06db4a8>"
+       ]
+      }
+     ],
+     "prompt_number": 25
+    },
+    {
+     "cell_type": "markdown",
+     "metadata": {},
+     "source": [
+      "Determinization by `translate()`.  The `generic` option allows any acceptance condition to be used instead of the default generalized B\u00fcchi."
+     ]
+    },
+    {
+     "cell_type": "code",
+     "collapsed": false,
+     "input": [
+      "spot.translate('FGa', 'generic', 'deterministic')"
+     ],
+     "language": "python",
+     "metadata": {},
+     "outputs": [
+      {
+       "metadata": {},
+       "output_type": "pyout",
+       "prompt_number": 26,
+       "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=\"170pt\" height=\"104pt\"\n",
+        " viewBox=\"0.00 0.00 170.00 104.47\" 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 100.465)\">\n",
+        "<title>G</title>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-100.465 166,-100.465 166,4 -4,4\"/>\n",
+        "<!-- I -->\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-30.4654\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-26.7654\" font-family=\"Lato\" font-size=\"14.00\">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.15491,-30.4654C2.79388,-30.4654 17.1543,-30.4654 30.6317,-30.4654\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-30.4654 30.9419,-33.6155 34.4419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 30.9419,-30.4655 34.4419,-30.4655 30.9418,-27.3155 37.9419,-30.4654 37.9419,-30.4654\"/>\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=\"M49.6208,-47.5027C48.3189,-57.3234 50.4453,-66.4654 56,-66.4654 60.166,-66.4654 62.4036,-61.323 62.7128,-54.6087\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-47.5027 65.8541,-54.3473 62.5434,-50.9989 62.7076,-54.495 62.7076,-54.495 62.7076,-54.495 62.5434,-50.9989 59.561,-54.6428 62.3792,-47.5027 62.3792,-47.5027\"/>\n",
+        "<text text-anchor=\"start\" x=\"50.5\" y=\"-70.2654\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "</g>\n",
+        "<!-- 1 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144\" cy=\"-30.4654\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"144\" y=\"-26.7654\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0&#45;&gt;1 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M74.0378,-33.3939C79.731,-34.2402 86.1223,-35.0477 92,-35.4654 99.0932,-35.9695 100.907,-35.9695 108,-35.4654 111.49,-35.2174 115.161,-34.832 118.759,-34.3826\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"125.962,-33.3939 119.456,-37.4666 122.495,-33.8699 119.027,-34.3459 119.027,-34.3459 119.027,-34.3459 122.495,-33.8699 118.599,-31.2251 125.962,-33.3939 125.962,-33.3939\"/>\n",
+        "<text text-anchor=\"start\" x=\"96.5\" y=\"-54.2654\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-39.2654\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M131.404,-17.3266C125.156,-11.2493 116.908,-4.67653 108,-1.46544 95.985,2.86544 83.5046,-4.00369 73.8973,-12.1402\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"68.5978,-17.0022 71.6264,-9.94872 71.1769,-14.636 73.7559,-12.2699 73.7559,-12.2699 73.7559,-12.2699 71.1769,-14.636 75.8855,-14.591 68.5978,-17.0022 68.5978,-17.0022\"/>\n",
+        "<text text-anchor=\"start\" x=\"94.5\" y=\"-20.2654\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-5.26544\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M136.332,-46.7557C134.483,-56.8546 137.039,-66.4654 144,-66.4654 149.221,-66.4654 151.964,-61.0593 152.229,-54.0958\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"151.668,-46.7557 155.342,-53.4954 151.935,-50.2455 152.201,-53.7354 152.201,-53.7354 152.201,-53.7354 151.935,-50.2455 149.06,-53.9754 151.668,-46.7557 151.668,-46.7557\"/>\n",
+        "<text text-anchor=\"start\" x=\"140.5\" y=\"-85.2654\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
+        "<text text-anchor=\"start\" x=\"136\" y=\"-70.2654\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</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 0x7f09a82ac480> >"
+       ]
+      }
+     ],
+     "prompt_number": 26
     }
    ],
    "metadata": {}
-- 
GitLab