From 6bad8aebdd76c32ba729a30ac3475e8b379fb77f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 7 Jan 2018 15:08:32 +0100 Subject: [PATCH] python: remove error recovery checks from the public notebooks * tests/python/_autparserr.ipynb: New files, containing error checking code from automata-io.ipynb and piperead.ipynb. * tests/python/automata-io.ipynb: Remove error checks, and pipe examples from piperead.ipynb. * tests/python/piperead.ipynb: Delete. * tests/python/word.ipynb: Move error checking code... * tests/python/_word.ipynb: ... in this new file. * doc/org/tut.org, tests/Makefile.am: Adjust. --- doc/org/tut.org | 2 - tests/Makefile.am | 3 +- tests/python/_autparserr.ipynb | 400 +++++++++++++++++++++++++ tests/python/_word.ipynb | 140 +++++++++ tests/python/automata-io.ipynb | 523 +++++++++++++++++++++------------ tests/python/piperead.ipynb | 499 ------------------------------- tests/python/word.ipynb | 262 +++-------------- 7 files changed, 917 insertions(+), 912 deletions(-) create mode 100644 tests/python/_autparserr.ipynb create mode 100644 tests/python/_word.ipynb delete mode 100644 tests/python/piperead.ipynb 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", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\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", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\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", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\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", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fa1c82ab900> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fa1c82e1120> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fa1c82ab930> >" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\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", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", "\n", - "0\n", - "\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a & !b\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f195c0860c0> >" + " *' at 0x7fa1c82e1120> >" ] }, - "metadata": {}, - "output_type": "display_data" - }, - { - "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": "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 \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" - ] - } - ], - "source": [ - "for a in spot.automata('example.aut'):\n", - " display(a)" - ] - }, - { - "cell_type": "code", - "execution_count": 11, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7f195c086600> >" - ] - }, - "execution_count": 11, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "spot.automaton('example.aut', timeout=100)" + "spot.automaton('ltl2tgba -s6 \"a U b\"|')" ] }, { "cell_type": "code", - "execution_count": 12, - "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": 14, + "execution_count": null, "metadata": {}, "outputs": [], "source": [ - "rm example.aut" + "!rm example.aut" ] } ], diff --git a/tests/python/piperead.ipynb b/tests/python/piperead.ipynb deleted file mode 100644 index 6e9b6db75..000000000 --- a/tests/python/piperead.ipynb +++ /dev/null @@ -1,499 +0,0 @@ -{ - "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": [ - "# 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." - ] - }, - { - "cell_type": "code", - "execution_count": 2, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fbd0404bab0> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fbd004afa50> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fbd004afae0> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fbd004afa80> >" - ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], - "source": [ - "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." - ] - }, - { - "cell_type": "code", - "execution_count": 3, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fbd004afa20> >" - ] - }, - "execution_count": 3, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "spot.automaton('ltl2tgba -s6 \"a U b\"|')" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Error handling\n", - "\n", - "If the shell command terminates with a non-zero exit status, we should get an exception." - ] - }, - { - "cell_type": "code", - "execution_count": 4, - "metadata": {}, - "outputs": [ - { - "ename": "CalledProcessError", - "evalue": "Command 'non-existing-command' 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-command|'\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: \"\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "I->1\n", - "\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "0\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fbd004af8d0> >" - ] - }, - "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|')" - ] - } - ], - "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 index d52e54964..6d6bc28ee 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -3,9 +3,7 @@ { "cell_type": "code", "execution_count": 1, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [], "source": [ "import spot\n", @@ -22,9 +20,7 @@ { "cell_type": "code", "execution_count": 2, - "metadata": { - "collapsed": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -149,7 +145,7 @@ "\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", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "a & b\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "2->3\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "!a & !b\n", "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "a\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb74c39d990> >" + " *' at 0x7ff77439aae0> >" ] }, - "execution_count": 14, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "w1.as_automaton()" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "The rest of this page tests some syntax errors, you (humans) may skip it, but the test suite will not." - ] - }, - { - "cell_type": "code", - "execution_count": 15, - "metadata": { - "collapsed": false - }, - "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": 16, - "metadata": { - "collapsed": false - }, - "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": 17, - "metadata": { - "collapsed": false - }, - "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": 18, - "metadata": { - "collapsed": false - }, - "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": 19, - "metadata": { - "collapsed": false - }, - "outputs": [], - "source": [ - "# Creating an empty word is OK...\n", - "w = spot.twa_word(spot._bdd_dict)" - ] - }, - { - "cell_type": "code", - "execution_count": 20, - "metadata": { - "collapsed": false - }, - "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)" + "w.as_automaton()" ] } ],