spot/tests/python/stutter-inv.ipynb

{
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.3"
  },
  "name": ""
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "import spot\n",
      "spot.setup(show_default='.ban')\n",
      "from IPython.display import display"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "# Stutter-invariant languages\n",
      "\n",
      "A language $L$ is said to be _stutter-invariant_ iff $\\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_{i+1}\\ldots\\in L \\iff \\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_i\\ell_{i+1}\\ldots\\in L$, i.e., if duplicating a letter in a word or removing a duplicated letter does not change the membership of that word to $L$.  These languages are also called _stutter-insensitive_.   We use the adjective _sutter-sensitive_ to describe a language that is not stutter-invariant.   Of course we can extend this vocabulary to LTL formulas or automata that represent stutter-invariant languages.\n",
      "\n",
      "Stutter-invariant languages play an important role in model checking.  When verifying a stutter-invariant specification against a system, we know that we have some freedom in how we discretize the time in the model: as long as we do not hide changes of model variables that are observed by the specification, we can merge multiple steps of the model.  This, combined by careful analysis of actions of the model that are independent, is the basis for a set of techniques known as _partial-order reductions_ (POR) that postpone the visit of some successors in the model, because we know we can always visit them later."
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "## Stutter-invariant formulas\n",
      "\n",
      "When the specification is expressed as an LTL formula, a well known way to ensure it is _stutter-invariant_ is to forbid the use of the `X` operator.  Testing whether a formula is `X`-free can be done in constant time using the `is_syntactic_stutter_invariant()` method."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('a U b')\n",
      "print(f.is_syntactic_stutter_invariant())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "True\n"
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('a U Xb')\n",
      "print(f.is_syntactic_stutter_invariant())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "False\n"
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "However some formula are syntactic-invariant despite their use of `X`.   Spot implements some [automaton-based check](https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf) to detect stutter-invariance reliably and efficiently.  This can be tested with the `is_stutter_invariant()` function."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "g = spot.formula('F(a & X(!a & Gb))')\n",
      "print(g.is_syntactic_stutter_invariant())\n",
      "print(spot.is_stutter_invariant(g))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "False\n",
        "True\n"
       ]
      }
     ],
     "prompt_number": 4
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Of course this `is_stutter_invariant()` function first checks whether the formula is `X`-free before wasting time building automata, so if you want to detect stutter-invariant formulas in your model checker, this is the only function to use.  Also, if you hapen to already have an automaton `aut_g` for `g`, you should pass it as a second argument to avoid it being recomputed: `spot.is_stutter_invariant(g, aut_g)`."
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "It is also known that any stutter-invariant LTL formula can be converted to an `X`-free LTL formula.  Several proofs of that exist.  Spot implements the rewriting of [K. Etessami](http://homepages.inf.ed.ac.uk/kousha/note_on_stut_tl_lpi.ps) under the name `remove_x()`.  Note that the output of this function is only equivalent to its input if the latter is stutter-invariant."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.remove_x(g)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\mathsf{F} (a \\land ((a \\land (a \\mathbin{\\mathsf{U}} (\\lnot a \\land \\mathsf{G} b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} \\lnot a) \\lor (b \\mathbin{\\mathsf{U}} \\lnot a))) \\lor (\\lnot a \\land (\\lnot a \\mathbin{\\mathsf{U}} (a \\land \\lnot a \\land \\mathsf{G} b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} a) \\lor (b \\mathbin{\\mathsf{U}} a))) \\lor (b \\land (b \\mathbin{\\mathsf{U}} (\\lnot a \\land \\lnot b \\land \\mathsf{G} b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} \\lnot b) \\lor (a \\mathbin{\\mathsf{U}} \\lnot b))) \\lor (\\lnot b \\land (\\lnot b \\mathbin{\\mathsf{U}} (\\lnot a \\land b \\land \\mathsf{G} b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} b) \\lor (a \\mathbin{\\mathsf{U}} b))) \\lor (\\lnot a \\land \\mathsf{G} b \\land (\\mathsf{G} \\lnot a \\lor \\mathsf{G} a) \\land (\\mathsf{G} b \\lor \\mathsf{G} \\lnot b))))$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 5,
       "text": [
        "F(a & ((a & (a U (!a & Gb)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & Gb)) & ((!b U a) | (b U a))) | (b & (b U (!a & !b & Gb)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b & Gb)) & ((!a U b) | (a U b))) | (!a & Gb & (G!a | Ga) & (Gb | G!b))))"
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Stutter-invariant automata"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Similarly to formulas, automata use a few bits to store some known properties about themselves, like whether they represent a stutter-invariant language.  This property can be checked with the `prop_stutter_invariant()` method, but that returns a `trival` instance (i.e., yes, no, or maybe).  Some algorithms will update that property whenever that is cheap or expliclitely asked for.   For instance `spot.translate()` only sets the property if the translated formula is `X`-free."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut = spot.translate(g)\n",
      "print(aut.prop_stutter_invariant())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "maybe\n"
       ]
      }
     ],
     "prompt_number": 6
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "As suggested above, we can call `is_stutter_invariant()` by passing a formula and its automaton, to save on one translation.  A second translation is still needed to complement the automaton."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(spot.is_stutter_invariant(g, aut))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "True\n"
       ]
      }
     ],
     "prompt_number": 7
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Note that `prop_stutter_invariant()` was updated as a side-effect so that any futher call to `is_stutter_invariant()` with this automaton will be instantaneous."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(aut.prop_stutter_invariant())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "yes\n"
       ]
      }
     ],
     "prompt_number": 8
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "You have to be aware of this property being set in your back because if while playing with `is_stutter_invariant()` you the incorrect formula for an automaton by mistake, the automaton will have its property set incorrectly, and running `is_stutter_inariant()` with the correct formula will simply return the cached property.\n",
      "\n",
      "In doubt, you can always reset the property as follows:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut.prop_stutter_invariant(spot.trival_maybe())\n",
      "print(aut.prop_stutter_invariant())"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "maybe\n"
       ]
      }
     ],
     "prompt_number": 9
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "In case you have an automaton for which you do not have formula, you can also use `is_stutter_invariant()` by passing this automaton as the first argument.  In that case a negated automaton will be constructed by determinization.  If you do happen to have a negated automaton handy, you can pass it as a second argument to avoid that."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "a1 = spot.automaton('''HOA: v1 \n",
      "AP: 1 \"a\" \n",
      "States: 2 \n",
      "Start: 0 \n",
      "Acceptance: 0 t\n",
      "--BODY-- \n",
      "State: 0 [0] 1 \n",
      "State: 1 [t] 0 \n",
      "--END--''')\n",
      "display(a1)\n",
      "print(spot.is_stutter_invariant(a1))"
     ],
     "language": "python",
     "metadata": {},
     "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=\"163pt\" height=\"84pt\"\n",
        " viewBox=\"0.00 0.00 163.00 84.35\" 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 80.3516)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-80.3516 159,-80.3516 159,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"74.5\" y=\"-61.1516\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
        "<text text-anchor=\"start\" x=\"66.5\" y=\"-46.1516\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-20.3516\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-16.6516\" 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,-20.3516C2.79388,-20.3516 17.1543,-20.3516 30.6317,-20.3516\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-20.3516 30.9419,-23.5017 34.4419,-20.3516 30.9419,-20.3517 30.9419,-20.3517 30.9419,-20.3517 34.4419,-20.3516 30.9418,-17.2017 37.9419,-20.3516 37.9419,-20.3516\"/>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"137\" cy=\"-20.3516\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-16.6516\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-20.3516C85.1153,-20.3516 99.5214,-20.3516 111.67,-20.3516\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-20.3516 111.892,-23.5017 115.392,-20.3516 111.892,-20.3517 111.892,-20.3517 111.892,-20.3517 115.392,-20.3516 111.892,-17.2017 118.892,-20.3516 118.892,-20.3516\"/>\n",
        "<text text-anchor=\"start\" x=\"93\" y=\"-24.1516\" font-family=\"Lato\" font-size=\"14.00\">a</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=\"M122.524,-9.39411C114.011,-3.78441 102.645,1.35158 92,-1.35158 87.1374,-2.58634 82.2193,-4.64763 77.668,-6.96768\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"71.3113,-10.4859 75.9105,-4.34007 74.3736,-8.79098 77.4359,-7.09611 77.4359,-7.09611 77.4359,-7.09611 74.3736,-8.79098 78.9613,-9.85216 71.3113,-10.4859 71.3113,-10.4859\"/>\n",
        "<text text-anchor=\"middle\" x=\"96.5\" y=\"-5.15158\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1c8045a660> >"
       ]
      },
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "False\n"
       ]
      }
     ],
     "prompt_number": 10
    },
    {
     "cell_type": "heading",
     "level": 2,
     "metadata": {},
     "source": [
      "Explaining why a formula is not sutter-invariant"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "As explained in our [Spin'15 paper](https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf) the sutter-invariant checks are implemented using simple operators suchs as `spot.closure(aut)`, that augment the language of L by adding words that can be obtained by removing duplicated letters, and `spot.sl(aut)` or `spot.sl2(aut)` that both augment the language that L by adding words that can be obtained by duplicating letters.  The default `is_stutter_invariant()` function is implemented as `spot.product(spot.closure(aut), spot.closure(neg_aut)).is_empty()`, but that is just one possible implementation selected because it was more efficient.\n",
      "\n",
      "Using these bricks, we can modify the original algorithm so it uses a counterexample to explain why a formula is stutter-sensitive."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "def explain_stut(f):\n",
      "    f = spot.formula(f)\n",
      "    pos = spot.translate(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",
      "        return\n",
      "    word.simplify()\n",
      "    waut = word.as_automaton()\n",
      "    if waut.intersects(pos):\n",
      "        acc, rej, aut = \"accepted\", \"rejected\", neg\n",
      "    else:\n",
      "        acc, rej, aut = \"rejected\", \"accepted\", pos\n",
      "    word2 = spot.sl2(waut).intersecting_word(aut)\n",
      "    word2.simplify()\n",
      "    print(\"\"\"{} is {} by {}\n",
      "  but if we stutter some of its letters, we get\n",
      "{} which is {} by {}\"\"\".format(word, acc, f, word2, rej, f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 25
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "explain_stut('GF(a & Xb)')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "cycle{!a & !b; a & b} is rejected by GF(a & Xb)\n",
        "  but if we stutter some of its letters, we get\n",
        "cycle{!a & !b; a & b; a & b} which is accepted by GF(a & Xb)\n"
       ]
      }
     ],
     "prompt_number": 26
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "## Detecting stutter-invariant states\n",
      "\n",
      "Even if the language of an automaton is not sutter invariant, some of its states may recognize a stutter-invariant language.  (We assume the language of a state is the language the automaton would have when starting from this state.)"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "### First example\n",
      "\n",
      "For instance let us build a disjunction of a stutter-invariant formula and a stutter-sensitive one:"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "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",
      "\n",
      "print(spot.is_stutter_invariant(f1))\n",
      "print(spot.is_stutter_invariant(f2))\n",
      "print(spot.is_stutter_invariant(f))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "True\n",
        "False\n",
        "False\n"
       ]
      }
     ],
     "prompt_number": 13
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "pos = spot.translate(f)\n",
      "display(pos)"
     ],
     "language": "python",
     "metadata": {},
     "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=\"518pt\" height=\"230pt\"\n",
        " viewBox=\"0.00 0.00 518.00 230.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 226)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-226 514,-226 514,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"234\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"256\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"272\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"232\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-78\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-74.3\" 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,-78C2.79388,-78 17.1543,-78 30.6317,-78\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-78 30.9419,-81.1501 34.4419,-78 30.9419,-78.0001 30.9419,-78.0001 30.9419,-78.0001 34.4419,-78 30.9418,-74.8501 37.9419,-78 37.9419,-78\"/>\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,-95.0373C48.3189,-104.858 50.4453,-114 56,-114 60.166,-114 62.4036,-108.858 62.7128,-102.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-95.0373 65.8541,-101.882 62.5434,-98.5335 62.7076,-102.03 62.7076,-102.03 62.7076,-102.03 62.5434,-98.5335 59.561,-102.177 62.3792,-95.0373 62.3792,-95.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"51.5\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"165\" cy=\"-103\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"160.5\" y=\"-99.3\" 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=\"M73.7188,-81.9062C91.6218,-86.0892 120.176,-92.7606 140.371,-97.4793\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"147.399,-99.1212 139.866,-100.596 143.99,-98.3248 140.582,-97.5285 140.582,-97.5285 140.582,-97.5285 143.99,-98.3248 141.299,-94.4611 147.399,-99.1212 147.399,-99.1212\"/>\n",
        "<text text-anchor=\"start\" x=\"107\" y=\"-98.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"165\" cy=\"-49\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"165\" y=\"-45.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M73.7153,-73.1495C79.4994,-71.4909 86.0282,-69.6409 92,-68 108.136,-63.5664 126.361,-58.7589 140.438,-55.0891\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"147.388,-53.2817 141.406,-58.0921 144.001,-54.1626 140.613,-55.0435 140.613,-55.0435 140.613,-55.0435 144.001,-54.1626 139.82,-51.9949 147.388,-53.2817 147.388,-53.2817\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"274\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"274\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M183.191,-103.321C200.897,-103.652 228.648,-104.171 248.616,-104.544\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.851,-104.679 248.794,-107.698 252.352,-104.614 248.852,-104.549 248.852,-104.549 248.852,-104.549 252.352,-104.614 248.911,-101.399 255.851,-104.679 255.851,-104.679\"/>\n",
        "<text text-anchor=\"start\" x=\"214\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g id=\"node6\" class=\"node\"><title>5</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"274\" cy=\"-48\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"274\" y=\"-44.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M183.191,-48.8393C200.897,-48.6739 228.648,-48.4145 248.616,-48.2279\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.851,-48.1603 248.881,-51.3756 252.351,-48.193 248.852,-48.2258 248.852,-48.2258 248.852,-48.2258 252.351,-48.193 248.822,-45.0759 255.851,-48.1603 255.851,-48.1603\"/>\n",
        "<text text-anchor=\"start\" x=\"201\" y=\"-52.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M264.767,-120.541C262.169,-130.909 265.246,-141 274,-141 280.702,-141 284.077,-135.085 284.124,-127.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"283.233,-120.541 287.229,-127.095 283.668,-124.014 284.103,-127.487 284.103,-127.487 284.103,-127.487 283.668,-124.014 280.977,-127.879 283.233,-120.541 283.233,-120.541\"/>\n",
        "<text text-anchor=\"start\" x=\"269.5\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node7\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"383\" cy=\"-120\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"383\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M292.191,-107.41C309.975,-109.903 337.892,-113.817 357.88,-116.619\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"364.851,-117.596 357.482,-119.744 361.385,-117.11 357.919,-116.624 357.919,-116.624 357.919,-116.624 361.385,-117.11 358.356,-113.505 364.851,-117.596 364.851,-117.596\"/>\n",
        "<text text-anchor=\"start\" x=\"311.5\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 6 -->\n",
        "<g id=\"node9\" class=\"node\"><title>6</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"383\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"383\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;6 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>5&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M291.719,-43.3125C309.7,-38.2709 338.426,-30.2169 358.637,-24.5505\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"365.399,-22.6546 359.509,-27.5774 362.029,-23.5995 358.659,-24.5444 358.659,-24.5444 358.659,-24.5444 362.029,-23.5995 357.808,-21.5114 365.399,-22.6546 365.399,-22.6546\"/>\n",
        "<text text-anchor=\"start\" x=\"310\" y=\"-41.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 7 -->\n",
        "<g id=\"node8\" class=\"node\"><title>7</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"492\" cy=\"-120\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"492\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;7 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M401.191,-120C418.897,-120 446.648,-120 466.616,-120\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"473.851,-120 466.851,-123.15 470.351,-120 466.851,-120 466.851,-120 466.851,-120 470.351,-120 466.851,-116.85 473.851,-120 473.851,-120\"/>\n",
        "<text text-anchor=\"start\" x=\"419\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 7&#45;&gt;7 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>7&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M482.767,-135.541C480.169,-145.909 483.246,-156 492,-156 498.702,-156 502.077,-150.085 502.124,-142.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"501.233,-135.541 505.229,-142.095 501.668,-139.014 502.103,-142.487 502.103,-142.487 502.103,-142.487 501.668,-139.014 498.977,-142.879 501.233,-135.541 501.233,-135.541\"/>\n",
        "<text text-anchor=\"start\" x=\"488.5\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"484\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M373.767,-33.5414C371.169,-43.9087 374.246,-54 383,-54 389.702,-54 393.077,-48.0847 393.124,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"392.233,-33.5414 396.229,-40.0955 392.668,-37.0143 393.103,-40.4871 393.103,-40.4871 393.103,-40.4871 392.668,-37.0143 389.977,-40.8788 392.233,-33.5414 392.233,-33.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"376.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "<text text-anchor=\"start\" x=\"375\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\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 0x7f1c803f4de0> >"
       ]
      }
     ],
     "prompt_number": 14
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "While the automaton as a whole is stutter-sensitive, we can see that eventually we will enter a sub-automaton that is stutter-invariant.\n",
      "\n",
      "The `stutter_invariant_states()` function returns a Boolean vector indiced by the state number.  A state is marked as `True` if either its language is stutter-invariant, or if it appear below a stutter-invariant state (see the second example later).  As always, the second argument, `f`, can be omitted (pass `None`) if the formula is unknown, or it can be replaced by a negated automaton if it is known. "
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.stutter_invariant_states(pos, f)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 15,
       "text": [
        "(False, True, False, True, True, True, True, True)"
       ]
      }
     ],
     "prompt_number": 15
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "For convenience, the `highligh_...()` version colors the stutter-invariant states of the automaton for display.\n",
      "(That 5 is the color number for red in Spot's hard-coded palette.)"
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.highlight_stutter_invariant_states(pos, f, 5)\n",
      "display(pos)"
     ],
     "language": "python",
     "metadata": {},
     "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=\"518pt\" height=\"230pt\"\n",
        " viewBox=\"0.00 0.00 518.00 230.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 226)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-226 514,-226 514,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"234\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"256\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"272\" y=\"-207.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"232\" y=\"-193.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-78\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-74.3\" 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,-78C2.79388,-78 17.1543,-78 30.6317,-78\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-78 30.9419,-81.1501 34.4419,-78 30.9419,-78.0001 30.9419,-78.0001 30.9419,-78.0001 34.4419,-78 30.9418,-74.8501 37.9419,-78 37.9419,-78\"/>\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,-95.0373C48.3189,-104.858 50.4453,-114 56,-114 60.166,-114 62.4036,-108.858 62.7128,-102.143\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-95.0373 65.8541,-101.882 62.5434,-98.5335 62.7076,-102.03 62.7076,-102.03 62.7076,-102.03 62.5434,-98.5335 59.561,-102.177 62.3792,-95.0373 62.3792,-95.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"51.5\" y=\"-117.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"165\" cy=\"-103\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"160.5\" y=\"-99.3\" 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=\"M73.7188,-81.9062C91.6218,-86.0892 120.176,-92.7606 140.371,-97.4793\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"147.399,-99.1212 139.866,-100.596 143.99,-98.3248 140.582,-97.5285 140.582,-97.5285 140.582,-97.5285 143.99,-98.3248 141.299,-94.4611 147.399,-99.1212 147.399,-99.1212\"/>\n",
        "<text text-anchor=\"start\" x=\"107\" y=\"-98.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"165\" cy=\"-49\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"165\" y=\"-45.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M73.7153,-73.1495C79.4994,-71.4909 86.0282,-69.6409 92,-68 108.136,-63.5664 126.361,-58.7589 140.438,-55.0891\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"147.388,-53.2817 141.406,-58.0921 144.001,-54.1626 140.613,-55.0435 140.613,-55.0435 140.613,-55.0435 144.001,-54.1626 139.82,-51.9949 147.388,-53.2817 147.388,-53.2817\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"274\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"274\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M183.191,-103.321C200.897,-103.652 228.648,-104.171 248.616,-104.544\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.851,-104.679 248.794,-107.698 252.352,-104.614 248.852,-104.549 248.852,-104.549 248.852,-104.549 252.352,-104.614 248.911,-101.399 255.851,-104.679 255.851,-104.679\"/>\n",
        "<text text-anchor=\"start\" x=\"214\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g id=\"node6\" class=\"node\"><title>5</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"274\" cy=\"-48\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"274\" y=\"-44.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M183.191,-48.8393C200.897,-48.6739 228.648,-48.4145 248.616,-48.2279\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.851,-48.1603 248.881,-51.3756 252.351,-48.193 248.852,-48.2258 248.852,-48.2258 248.852,-48.2258 252.351,-48.193 248.822,-45.0759 255.851,-48.1603 255.851,-48.1603\"/>\n",
        "<text text-anchor=\"start\" x=\"201\" y=\"-52.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M264.767,-120.541C262.169,-130.909 265.246,-141 274,-141 280.702,-141 284.077,-135.085 284.124,-127.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"283.233,-120.541 287.229,-127.095 283.668,-124.014 284.103,-127.487 284.103,-127.487 284.103,-127.487 283.668,-124.014 280.977,-127.879 283.233,-120.541 283.233,-120.541\"/>\n",
        "<text text-anchor=\"start\" x=\"269.5\" y=\"-144.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node7\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"383\" cy=\"-120\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"383\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M292.191,-107.41C309.975,-109.903 337.892,-113.817 357.88,-116.619\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"364.851,-117.596 357.482,-119.744 361.385,-117.11 357.919,-116.624 357.919,-116.624 357.919,-116.624 361.385,-117.11 358.356,-113.505 364.851,-117.596 364.851,-117.596\"/>\n",
        "<text text-anchor=\"start\" x=\"311.5\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 6 -->\n",
        "<g id=\"node9\" class=\"node\"><title>6</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"383\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"383\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;6 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>5&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M291.719,-43.3125C309.7,-38.2709 338.426,-30.2169 358.637,-24.5505\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"365.399,-22.6546 359.509,-27.5774 362.029,-23.5995 358.659,-24.5444 358.659,-24.5444 358.659,-24.5444 362.029,-23.5995 357.808,-21.5114 365.399,-22.6546 365.399,-22.6546\"/>\n",
        "<text text-anchor=\"start\" x=\"310\" y=\"-41.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 7 -->\n",
        "<g id=\"node8\" class=\"node\"><title>7</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"492\" cy=\"-120\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"492\" y=\"-116.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;7 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>4&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M401.191,-120C418.897,-120 446.648,-120 466.616,-120\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"473.851,-120 466.851,-123.15 470.351,-120 466.851,-120 466.851,-120 466.851,-120 470.351,-120 466.851,-116.85 473.851,-120 473.851,-120\"/>\n",
        "<text text-anchor=\"start\" x=\"419\" y=\"-123.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 7&#45;&gt;7 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>7&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M482.767,-135.541C480.169,-145.909 483.246,-156 492,-156 498.702,-156 502.077,-150.085 502.124,-142.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"501.233,-135.541 505.229,-142.095 501.668,-139.014 502.103,-142.487 502.103,-142.487 502.103,-142.487 501.668,-139.014 498.977,-142.879 501.233,-135.541 501.233,-135.541\"/>\n",
        "<text text-anchor=\"start\" x=\"488.5\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"484\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 6&#45;&gt;6 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>6&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M373.767,-33.5414C371.169,-43.9087 374.246,-54 383,-54 389.702,-54 393.077,-48.0847 393.124,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"392.233,-33.5414 396.229,-40.0955 392.668,-37.0143 393.103,-40.4871 393.103,-40.4871 393.103,-40.4871 392.668,-37.0143 389.977,-40.8788 392.233,-33.5414 392.233,-33.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"376.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!b</text>\n",
        "<text text-anchor=\"start\" x=\"375\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\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 0x7f1c803f4de0> >"
       ]
      }
     ],
     "prompt_number": 16
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Such a procedure gives us map of where POR can be enabled when model checking using such an automaton."
     ]
    },
    {
     "cell_type": "heading",
     "level": 3,
     "metadata": {},
     "source": [
      "Second example"
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "This second example illustrates the fact that a state can be marked if it it not sutter-invariant but appear below a stutter-invariant state.  We build our example automaton as the disjuction of the following two stutter-sensitive formulas, whose union is equivalent to the sutter-invariant formula `GF!a`."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "g1 = spot.formula('GF(a & Xa) & GF!a')\n",
      "g2 = spot.formula('!GF(a & Xa) & GF!a')\n",
      "g = spot.formula_Or([g1, g2])"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 17
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "print(spot.is_stutter_invariant(g1))\n",
      "print(spot.is_stutter_invariant(g2))\n",
      "print(spot.is_stutter_invariant(g))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "output_type": "stream",
       "stream": "stdout",
       "text": [
        "False\n",
        "False\n",
        "True\n"
       ]
      }
     ],
     "prompt_number": 18
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Here are the automata for `g1` and `g2`, note that none of the states are stutter-invariant."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut1 = spot.translate(g1)\n",
      "aut1.set_name(str(g1))\n",
      "spot.highlight_stutter_invariant_states(aut1, g1, 5)\n",
      "display(aut1)\n",
      "\n",
      "aut2 = spot.translate(g2)\n",
      "aut2.set_name(str(g2))\n",
      "spot.highlight_stutter_invariant_states(aut2, g2, 5)\n",
      "display(aut2)"
     ],
     "language": "python",
     "metadata": {},
     "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=\"170pt\" height=\"178pt\"\n",
        " viewBox=\"0.00 0.00 170.00 177.75\" 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 173.75)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-173.75 166,-173.75 166,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"25\" y=\"-155.55\" font-family=\"Lato\" font-size=\"14.00\">G(F(a &amp; Xa) &amp; F!a)</text>\n",
        "<text text-anchor=\"start\" x=\"34\" y=\"-141.55\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"56\" y=\"-141.55\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"72\" y=\"-141.55\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"108\" y=\"-141.55\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"124\" y=\"-141.55\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"37\" y=\"-127.55\" font-family=\"Lato\" font-size=\"14.00\">[gen. B\u00fcchi 2]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-20.7502\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-17.0502\" 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,-20.7502C2.79388,-20.7502 17.1543,-20.7502 30.6317,-20.7502\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-20.7502 30.9419,-23.9003 34.4419,-20.7502 30.9419,-20.7503 30.9419,-20.7503 30.9419,-20.7503 34.4419,-20.7502 30.9418,-17.6003 37.9419,-20.7502 37.9419,-20.7502\"/>\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=\"M52.7643,-38.5319C52.2144,-48.0651 53.293,-56.7502 56,-56.7502 57.988,-56.7502 59.0977,-52.0663 59.3292,-45.8023\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"59.2357,-38.5319 62.4756,-45.4908 59.2808,-42.0316 59.3258,-45.5313 59.3258,-45.5313 59.3258,-45.5313 59.2808,-42.0316 56.1761,-45.5719 59.2357,-38.5319 59.2357,-38.5319\"/>\n",
        "<text text-anchor=\"start\" x=\"50.5\" y=\"-75.5502\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"48\" y=\"-60.5502\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M50.9906,-38.3273C47.5451,-59.4682 49.2148,-86.7502 56,-86.7502 62.043,-86.7502 64.0285,-65.1097 61.9564,-45.4408\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"61.0094,-38.3273 65.0556,-44.8504 61.4713,-41.7967 61.9332,-45.2661 61.9332,-45.2661 61.9332,-45.2661 61.4713,-41.7967 58.8107,-45.6818 61.0094,-38.3273 61.0094,-38.3273\"/>\n",
        "<text text-anchor=\"start\" x=\"52.5\" y=\"-90.5502\" 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=\"-20.7502\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"144\" y=\"-17.0502\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.4034,-20.7502C87.1928,-20.7502 104.732,-20.7502 118.874,-20.7502\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"125.916,-20.7502 118.916,-23.9003 122.416,-20.7502 118.916,-20.7503 118.916,-20.7503 118.916,-20.7503 122.416,-20.7502 118.916,-17.6003 125.916,-20.7502 125.916,-20.7502\"/>\n",
        "<text text-anchor=\"start\" x=\"96.5\" y=\"-39.5502\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-24.5502\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M128.689,-10.8844C122.598,-7.25669 115.237,-3.58794 108,-1.75016 101.108,-0 98.8924,-0 92,-1.75016 87.1374,-2.98492 82.2193,-5.0462 77.668,-7.36626\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"71.3113,-10.8844 75.9105,-4.73864 74.3736,-9.18956 77.4359,-7.49469 77.4359,-7.49469 77.4359,-7.49469 74.3736,-9.18956 78.9613,-10.2507 71.3113,-10.8844 71.3113,-10.8844\"/>\n",
        "<text text-anchor=\"start\" x=\"96.5\" y=\"-5.55016\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M136.332,-37.0404C134.483,-47.1393 137.039,-56.7502 144,-56.7502 149.221,-56.7502 151.964,-51.3441 152.229,-44.3805\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"151.668,-37.0404 155.342,-43.7801 151.935,-40.5303 152.201,-44.0201 152.201,-44.0201 152.201,-44.0201 151.935,-40.5303 149.06,-44.2601 151.668,-37.0404 151.668,-37.0404\"/>\n",
        "<text text-anchor=\"start\" x=\"140.5\" y=\"-75.5502\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"136\" y=\"-60.5502\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\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 0x7f1c80480540> >"
       ]
      },
      {
       "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=\"253pt\" height=\"172pt\"\n",
        " viewBox=\"0.00 0.00 253.00 172.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 168)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-168 249,-168 249,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"88.5\" y=\"-149.8\" font-family=\"Lato\" font-size=\"14.00\">FG(!a | X!a)</text>\n",
        "<text text-anchor=\"start\" x=\"101.5\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"123.5\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"139.5\" y=\"-135.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"99.5\" y=\"-121.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</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\">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,-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",
        "<!-- 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,-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=\"start\" x=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"139\" cy=\"-48\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"134.5\" y=\"-44.3\" 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=\"M73.003,-23.927C85.017,-28.3767 101.638,-34.5325 115.064,-39.5053\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"121.753,-41.9826 114.095,-42.5052 118.471,-40.767 115.189,-39.5513 115.189,-39.5513 115.189,-39.5513 118.471,-40.767 116.283,-36.5974 121.753,-41.9826 121.753,-41.9826\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"227\" cy=\"-30\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"227\" y=\"-26.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M73.3505,-13.1706C93.2093,-7.96467 127.69,-1.04806 157,-6 173.081,-8.71684 190.415,-14.7595 203.687,-20.1014\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"210.229,-22.8097 202.557,-23.0425 206.995,-21.4709 203.762,-20.1321 203.762,-20.1321 203.762,-20.1321 206.995,-21.4709 204.966,-17.2216 210.229,-22.8097 210.229,-22.8097\"/>\n",
        "<text text-anchor=\"start\" x=\"135.5\" y=\"-9.8\" font-family=\"Lato\" font-size=\"14.00\">a</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=\"M131.969,-64.6641C130.406,-74.625 132.75,-84 139,-84 143.688,-84 146.178,-78.7266 146.471,-71.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"146.031,-64.6641 149.601,-71.4598 146.244,-68.1576 146.456,-71.6511 146.456,-71.6511 146.456,-71.6511 146.244,-68.1576 143.312,-71.8425 146.031,-64.6641 146.031,-64.6641\"/>\n",
        "<text text-anchor=\"start\" x=\"133.5\" y=\"-102.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"131\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M155.003,-56.5894C165.311,-61.3438 179.21,-65.4707 191,-61 197.945,-58.3667 204.396,-53.6555 209.82,-48.6883\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"214.881,-43.7031 212.105,-50.8594 212.388,-46.1591 209.894,-48.6152 209.894,-48.6152 209.894,-48.6152 212.388,-46.1591 207.684,-46.3709 214.881,-43.7031 214.881,-43.7031\"/>\n",
        "<text text-anchor=\"start\" x=\"179.5\" y=\"-80.8\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"175\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M209.173,-26.2984C199.09,-24.7439 186.112,-23.9222 175,-27 169.835,-28.4305 164.668,-30.8484 159.95,-33.5456\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"153.837,-37.33 158.131,-30.967 156.813,-35.4876 159.789,-33.6452 159.789,-33.6452 159.789,-33.6452 156.813,-35.4876 161.447,-36.3235 153.837,-37.33 153.837,-37.33\"/>\n",
        "<text text-anchor=\"start\" x=\"177.5\" y=\"-45.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"175\" y=\"-30.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\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 0x7f1c8045a6c0> >"
       ]
      }
     ],
     "prompt_number": 19
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Now we build the sum of these to automata.  The stutter-invariance check detects that the initial state is stutter-invariant (i.e., the entire language is stutter-invariant) so all states below it are marked despite the fact that the language recognized from these individual states would not be stutter-invariant."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut = spot.sum(aut1, aut2)\n",
      "# At this point it is unknown if AUT is stutter-invariant\n",
      "assert(aut.prop_stutter_invariant().is_maybe())\n",
      "spot.highlight_stutter_invariant_states(aut, g, 5)\n",
      "display(aut)\n",
      "# The stutter_invariant property is set on AUT as a side effect\n",
      "# of calling sutter_invariant_states() or any variant of it.\n",
      "assert(aut.prop_stutter_invariant().is_true())"
     ],
     "language": "python",
     "metadata": {},
     "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=\"339pt\" height=\"348pt\"\n",
        " viewBox=\"0.00 0.00 339.00 348.13\" 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 344.135)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-344.135 335,-344.135 335,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"89\" y=\"-325.935\" font-family=\"Lato\" font-size=\"14.00\">(Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"114\" y=\"-325.935\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"130\" y=\"-325.935\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"166\" y=\"-325.935\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"182\" y=\"-325.935\" font-family=\"Lato\" font-size=\"14.00\">)) | Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"222\" y=\"-325.935\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">\u2777</text>\n",
        "<text text-anchor=\"start\" x=\"238\" y=\"-325.935\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<!-- I -->\n",
        "<!-- 5 -->\n",
        "<g id=\"node2\" class=\"node\"><title>5</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"56\" cy=\"-80.1347\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-76.4347\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;5 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-80.1347C2.79388,-80.1347 17.1543,-80.1347 30.6317,-80.1347\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-80.1347 30.9419,-83.2848 34.4419,-80.1348 30.9419,-80.1348 30.9419,-80.1348 30.9419,-80.1348 34.4419,-80.1348 30.9418,-76.9848 37.9419,-80.1347 37.9419,-80.1347\"/>\n",
        "</g>\n",
        "<!-- 0 -->\n",
        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"137\" cy=\"-218.135\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-214.435\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;0 -->\n",
        "<g id=\"edge16\" class=\"edge\"><title>5&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M60.142,-97.8716C64.552,-119.133 74.1191,-155.143 92,-181.135 98.1307,-190.046 106.956,-198.044 115.096,-204.304\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"121.131,-208.738 113.625,-207.132 118.311,-206.666 115.49,-204.593 115.49,-204.593 115.49,-204.593 118.311,-206.666 117.356,-202.055 121.131,-208.738 121.131,-208.738\"/>\n",
        "<text text-anchor=\"middle\" x=\"96.5\" y=\"-193.935\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node4\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"225\" cy=\"-200.135\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"225\" y=\"-196.435\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;1 -->\n",
        "<g id=\"edge14\" class=\"edge\"><title>5&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M68.9809,-93.5334C80.8933,-106.399 100.075,-125.924 119,-140.135 145.779,-160.243 179.948,-178.586 201.904,-189.557\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"208.304,-192.719 200.633,-192.442 205.166,-191.169 202.028,-189.618 202.028,-189.618 202.028,-189.618 205.166,-191.169 203.423,-186.794 208.304,-192.719 208.304,-192.719\"/>\n",
        "<text text-anchor=\"start\" x=\"133.5\" y=\"-166.935\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node5\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"137\" cy=\"-80.1347\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-76.4347\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;2 -->\n",
        "<g id=\"edge17\" class=\"edge\"><title>5&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M74.1418,-80.1347C85.1153,-80.1347 99.5214,-80.1347 111.67,-80.1347\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"118.892,-80.1347 111.892,-83.2848 115.392,-80.1348 111.892,-80.1348 111.892,-80.1348 111.892,-80.1348 115.392,-80.1348 111.892,-76.9848 118.892,-80.1347 118.892,-80.1347\"/>\n",
        "<text text-anchor=\"middle\" x=\"96.5\" y=\"-83.9347\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node6\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"225\" cy=\"-29.1347\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"225\" y=\"-25.4347\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;3 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>5&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M70.1607,-68.239C82.0078,-58.3029 100.373,-44.7335 119,-38.1347 145.38,-28.7895 177.723,-27.3989 199.484,-27.7934\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"206.713,-27.9973 199.627,-30.9486 203.215,-27.8986 199.716,-27.7999 199.716,-27.7999 199.716,-27.7999 203.215,-27.8986 199.805,-24.6511 206.713,-27.9973 206.713,-27.9973\"/>\n",
        "<text text-anchor=\"start\" x=\"131.5\" y=\"-41.9347\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node7\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"313\" cy=\"-48.1347\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"313\" y=\"-44.4347\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;4 -->\n",
        "<g id=\"edge15\" class=\"edge\"><title>5&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M68.1907,-66.2828C74.6999,-58.6833 83.3143,-49.3648 92,-42.1347 133.591,-7.51392 153.092,-6.85489 207,-2.13474 238.606,0.632674 250.214,0.869389 277,-16.1347 283.36,-20.1723 289.645,-25.4116 295.096,-30.4779\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"300.241,-35.4355 293.014,-32.8465 297.72,-33.0069 295.2,-30.5783 295.2,-30.5783 295.2,-30.5783 297.72,-33.0069 297.386,-28.31 300.241,-35.4355 300.241,-35.4355\"/>\n",
        "<text text-anchor=\"start\" x=\"177.5\" y=\"-8.93474\" 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=\"M133.405,-235.916C132.794,-245.45 133.992,-254.135 137,-254.135 139.209,-254.135 140.442,-249.451 140.699,-243.187\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"140.595,-235.916 143.845,-242.871 140.645,-239.416 140.695,-242.916 140.695,-242.916 140.695,-242.916 140.645,-239.416 137.546,-242.961 140.595,-235.916 140.595,-235.916\"/>\n",
        "<text text-anchor=\"start\" x=\"131.5\" y=\"-272.935\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"129\" y=\"-257.935\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M131.494,-235.384C127.587,-256.569 129.422,-284.135 137,-284.135 143.749,-284.135 145.943,-262.269 143.582,-242.52\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"142.506,-235.384 146.665,-241.836 143.028,-238.845 143.55,-242.306 143.55,-242.306 143.55,-242.306 143.028,-238.845 140.435,-242.775 142.506,-235.384 142.506,-235.384\"/>\n",
        "<text text-anchor=\"start\" x=\"133.5\" y=\"-287.935\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M152.796,-209.188C158.84,-206.01 166.038,-202.808 173,-201.135 181.525,-199.086 191.083,-198.472 199.601,-198.49\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"206.766,-198.648 199.698,-201.643 203.267,-198.571 199.768,-198.493 199.768,-198.493 199.768,-198.493 203.267,-198.571 199.837,-195.344 206.766,-198.648 206.766,-198.648\"/>\n",
        "<text text-anchor=\"start\" x=\"177.5\" y=\"-219.935\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"173\" y=\"-204.935\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M212.881,-213.838C206.643,-220.419 198.26,-227.624 189,-231.135 179.605,-234.697 168.87,-232.8 159.681,-229.477\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"153.003,-226.724 160.675,-226.48 156.239,-228.058 159.475,-229.392 159.475,-229.392 159.475,-229.392 156.239,-228.058 158.274,-232.304 153.003,-226.724 153.003,-226.724\"/>\n",
        "<text text-anchor=\"start\" x=\"177.5\" y=\"-235.935\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M217.332,-216.425C215.483,-226.524 218.039,-236.135 225,-236.135 230.221,-236.135 232.964,-230.729 233.229,-223.765\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"232.668,-216.425 236.342,-223.165 232.935,-219.915 233.201,-223.405 233.201,-223.405 233.201,-223.405 232.935,-219.915 230.06,-223.645 232.668,-216.425 232.668,-216.425\"/>\n",
        "<text text-anchor=\"start\" x=\"221.5\" y=\"-254.935\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"217\" y=\"-239.935\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M129.969,-96.7988C128.406,-106.76 130.75,-116.135 137,-116.135 141.688,-116.135 144.178,-110.861 144.471,-104.022\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"144.031,-96.7988 147.601,-103.595 144.244,-100.292 144.456,-103.786 144.456,-103.786 144.456,-103.786 144.244,-100.292 141.312,-103.977 144.031,-96.7988 144.031,-96.7988\"/>\n",
        "<text text-anchor=\"middle\" x=\"137\" y=\"-119.935\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M152.98,-71.2512C166.792,-63.0606 187.435,-50.8189 202.91,-41.6413\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"209.192,-37.9165 204.777,-44.1965 206.181,-39.7017 203.171,-41.487 203.171,-41.487 203.171,-41.487 206.181,-39.7017 201.564,-38.7776 209.192,-37.9165 209.192,-37.9165\"/>\n",
        "<text text-anchor=\"start\" x=\"175.5\" y=\"-62.9347\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M153.267,-87.8495C173.671,-97.1907 210.98,-110.884 243,-104.135 259.161,-100.728 263.751,-98.9961 277,-89.1347 284.625,-83.4596 291.709,-75.8342 297.48,-68.6994\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"302.003,-62.8751 300.198,-70.3359 299.856,-65.6395 297.71,-68.4039 297.71,-68.4039 297.71,-68.4039 299.856,-65.6395 295.222,-66.4719 302.003,-62.8751 302.003,-62.8751\"/>\n",
        "<text text-anchor=\"start\" x=\"221.5\" y=\"-108.935\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M217.332,-45.425C215.483,-55.5239 218.039,-65.1347 225,-65.1347 230.221,-65.1347 232.964,-59.7286 233.229,-52.7651\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"232.668,-45.425 236.342,-52.1647 232.935,-48.9148 233.201,-52.4047 233.201,-52.4047 233.201,-52.4047 232.935,-48.9148 230.06,-52.6447 232.668,-45.425 232.668,-45.425\"/>\n",
        "<text text-anchor=\"start\" x=\"219.5\" y=\"-83.9347\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"217\" y=\"-68.9347\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">\u2777</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M242.417,-23.7475C252.584,-21.2508 265.793,-19.5434 277,-23.1347 282.929,-25.0347 288.708,-28.3489 293.807,-31.9545\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"299.447,-36.2538 291.971,-34.5156 296.664,-34.1321 293.88,-32.0104 293.88,-32.0104 293.88,-32.0104 296.664,-34.1321 295.79,-29.5051 299.447,-36.2538 299.447,-36.2538\"/>\n",
        "<text text-anchor=\"start\" x=\"265.5\" y=\"-41.9347\" font-family=\"Lato\" font-size=\"14.00\">a</text>\n",
        "<text text-anchor=\"start\" x=\"261\" y=\"-26.9347\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">\u2777</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>4&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M295.59,-52.9645C285.426,-55.1732 272.217,-56.6112 261,-53.1347 255.359,-51.3865 249.819,-48.3801 244.87,-45.0748\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"238.954,-40.8006 246.473,-42.3468 241.791,-42.8503 244.628,-44.9001 244.628,-44.9001 244.628,-44.9001 241.791,-42.8503 242.784,-47.4534 238.954,-40.8006 238.954,-40.8006\"/>\n",
        "<text text-anchor=\"start\" x=\"263.5\" y=\"-73.9347\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "<text text-anchor=\"start\" x=\"261\" y=\"-58.9347\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">\u2777</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 0x7f1c80480660> >"
       ]
      }
     ],
     "prompt_number": 20
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "### Third example\n",
      "\n",
      "These procedures work regardless of the acceptance condition.  Here is an example with state-based co-B\u00fcchi acceptance.\n",
      "\n",
      "In this case we do not even have a formula to pass as second argument, so the check will perform a costly complementation by determinization."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut = spot.automaton('genaut --ks-nca=2 |')\n",
      "spot.highlight_stutter_invariant_states(aut, None, 5, True)\n",
      "display(aut)"
     ],
     "language": "python",
     "metadata": {},
     "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=\"602pt\" height=\"253pt\"\n",
        " viewBox=\"0.00 0.00 601.74 253.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 249)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-249 597.74,-249 597.74,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"274.37\" y=\"-230.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
        "<text text-anchor=\"start\" x=\"299.37\" y=\"-230.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"315.37\" y=\"-230.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"264.37\" y=\"-216.8\" font-family=\"Lato\" font-size=\"14.00\">[co&#45;B\u00fcchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"64.8701\" cy=\"-105\" rx=\"26.7407\" ry=\"26.7407\"/>\n",
        "<text text-anchor=\"start\" x=\"60.3701\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
        "<text text-anchor=\"start\" x=\"56.8701\" y=\"-93.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</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.04557,-105C1.94668,-105 16.0699,-105 30.6965,-105\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.8616,-105 30.8617,-108.15 34.3616,-105 30.8616,-105 30.8616,-105 30.8616,-105 34.3616,-105 30.8616,-101.85 37.8616,-105 37.8616,-105\"/>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"186.74\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"186.74\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M87.0245,-89.6464C109.264,-73.5052 143.988,-48.3029 165.771,-32.493\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"171.551,-28.2982 167.736,-34.9592 168.719,-30.354 165.886,-32.4099 165.886,-32.4099 165.886,-32.4099 168.719,-30.354 164.036,-29.8606 171.551,-28.2982 171.551,-28.2982\"/>\n",
        "<text text-anchor=\"middle\" x=\"130.24\" y=\"-74.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"357.74\" cy=\"-69\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"357.74\" y=\"-65.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M91.9203,-106.884C138.901,-109.495 240.49,-111.526 321.74,-88 326.559,-86.6047 331.458,-84.4738 336.005,-82.1365\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"342.364,-78.6261 337.758,-84.7669 339.3,-80.3177 336.236,-82.0093 336.236,-82.0093 336.236,-82.0093 339.3,-80.3177 334.713,-79.2516 342.364,-78.6261 342.364,-78.6261\"/>\n",
        "<text text-anchor=\"middle\" x=\"186.74\" y=\"-111.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"466.74\" cy=\"-103\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"466.74\" y=\"-99.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M89.6166,-115.618C96.0337,-118.094 103.055,-120.455 109.74,-122 135.381,-127.926 142.454,-125.734 168.74,-127 260.638,-131.425 284.644,-141.895 375.74,-129 399.197,-125.68 425.098,-117.72 443.068,-111.476\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"449.781,-109.095 444.237,-114.404 446.482,-110.265 443.183,-111.435 443.183,-111.435 443.183,-111.435 446.482,-110.265 442.13,-108.466 449.781,-109.095 449.781,-109.095\"/>\n",
        "<text text-anchor=\"middle\" x=\"272.24\" y=\"-138.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"575.74\" cy=\"-103\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"575.74\" y=\"-99.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>0&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M81.0053,-126.544C101.471,-152.884 140.64,-194 185.74,-194 185.74,-194 185.74,-194 467.74,-194 510.409,-194 544.736,-151.489 562.192,-124.578\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"566.06,-118.437 564.994,-126.039 564.195,-121.398 562.329,-124.36 562.329,-124.36 562.329,-124.36 564.195,-121.398 559.664,-122.681 566.06,-118.437 566.06,-118.437\"/>\n",
        "<text text-anchor=\"middle\" x=\"357.74\" y=\"-197.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;0 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M168.873,-14.9899C152.427,-12.9911 127.382,-12.527 109.74,-24 92.6966,-35.0838 81.762,-55.1336 75.072,-72.5116\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"72.6279,-79.2636 72.0486,-71.6093 73.8192,-75.9725 75.0106,-72.6815 75.0106,-72.6815 75.0106,-72.6815 73.8192,-75.9725 77.9725,-73.7537 72.6279,-79.2636 72.6279,-79.2636\"/>\n",
        "<text text-anchor=\"start\" x=\"109.74\" y=\"-27.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M177.166,-33.5414C174.47,-43.9087 177.662,-54 186.74,-54 193.691,-54 197.19,-48.0847 197.24,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"196.315,-33.5414 200.341,-40.0771 196.766,-37.0123 197.217,-40.4831 197.217,-40.4831 197.217,-40.4831 196.766,-37.0123 194.093,-40.889 196.315,-33.5414 196.315,-33.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"169.74\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M199.002,-31.6019C205.281,-38.2463 213.655,-45.7148 222.74,-50 258.287,-66.7677 304.592,-69.7349 332.418,-69.7776\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"339.753,-69.7211 332.777,-72.925 336.253,-69.7481 332.753,-69.7751 332.753,-69.7751 332.753,-69.7751 336.253,-69.7481 332.729,-66.6252 339.753,-69.7211 339.753,-69.7211\"/>\n",
        "<text text-anchor=\"start\" x=\"222.74\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">(!a &amp; b) | (a &amp; !b)</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;1 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M347.237,-54.2193C341.042,-45.9111 332.18,-36.193 321.74,-31 286.585,-13.5128 239.867,-13.3781 211.899,-15.3524\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"204.872,-15.9213 211.595,-12.2166 208.361,-15.6388 211.849,-15.3563 211.849,-15.3563 211.849,-15.3563 208.361,-15.6388 212.104,-18.4961 204.872,-15.9213 204.872,-15.9213\"/>\n",
        "<text text-anchor=\"start\" x=\"253.74\" y=\"-34.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge10\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M348.507,-84.5414C345.909,-94.9087 348.986,-105 357.74,-105 364.442,-105 367.817,-99.0847 367.865,-91.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"366.973,-84.5414 370.969,-91.0955 367.408,-88.0143 367.843,-91.4871 367.843,-91.4871 367.843,-91.4871 367.408,-88.0143 364.718,-91.8788 366.973,-84.5414 366.973,-84.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"308.24\" y=\"-108.8\" font-family=\"Lato\" font-size=\"14.00\">(!a &amp; !b) | (a &amp; b)</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge11\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M374.991,-74.1639C392.981,-79.8803 422.127,-89.1416 442.52,-95.6218\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"449.336,-97.7875 441.711,-98.6697 446.001,-96.7276 442.665,-95.6676 442.665,-95.6676 442.665,-95.6676 446.001,-96.7276 443.619,-92.6655 449.336,-97.7875 449.336,-97.7875\"/>\n",
        "<text text-anchor=\"start\" x=\"393.74\" y=\"-94.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g id=\"edge12\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M457.507,-118.541C454.909,-128.909 457.986,-139 466.74,-139 473.442,-139 476.817,-133.085 476.865,-125.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"475.973,-118.541 479.969,-125.095 476.408,-122.014 476.843,-125.487 476.843,-125.487 476.843,-125.487 476.408,-122.014 473.718,-125.879 475.973,-118.541 475.973,-118.541\"/>\n",
        "<text text-anchor=\"start\" x=\"451.24\" y=\"-142.8\" font-family=\"Lato\" font-size=\"14.00\">!a | b</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge13\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M484.932,-103C502.637,-103 530.388,-103 550.356,-103\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"557.591,-103 550.591,-106.15 554.091,-103 550.591,-103 550.591,-103 550.591,-103 554.091,-103 550.591,-99.8501 557.591,-103 557.591,-103\"/>\n",
        "<text text-anchor=\"start\" x=\"502.74\" y=\"-106.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;1 -->\n",
        "<g id=\"edge14\" class=\"edge\"><title>4&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M559.244,-95.5387C520.4,-77.3013 415.284,-30.8042 321.74,-15 283.779,-8.58658 238.917,-11.7158 211.929,-14.732\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"204.811,-15.5717 211.394,-11.6232 208.287,-15.1616 211.763,-14.7515 211.763,-14.7515 211.763,-14.7515 208.287,-15.1616 212.132,-17.8798 204.811,-15.5717 204.811,-15.5717\"/>\n",
        "<text text-anchor=\"start\" x=\"393.74\" y=\"-45.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge15\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M566.507,-118.541C563.909,-128.909 566.986,-139 575.74,-139 582.442,-139 585.817,-133.085 585.865,-125.659\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"584.973,-118.541 588.969,-125.095 585.408,-122.014 585.843,-125.487 585.843,-125.487 585.843,-125.487 585.408,-122.014 582.718,-125.879 584.973,-118.541 584.973,-118.541\"/>\n",
        "<text text-anchor=\"start\" x=\"560.24\" y=\"-142.8\" font-family=\"Lato\" font-size=\"14.00\">!a | b</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 0x7f1c80370300> >"
       ]
      }
     ],
     "prompt_number": 27
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "If the negated automaton is already known, it can be passed as second argument (instead of the positive formula) to avoid unnecessary work."
     ]
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "## Global vs Local stuttering (experimental)\n",
      "\n",
      "Do not build anything on top of what follows, as it is likely to be removed."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "h = spot.formula('F(a & X(!a & X(b & Xb)))')\n",
      "aut = spot.translate(h)\n",
      "spot.highlight_stutter_invariant_states(aut, h, 5)\n",
      "display(aut)"
     ],
     "language": "python",
     "metadata": {},
     "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=\"406pt\" height=\"128pt\"\n",
        " viewBox=\"0.00 0.00 406.00 128.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 124)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-124 402,-124 402,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"178\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"200\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"216\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"176\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</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\">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,-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",
        "<!-- 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,-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=\"start\" x=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"130.5\" y=\"-14.3\" 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.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",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M153.178,-18C164.669,-18 179.959,-18 192.693,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"199.847,-18 192.847,-21.1501 196.347,-18 192.847,-18.0001 192.847,-18.0001 192.847,-18.0001 196.347,-18 192.847,-14.8501 199.847,-18 199.847,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"171\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"299\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"299\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M236.142,-18C247.115,-18 261.521,-18 273.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"280.892,-18 273.892,-21.1501 277.392,-18 273.892,-18.0001 273.892,-18.0001 273.892,-18.0001 277.392,-18 273.892,-14.8501 280.892,-18 280.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"254\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"380\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"380\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M317.142,-18C328.115,-18 342.521,-18 354.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"361.892,-18 354.892,-21.1501 358.392,-18 354.892,-18.0001 354.892,-18.0001 354.892,-18.0001 358.392,-18 354.892,-14.8501 361.892,-18 361.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"335\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M372.969,-34.6641C371.406,-44.625 373.75,-54 380,-54 384.688,-54 387.178,-48.7266 387.471,-41.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"387.031,-34.6641 390.601,-41.4598 387.244,-38.1576 387.456,-41.6511 387.456,-41.6511 387.456,-41.6511 387.244,-38.1576 384.312,-41.8425 387.031,-34.6641 387.031,-34.6641\"/>\n",
        "<text text-anchor=\"start\" x=\"375.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"372\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\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 0x7f1c8045a690> >"
       ]
      }
     ],
     "prompt_number": 22
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "The above result uses a natural definition of \"stutter-invariant state\": a state is stutter-invariant if the language accepted from this state is.\n",
      "\n",
      "We can also have a \"local\" variant of the stutter invariance check that considers the state as stutter invariant if you can stutter on (or remove duplicates of) the first letter read from that state, but not necessary do the same operations on a different letter that follows.  \n",
      "In other words, state $q$ is a local stutter-invariant state iff $\\ell_1\\ell_2\\ldots \\in L(q) \\iff \\ell_1\\ell_1\\ell_2\\ldots \\in L(q)$.\n",
      "\n",
      "Just pass `True` as the last optional parameter, as below."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "spot.highlight_stutter_invariant_states(aut, h, 5, True)\n",
      "display(aut)"
     ],
     "language": "python",
     "metadata": {},
     "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=\"406pt\" height=\"128pt\"\n",
        " viewBox=\"0.00 0.00 406.00 128.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 124)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-124 402,-124 402,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"178\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"200\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"216\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"176\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">[B\u00fcchi]</text>\n",
        "<!-- I -->\n",
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" 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\">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,-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",
        "<!-- 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,-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=\"start\" x=\"51.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"135\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"130.5\" y=\"-14.3\" 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.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",
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M153.178,-18C164.669,-18 179.959,-18 192.693,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"199.847,-18 192.847,-21.1501 196.347,-18 192.847,-18.0001 192.847,-18.0001 192.847,-18.0001 196.347,-18 192.847,-14.8501 199.847,-18 199.847,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"171\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">!a</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"299\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"299\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;3 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>2&#45;&gt;3</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M236.142,-18C247.115,-18 261.521,-18 273.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"280.892,-18 273.892,-21.1501 277.392,-18 273.892,-18.0001 273.892,-18.0001 273.892,-18.0001 277.392,-18 273.892,-14.8501 280.892,-18 280.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"254\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node6\" class=\"node\"><title>4</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"#e31a1c\" stroke-width=\"2\" cx=\"380\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"380\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>3&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M317.142,-18C328.115,-18 342.521,-18 354.67,-18\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"361.892,-18 354.892,-21.1501 358.392,-18 354.892,-18.0001 354.892,-18.0001 354.892,-18.0001 358.392,-18 354.892,-14.8501 361.892,-18 361.892,-18\"/>\n",
        "<text text-anchor=\"start\" x=\"335\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>4&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M372.969,-34.6641C371.406,-44.625 373.75,-54 380,-54 384.688,-54 387.178,-48.7266 387.471,-41.8876\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"387.031,-34.6641 390.601,-41.4598 387.244,-38.1576 387.456,-41.6511 387.456,-41.6511 387.456,-41.6511 387.244,-38.1576 384.312,-41.8425 387.031,-34.6641 387.031,-34.6641\"/>\n",
        "<text text-anchor=\"start\" x=\"375.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
        "<text text-anchor=\"start\" x=\"372\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\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 0x7f1c8045a690> >"
       ]
      }
     ],
     "prompt_number": 23
    },
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "Note that an SCC can contain a mix of locally stutter-invariant and local stutter-sensitive states.  Here is the deterministic version of the above automaton for example."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "aut = spot.translate(h, 'deterministic')\n",
      "spot.highlight_stutter_invariant_states(aut, h, 5, True)\n",
      "display(aut.show('.abs'))"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "display_data",
       "svg": [
        "<svg height=\"234pt\" viewBox=\"0.00 0.00 507.74 234.00\" width=\"508pt\" 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 230)\">\n",
        "<title>G</title>\n",
        "<polygon fill=\"white\" points=\"-4,4 -4,-230 503.74,-230 503.74,4 -4,4\" stroke=\"none\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"228.87\" y=\"-211.8\">Inf(</text>\n",
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"250.87\" y=\"-211.8\">\u24ff</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"266.87\" y=\"-211.8\">)</text>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"226.87\" y=\"-197.8\">[B\u00fcchi]</text>\n",
        "<g class=\"cluster\" id=\"clust1\"><title>cluster_0</title>\n",
        "<polygon fill=\"none\" points=\"422,-64 422,-167 491.74,-167 491.74,-64 422,-64\" stroke=\"green\"/>\n",
        "</g>\n",
        "<g class=\"cluster\" id=\"clust2\"><title>cluster_1</title>\n",
        "<polygon fill=\"none\" points=\"30,-8 30,-182 393,-182 393,-8 30,-8\" stroke=\"red\"/>\n",
        "</g>\n",
        "<!-- I -->\n",
        "<!-- 3 -->\n",
        "<g class=\"node\" id=\"node2\"><title>3</title>\n",
        "<ellipse cx=\"56\" cy=\"-87\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#e31a1c\" stroke-width=\"2\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"56\" y=\"-83.3\">3</text>\n",
        "</g>\n",
        "<!-- I&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge1\"><title>I-&gt;3</title>\n",
        "<path d=\"M1.15491,-87C2.79388,-87 17.1543,-87 30.6317,-87\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"37.9419,-87 30.9419,-90.1501 34.4419,-87 30.9419,-87.0001 30.9419,-87.0001 30.9419,-87.0001 34.4419,-87 30.9418,-83.8501 37.9419,-87 37.9419,-87\" stroke=\"black\"/>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge12\"><title>3-&gt;3</title>\n",
        "<path d=\"M49.6208,-104.037C48.3189,-113.858 50.4453,-123 56,-123 60.166,-123 62.4036,-117.858 62.7128,-111.143\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"62.3792,-104.037 65.8541,-110.882 62.5434,-107.533 62.7076,-111.03 62.7076,-111.03 62.7076,-111.03 62.5434,-107.533 59.561,-111.177 62.3792,-104.037 62.3792,-104.037\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"50.5\" y=\"-126.8\">!a</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g class=\"node\" id=\"node4\"><title>4</title>\n",
        "<ellipse cx=\"137.5\" cy=\"-87\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"137.5\" y=\"-83.3\">4</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge13\"><title>3-&gt;4</title>\n",
        "<path d=\"M74.2503,-87C85.2932,-87 99.7905,-87 112.016,-87\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"119.283,-87 112.283,-90.1501 115.783,-87 112.283,-87.0001 112.283,-87.0001 112.283,-87.0001 115.783,-87 112.283,-83.8501 119.283,-87 119.283,-87\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"92\" y=\"-90.8\">a</text>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g class=\"node\" id=\"node3\"><title>5</title>\n",
        "<ellipse cx=\"456.87\" cy=\"-99\" fill=\"#ffffaa\" rx=\"26.7407\" ry=\"26.7407\" stroke=\"#e31a1c\" stroke-width=\"2\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"452.37\" y=\"-102.8\">5</text>\n",
        "<text fill=\"#1f78b4\" font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"448.87\" y=\"-87.8\">\u24ff</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge16\"><title>5-&gt;5</title>\n",
        "<path d=\"M447.949,-124.37C447.334,-134.924 450.308,-143.87 456.87,-143.87 461.894,-143.87 464.815,-138.626 465.632,-131.431\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"465.791,-124.37 468.783,-131.439 465.712,-127.869 465.633,-131.368 465.633,-131.368 465.633,-131.368 465.712,-127.869 462.484,-131.297 465.791,-124.37 465.791,-124.37\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"456.87\" y=\"-147.67\">1</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge15\"><title>4-&gt;4</title>\n",
        "<path d=\"M130.117,-103.664C128.477,-113.625 130.938,-123 137.5,-123 142.422,-123 145.037,-117.727 145.344,-110.888\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"144.883,-103.664 148.473,-110.449 145.106,-107.157 145.329,-110.65 145.329,-110.65 145.329,-110.65 145.106,-107.157 142.186,-110.851 144.883,-103.664 144.883,-103.664\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"134\" y=\"-126.8\">a</text>\n",
        "</g>\n",
        "<!-- 0 -->\n",
        "<g class=\"node\" id=\"node5\"><title>0</title>\n",
        "<ellipse cx=\"253.5\" cy=\"-85\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"253.5\" y=\"-81.3\">0</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge14\"><title>4-&gt;0</title>\n",
        "<path d=\"M155.655,-87.2775C171.561,-87.469 195.884,-87.5943 217,-87 220.685,-86.8963 224.583,-86.7321 228.393,-86.5414\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"235.534,-86.1506 228.717,-89.6784 232.04,-86.3419 228.545,-86.5331 228.545,-86.5331 228.545,-86.5331 232.04,-86.3419 228.373,-83.3878 235.534,-86.1506 235.534,-86.1506\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"191\" y=\"-91.8\">!a</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge4\"><title>0-&gt;3</title>\n",
        "<path d=\"M238.207,-75.0981C213.44,-59.2074 160.979,-31.1368 117,-45 101.303,-49.948 86.1407,-60.6296 74.985,-69.9818\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"69.5349,-74.7139 72.7554,-67.746 72.1778,-72.4192 74.8206,-70.1246 74.8206,-70.1246 74.8206,-70.1246 72.1778,-72.4192 76.8858,-72.5031 69.5349,-74.7139 69.5349,-74.7139\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"117\" y=\"-48.8\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge5\"><title>0-&gt;4</title>\n",
        "<path d=\"M236.925,-77.9539C230.84,-75.5609 223.721,-73.1919 217,-72 199.058,-68.8181 193.893,-68.554 176,-72 170.888,-72.9846 165.586,-74.6598 160.635,-76.5423\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"154.153,-79.1924 159.44,-73.6279 157.392,-77.868 160.632,-76.5437 160.632,-76.5437 160.632,-76.5437 157.392,-77.868 161.824,-79.4595 154.153,-79.1924 154.153,-79.1924\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"178\" y=\"-75.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g class=\"node\" id=\"node6\"><title>1</title>\n",
        "<ellipse cx=\"367\" cy=\"-138\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"#e31a1c\" stroke-width=\"2\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"367\" y=\"-134.3\">1</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
        "<g class=\"edge\" id=\"edge2\"><title>0-&gt;1</title>\n",
        "<path d=\"M270.004,-92.3694C289.2,-101.494 322.03,-117.099 343.87,-127.481\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"350.269,-130.522 342.594,-130.362 347.108,-129.02 343.946,-127.517 343.946,-127.517 343.946,-127.517 347.108,-129.02 345.299,-124.672 350.269,-130.522 350.269,-130.522\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"292\" y=\"-124.8\">!a &amp; b</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g class=\"node\" id=\"node7\"><title>2</title>\n",
        "<ellipse cx=\"367\" cy=\"-59\" fill=\"#ffffaa\" rx=\"18\" ry=\"18\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"middle\" x=\"367\" y=\"-55.3\">2</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;2 -->\n",
        "<g class=\"edge\" id=\"edge3\"><title>0-&gt;2</title>\n",
        "<path d=\"M265.421,-71.1933C271.766,-64.313 280.395,-56.6899 290,-53 306.776,-46.555 327.136,-48.6347 342.56,-52.0093\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"349.697,-53.7383 342.152,-55.1516 346.295,-52.9142 342.894,-52.0902 342.894,-52.0902 342.894,-52.0902 346.295,-52.9142 343.635,-49.0287 349.697,-53.7383 349.697,-53.7383\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"293.5\" y=\"-56.8\">a &amp; b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
        "<g class=\"edge\" id=\"edge6\"><title>1-&gt;3</title>\n",
        "<path d=\"M349.563,-143.472C308.171,-156.255 197.224,-184.276 117,-147 98.1796,-138.255 81.9033,-120.965 71.0704,-107.183\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"66.7694,-101.527 73.5137,-105.192 68.8878,-104.313 71.0062,-107.099 71.0062,-107.099 71.0062,-107.099 68.8878,-104.313 68.4987,-109.005 66.7694,-101.527 66.7694,-101.527\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"176\" y=\"-168.8\">!a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge8\"><title>1-&gt;5</title>\n",
        "<path d=\"M383.709,-131.028C395.248,-125.906 411.292,-118.786 425.322,-112.559\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"432.019,-109.586 426.899,-115.305 428.82,-111.006 425.621,-112.426 425.621,-112.426 425.621,-112.426 428.82,-111.006 424.343,-109.547 432.019,-109.586 432.019,-109.586\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"403\" y=\"-125.8\">b</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge7\"><title>1-&gt;4</title>\n",
        "<path d=\"M349.004,-140.059C333.54,-141.551 310.125,-142.854 290,-140 237.776,-132.593 224.868,-126.852 176,-107 170.617,-104.813 164.997,-102.079 159.795,-99.3416\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"153.48,-95.913 161.135,-96.4845 156.556,-97.5829 159.632,-99.2528 159.632,-99.2528 159.632,-99.2528 156.556,-97.5829 158.129,-102.021 153.48,-95.913 153.48,-95.913\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-141.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
        "<g class=\"edge\" id=\"edge11\"><title>2-&gt;5</title>\n",
        "<path d=\"M383.709,-66.1512C395.248,-71.4039 411.292,-78.7072 425.322,-85.0938\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"432.019,-88.1425 424.343,-88.1092 428.833,-86.6923 425.648,-85.2422 425.648,-85.2422 425.648,-85.2422 428.833,-86.6923 426.953,-82.3753 432.019,-88.1425 432.019,-88.1425\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"403\" y=\"-82.8\">b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
        "<g class=\"edge\" id=\"edge10\"><title>2-&gt;4</title>\n",
        "<path d=\"M350.333,-51.3873C344.416,-48.8747 337.533,-46.3732 331,-45 327.069,-44.1736 248.501,-40.4615 235,-43 207.441,-48.1818 178.519,-62.7706 159.61,-73.7398\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"153.117,-77.5932 157.529,-71.3116 156.127,-75.8068 159.137,-74.0204 159.137,-74.0204 159.137,-74.0204 156.127,-75.8068 160.744,-76.7293 153.117,-77.5932 153.117,-77.5932\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"235\" y=\"-46.8\">a &amp; !b</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;0 -->\n",
        "<g class=\"edge\" id=\"edge9\"><title>2-&gt;0</title>\n",
        "<path d=\"M349.293,-63.4158C343.51,-64.9126 336.979,-66.5673 331,-68 313.376,-72.2229 293.381,-76.6538 278.254,-79.9329\" fill=\"none\" stroke=\"black\"/>\n",
        "<polygon fill=\"black\" points=\"271.251,-81.4442 277.429,-76.8884 274.672,-80.7059 278.093,-79.9675 278.093,-79.9675 278.093,-79.9675 274.672,-80.7059 278.758,-83.0467 271.251,-81.4442 271.251,-81.4442\" stroke=\"black\"/>\n",
        "<text font-family=\"Lato\" font-size=\"14.00\" text-anchor=\"start\" x=\"290\" y=\"-81.8\">!a &amp; !b</text>\n",
        "</g>\n",
        "</g>\n",
        "</svg>"
       ],
       "text": [
        "<IPython.core.display.SVG object>"
       ]
      }
     ],
     "prompt_number": 24
    }
   ],
   "metadata": {}
  }
 ]
}