alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/tests/python/_autparserr.ipynb
Alexandre Duret-Lutz 3034e8fcc3 python: render <svg> via _repr_html_ 
Work around a recent decision in Jupyter Lab and Notebook to render
<svg> is inline <img>, breaking tooltips or text selection.

(Rerendering all notebooks was painful.)

* NEWS: Mention the change.
* python/spot/__init__.py: Add a _repr_html_ method to all
classes that had a _repr_svg_.  It seems Jupyter will use
_repr_html_ by default.
* python/spot/jupyter.py: SVG replace the _repr_svg_ method
by a _repr_html.
* tests/python/_altscc.ipynb, tests/python/_autparserr.ipynb,
tests/python/_aux.ipynb, tests/python/_mealy.ipynb,
tests/python/_partitioned_relabel.ipynb,
tests/python/_product_susp.ipynb, tests/python/_product_weak.ipynb,
tests/python/_synthesis.ipynb, tests/python/aliases.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
tests/python/atva16-fig2b.ipynb, tests/python/automata-io.ipynb,
tests/python/automata.ipynb, tests/python/cav22-figs.ipynb,
tests/python/contains.ipynb, tests/python/decompose.ipynb,
tests/python/formulas.ipynb, tests/python/games.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/parity.ipynb, tests/python/product.ipynb,
tests/python/randaut.ipynb, tests/python/satmin.ipynb,
tests/python/stutter-inv.ipynb, tests/python/synthesis.ipynb,
tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb,
tests/python/word.ipynb, tests/python/zlktree.ipynb: Update all
notebooks.
2024-02-09 15:06:07 +01:00

586 lines
42 KiB
Text
Raw Blame History

