diff --git a/doc/org/tut.org b/doc/org/tut.org
index d11352df7..c0b4064c7 100644
--- a/doc/org/tut.org
+++ b/doc/org/tut.org
@@ -58,8 +58,6 @@ real notebooks instead.
- [[https://spot.lrde.epita.fr/ipynb/automata.html][=automata.ipynb=]] covers translation from formulas to automata,
automata printing, and some lights transformations
- [[https://spot.lrde.epita.fr/ipynb/automata-io.html][=automata-io.ipynb=]] shows how to save and read automata from files
-- [[https://spot.lrde.epita.fr/ipynb/piperead.html][=piperead.ipynb=]] shows how to save and read automata output from other
- commands, using pipes
- [[https://spot.lrde.epita.fr/ipynb/randaut.html][=randaut.ipynb=]] shows a simple case where the [[file:randaut.org][=randaut=]] commands
generated random automata, which are displayed in a table before and
after acceptance simplification
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 948083f12..ed0f6c4bc 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -334,7 +334,6 @@ TESTS_ipython = \
python/highlighting.ipynb \
python/ltsmin-dve.ipynb \
python/ltsmin-pml.ipynb \
- python/piperead.ipynb \
python/parity.ipynb \
python/product.ipynb \
python/randaut.ipynb \
@@ -348,7 +347,9 @@ TESTS_ipython = \
# with a _.
TESTS_python = \
python/_altscc.ipynb \
+ python/_autparserr.ipynb \
python/_aux.ipynb \
+ python/_word.ipynb \
python/accparse2.py \
python/alarm.py \
python/alternating.py \
diff --git a/tests/python/_autparserr.ipynb b/tests/python/_autparserr.ipynb
new file mode 100644
index 000000000..2aa9b219f
--- /dev/null
+++ b/tests/python/_autparserr.ipynb
@@ -0,0 +1,400 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "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": [
+ "Overwriting _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": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fbec845de70> >"
+ ]
+ },
+ "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 ()",
+ "output_type": "error",
+ "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 \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": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fbec846c5a0> >"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "spot.automaton('_example.aut', timeout=100)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Error reading from pipe"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CalledProcessError",
+ "evalue": "Command 'non-existing-cmd ' 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)",
+ "\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/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 479\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 480\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 481\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\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[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 482\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 483\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/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)\u001b[0m\n\u001b[1;32m 464\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 465\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[0;32m--> 466\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\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[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 467\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 468\u001b[0m \u001b[0;31m# reporting the following error: \"\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'sleep 3; cat _example.aut |'\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0;36m1\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
+ "\u001b[0;32m/home/adl/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 479\u001b[0m See `spot.automata` for a list of supported formats.\"\"\"\n\u001b[1;32m 480\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 481\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\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[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 482\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 483\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/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)\u001b[0m\n\u001b[1;32m 423\u001b[0m \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 424\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 425\u001b[0;31m \u001b[0mout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0merr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcommunicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 426\u001b[0m \u001b[0;32mexcept\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mTimeoutExpired\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 427\u001b[0m \u001b[0;31m# Using subprocess.check_output() with timeout\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
+ "\u001b[0;32m/usr/lib/python3.6/subprocess.py\u001b[0m in \u001b[0;36mcommunicate\u001b[0;34m(self, input, timeout)\u001b[0m\n\u001b[1;32m 841\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 842\u001b[0m \u001b[0;32mtry\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 843\u001b[0;31m \u001b[0mstdout\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mstderr\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_communicate\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0minput\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mendtime\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 844\u001b[0m \u001b[0;32mfinally\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 845\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_communication_started\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;32mTrue\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
+ "\u001b[0;32m/usr/lib/python3.6/subprocess.py\u001b[0m in \u001b[0;36m_communicate\u001b[0;34m(self, input, endtime, orig_timeout)\u001b[0m\n\u001b[1;32m 1513\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 1514\u001b[0m \u001b[0mready\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mselector\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mselect\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtimeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 1515\u001b[0;31m \u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0m_check_timeout\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mendtime\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0morig_timeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 1516\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 1517\u001b[0m \u001b[0;31m# XXX Rewrite these to use non-blocking I/O on the file\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
+ "\u001b[0;32m/usr/lib/python3.6/subprocess.py\u001b[0m in \u001b[0;36m_check_timeout\u001b[0;34m(self, endtime, orig_timeout)\u001b[0m\n\u001b[1;32m 869\u001b[0m \u001b[0;32mreturn\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 870\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0m_time\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m>\u001b[0m \u001b[0mendtime\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 871\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mTimeoutExpired\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0margs\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0morig_timeout\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 872\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 873\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\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": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fbec846c570> >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "ename": "CalledProcessError",
+ "evalue": "Command 'ltl2tgba \"syntax U U error\"' 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)",
+ "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0;32mfor\u001b[0m \u001b[0ma\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mspot\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mautomata\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"ltl2tgba 'a U b'|\"\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m'ltl2tgba \"syntax U U error\"|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 2\u001b[0m \u001b[0mdisplay\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[0;32m/home/adl/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomata\u001b[0;34m(timeout, ignore_abort, trust_hoa, no_sid, debug, *sources)\u001b[0m\n\u001b[1;32m 464\u001b[0m \u001b[0;32mdel\u001b[0m \u001b[0mproc\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 465\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[0;32m--> 466\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0msubprocess\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mCalledProcessError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mret\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[0;36m1\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 467\u001b[0m \u001b[0;31m# deleting o explicitely now prevents Python 3.5 from\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 468\u001b[0m \u001b[0;31m# reporting the following error: \" 481\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\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[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 482\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[0;31mStopIteration\u001b[0m: ",
+ "\nDuring handling of the above exception, another exception occurred:\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'true|'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
+ "\u001b[0;32m/home/adl/git/spot/python/spot/__init__.py\u001b[0m in \u001b[0;36mautomaton\u001b[0;34m(filename, **kwargs)\u001b[0m\n\u001b[1;32m 481\u001b[0m \u001b[0;32mreturn\u001b[0m \u001b[0mnext\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[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 482\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[0;32m--> 483\u001b[0;31m \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[0m\u001b[1;32m 484\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 485\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\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"
+ ]
+ }
+ ],
+ "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
+}
diff --git a/tests/python/_word.ipynb b/tests/python/_word.ipynb
new file mode 100644
index 000000000..213299347
--- /dev/null
+++ b/tests/python/_word.ipynb
@@ -0,0 +1,140 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "import spot\n",
+ "spot.setup()"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "SyntaxError",
+ "evalue": "\n>>> a; b&!a; b\n ^\nA twa_word must contain a cycle\n ()",
+ "output_type": "error",
+ "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 \n>>> a; b&!a; b\n ^\nA twa_word must contain a cycle\n\n"
+ ]
+ }
+ ],
+ "source": [
+ "print(spot.parse_word('a; b&!a; b'))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "SyntaxError",
+ "evalue": "\n>>> a; b; c}\n ^\nExpected ';' delimiter: '}' stands for ending a cycle\n ()",
+ "output_type": "error",
+ "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 \n>>> a; b; c}\n ^\nExpected ';' delimiter: '}' stands for ending a cycle\n\n"
+ ]
+ }
+ ],
+ "source": [
+ "print(spot.parse_word('a; b; c}'))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "SyntaxError",
+ "evalue": "\n>>> a; cycle{}\n ^\nempty input\n\n ()",
+ "output_type": "error",
+ "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 \n>>> a; cycle{}\n ^\nempty input\n\n\n"
+ ]
+ }
+ ],
+ "source": [
+ "print(spot.parse_word('a; cycle{}'))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "SyntaxError",
+ "evalue": "\n>>> a; cycle{!a}; a\n ^\nInput should be finished after cycle\n ()",
+ "output_type": "error",
+ "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 \n>>> a; cycle{!a}; a\n ^\nInput should be finished after cycle\n\n"
+ ]
+ }
+ ],
+ "source": [
+ "print(spot.parse_word('a; cycle{!a}; a'))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "# Creating an empty word is OK...\n",
+ "w = spot.twa_word(spot._bdd_dict)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "RuntimeError",
+ "evalue": "a twa_word may not have an empty cycle",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
+ "\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[1;32m 1\u001b[0m \u001b[0;31m# ... as long as this word is not printed.\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 2\u001b[0;31m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mw\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
+ "\u001b[0;32m/home/adl/git/spot/python/spot/impl.py\u001b[0m in \u001b[0;36m__str__\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 4922\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4923\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0m__str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m->\u001b[0m \u001b[0;34m\"std::string\"\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m-> 4924\u001b[0;31m \u001b[0;32mreturn\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word___str__\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 4925\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0m_impl\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 4926\u001b[0m \u001b[0mtwa_word_swigregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mtwa_word\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
+ "\u001b[0;31mRuntimeError\u001b[0m: a twa_word may not have an empty cycle"
+ ]
+ }
+ ],
+ "source": [
+ "# ... as long as this word is not printed.\n",
+ "print(w)"
+ ]
+ }
+ ],
+ "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
+}
diff --git a/tests/python/automata-io.ipynb b/tests/python/automata-io.ipynb
index 9304361d0..ea4395d4f 100644
--- a/tests/python/automata-io.ipynb
+++ b/tests/python/automata-io.ipynb
@@ -11,6 +11,20 @@
"spot.setup()"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Converting automata to strings"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Use `to_str()` to output a string representing the automaton in different formats."
+ ]
+ },
{
"cell_type": "code",
"execution_count": 2,
@@ -80,6 +94,20 @@
" print(a.to_str(fmt))"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Saving automata to files"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Use `save()` to save the automaton into a file."
+ ]
+ },
{
"cell_type": "code",
"execution_count": 3,
@@ -138,7 +166,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f195c050a20> >"
+ " *' at 0x7fa1c833b9f0> >"
]
},
"execution_count": 3,
@@ -189,6 +217,20 @@
"!cat example.aut"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Reading automata from files"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Use `spot.automata()` to read multiple automata from a file, and `spot.automaton()` to read only one."
+ ]
+ },
{
"cell_type": "code",
"execution_count": 5,
@@ -247,7 +289,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f195f3ecab0> >"
+ " *' at 0x7fa1c82e10c0> >"
]
},
"metadata": {},
@@ -306,7 +348,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f195c050960> >"
+ " *' at 0x7fa1c82abab0> >"
]
},
"metadata": {},
@@ -322,8 +364,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "Test `--ABORT--`\n",
- "----------------"
+ "The `--ABORT--` feature of the HOA format allows discarding the automaton being read and starting over."
]
},
{
@@ -423,7 +464,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f195c050a50> >"
+ " *' at 0x7fa1c82ab870> >"
]
},
"metadata": {},
@@ -435,6 +476,20 @@
" display(a)"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Reading automata from strings"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Instead of passing a filename, you can also pass the contents of a file. `spot.automata()` and `spot.automaton()` look for the absence of newline to decide if this is a filename or a string containing some actual automaton text."
+ ]
+ },
{
"cell_type": "code",
"execution_count": 8,
@@ -493,7 +548,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f195c086120> >"
+ " *' at 0x7fa1c82aba50> >"
]
},
"metadata": {},
@@ -543,7 +598,7 @@
"\n"
],
"text/plain": [
- " *' at 0x7f195c050900> >"
+ " *' at 0x7fa1c82e10f0> >"
]
},
"metadata": {},
@@ -584,8 +639,9 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "Test syntax errors\n",
- "------------------"
+ "# Reading automata output from processes\n",
+ "\n",
+ "If an argument of `spot.automata` ends with `|`, then it is interpreted as a shell command that outputs one automaton or more."
]
},
{
@@ -594,39 +650,235 @@
"metadata": {},
"outputs": [
{
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "Overwriting example.aut\n"
- ]
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa1c82ab900> >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa1c82e1120> >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa1c82ab930> >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "image/svg+xml": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text/plain": [
+ " *' at 0x7fa1c82e1030> >"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
}
],
"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--"
+ "for a in spot.automata('ltl2tgba -s \"a U b\"; ltl2tgba --lbtt \"b\"|', 'ltl2tgba -H \"GFa\" \"a & GFb\"|'):\n",
+ " display(a)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "A single automaton can be read using `spot.automaton()`, with the same convention."
]
},
{
@@ -643,184 +895,69 @@
"\n",
"\n",
- "\n"
],
"text/plain": [
- " *' at 0x7fb74c39da80> >"
+ " *' at 0x7ff774426a50> >"
]
},
"execution_count": 2,
@@ -171,9 +167,7 @@
{
"cell_type": "code",
"execution_count": 3,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -207,9 +201,7 @@
{
"cell_type": "code",
"execution_count": 4,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"name": "stdout",
@@ -235,9 +227,7 @@
{
"cell_type": "code",
"execution_count": 5,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -264,9 +254,7 @@
{
"cell_type": "code",
"execution_count": 6,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -301,9 +289,7 @@
{
"cell_type": "code",
"execution_count": 7,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"name": "stdout",
@@ -331,9 +317,7 @@
{
"cell_type": "code",
"execution_count": 8,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -361,9 +345,7 @@
{
"cell_type": "code",
"execution_count": 9,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -390,9 +372,7 @@
{
"cell_type": "code",
"execution_count": 10,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"name": "stdout",
@@ -413,9 +393,7 @@
{
"cell_type": "code",
"execution_count": 11,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -436,9 +414,7 @@
{
"cell_type": "code",
"execution_count": 12,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -473,20 +449,7 @@
{
"cell_type": "code",
"execution_count": 13,
- "metadata": {
- "collapsed": false
- },
- "outputs": [],
- "source": [
- "w1 = spot.parse_word('a; !a; cycle{a; !a; a}')"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 14,
- "metadata": {
- "collapsed": false
- },
+ "metadata": {},
"outputs": [
{
"data": {
@@ -497,210 +460,75 @@
"\n",
"\n",
- "