{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import spot\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's build a small automaton to use as example."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7ff774426a50> >"
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut = spot.translate('!a & G(Fa <-> XXb)'); aut"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Build an accepting run:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Prefix:\n",
" 0\n",
" | !a\n",
" 1\n",
" | a\n",
"Cycle:\n",
" 2\n",
" | a & b\t{0}"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"run = aut.accepting_run(); run"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Accessing the contents of the run can be done via the `prefix` and `cycle` lists."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"!a\n",
"{0}\n"
]
}
],
"source": [
"print(spot.bdd_format_formula(aut.get_dict(), run.prefix[0].label))\n",
"print(run.cycle[0].acc)"
]
},
{
"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",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"!a; a; cycle{a & b}"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"word = spot.twa_word(run); word"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"A word can be represented as a collection of signals (one for each atomic proposition). The cycle part is shown twice."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"word.show()"
]
},
{
"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",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"!a\n",
"a\n",
"a & b\n"
]
}
],
"source": [
"print(spot.bdd_format_formula(aut.get_dict(), word.prefix[0]))\n",
"print(spot.bdd_format_formula(aut.get_dict(), word.prefix[1]))\n",
"print(spot.bdd_format_formula(aut.get_dict(), word.cycle[0]))"
]
},
{
"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, allowing us to remove the prefix."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"!a; cycle{a & b}"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"word.simplify()\n",
"word"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Such a simplified word can be created directly from the automaton:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"!a; cycle{a & b}"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"aut.accepting_word()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Words can be created using the `parse_word` function:"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"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"
]
}
],
"source": [
"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}'))"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"a; a & b; cycle{!a & !b; !a & b}"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# make sure that we can parse a word back after it has been printed\n",
"w = spot.parse_word(str(spot.parse_word('a;b&a;cycle{!a&!b;!a&b}'))); w"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"w.show()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Words can be easily converted as automata"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text/plain": [
" *' at 0x7ff77439aae0> >"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"w.as_automaton()"
]
}
],
"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.4"
}
},
"nbformat": 4,
"nbformat_minor": 2
}