{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"from IPython.display import display\n",
"import spot\n",
"spot.setup()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Test syntax errors\n",
"------------------"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Writing _example.aut\n"
]
}
],
"source": [
"%%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--"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"133pt\" height=\"124pt\"\n",
" viewBox=\"0.00 0.00 133.00 124.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 120)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-120 129,-120 129,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"41\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"107\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M23.06,-62.98C24.67,-62.58 58.27,-54.08 82.2,-48.02\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.27,-46.23 83.26,-51 85.88,-47.09 82.49,-47.95 82.49,-47.95 82.49,-47.95 85.88,-47.09 81.71,-44.9 89.27,-46.23 89.27,-46.23\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M99.97,-58.66C98.41,-68.62 100.75,-78 107,-78 111.69,-78 114.18,-72.73 114.47,-65.89\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"114.03,-58.66 117.6,-65.46 114.24,-62.16 114.46,-65.65 114.46,-65.65 114.46,-65.65 114.24,-62.16 111.31,-65.84 114.03,-58.66 114.03,-58.66\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"22\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M43.52,-26.94C55.31,-29.79 70.18,-33.37 82.46,-36.33\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.34,-37.99 81.8,-39.41 85.94,-37.17 82.53,-36.35 82.53,-36.35 82.53,-36.35 85.94,-37.17 83.27,-33.28 89.34,-37.99 89.34,-37.99\"/>\n",
"<text text-anchor=\"middle\" x=\"66.5\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/html": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"133pt\" height=\"124pt\"\n",
" viewBox=\"0.00 0.00 133.00 124.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 120)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-120 129,-120 129,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"41\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"107\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M23.06,-62.98C24.67,-62.58 58.27,-54.08 82.2,-48.02\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.27,-46.23 83.26,-51 85.88,-47.09 82.49,-47.95 82.49,-47.95 82.49,-47.95 85.88,-47.09 81.71,-44.9 89.27,-46.23 89.27,-46.23\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M99.97,-58.66C98.41,-68.62 100.75,-78 107,-78 111.69,-78 114.18,-72.73 114.47,-65.89\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"114.03,-58.66 117.6,-65.46 114.24,-62.16 114.46,-65.65 114.46,-65.65 114.46,-65.65 114.24,-62.16 111.31,-65.84 114.03,-58.66 114.03,-58.66\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"22\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M43.52,-26.94C55.31,-29.79 70.18,-33.37 82.46,-36.33\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.34,-37.99 81.8,-39.41 85.94,-37.17 82.53,-36.35 82.53,-36.35 82.53,-36.35 85.94,-37.17 83.27,-33.28 89.34,-37.99 89.34,-37.99\"/>\n",
"<text text-anchor=\"middle\" x=\"66.5\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f695c599f50> >"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"ename": "SyntaxError",
"evalue": "\n_example.aut:20.2: syntax error, unexpected identifier\n_example.aut:20.1-3: ignoring this invalid label\n_example.aut:20.5: state number is larger than state count...\n_example.aut:14.1-9: ... declared here.\n (<string>)",
"output_type": "error",
"traceback": [
"Traceback \u001b[0;36m(most recent call last)\u001b[0m:\n",
"\u001b[0m File \u001b[1;32m/usr/lib/python3/dist-packages/IPython/core/interactiveshell.py:3553\u001b[0m in \u001b[1;35mrun_code\u001b[0m\n exec(code_obj, self.user_global_ns, self.user_ns)\u001b[0m\n",
"\u001b[0m Cell \u001b[1;32mIn[3], line 1\u001b[0m\n for a in spot.automata('_example.aut'):\u001b[0m\n",
"\u001b[0;36m File \u001b[0;32m~/git/spot/python/spot/__init__.py:718\u001b[0;36m in \u001b[0;35mautomata\u001b[0;36m\n\u001b[0;31m res = p.parse(_bdd_dict)\u001b[0;36m\n",
"\u001b[0;36m File \u001b[0;32m<string>\u001b[0;36m\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n_example.aut:20.2: syntax error, unexpected identifier\n_example.aut:20.1-3: ignoring this invalid label\n_example.aut:20.5: state number is larger than state count...\n_example.aut:14.1-9: ... declared here.\n\n"
]
}
],
"source": [
"for a in spot.automata('_example.aut'):\n",
" display(a)"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"133pt\" height=\"124pt\"\n",
" viewBox=\"0.00 0.00 133.00 124.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 120)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-120 129,-120 129,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"41\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"107\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M23.06,-62.98C24.67,-62.58 58.27,-54.08 82.2,-48.02\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.27,-46.23 83.26,-51 85.88,-47.09 82.49,-47.95 82.49,-47.95 82.49,-47.95 85.88,-47.09 81.71,-44.9 89.27,-46.23 89.27,-46.23\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M99.97,-58.66C98.41,-68.62 100.75,-78 107,-78 111.69,-78 114.18,-72.73 114.47,-65.89\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"114.03,-58.66 117.6,-65.46 114.24,-62.16 114.46,-65.65 114.46,-65.65 114.46,-65.65 114.24,-62.16 111.31,-65.84 114.03,-58.66 114.03,-58.66\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"22\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M43.52,-26.94C55.31,-29.79 70.18,-33.37 82.46,-36.33\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.34,-37.99 81.8,-39.41 85.94,-37.17 82.53,-36.35 82.53,-36.35 82.53,-36.35 85.94,-37.17 83.27,-33.28 89.34,-37.99 89.34,-37.99\"/>\n",
"<text text-anchor=\"middle\" x=\"66.5\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/html": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"133pt\" height=\"124pt\"\n",
" viewBox=\"0.00 0.00 133.00 124.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 120)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-120 129,-120 129,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"41\" y=\"-100.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"107\" cy=\"-42\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-38.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M23.06,-62.98C24.67,-62.58 58.27,-54.08 82.2,-48.02\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.27,-46.23 83.26,-51 85.88,-47.09 82.49,-47.95 82.49,-47.95 82.49,-47.95 85.88,-47.09 81.71,-44.9 89.27,-46.23 89.27,-46.23\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M99.97,-58.66C98.41,-68.62 100.75,-78 107,-78 111.69,-78 114.18,-72.73 114.47,-65.89\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"114.03,-58.66 117.6,-65.46 114.24,-62.16 114.46,-65.65 114.46,-65.65 114.46,-65.65 114.24,-62.16 111.31,-65.84 114.03,-58.66 114.03,-58.66\"/>\n",
"<text text-anchor=\"middle\" x=\"107\" y=\"-81.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"22\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"22\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M43.52,-26.94C55.31,-29.79 70.18,-33.37 82.46,-36.33\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"89.34,-37.99 81.8,-39.41 85.94,-37.17 82.53,-36.35 82.53,-36.35 82.53,-36.35 85.94,-37.17 83.27,-33.28 89.34,-37.99 89.34,-37.99\"/>\n",
"<text text-anchor=\"middle\" x=\"66.5\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f695c59a370> >"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.automaton('_example.aut', timeout=100)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Error reading from pipe\n",
"\n",
"We redirect stderr to /dev/null to avoid difference between ipykernel 5 (that sends stderr to the console) and ipykernel 6 (that captures stderr for the notebook)."
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"ename": "CalledProcessError",
"evalue": "Command 'non-existing-cmd 2>/dev/null ' returned non-zero exit status 127.",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)",
"Cell \u001b[0;32mIn[5], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mspot\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mautomaton\u001b[49m\u001b[43m(\u001b[49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[38;5;124;43mnon-existing-cmd 2>/dev/null |\u001b[39;49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[43m)\u001b[49m\n",
"File \u001b[0;32m~/git/spot/python/spot/__init__.py:747\u001b[0m, in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 743\u001b[0m \u001b[38;5;250m\u001b[39m\u001b[38;5;124;03m\"\"\"Read a single automaton from a file.\u001b[39;00m\n\u001b[1;32m 744\u001b[0m \n\u001b[1;32m 745\u001b[0m \u001b[38;5;124;03mSee `spot.automata` for a list of supported formats.\"\"\"\u001b[39;00m\n\u001b[1;32m 746\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[0;32m--> 747\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28;43mnext\u001b[39;49m\u001b[43m(\u001b[49m\u001b[43mautomata\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfilename\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;241;43m*\u001b[39;49m\u001b[38;5;241;43m*\u001b[39;49m\u001b[43mkwargs\u001b[49m\u001b[43m)\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 748\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m \u001b[38;5;167;01mStopIteration\u001b[39;00m:\n\u001b[1;32m 749\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mFailed to read automaton from \u001b[39m\u001b[38;5;132;01m{}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;241m.\u001b[39mformat(filename))\n",
"File \u001b[0;32m~/git/spot/python/spot/__init__.py:732\u001b[0m, in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, want_kripke, drop_false_edges, *sources)\u001b[0m\n\u001b[1;32m 729\u001b[0m \u001b[38;5;66;03m# Do not complain about the exit code if we are already raising\u001b[39;00m\n\u001b[1;32m 730\u001b[0m \u001b[38;5;66;03m# an exception.\u001b[39;00m\n\u001b[1;32m 731\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m ret \u001b[38;5;129;01mand\u001b[39;00m sys\u001b[38;5;241m.\u001b[39mexc_info()[\u001b[38;5;241m0\u001b[39m] \u001b[38;5;129;01mis\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m:\n\u001b[0;32m--> 732\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m subprocess\u001b[38;5;241m.\u001b[39mCalledProcessError(ret, filename[:\u001b[38;5;241m-\u001b[39m\u001b[38;5;241m1\u001b[39m])\n\u001b[1;32m 733\u001b[0m \u001b[38;5;66;03m# deleting o explicitly now prevents Python 3.5 from\u001b[39;00m\n\u001b[1;32m 734\u001b[0m \u001b[38;5;66;03m# reporting the following error: \"<built-in function\u001b[39;00m\n\u001b[1;32m 735\u001b[0m \u001b[38;5;66;03m# delete_automaton_parser_options> returned a result with\u001b[39;00m\n\u001b[1;32m 736\u001b[0m \u001b[38;5;66;03m# an error set\". It's not clear to me if the bug is in Python\u001b[39;00m\n\u001b[1;32m 737\u001b[0m \u001b[38;5;66;03m# or Swig. At least it's related to the use of generators.\u001b[39;00m\n\u001b[1;32m 738\u001b[0m \u001b[38;5;28;01mdel\u001b[39;00m o\n",
"\u001b[0;31mCalledProcessError\u001b[0m: Command 'non-existing-cmd 2>/dev/null ' returned non-zero exit status 127."
]
}
],
"source": [
"spot.automaton('non-existing-cmd 2>/dev/null |')"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"ename": "TimeoutExpired",
"evalue": "Command 'sleep 3; cat _example.aut ' timed out after 1 seconds",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mTimeoutExpired\u001b[0m Traceback (most recent call last)",
"Cell \u001b[0;32mIn[6], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mspot\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mautomaton\u001b[49m\u001b[43m(\u001b[49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[38;5;124;43msleep 3; cat _example.aut |\u001b[39;49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mtimeout\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[38;5;241;43m1\u001b[39;49m\u001b[43m)\u001b[49m\n",
"File \u001b[0;32m~/git/spot/python/spot/__init__.py:747\u001b[0m, in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 743\u001b[0m \u001b[38;5;250m\u001b[39m\u001b[38;5;124;03m\"\"\"Read a single automaton from a file.\u001b[39;00m\n\u001b[1;32m 744\u001b[0m \n\u001b[1;32m 745\u001b[0m \u001b[38;5;124;03mSee `spot.automata` for a list of supported formats.\"\"\"\u001b[39;00m\n\u001b[1;32m 746\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[0;32m--> 747\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28;43mnext\u001b[39;49m\u001b[43m(\u001b[49m\u001b[43mautomata\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfilename\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;241;43m*\u001b[39;49m\u001b[38;5;241;43m*\u001b[39;49m\u001b[43mkwargs\u001b[49m\u001b[43m)\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 748\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m \u001b[38;5;167;01mStopIteration\u001b[39;00m:\n\u001b[1;32m 749\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mFailed to read automaton from \u001b[39m\u001b[38;5;132;01m{}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;241m.\u001b[39mformat(filename))\n",
"File \u001b[0;32m~/git/spot/python/spot/__init__.py:687\u001b[0m, in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, want_kripke, drop_false_edges, *sources)\u001b[0m\n\u001b[1;32m 685\u001b[0m \u001b[38;5;28;01melse\u001b[39;00m:\n\u001b[1;32m 686\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[0;32m--> 687\u001b[0m out, err \u001b[38;5;241m=\u001b[39m \u001b[43mproc\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mcommunicate\u001b[49m\u001b[43m(\u001b[49m\u001b[43mtimeout\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[43mtimeout\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 688\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m subprocess\u001b[38;5;241m.\u001b[39mTimeoutExpired:\n\u001b[1;32m 689\u001b[0m \u001b[38;5;66;03m# Using subprocess.check_output() with timeout\u001b[39;00m\n\u001b[1;32m 690\u001b[0m \u001b[38;5;66;03m# would just kill the shell, not its children.\u001b[39;00m\n\u001b[1;32m 691\u001b[0m os\u001b[38;5;241m.\u001b[39mkillpg(proc\u001b[38;5;241m.\u001b[39mpid, signal\u001b[38;5;241m.\u001b[39mSIGKILL)\n",
"File \u001b[0;32m/usr/lib/python3.11/subprocess.py:1209\u001b[0m, in \u001b[0;36mPopen.communicate\u001b[0;34m(self, input, timeout)\u001b[0m\n\u001b[1;32m 1206\u001b[0m endtime \u001b[38;5;241m=\u001b[39m \u001b[38;5;28;01mNone\u001b[39;00m\n\u001b[1;32m 1208\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[0;32m-> 1209\u001b[0m stdout, stderr \u001b[38;5;241m=\u001b[39m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m_communicate\u001b[49m\u001b[43m(\u001b[49m\u001b[38;5;28;43minput\u001b[39;49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mendtime\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mtimeout\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 1210\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m \u001b[38;5;167;01mKeyboardInterrupt\u001b[39;00m:\n\u001b[1;32m 1211\u001b[0m \u001b[38;5;66;03m# https://bugs.python.org/issue25942\u001b[39;00m\n\u001b[1;32m 1212\u001b[0m \u001b[38;5;66;03m# See the detailed comment in .wait().\u001b[39;00m\n\u001b[1;32m 1213\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m timeout \u001b[38;5;129;01mis\u001b[39;00m \u001b[38;5;129;01mnot\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m:\n",
"File \u001b[0;32m/usr/lib/python3.11/subprocess.py:2109\u001b[0m, in \u001b[0;36mPopen._communicate\u001b[0;34m(self, input, endtime, orig_timeout)\u001b[0m\n\u001b[1;32m 2104\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m( \u001b[38;5;66;03m# Impossible :)\u001b[39;00m\n\u001b[1;32m 2105\u001b[0m \u001b[38;5;124m'\u001b[39m\u001b[38;5;124m_check_timeout(..., skip_check_and_raise=True) \u001b[39m\u001b[38;5;124m'\u001b[39m\n\u001b[1;32m 2106\u001b[0m \u001b[38;5;124m'\u001b[39m\u001b[38;5;124mfailed to raise TimeoutExpired.\u001b[39m\u001b[38;5;124m'\u001b[39m)\n\u001b[1;32m 2108\u001b[0m ready \u001b[38;5;241m=\u001b[39m selector\u001b[38;5;241m.\u001b[39mselect(timeout)\n\u001b[0;32m-> 2109\u001b[0m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m_check_timeout\u001b[49m\u001b[43m(\u001b[49m\u001b[43mendtime\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43morig_timeout\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mstdout\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mstderr\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 2111\u001b[0m \u001b[38;5;66;03m# XXX Rewrite these to use non-blocking I/O on the file\u001b[39;00m\n\u001b[1;32m 2112\u001b[0m \u001b[38;5;66;03m# objects; they are no longer using C stdio!\u001b[39;00m\n\u001b[1;32m 2114\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m key, events \u001b[38;5;129;01min\u001b[39;00m ready:\n",
"File \u001b[0;32m/usr/lib/python3.11/subprocess.py:1253\u001b[0m, in \u001b[0;36mPopen._check_timeout\u001b[0;34m(self, endtime, orig_timeout, stdout_seq, stderr_seq, skip_check_and_raise)\u001b[0m\n\u001b[1;32m 1251\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m\n\u001b[1;32m 1252\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m skip_check_and_raise \u001b[38;5;129;01mor\u001b[39;00m _time() \u001b[38;5;241m>\u001b[39m endtime:\n\u001b[0;32m-> 1253\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m TimeoutExpired(\n\u001b[1;32m 1254\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39margs, orig_timeout,\n\u001b[1;32m 1255\u001b[0m output\u001b[38;5;241m=\u001b[39m\u001b[38;5;124mb\u001b[39m\u001b[38;5;124m'\u001b[39m\u001b[38;5;124m'\u001b[39m\u001b[38;5;241m.\u001b[39mjoin(stdout_seq) \u001b[38;5;28;01mif\u001b[39;00m stdout_seq \u001b[38;5;28;01melse\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m,\n\u001b[1;32m 1256\u001b[0m stderr\u001b[38;5;241m=\u001b[39m\u001b[38;5;124mb\u001b[39m\u001b[38;5;124m'\u001b[39m\u001b[38;5;124m'\u001b[39m\u001b[38;5;241m.\u001b[39mjoin(stderr_seq) \u001b[38;5;28;01mif\u001b[39;00m stderr_seq \u001b[38;5;28;01melse\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m)\n",
"\u001b[0;31mTimeoutExpired\u001b[0m: Command 'sleep 3; cat _example.aut ' timed out after 1 seconds"
]
}
],
"source": [
"spot.automaton('sleep 3; cat _example.aut |', timeout=1)"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Title: a U b Pages: 1 -->\n",
"<svg width=\"170pt\" height=\"108pt\"\n",
" viewBox=\"0.00 0.00 170.00 108.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 104)\">\n",
"<title>a U b</title>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-104 166,-104 166,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"59.5\" y=\"-84.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-22C2.79,-22 17.15,-22 30.63,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-22 30.94,-25.15 34.44,-22 30.94,-22 30.94,-22 30.94,-22 34.44,-22 30.94,-18.85 37.94,-22 37.94,-22\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.62,-39.04C48.32,-48.86 50.45,-58 56,-58 60.17,-58 62.4,-52.86 62.71,-46.14\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-39.04 65.85,-45.88 62.54,-42.53 62.71,-46.03 62.71,-46.03 62.71,-46.03 62.54,-42.53 59.56,-46.18 62.38,-39.04 62.38,-39.04\"/>\n",
"<text text-anchor=\"start\" x=\"38\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"140\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"140\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"140\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.39,-22C84.9,-22 98.55,-22 110.6,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"117.85,-22 110.85,-25.15 114.35,-22 110.85,-22 110.85,-22 110.85,-22 114.35,-22 110.85,-18.85 117.85,-22 117.85,-22\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M131.99,-42.58C130.89,-52.84 133.55,-62 140,-62 144.83,-62 147.54,-56.85 148.13,-49.95\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"148.01,-42.58 151.27,-49.53 148.06,-46.08 148.12,-49.58 148.12,-49.58 148.12,-49.58 148.06,-46.08 144.97,-49.63 148.01,-42.58 148.01,-42.58\"/>\n",
"<text text-anchor=\"middle\" x=\"140\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/html": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Title: a U b Pages: 1 -->\n",
"<svg width=\"170pt\" height=\"108pt\"\n",
" viewBox=\"0.00 0.00 170.00 108.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 104)\">\n",
"<title>a U b</title>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-104 166,-104 166,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"59.5\" y=\"-84.8\" font-family=\"Lato\" font-size=\"14.00\">[Büchi]</text>\n",
"<!-- I -->\n",
"<!-- 1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>1</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"56\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- I&#45;&gt;1 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M1.15,-22C2.79,-22 17.15,-22 30.63,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-22 30.94,-25.15 34.44,-22 30.94,-22 30.94,-22 30.94,-22 34.44,-22 30.94,-18.85 37.94,-22 37.94,-22\"/>\n",
"</g>\n",
"<!-- 1&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>1&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M49.62,-39.04C48.32,-48.86 50.45,-58 56,-58 60.17,-58 62.4,-52.86 62.71,-46.14\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.38,-39.04 65.85,-45.88 62.54,-42.53 62.71,-46.03 62.71,-46.03 62.71,-46.03 62.54,-42.53 59.56,-46.18 62.38,-39.04 62.38,-39.04\"/>\n",
"<text text-anchor=\"start\" x=\"38\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"140\" cy=\"-22\" rx=\"18\" ry=\"18\"/>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"140\" cy=\"-22\" rx=\"22\" ry=\"22\"/>\n",
"<text text-anchor=\"middle\" x=\"140\" y=\"-18.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>1&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M74.39,-22C84.9,-22 98.55,-22 110.6,-22\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"117.85,-22 110.85,-25.15 114.35,-22 110.85,-22 110.85,-22 110.85,-22 114.35,-22 110.85,-18.85 117.85,-22 117.85,-22\"/>\n",
"<text text-anchor=\"start\" x=\"92\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">b</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M131.99,-42.58C130.89,-52.84 133.55,-62 140,-62 144.83,-62 147.54,-56.85 148.13,-49.95\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"148.01,-42.58 151.27,-49.53 148.06,-46.08 148.12,-49.58 148.12,-49.58 148.12,-49.58 148.06,-46.08 144.97,-49.63 148.01,-42.58 148.01,-42.58\"/>\n",
"<text text-anchor=\"middle\" x=\"140\" y=\"-65.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f6945207210> >"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"ename": "CalledProcessError",
"evalue": "Command 'ltl2tgba \"syntax U U error\" 2>/dev/null ' returned non-zero exit status 2.",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mCalledProcessError\u001b[0m Traceback (most recent call last)",
"Cell \u001b[0;32mIn[7], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[38;5;28;43;01mfor\u001b[39;49;00m\u001b[43m \u001b[49m\u001b[43ma\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;129;43;01min\u001b[39;49;00m\u001b[43m \u001b[49m\u001b[43mspot\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mautomata\u001b[49m\u001b[43m(\u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mltl2tgba \u001b[39;49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[38;5;124;43ma U b\u001b[39;49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[38;5;124;43m|\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[38;5;124;43mltl2tgba \u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43msyntax U U error\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43m 2>/dev/null |\u001b[39;49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[43m)\u001b[49m\u001b[43m:\u001b[49m\n\u001b[1;32m 2\u001b[0m \u001b[43m \u001b[49m\u001b[43mdisplay\u001b[49m\u001b[43m(\u001b[49m\u001b[43ma\u001b[49m\u001b[43m)\u001b[49m\n",
"File \u001b[0;32m~/git/spot/python/spot/__init__.py:732\u001b[0m, in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, want_kripke, drop_false_edges, *sources)\u001b[0m\n\u001b[1;32m 729\u001b[0m \u001b[38;5;66;03m# Do not complain about the exit code if we are already raising\u001b[39;00m\n\u001b[1;32m 730\u001b[0m \u001b[38;5;66;03m# an exception.\u001b[39;00m\n\u001b[1;32m 731\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m ret \u001b[38;5;129;01mand\u001b[39;00m sys\u001b[38;5;241m.\u001b[39mexc_info()[\u001b[38;5;241m0\u001b[39m] \u001b[38;5;129;01mis\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m:\n\u001b[0;32m--> 732\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m subprocess\u001b[38;5;241m.\u001b[39mCalledProcessError(ret, filename[:\u001b[38;5;241m-\u001b[39m\u001b[38;5;241m1\u001b[39m])\n\u001b[1;32m 733\u001b[0m \u001b[38;5;66;03m# deleting o explicitly now prevents Python 3.5 from\u001b[39;00m\n\u001b[1;32m 734\u001b[0m \u001b[38;5;66;03m# reporting the following error: \"<built-in function\u001b[39;00m\n\u001b[1;32m 735\u001b[0m \u001b[38;5;66;03m# delete_automaton_parser_options> returned a result with\u001b[39;00m\n\u001b[1;32m 736\u001b[0m \u001b[38;5;66;03m# an error set\". It's not clear to me if the bug is in Python\u001b[39;00m\n\u001b[1;32m 737\u001b[0m \u001b[38;5;66;03m# or Swig. At least it's related to the use of generators.\u001b[39;00m\n\u001b[1;32m 738\u001b[0m \u001b[38;5;28;01mdel\u001b[39;00m o\n",
"\u001b[0;31mCalledProcessError\u001b[0m: Command 'ltl2tgba \"syntax U U error\" 2>/dev/null ' returned non-zero exit status 2."
]
}
],
"source": [
"for a in spot.automata(\"ltl2tgba 'a U b'|\", 'ltl2tgba \"syntax U U error\" 2>/dev/null |'):\n",
" display(a)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Reading an empty file with `spot.automaton()` is an error."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"ename": "RuntimeError",
"evalue": "Failed to read automaton from true|",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mStopIteration\u001b[0m Traceback (most recent call last)",
"File \u001b[0;32m~/git/spot/python/spot/__init__.py:747\u001b[0m, in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 746\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[0;32m--> 747\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28;43mnext\u001b[39;49m\u001b[43m(\u001b[49m\u001b[43mautomata\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfilename\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;241;43m*\u001b[39;49m\u001b[38;5;241;43m*\u001b[39;49m\u001b[43mkwargs\u001b[49m\u001b[43m)\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 748\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m \u001b[38;5;167;01mStopIteration\u001b[39;00m:\n",
"\u001b[0;31mStopIteration\u001b[0m: ",
"\nDuring handling of the above exception, another exception occurred:\n",
"\u001b[0;31mRuntimeError\u001b[0m Traceback (most recent call last)",
"Cell \u001b[0;32mIn[8], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mspot\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mautomaton\u001b[49m\u001b[43m(\u001b[49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[38;5;124;43mtrue|\u001b[39;49m\u001b[38;5;124;43m'\u001b[39;49m\u001b[43m)\u001b[49m\n",
"File \u001b[0;32m~/git/spot/python/spot/__init__.py:749\u001b[0m, in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 747\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28mnext\u001b[39m(automata(filename, \u001b[38;5;241m*\u001b[39m\u001b[38;5;241m*\u001b[39mkwargs))\n\u001b[1;32m 748\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m \u001b[38;5;167;01mStopIteration\u001b[39;00m:\n\u001b[0;32m--> 749\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mRuntimeError\u001b[39;00m(\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mFailed to read automaton from \u001b[39m\u001b[38;5;132;01m{}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;241m.\u001b[39mformat(filename))\n",
"\u001b[0;31mRuntimeError\u001b[0m: Failed to read automaton from true|"
]
}
],
"source": [
"spot.automaton('true|')"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [],
"source": [
"!rm _example.aut"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"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.11.7"
}
},
"nbformat": 4,
"nbformat_minor": 2
}
Reference in a new issue View git blame Copy permalink