diff --git a/NEWS b/NEWS
index f86d8aa3d..b86947f70 100644
--- a/NEWS
+++ b/NEWS
@@ -81,6 +81,10 @@ New in spot 2.5.3.dev  (not yet released)
     See https://spot.lrde.epita.fr/ipynb/alternation.html for some
     examples.
 
+  - Strings are now implicitely converted into formulas when passed
+    as arguments to functions that expect formulas.  Previously this
+    was done only for a few functions.
+
   Bugs fixed:
 
   - print_dot() will correctly escape strings containing \n in HTML
diff --git a/doc/org/tut02.org b/doc/org/tut02.org
index 22abe6be3..ddad6dd33 100644
--- a/doc/org/tut02.org
+++ b/doc/org/tut02.org
@@ -62,18 +62,17 @@ pairs of atomic propositions of the form (new-name, old-name).
 
 #+BEGIN_SRC python :results output :exports both
 import spot
-f = spot.formula('"Proc@Here" U ("var > 10" | "var < 4")')
 m = spot.relabeling_map()
-g = spot.relabel(f, spot.Pnn, m)
+g = spot.relabel('"Proc@Here" U ("var > 10" | "var < 4")', spot.Pnn, m)
 for newname, oldname in m.items():
   print("#define {} ({})".format(newname.to_str(), oldname.to_str('spin', True)))
 print(g.to_str('spin', True))
 #+END_SRC
 
 #+RESULTS:
-: #define p0 ((Proc@Here))
-: #define p1 ((var < 4))
-: #define p2 ((var > 10))
+: #define p0 (Proc@Here)
+: #define p1 (var < 4)
+: #define p2 (var > 10)
 : (p0) U ((p1) || (p2))
 
 * C++
diff --git a/python/spot/__init__.py b/python/spot/__init__.py
index e43331a54..c0f4a83cf 100644
--- a/python/spot/__init__.py
+++ b/python/spot/__init__.py
@@ -675,26 +675,18 @@ def translate(formula, *args, dict=_bdd_dict):
 formula.translate = translate
 
 
-def contains(left, right):
-    from spot.impl import contains as contains_impl
-    if type(left) is str:
-        left = formula(left)
-    if type(right) is str:
-        right = formula(right)
-    return contains_impl(left, right)
+# Wrap C++-functions into lambdas so that they get converted into
+# instance methods (i.e., self passed as first argument
+# automatically), because only user-defined functions are converted as
+# instance methods.
+def _add_formula(meth, name = None):
+    setattr(formula, name or meth, (lambda self, *args, **kwargs:
+                                    globals()[meth](self, *args, **kwargs)))
 
-def are_equivalent(left, right):
-    from spot.impl import are_equivalent as equiv
-    if type(left) is str:
-        left = formula(left)
-    if type(right) is str:
-        right = formula(right)
-    return equiv(left, right)
 
-formula.contains = contains
-formula.equivalent_to = are_equivalent
-twa.contains = contains
-twa.equivalent_to = are_equivalent
+_add_formula('contains')
+_add_formula('are_equivalent', 'equivalent_to')
+
 
 def postprocess(automaton, *args, formula=None):
     """Post process an automaton.
diff --git a/python/spot/impl.i b/python/spot/impl.i
index cc8e1e789..41d6ff670 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -365,7 +365,8 @@ namespace swig
 // default to None on the Python side.
 %typemap(in) spot::formula {
     void *tmp;
-    int res = SWIG_ConvertPtr($input, &tmp, $descriptor(spot::formula*), 0);
+    int res = SWIG_ConvertPtr($input, &tmp, $descriptor(spot::formula*),
+                              SWIG_POINTER_IMPLICIT_CONV);
     if (!SWIG_IsOK(res)) {
       %argument_fail(res, "spot::formula", $symname, $argnum);
     }
@@ -377,9 +378,10 @@ namespace swig
     // if tmp == nullptr, then the default value of $1 is fine.
 }
 
-%typemap(typecheck) spot::formula {
+%typemap(typecheck, precedence=2000) spot::formula {
     $1 = SWIG_CheckState(SWIG_ConvertPtr($input, nullptr,
-					 $descriptor(spot::formula*), 0));
+					 $descriptor(spot::formula*),
+                                         SWIG_POINTER_IMPLICIT_CONV));
 }
 
 %typemap(out) spot::formula {
@@ -427,6 +429,7 @@ namespace swig
 %include <spot/misc/trival.hh>
 
 %implicitconv std::vector<spot::formula>;
+%implicitconv spot::formula;
 
 %include <spot/tl/formula.hh>
 
diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb
index 0317161c2..66c50b728 100644
--- a/tests/python/atva16-fig2a.ipynb
+++ b/tests/python/atva16-fig2a.ipynb
@@ -4,7 +4,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "This example is the left part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"."
+    "This example is the left part of Fig.2 in our ATVA'16 paper titled [\"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"](https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf), slightly updated to the current version of Spot."
    ]
   },
   {
@@ -14,7 +14,7 @@
    "outputs": [],
    "source": [
     "import spot\n",
-    "spot.setup(show_default='.abr')"
+    "spot.setup(show_default='.b')"
    ]
   },
   {
@@ -155,7 +155,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3264654bd0> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f81a85ea1e0> >"
       ]
      },
      "execution_count": 3,
@@ -175,7 +175,7 @@
    "source": [
     "def implies(f, g):\n",
     "    f = spot.formula(f)\n",
-    "    g = spot.formula_Not(spot.formula(g))\n",
+    "    g = spot.formula.Not(g)\n",
     "    return spot.product(f.translate(), g.translate()).is_empty()\n",
     "def equiv(f, g):\n",
     "    return implies(f, g) and implies(g, f)"
diff --git a/tests/python/atva16-fig2b.ipynb b/tests/python/atva16-fig2b.ipynb
index aa218221e..900bfd3aa 100644
--- a/tests/python/atva16-fig2b.ipynb
+++ b/tests/python/atva16-fig2b.ipynb
@@ -4,7 +4,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "This example is the right part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"."
+    "This example is the right part of Fig.2 in our ATVA'16 paper titled [\"*Spot 2.0 — a framework for LTL and ω-automata manipulation*\"](https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf) slightly updated to benefit from improvements in more recent versions of Spot."
    ]
   },
   {
@@ -15,8 +15,8 @@
    "source": [
     "import spot\n",
     "import spot.ltsmin\n",
-    "spot.setup(show_default='.abr', max_states=10)\n",
-    "# This extra line ensures that our test-suite skips this test if divine is not installed.\n",
+    "spot.setup(show_default='.Ab', max_states=10)\n",
+    "# This extra line ensures that our test suite skips this test if divine is not installed.\n",
     "spot.ltsmin.require('divine')"
    ]
   },
@@ -82,12 +82,10 @@
        "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
        " -->\n",
        "<!-- Pages: 1 -->\n",
-       "<svg width=\"734pt\" height=\"177pt\"\n",
-       " viewBox=\"0.00 0.00 734.00 177.35\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(.5617 .5617) rotate(0) translate(4 311.7401)\">\n",
-       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-311.7401 1302.7729,-311.7401 1302.7729,4 -4,4\"/>\n",
-       "<text text-anchor=\"start\" x=\"646.3864\" y=\"-292.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">t</text>\n",
-       "<text text-anchor=\"start\" x=\"638.3864\" y=\"-277.5401\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#000000\">[all]</text>\n",
+       "<svg width=\"734pt\" height=\"156pt\"\n",
+       " viewBox=\"0.00 0.00 734.00 156.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(.5617 .5617) rotate(0) translate(4 273.7401)\">\n",
+       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-273.7401 1302.7729,-273.7401 1302.7729,4 -4,4\"/>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
@@ -289,7 +287,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f7cac317630> >"
+       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f4dc45626f0> >"
       ]
      },
      "execution_count": 4,
@@ -308,10 +306,9 @@
    "outputs": [],
    "source": [
     "def model_check(model, f):\n",
-    "    f = spot.formula(f)\n",
-    "    ss = model.kripke(spot.atomic_prop_collect(f))\n",
-    "    nf = spot.formula_Not(f).translate()\n",
-    "    return spot.otf_product(ss, nf).is_empty()"
+    "    nf = spot.formula.Not(f)\n",
+    "    ss = model.kripke(spot.atomic_prop_collect(nf))\n",
+    "    return not ss.intersects(nf.translate())"
    ]
   },
   {
diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb
index 4f20ffc1f..9878b793e 100644
--- a/tests/python/formulas.ipynb
+++ b/tests/python/formulas.ipynb
@@ -11,9 +11,7 @@
   {
    "cell_type": "code",
    "execution_count": 1,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [],
    "source": [
     "import spot"
@@ -29,9 +27,7 @@
   {
    "cell_type": "code",
    "execution_count": 2,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -55,9 +51,7 @@
   {
    "cell_type": "code",
    "execution_count": 3,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -87,9 +81,7 @@
   {
    "cell_type": "code",
    "execution_count": 4,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -119,9 +111,7 @@
   {
    "cell_type": "code",
    "execution_count": 5,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -152,9 +142,7 @@
   {
    "cell_type": "code",
    "execution_count": 6,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -181,9 +169,7 @@
   {
    "cell_type": "code",
    "execution_count": 7,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -214,9 +200,7 @@
   {
    "cell_type": "code",
    "execution_count": 8,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -251,9 +235,7 @@
   {
    "cell_type": "code",
    "execution_count": 9,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -316,9 +298,7 @@
   {
    "cell_type": "code",
    "execution_count": 10,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -338,9 +318,7 @@
   {
    "cell_type": "code",
    "execution_count": 11,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -367,9 +345,7 @@
   {
    "cell_type": "code",
    "execution_count": 12,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -389,9 +365,7 @@
   {
    "cell_type": "code",
    "execution_count": 13,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -411,9 +385,7 @@
   {
    "cell_type": "code",
    "execution_count": 14,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -440,9 +412,7 @@
   {
    "cell_type": "code",
    "execution_count": 15,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -465,9 +435,7 @@
   {
    "cell_type": "code",
    "execution_count": 16,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -490,9 +458,7 @@
   {
    "cell_type": "code",
    "execution_count": 17,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -522,9 +488,7 @@
   {
    "cell_type": "code",
    "execution_count": 18,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -661,9 +625,7 @@
   {
    "cell_type": "code",
    "execution_count": 19,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -709,9 +671,7 @@
   {
    "cell_type": "code",
    "execution_count": 20,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -731,9 +691,7 @@
   {
    "cell_type": "code",
    "execution_count": 21,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -763,9 +721,7 @@
   {
    "cell_type": "code",
    "execution_count": 22,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -795,9 +751,7 @@
   {
    "cell_type": "code",
    "execution_count": 23,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -821,9 +775,7 @@
   {
    "cell_type": "code",
    "execution_count": 24,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "data": {
@@ -853,9 +805,7 @@
   {
    "cell_type": "code",
    "execution_count": 25,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -898,7 +848,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.6.4"
+   "version": "3.6.5"
   }
  },
  "nbformat": 4,
diff --git a/tests/python/ltsmin-dve.ipynb b/tests/python/ltsmin-dve.ipynb
index 83e4ac8d4..edbb35fcd 100644
--- a/tests/python/ltsmin-dve.ipynb
+++ b/tests/python/ltsmin-dve.ipynb
@@ -436,7 +436,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f77f84535a0> >"
+       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f2214652270> >"
       ]
      },
      "execution_count": 9,
@@ -1194,6 +1194,13 @@
     "k.show('.<0')  # unlimited output"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "If we have an LTL proposition to check, we can convert it into an automaton using `spot.translate()`, and synchronize that automaton with the Kripke structure using `spot.otf_product()`.  This `otf_product()` function returns product automaton that builds itself on-the-fly, as needed by whatever algorithm \"consumes\" it (here the display routine). "
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": 12,
@@ -1258,7 +1265,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f77f83e2ae0> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f22145bdb40> >"
       ]
      },
      "execution_count": 12,
@@ -1446,7 +1453,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f77f84536f0> >"
+       "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7f221462dae0> >"
       ]
      },
      "execution_count": 13,
@@ -1495,10 +1502,9 @@
    "outputs": [],
    "source": [
     "def model_check(f, m):\n",
-    "    f = spot.formula(f)\n",
-    "    ss = m.kripke(spot.atomic_prop_collect(f))\n",
-    "    nf = spot.formula_Not(f).translate()\n",
-    "    return spot.otf_product(ss, nf).is_empty() "
+    "    nf = spot.formula.Not(f)\n",
+    "    ss = m.kripke(spot.atomic_prop_collect(nf))\n",
+    "    return spot.otf_product(ss, nf.translate()).is_empty() "
    ]
   },
   {
@@ -1535,10 +1541,9 @@
    "outputs": [],
    "source": [
     "def model_debug(f, m):\n",
-    "    f = spot.formula(f)\n",
-    "    ss = m.kripke(spot.atomic_prop_collect(f))\n",
-    "    nf = spot.formula_Not(f).translate()\n",
-    "    return ss.intersecting_run(nf)"
+    "    nf = spot.formula.Not(f)\n",
+    "    ss = m.kripke(spot.atomic_prop_collect(nf))\n",
+    "    return ss.intersecting_run(nf.translate())"
    ]
   },
   {
@@ -1660,7 +1665,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f77f83ee270> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f221464a870> >"
       ]
      },
      "execution_count": 19,
diff --git a/tests/python/ltsmin-pml.ipynb b/tests/python/ltsmin-pml.ipynb
index 67dba3ed2..bf2d51539 100644
--- a/tests/python/ltsmin-pml.ipynb
+++ b/tests/python/ltsmin-pml.ipynb
@@ -38,8 +38,8 @@
       "SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n",
       "(C) University of Twente, Formal Methods and Tools group\n",
       "\n",
-      "Parsing tmp_kk6cvzf.pml...\n",
-      "Parsing tmp_kk6cvzf.pml done (0.0 sec)\n",
+      "Parsing tmps8i1kbv6.pml...\n",
+      "Parsing tmps8i1kbv6.pml done (0.0 sec)\n",
       "\n",
       "Optimizing graphs...\n",
       "   StateMerging changed 0 states/transitions.\n",
@@ -225,8 +225,8 @@
       "   Found          2 /          2 (100.0%) Commuting actions               \n",
       "Generating guard dependency matrices done (0.0 sec)\n",
       "\n",
-      "Written C code to /home/adl/git/spot/tests/python/tmp_kk6cvzf.pml.spins.c\n",
-      "Compiled C code to PINS library tmp_kk6cvzf.pml.spins\n",
+      "Written C code to /home/adl/git/spot/tests/python/tmps8i1kbv6.pml.spins.c\n",
+      "Compiled C code to PINS library tmps8i1kbv6.pml.spins\n",
       "\n"
      ]
     }
@@ -560,7 +560,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7fa8d4065b40> >"
+       "<spot.impl.kripke; proxy of <Swig Object of type 'std::shared_ptr< spot::kripke > *' at 0x7f44743b5ae0> >"
       ]
      },
      "execution_count": 4,
@@ -603,7 +603,7 @@
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node2\">\n",
        "<title>0</title>\n",
-       "<g id=\"a_node2\"><a xlink:title=\"P_0._pc=1, P_0.a=0, P_0.b=0\n",
+       "<g id=\"a_node2\"><a xlink:title=\"P_0._pc=0, P_0.a=0, P_0.b=0\n",
        "&quot;P_0.a &lt; 2&quot; &amp; !&quot;P_0.b &gt; 1&quot; &amp; !dead\">\n",
        "<ellipse cx=\"55\" cy=\"-117\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#000000\"/>\n",
        "<text fill=\"#000000\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"55\" y=\"-113.3\">0</text>\n",
diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb
index 69068fca7..3010ce323 100644
--- a/tests/python/stutter-inv.ipynb
+++ b/tests/python/stutter-inv.ipynb
@@ -7,7 +7,7 @@
    "outputs": [],
    "source": [
     "import spot\n",
-    "spot.setup(show_default='.ban')\n",
+    "spot.setup(show_default='.bn')\n",
     "from IPython.display import display"
    ]
   },
@@ -302,7 +302,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa2444ce810> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642b47b0> >"
       ]
      },
      "metadata": {},
@@ -355,7 +355,7 @@
     "def explain_stut(f):\n",
     "    f = spot.formula(f)\n",
     "    pos = spot.translate(f)\n",
-    "    neg = spot.translate(spot.formula_Not(f))\n",
+    "    neg = spot.translate(spot.formula.Not(f))\n",
     "    word = spot.product(spot.closure(pos), spot.closure(neg)).accepting_word()\n",
     "    if word is None:\n",
     "        print(f, \"is stutter invariant\")\n",
@@ -428,7 +428,7 @@
    "source": [
     "f1 = spot.formula('F(a & X!a & XF(b & X!b & Ga))')\n",
     "f2 = spot.formula('F(a & Xa & XXa & G!b)')\n",
-    "f = spot.formula_Or([f1, f2])\n",
+    "f = spot.formula.Or([f1, f2])\n",
     "\n",
     "print(spot.is_stutter_invariant(f1))\n",
     "print(spot.is_stutter_invariant(f2))\n",
@@ -595,7 +595,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24445d270> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642c22d0> >"
       ]
      },
      "metadata": {},
@@ -804,7 +804,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24445d270> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642c22d0> >"
       ]
      },
      "metadata": {},
@@ -845,7 +845,7 @@
    "source": [
     "g1 = spot.formula('GF(a & Xa) & GF!a')\n",
     "g2 = spot.formula('!GF(a & Xa) & GF!a')\n",
-    "g = spot.formula_Or([g1, g2])"
+    "g = spot.formula.Or([g1, g2])"
    ]
   },
   {
@@ -963,7 +963,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa2444ce8a0> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642b4750> >"
       ]
      },
      "metadata": {},
@@ -1062,7 +1062,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24446e5d0> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642d26c0> >"
       ]
      },
      "metadata": {},
@@ -1279,7 +1279,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24446e660> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642d2720> >"
       ]
      },
      "metadata": {},
@@ -1408,7 +1408,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa244d50270> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1643175a0> >"
       ]
      },
      "metadata": {},
@@ -1539,7 +1539,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa24446eb70> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642d2ea0> >"
       ]
      },
      "metadata": {},
@@ -1799,7 +1799,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa244480540> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642e62a0> >"
       ]
      },
      "metadata": {},
@@ -1819,7 +1819,7 @@
     "State: 6 [!0] 0\n",
     "State: 7 [!0] 6 [0] 5\n",
     "--END--\"\"\")\n",
-    "spot.highlight_stutter_invariant_states(ex1,None,  5)\n",
+    "spot.highlight_stutter_invariant_states(ex1, None, 5)\n",
     "display(ex1)"
    ]
   },
@@ -2113,7 +2113,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa244480540> >"
+       "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc1642e62a0> >"
       ]
      },
      "metadata": {},
@@ -2189,69 +2189,69 @@
      "output_type": "stream",
      "text": [
       "formula                                  states SIstates fwd_closed\n",
-      "(p1 & X(!p0 U p2)) R !p0                      3        2          1\n",
-      "(!p1 U (p0 | (!p1 & p2 & X(!p1 U p3))))       4        3          1\n",
-      "!p0 | ((p2 & X(!p1 U p3)) R !p1)              4        2          1\n",
-      "G(!p0 | (!p2 U (p1 | (!p2 & p3 & X(!p2 U      4        1          1\n",
-      "G(!p0 | (!p1 W (p2 | (!p1 & p3 & X(!p1 U      3        0          1\n",
-      "(!p0 U p2) | G(!p0 | XG!p1)                   3        2          1\n",
-      "G!p0 | ((p0 | !p1 | X(!p2 W p0)) U (p0 |      4        3          1\n",
-      "!p0 W (p0 & ((!p1 U p3) | G(!p1 | XG!p2)      4        2          1\n",
-      "G(!p0 | G!p1 | ((p1 | !p2 | X(!p3 W p1))      4        1          1\n",
-      "G(!p0 | ((p1 | !p2 | X(!p3 W p1)) U (p1       3        0          1\n",
-      "G(!p0 | X(F(p1 & Fp2) | G!p1))                6        1          1\n",
-      "G!p0 | ((!p1 | X((!p0 U (p2 & Fp3)) | (p      6        2          1\n",
-      "G(!p0 | G(!p1 | X(!p2 W (p2 & Fp3))))         5        0          1\n",
-      "G(!p0 | G!p1 | ((!p2 | X((!p1 U (p3 & Fp     10        2          1\n",
-      "G(!p0 | ((!p1 | X((!p2 U (p3 & Fp4)) | (     10        0          1\n",
-      "G(!p0 | F(p1 & XFp2))                         4        0          1\n",
-      "G!p0 | ((!p1 | ((p2 & X(!p0 U p3)) M !p0      4        1          1\n",
-      "G(!p0 | G(!p1 | (p2 & XFp3)))                 3        3          1\n",
-      "G(!p0 | G!p1 | ((!p2 | ((p3 & X(!p1 U p4      4        0          1\n",
-      "G(!p0 | ((!p1 | ((p3 & X(!p2 U p4)) M !p      6        2          1\n",
-      "G(!p0 | F(p1 & !p2 & X(!p2 U p3)))            4        0          1\n",
-      "G!p0 | ((!p1 | ((p2 & !p3 & X((!p0 & !p3      4        1          1\n",
-      "G(!p0 | G(!p1 | (p2 & !p3 & X(!p3 U p4))      3        3          1\n",
-      "G(!p0 | G!p1 | ((!p2 | ((p3 & !p4 & X((!      4        0          1\n",
-      "G(!p0 | ((!p1 | ((p3 & !p4 & X((!p2 & !p      6        2          1\n",
+      "Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2)))       3        2          1\n",
+      "Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U       4        3          1\n",
+      "G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1      4        2          1\n",
+      "G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 &      4        1          1\n",
+      "G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 &      3        0          1\n",
+      "F(p0 & XFp1) -> (!p0 U p2)                    3        2          1\n",
+      "Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))      4        3          1\n",
+      "G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p      4        2          1\n",
+      "G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!      4        1          1\n",
+      "G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3      3        0          1\n",
+      "G((p0 & XFp1) -> XF(p1 & Fp2))                6        1          1\n",
+      "Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (      6        2          1\n",
+      "G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & F      5        0          1\n",
+      "G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) ->      10        2          1\n",
+      "G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U      10        0          1\n",
+      "G(p0 -> F(p1 & XFp2))                         4        0          1\n",
+      "Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0       4        1          1\n",
+      "G(p0 -> G(p1 -> (p2 & XFp3)))                 3        3          1\n",
+      "G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3      4        0          1\n",
+      "G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2      6        2          1\n",
+      "G(p0 -> F(p1 & !p2 & X(!p2 U p3)))            4        0          1\n",
+      "Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 &       4        1          1\n",
+      "G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4))      3        3          1\n",
+      "G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3      4        0          1\n",
+      "G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 &      6        2          1\n",
       "p0 U (p1 & X(p2 U p3))                        3        2          1\n",
       "p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 &      7        2          1\n",
       "F(p0 & XGp1)                                  2        2          1\n",
       "F(p0 & X(p1 & XFp2))                          4        2          1\n",
       "F(p0 & X(p1 U p2))                            3        1          1\n",
-      "G(p0 & Fp1 & Fp2 & Fp3)                       1        1          1\n",
-      "GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp      4        4          1\n",
-      "GF((!p0 & Xp0) | (p0 & X!p0) | (!p1 & Xp      9        9          1\n",
-      "G(!p0 | !p1 | p2 | X(!p2 | p3 | X(!p1 |       3        0          1\n",
-      "G(!p0 | !p1 | p2 | X(!p2 | (p2 U (!p2 U       5        5          1\n",
-      "1                                             1        1          1\n",
-      "G(p0 | !p1 | Xp2)                             2        0          1\n",
-      "G(!p0 | X(p0 | p1))                           2        2          1\n",
-      "G((((p1 & Xp1) | (!p1 & X!p1)) & ((p0 &      34       34          1\n",
-      "G(!p0 | p1 | !p2 | X(!p0 | !p1 | p3))         2        2          1\n",
-      "G(!p0 | X(!p0 U p1))                          2        0          1\n",
-      "G(p0 | X(!p0 | (p0 W p1)))                    3        3          1\n",
-      "G(p0 | X(!p0 | ((!p1 & X(p0 & p1)) M p0)      4        4          1\n",
-      "G(p0 | X(!p0 | ((!p1 & X(p1 & ((!p1 & X(      6        6          1\n",
-      "G(!p0 | X(p0 | ((!p1 & X(p1 & ((!p1 & X(      6        6          1\n",
-      "G(!p0 | X(p0 | ((!p1 & X(p1 & ((!p1 & X(      8        8          1\n",
-      "G(p0 | X(!p0 | ((p0 | X!p0) U (!p1 & Xp1      6        6          1\n",
+      "G(p0 & XF(p1 & XF(p2 & XFp3)))                1        1          1\n",
+      "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0))             4        4          1\n",
+      "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2       9        9          1\n",
+      "G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1       3        0          1\n",
+      "G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2       5        5          1\n",
+      "G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U      1        1          1\n",
+      "G((!p0 & p1) -> Xp2)                          2        0          1\n",
+      "G(p0 -> X(p0 | p1))                           2        2          1\n",
+      "G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2      34       34          1\n",
+      "G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3))      2        2          1\n",
+      "G(p0 -> X(!p0 U p1))                          2        0          1\n",
+      "G((!p0 & Xp0) -> X((p0 U p1) | Gp0))          3        3          1\n",
+      "G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0      4        4          1\n",
+      "G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0      6        6          1\n",
+      "G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(      6        6          1\n",
+      "G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(      8        8          1\n",
+      "G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 &      6        6          1\n",
       "G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 |      12        0          1\n",
-      "G((!p0 & Xp0) | (p1 & Xp1) | (!p1 & X!p1      4        4          1\n",
-      "G((!p0 & Xp0) | ((!p1 | Xp1) & (p1 | X!p      4        4          1\n",
+      "G((Xp0 -> p0) -> (p1 <-> Xp1))                4        4          1\n",
+      "G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 ->       4        4          1\n",
       "p0 & XG!p0                                    2        1          1\n",
-      "XG(!p0 | p2 | G!p1 | X(p2 M !p1))             4        1          1\n",
-      "XG(!p0 | p1 | (!p1 W p2))                     3        2          1\n",
-      "XG(!p0 | !p1 | (p1 W p2))                     3        2          1\n",
-      "Xp0 & G(p0 | X(!p0 | Xp0))                    5        0          1\n",
-      "1                                             1        1          1\n",
-      "1                                             1        1          1\n",
-      "G(!p0 | Fp1)                                  2        2          1\n",
-      "G(!p0 | Fp1)                                  2        2          1\n",
-      "F(p0 & X(!p1 U !p2))                          3        1          1\n",
-      "(p0 & Xp1) R X(p2 R p0)                       5        3          1\n",
-      "G((p0 | XGp1) & (p2 | XG!p1))                 3        2          1\n",
-      "Gp0                                           1        1          1\n"
+      "XG(p0 -> (G!p1 | (!Xp1 U p2)))                4        1          1\n",
+      "XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))         3        2          1\n",
+      "XG((p0 & p1) -> (Gp1 | (p1 U p2)))            3        2          1\n",
+      "Xp0 & G((!p0 & Xp0) -> XXp0)                  5        0          1\n",
+      "(Xp0 U Xp1) | !X(p0 U p1)                     1        1          1\n",
+      "(Xp0 U p1) | !X(p0 U (p0 & p1))               1        1          1\n",
+      "((Xp0 U p1) | !X(p0 U (p0 & p1))) & G(p0      2        2          1\n",
+      "((Xp0 U Xp1) | !X(p0 U p1)) & G(p0 -> Fp      2        2          1\n",
+      "!G(p0 -> X(p1 R p2))                          3        1          1\n",
+      "(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R       5        3          1\n",
+      "G(p0 | XGp1) & G(p2 | XG!p1)                  3        2          1\n",
+      "G(p0 | (Xp1 & X!p1))                          1        1          1\n"
      ]
     }
    ],
@@ -2272,6 +2272,7 @@
     "fmt = \"{:40.40} {:>6} {:>8} {:>10}\"\n",
     "print(fmt.format(\"formula\", \"states\", \"SIstates\", \"fwd_closed\"))\n",
     "for f in formulas:\n",
+    "    s = f.to_str()\n",
     "    aut = spot.translate(f)\n",
     "    aut_size.append(aut.num_states())\n",
     "    sistates = spot.stutter_invariant_states(aut, f)\n",
@@ -2279,7 +2280,7 @@
     "    sistates_size.append(sisz)\n",
     "    fc = spot.is_stutter_invariant_forward_closed(aut, sistates) == -1\n",
     "    fwd_closed.append(fc)\n",
-    "    print(fmt.format(f.to_str(), aut.num_states(), sisz, fc))"
+    "    print(fmt.format(s, aut.num_states(), sisz, fc))"
    ]
   },
   {
@@ -2335,6 +2336,13 @@
    "source": [
     "100*sum(sistates_size)/sum(aut_size)"
    ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
   }
  ],
  "metadata": {