{
"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.4.3+"
},
"name": ""
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"from IPython.display import display\n",
"import spot\n",
"spot.setup()"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 1
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To build an automaton, simply call `translate()` with a formula, and a list of options to characterize the automaton you want (those options have the same name as the long options name of the `ltl2tgba` tool, and they can be abbreviated)."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.translate('(a U b) & GFc & GFd', 'BA', 'complete'); a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 2,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c25174540> >"
]
}
],
"prompt_number": 2
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The call the `spot.setup()` in the first cells has installed a default style for the graphviz output. If you want to change this style temporarily, you can call the `show(style)` method explicitely. For instance here is a vertical layout with the default font of GraphViz."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a.show(\"v\")"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 3
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If you want to add some style options to the existing one, pass a dot to the `show()` function in addition to your own style options:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a.show(\".ast\")"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 4,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 4
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The `translate()` function can also be called with a formula object. Either as a function, or as a method."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f = spot.formula('a U b'); f"
],
"language": "python",
"metadata": {},
"outputs": [
{
"latex": [
"$a \\mathbin{\\mathsf{U}} b$"
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 5,
"text": [
"a U b"
]
}
],
"prompt_number": 5
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.translate(f)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 6,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515b810> >"
]
}
],
"prompt_number": 6
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 7,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515b690> >"
]
}
],
"prompt_number": 7
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"When used as a method, all the arguments are translation options. Here is a monitor:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate('mon')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 8,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515b6f0> >"
]
}
],
"prompt_number": 8
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The following three cells show a formulas for which it makes a difference to select `'small'` or `'deterministic'`."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f = spot.formula('Ga | Gb | Gc'); f"
],
"language": "python",
"metadata": {},
"outputs": [
{
"latex": [
"$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$"
],
"metadata": {},
"output_type": "pyout",
"prompt_number": 9,
"text": [
"Ga | Gb | Gc"
]
}
],
"prompt_number": 9
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate('ba', 'small').show('v')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 10,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 10
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"f.translate('ba', 'det').show('v.')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 11,
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 11
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Here is how to build an unambiguous automaton:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.translate('GFa -> GFb', 'unambig')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 12,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515be10> >"
]
}
],
"prompt_number": 12
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Compare with the standard translation:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.translate('GFa -> GFb')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 13,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515bed0> >"
]
}
],
"prompt_number": 13
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"And here is the automaton above with state-based acceptance:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.translate('GFa -> GFb', 'sbacc')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 14,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515b630> >"
]
}
],
"prompt_number": 14
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Some example of running the self-loopization algorithm on an automaton:"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.translate('F(a & X(!a &Xb))', \"any\"); a"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 15,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515b6c0> >"
]
}
],
"prompt_number": 15
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.sl(a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 16,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515b450> >"
]
}
],
"prompt_number": 16
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a.is_empty()"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 17,
"text": [
"False"
]
}
],
"prompt_number": 17
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Reading from file (see `automaton-io.ipynb` for more examples)."
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"%%file example1.aut\n",
"HOA: v1\n",
"States: 3\n",
"Start: 0\n",
"AP: 2 \"a\" \"b\"\n",
"acc-name: Buchi\n",
"Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(1)\n",
"--BODY--\n",
"State: 0 {3}\n",
"[t] 0\n",
"[0] 1 {1}\n",
"[!0] 2 {0}\n",
"State: 1 {3}\n",
"[1] 0\n",
"[0&1] 1 {0}\n",
"[!0&1] 2 {2}\n",
"State: 2\n",
"[!1] 0\n",
"[0&!1] 1 {0}\n",
"[!0&!1] 2 {0}\n",
"--END--"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"Writing example1.aut\n"
]
}
],
"prompt_number": 18
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a = spot.automaton('example1.aut')\n",
"display(a.show('.a'))\n",
"display(spot.remove_fin(a).show('.a'))\n",
"display(a.postprocess('TGBA', 'complete').show('.a'))\n",
"display(a.postprocess('BA'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c2515b840> >"
]
}
],
"prompt_number": 19
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"!rm example1.aut"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 20
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.complete(a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 21,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c250f61e0> >"
]
}
],
"prompt_number": 21
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.complete(spot.translate('Ga'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 22,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f3c250f6150> >"
]
}
],
"prompt_number": 22
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"# Using +1 in the display options is a convient way to shift the \n",
"# set numbers in the output, as an aid in reading the product.\n",
"a1 = spot.translate('a W c'); display(a1.show('.bat'))\n",
"a2 = spot.translate('a U b'); display(a2.show('.bat+1'))\n",
"# the product should display pairs of states, unless asked not to (using 1).\n",
"p = spot.product(a1, a2); display(p.show('.bat')); display(p.show('.bat1'))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
""
],
"text": [
""
]
}
],
"prompt_number": 23
},
{
"cell_type": "code",
"collapsed": true,
"input": [],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": null
}
],
"metadata": {}
}
]
}