{
"metadata": {
"name": "",
"signature": "sha256:261c16336ba5deefb7e9ebe705cc5c24f1cbba8622030874d2719f5045289c53"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import spot\n",
"spot.setup()"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's build a small automaton to use as example."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"aut = spot.translate('G(Fa <-> Xb)'); aut"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7fa33c302870> >"
]
}
],
"prompt_number": 2
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The call to `couvreur99()` just instanciate the emptiness check, but does not run the check. Calling `check()` will return `None` if no accepting run was found. Otherwise the presence of the accepting run is established, but an accepting run hasn't necessarily been calculated: calling `accepting_run()` on the result will cause this computation to happen.\n",
"\n",
"\n",
"In the example below, we do not check the result of `check()` because we know that the input formula is satisfiable, so the automaton has an accepting run."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"run = spot.couvreur99(aut).check().accepting_run(); run"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"text": [
"Prefix:\n",
" 0\n",
" | !a\n",
"Cycle:\n",
" 1\n",
" | a & b\t{0}\n",
" 2\n",
" | !a & b"
]
}
],
"prompt_number": 3
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Accessing the contents of the run can be done via the `prefix` and `cycle` lists."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.bdd_format_formula(aut.get_dict(), run.prefix[0].label))\n",
"print(run.cycle[0].acc)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"!a\n",
"{0}\n"
]
}
],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To convert the run into a word, using `spot.twa_word()`. Note that our runs are labeled by Boolean formulas that are not necessarily a conjunction of all involved litterals. The word is just the projection of the run on its labels."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"word = spot.twa_word(run); word"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 5,
"text": [
"!a; cycle{a & b; !a & b}"
]
}
],
"prompt_number": 5
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Accessing the different formulas (stored as BDDs) can be done again via the `prefix` and `cycle` lists."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))\n",
"print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))\n",
"print(spot.bdd_format_formula(aut.get_dict(), word.cycle[1]))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"!a\n",
"a & b\n",
"!a & b\n"
]
}
],
"prompt_number": 6
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the initial `!a` is compatible with both `a & b` and `!a & b`. The word obtained by restricting `!a` to `!a & b` is therefore still accepted, but it allows removing the prefix by rotating the cycle:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"word.simplify()\n",
"word"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 7,
"text": [
"cycle{!a & b; a & b}"
]
}
],
"prompt_number": 7
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Words can be created using the `parse_word` function:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.parse_word('a; b; cycle{a&b}'))\n",
"print(spot.parse_word('cycle{a&bb|bac&(aaa|bbb)}'))\n",
"print(spot.parse_word('a; b;b; qiwuei;\"a;b&c;a\" ;cycle{a}'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"a; b; cycle{a & b}\n",
"cycle{(a & bb) | (aaa & bac) | (bac & bbb)}\n",
"a; b; b; qiwuei; \"a;b&c;a\"; cycle{a}\n"
]
}
],
"prompt_number": 8
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"# make sure that we can parse a word back after it has been printed\n",
"spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b}')))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 9,
"text": [
"a; a & b; cycle{!a & !b}"
]
}
],
"prompt_number": 9
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Words can be easily converted as automata"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"w1 = spot.parse_word('a; !a; cycle{a; !a; a}')"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 10
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"w1.as_automaton()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 11,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7fa33c3028d0> >"
]
}
],
"prompt_number": 11
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Test some syntax errors"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.parse_word('a; b&!a; b'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"ename": "SyntaxError",
"evalue": "\n>>> a; b&!a; b\n ^\nA twa_word must contain a cycle\n ()",
"output_type": "pyerr",
"traceback": [
"\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; b&!a; b\n ^\nA twa_word must contain a cycle\n\n"
]
}
],
"prompt_number": 12
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.parse_word('a; b; c}'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"ename": "SyntaxError",
"evalue": "\n>>> a; b; c}\n ^\nExpected ';' delimiter: '}' stands for ending a cycle\n ()",
"output_type": "pyerr",
"traceback": [
"\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; b; c}\n ^\nExpected ';' delimiter: '}' stands for ending a cycle\n\n"
]
}
],
"prompt_number": 13
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.parse_word('a; cycle{}'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"ename": "SyntaxError",
"evalue": "\n>>> a; cycle{}\n ^\nempty input\n\n ()",
"output_type": "pyerr",
"traceback": [
"\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; cycle{}\n ^\nempty input\n\n\n"
]
}
],
"prompt_number": 14
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"print(spot.parse_word('a; cycle{!a}; a'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"ename": "SyntaxError",
"evalue": "\n>>> a; cycle{!a}; a\n ^\nInput should be finished after cycle\n ()",
"output_type": "pyerr",
"traceback": [
"\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; cycle{!a}; a\n ^\nInput should be finished after cycle\n\n"
]
}
],
"prompt_number": 15
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"# Creating an empty word is OK...\n",
"w = spot.twa_word(spot._bdd_dict)"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 16
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"# ... as long as this word is not printed.\n",
"print(w)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"ename": "RuntimeError",
"evalue": "a twa_word may not have an empty cycle",
"output_type": "pyerr",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m\n\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)",
"\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 3511\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3512\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 3513\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 3514\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3515\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;31mRuntimeError\u001b[0m: a twa_word may not have an empty cycle"
]
}
],
"prompt_number": 17
}
],
"metadata": {}
}
]
}