{
"metadata": {
"name": "",
"signature": "sha256:87a09325e40a5df4abe3f3cdf6cdaf097b1673b1acd1a5dff28332d1c9775a38"
},
"nbformat": 3,
"nbformat_minor": 0,
"worksheets": [
{
"cells": [
{
"cell_type": "code",
"collapsed": false,
"input": [
"import os\n",
"from IPython.display import display\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": "code",
"collapsed": false,
"input": [
"a = spot.translate('a U b')\n",
"for fmt in ('hoa', 'spin', 'dot', 'lbtt'):\n",
" print(a.to_str(fmt))"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"HOA: v1\n",
"States: 2\n",
"Start: 1\n",
"AP: 2 \"a\" \"b\"\n",
"acc-name: Buchi\n",
"Acceptance: 1 Inf(0)\n",
"properties: trans-labels explicit-labels state-acc deterministic\n",
"properties: stutter-invariant inherently-weak\n",
"--BODY--\n",
"State: 0 {0}\n",
"[t] 0\n",
"State: 1\n",
"[1] 0\n",
"[0&!1] 1\n",
"--END--\n",
"never {\n",
"T0_init:\n",
" if\n",
" :: ((b)) -> goto accept_all\n",
" :: ((a) && (!(b))) -> goto T0_init\n",
" fi;\n",
"accept_all:\n",
" skip\n",
"}\n",
"\n",
"digraph G {\n",
" rankdir=LR\n",
" node [shape=\"circle\"]\n",
" fontname=\"Lato\"\n",
" node [fontname=\"Lato\"]\n",
" edge [fontname=\"Lato\"]\n",
" size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]\n",
" I [label=\"\", style=invis, width=0]\n",
" I -> 1\n",
" 0 [label=<0
\u24ff>]\n",
" 0 -> 0 [label=<1>]\n",
" 1 [label=<1>]\n",
" 1 -> 0 [label=]\n",
" 1 -> 1 [label=]\n",
"}\n",
"\n",
"2 1t\n",
"0 1\n",
"1 -1 \"b\"\n",
"0 -1 & \"a\" ! \"b\"\n",
"-1\n",
"1 0\n",
"1 0 -1 t\n",
"-1\n",
"\n"
]
}
],
"prompt_number": 2
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"a.save('example.aut').save('example.aut', format='lbtt', append=True)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "pyout",
"prompt_number": 3,
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f48240566f0> >"
]
}
],
"prompt_number": 3
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"!cat example.aut"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"HOA: v1\r\n",
"States: 2\r\n",
"Start: 1\r\n",
"AP: 2 \"a\" \"b\"\r\n",
"acc-name: Buchi\r\n",
"Acceptance: 1 Inf(0)\r\n",
"properties: trans-labels explicit-labels state-acc deterministic\r\n",
"properties: stutter-invariant inherently-weak\r\n",
"--BODY--\r\n",
"State: 0 {0}\r\n",
"[t] 0\r\n",
"State: 1\r\n",
"[1] 0\r\n",
"[0&!1] 1\r\n",
"--END--\r\n",
"2 1t\r\n",
"0 1\r\n",
"1 -1 \"b\"\r\n",
"0 -1 & \"a\" ! \"b\"\r\n",
"-1\r\n",
"1 0\r\n",
"1 0 -1 t\r\n",
"-1\r\n"
]
}
],
"prompt_number": 4
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"for a in spot.automata('example.aut'):\n",
" display(a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f4824056960> >"
]
},
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f4824056990> >"
]
}
],
"prompt_number": 5
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Test `--ABORT--`\n",
"----------------"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"%%file example.aut\n",
"HOA: v1\n",
"States: 2\n",
"Start: 1\n",
"AP: 2 \"a\" \"b\"\n",
"acc-name: Buchi\n",
"Acceptance: 1 Inf(0)\n",
"--BODY--\n",
"State: 0 {0}\n",
"[t] 0\n",
"--ABORT-- /* the previous automaton should be ignored */\n",
"HOA: v1\n",
"States: 2\n",
"Start: 1\n",
"AP: 2 \"a\" \"b\"\n",
"Acceptance: 1 Inf(0)\n",
"--BODY--\n",
"State: 0 {0}\n",
"[t] 0\n",
"State: 1\n",
"[1] 0\n",
"[0&!1] 1\n",
"--END--"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"Overwriting example.aut\n"
]
}
],
"prompt_number": 6
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"for a in spot.automata('example.aut'):\n",
" display(a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f4824056ba0> >"
]
}
],
"prompt_number": 7
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Test syntax errors\n",
"------------------"
]
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"%%file example.aut\n",
"HOA: v1\n",
"States: 2\n",
"Start: 1\n",
"AP: 2 \"a\" \"b\"\n",
"acc-name: Buchi\n",
"Acceptance: 1 Inf(0)\n",
"--BODY--\n",
"State: 0 {0}\n",
"[t] 1\n",
"State: 1\n",
"[t] 1\n",
"--END--\n",
"HOA: v1\n",
"States: 2\n",
"Start: 1\n",
"AP: 2 \"a\" \"b\"\n",
"Acceptance: 1 Inf(0)\n",
"--BODY--\n",
"State: 0 {0}\n",
"[a] 3\n",
"State: 1\n",
"[1] 0\n",
"[0&!1] 1\n",
"--END--"
],
"language": "python",
"metadata": {},
"outputs": [
{
"output_type": "stream",
"stream": "stdout",
"text": [
"Overwriting example.aut\n"
]
}
],
"prompt_number": 8
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"for a in spot.automata('example.aut'):\n",
" display(a)"
],
"language": "python",
"metadata": {},
"outputs": [
{
"metadata": {},
"output_type": "display_data",
"svg": [
"\n",
"\n",
"\n",
"\n",
"\n"
],
"text": [
" *' at 0x7f4824056d20> >"
]
},
{
"ename": "SyntaxError",
"evalue": "\nexample.aut:20.2: syntax error, unexpected identifier\nexample.aut:20.1-3: ignoring this invalid label\nexample.aut:20.5: state number is larger than state count...\nexample.aut:14.1-9: ... declared here.\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 \nexample.aut:20.2: syntax error, unexpected identifier\nexample.aut:20.1-3: ignoring this invalid label\nexample.aut:20.5: state number is larger than state count...\nexample.aut:14.1-9: ... declared here.\n\n"
]
}
],
"prompt_number": 9
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"rm example.aut"
],
"language": "python",
"metadata": {},
"outputs": [],
"prompt_number": 10
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.automaton('example.aut')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"ename": "RuntimeError",
"evalue": "Cannot open file example.aut",
"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[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'example.aut'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename)\u001b[0m\n\u001b[1;32m 179\u001b[0m \u001b[0ma\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 180\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 181\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 182\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 183\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(*filenames)\u001b[0m\n\u001b[1;32m 141\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mfilename\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0;34m-\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m \u001b[0;34m!=\u001b[0m \u001b[0;34m'|'\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 142\u001b[0m \u001b[0mproc\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;32mNone\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 143\u001b[0;31m \u001b[0mp\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mhoa_stream_parser\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;32mTrue\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 144\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 145\u001b[0m proc = subprocess.Popen(filename[:-1], shell=True,\n",
"\u001b[0;32m/home/adl/git/spot/wrap/python/spot_impl.py\u001b[0m in \u001b[0;36m__init__\u001b[0;34m(self, *args)\u001b[0m\n\u001b[1;32m 2206\u001b[0m \u001b[0m__repr__\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_swig_repr\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 2207\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__init__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m*\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 2208\u001b[0;31m \u001b[0mthis\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_spot_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mnew_hoa_stream_parser\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 2209\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mthis\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mappend\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mthis\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 2210\u001b[0m \u001b[0;32mexcept\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mthis\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mthis\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;31mRuntimeError\u001b[0m: Cannot open file example.aut"
]
}
],
"prompt_number": 11
},
{
"cell_type": "code",
"collapsed": false,
"input": [
"spot.automaton('non-existing-cmd |')"
],
"language": "python",
"metadata": {},
"outputs": [
{
"ename": "RuntimeError",
"evalue": "Command non-existing-cmd exited with exit status 127",
"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[0;32m----> 1\u001b[0;31m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'non-existing-cmd |'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename)\u001b[0m\n\u001b[1;32m 179\u001b[0m \u001b[0ma\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 180\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 181\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 182\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 183\u001b[0m \u001b[0;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;32m/home/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(*filenames)\u001b[0m\n\u001b[1;32m 170\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 171\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[0;32m--> 172\u001b[0;31m .format(filename[:-1], ret))\n\u001b[0m\u001b[1;32m 173\u001b[0m \u001b[0;32mreturn\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 174\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;31mRuntimeError\u001b[0m: Command non-existing-cmd exited with exit status 127"
]
}
],
"prompt_number": 12
},
{
"cell_type": "code",
"collapsed": false,
"input": [],
"language": "python",
"metadata": {},
"outputs": []
}
],
"metadata": {}
}
]
}