{
"metadata": {
"name": "",
"signature": "sha256:89d455537d395ae2842b209c6c14a262e15747fd501a731df0cd235f8c95011f"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import os\n",
"from IPython.display import display, HTML\n",
"# Note that Spot (loaded by the kernel) will store a copy of\n",
"# the environment variables the first time it reads them, so\n",
"# if you change those variables, the new values will be ignored\n",
"# until you restart the kernel.\n",
"os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n",
"os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
"import spot"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To translate a formula into a Testing Automaton\n",
"\n",
"Start by building a Buchi automaton"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f = spot.formula('a U Gb')\n",
"a = f.translate('ba')\n",
"a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f1eb80416f0> >"
]
}
],
"prompt_number": 2
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Then, gather all the atomic proposition in the formula, and create an automaton with changesets"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"propset = spot.atomic_prop_collect_as_bdd(f, a)\n",
"ta = spot.tgba_to_ta(a, propset, True, True, False, False, True)\n",
"ta.show('.A')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 3
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Then, remove dead states, and remove stuttering transitions (i.e., transitions labeled by `{}`), marking as *livelock accepting* (rectangles) any states from which there exists a an accepting path labeled by `{}`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"ta = spot.tgba_to_ta(a, propset, True, True, False, False, False)\n",
"ta.show('.A')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally, use bisimulation to minimize the number of states."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.minimize_ta(ta).show('.A')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 5,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [],
"language": "python",
"metadata": {},
"outputs": []
}
],
"metadata": {}
}
]
}