diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index 14e185148..2a7d82e12 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -1620,6 +1620,15 @@ namespace spot
throw std::runtime_error(std::string("Cannot open file ") + name);
}
+ hoa_stream_parser::hoa_stream_parser(int fd,
+ const std::string& name,
+ bool ignore_abort)
+ : filename_(name), ignore_abort_(ignore_abort)
+ {
+ if (hoayyopen(fd))
+ throw std::runtime_error(std::string("Cannot open file ") + name);
+ }
+
hoa_stream_parser::~hoa_stream_parser()
{
hoayyclose();
diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll
index 063b7788f..95eef0e04 100644
--- a/src/hoaparse/hoascan.ll
+++ b/src/hoaparse/hoascan.ll
@@ -388,6 +388,31 @@ namespace spot
return 0;
}
+ int
+ hoayyopen(int fd)
+ {
+ bool want_interactive = false;
+
+ yyin = fdopen(fd, "r");
+
+ // If the input is a pipe, make the scanner
+ // interactive so that it does not wait for the input
+ // buffer to be full to process automata.
+ struct stat s;
+ if (fstat(fd, &s) < 0)
+ throw std::runtime_error("fstat failed");
+ if (S_ISFIFO(s.st_mode))
+ want_interactive = true;
+
+ // Reset the lexer in case a previous parse
+ // ended badly.
+ YY_NEW_FILE;
+ hoayyreset();
+ if (want_interactive)
+ yy_set_interactive(true);
+ return 0;
+ }
+
void
hoayyclose()
{
diff --git a/src/hoaparse/parsedecl.hh b/src/hoaparse/parsedecl.hh
index 286b8b773..5864d6a49 100644
--- a/src/hoaparse/parsedecl.hh
+++ b/src/hoaparse/parsedecl.hh
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2014 Laboratoire de Recherche et Développement
+// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
// de l'EPITA.
//
// This file is part of Spot, a model checking library.
@@ -33,6 +33,7 @@ namespace spot
{
void hoayyreset();
int hoayyopen(const std::string& name);
+ int hoayyopen(int fd);
void hoayyclose();
// This exception is thrown by the lexer when it reads "--ABORT--".
diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh
index ba1a3c6ed..f65beafad 100644
--- a/src/hoaparse/public.hh
+++ b/src/hoaparse/public.hh
@@ -64,6 +64,10 @@ namespace spot
bool ignore_abort_;
public:
hoa_stream_parser(const std::string& filename, bool ignore_abort = false);
+ // Read from an already open file descriptor.
+ // Use filename in error messages.
+ hoa_stream_parser(int fd, const std::string& filename,
+ bool ignore_abort = false);
~hoa_stream_parser();
hoa_aut_ptr parse(hoa_parse_error_list& error_list,
const bdd_dict_ptr& dict,
diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index 1a26386f8..bd91a62ba 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -111,14 +111,54 @@ def _tgba_save(a, filename, format='hoa', opt=None, append=False):
tgba.to_str = _tgba_to_str
tgba.save = _tgba_save
-def automata(filename):
- p = hoa_stream_parser(filename, True)
- while True:
- a = p.parse_strict(_bdd_dict)
- if a == None:
- return
- yield a
+def automata(*filenames):
+ """Read automata from a list of filenames.
+ The automata can be written in the
+ [HOA format](http://adl.github.io/hoaf/), as
+ [never claims](http://spinroot.com/spin/Man/never.html),
+ or in [LBTT's format]
+ (http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html).
+
+ If a filename ends with a `|`, then the filename is interpreted as
+ a shell command, and the output of that command (without the `|`)
+ is parsed."""
+
+ for filename in filenames:
+ try:
+ if filename[-1] != '|':
+ proc = None
+ p = hoa_stream_parser(filename, True)
+ else:
+ proc = subprocess.Popen(filename[:-1], shell=True,
+ stdout=subprocess.PIPE)
+ p = hoa_stream_parser(proc.stdout.fileno(), filename, True)
+ a = True
+ while a:
+ a = p.parse_strict(_bdd_dict)
+ if a:
+ yield a
+ finally:
+ # Make sure we destroy the parser and the subprocess in
+ # the correct order...
+ del p
+ if proc != None:
+ proc.poll()
+ ret = proc.returncode
+ del proc
+ if ret:
+ raise RuntimeError("Command {} exited with exit status {}"
+ .format(filename[:-1], ret))
+ return
+
+def automaton(filename):
+ """Read a single automaton from a file.
+
+ See `spot.automata()` for a list of supported format."""
+ try:
+ return next(automata(filename))
+ except StopIteration:
+ raise RuntimeError("Failed to read automaton from {}".format(filename))
def translate(formula, output='tgba', pref='small', level='high',
complete=False):
diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am
index 1d1ed3b63..c01f198c0 100644
--- a/wrap/python/tests/Makefile.am
+++ b/wrap/python/tests/Makefile.am
@@ -44,5 +44,6 @@ TESTS = \
minato.py \
optionmap.py \
parsetgba.py \
+ piperead.ipynb \
randltl.ipynb \
setxor.py
diff --git a/wrap/python/tests/piperead.ipynb b/wrap/python/tests/piperead.ipynb
new file mode 100644
index 000000000..df7bc0510
--- /dev/null
+++ b/wrap/python/tests/piperead.ipynb
@@ -0,0 +1,512 @@
+{
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Python 3",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.4.2"
+ },
+ "name": ""
+ },
+ "nbformat": 3,
+ "nbformat_minor": 0,
+ "worksheets": [
+ {
+ "cells": [
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "from IPython.display import display \n",
+ "import os\n",
+ "# Note that Spot (loaded by the kernel) will store a copy of\n",
+ "# the environment variables the first time it reads them, so\n",
+ "# if you change those variables, the new values will be ignored\n",
+ "# until you restart the kernel.\n",
+ "os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n",
+ "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n",
+ "import spot"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 1
+ },
+ {
+ "cell_type": "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 and automaton."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "for a in spot.automata('ltl2tgba -s \"a U b\"; ltl2tgba --lbtt \"b\"|', 'ltl2tgba -H \"GFa\" \"a & GFb\"|'):\n",
+ " display(a)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "display_data",
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f5b14173270> >"
+ ]
+ },
+ {
+ "metadata": {},
+ "output_type": "display_data",
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f5b141733f0> >"
+ ]
+ },
+ {
+ "metadata": {},
+ "output_type": "display_data",
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f5b14173450> >"
+ ]
+ },
+ {
+ "metadata": {},
+ "output_type": "display_data",
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f5b141733c0> >"
+ ]
+ }
+ ],
+ "prompt_number": 2
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "A single automaton can be read using `spot.automaton()`, with the same convention."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.automaton('ltl2tgba -s6 \"a U b\"|')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 3,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f5b14173450> >"
+ ]
+ }
+ ],
+ "prompt_number": 3
+ },
+ {
+ "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",
+ "collapsed": false,
+ "input": [
+ "spot.automaton('non-existing-command|')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "RuntimeError",
+ "evalue": "Command non-existing-command exited with exit status 127",
+ "output_type": "pyerr",
+ "traceback": [
+ "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[1;31mRuntimeError\u001b[0m Traceback (most recent call last)",
+ "\u001b[1;32m\u001b[0m in \u001b[0;36m\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mspot\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'non-existing-command|'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
+ "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[1;34m(filename)\u001b[0m\n\u001b[0;32m 157\u001b[0m See `spot.automata()` for a list of supported format.\"\"\"\n\u001b[0;32m 158\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 159\u001b[1;33m \u001b[1;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 160\u001b[0m \u001b[1;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 161\u001b[0m \u001b[1;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
+ "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 149\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 150\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 151\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 152\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 153\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
+ "\u001b[1;31mRuntimeError\u001b[0m: Command non-existing-command exited with exit status 127"
+ ]
+ }
+ ],
+ "prompt_number": 4
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "for a in spot.automata(\"ltl2tgba -H 'a U b'|\", 'ltl2tgba -f \"syntax U U error\"|'):\n",
+ " display(a)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "display_data",
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f5b141733f0> >"
+ ]
+ },
+ {
+ "ename": "RuntimeError",
+ "evalue": "Command ltl2tgba -f \"syntax U U error\" exited with exit status 2",
+ "output_type": "pyerr",
+ "traceback": [
+ "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[1;31mRuntimeError\u001b[0m Traceback (most recent call last)",
+ "\u001b[1;32m\u001b[0m in \u001b[0;36m\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[1;32mfor\u001b[0m \u001b[0ma\u001b[0m \u001b[1;32min\u001b[0m \u001b[0mspot\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"ltl2tgba -H 'a U b'|\"\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'ltl2tgba -f \"syntax U U error\"|'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 2\u001b[0m \u001b[0mdisplay\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0ma\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
+ "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomata\u001b[1;34m(*filenames)\u001b[0m\n\u001b[0;32m 149\u001b[0m \u001b[1;32mif\u001b[0m \u001b[0mret\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 150\u001b[0m raise RuntimeError(\"Command {} exited with exit status {}\"\n\u001b[1;32m--> 151\u001b[1;33m .format(filename[:-1], ret))\n\u001b[0m\u001b[0;32m 152\u001b[0m \u001b[1;32mreturn\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 153\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
+ "\u001b[1;31mRuntimeError\u001b[0m: Command ltl2tgba -f \"syntax U U error\" exited with exit status 2"
+ ]
+ }
+ ],
+ "prompt_number": 5
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Reading an empty file with `spot.automaton()` is an error."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.automaton('true|')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "RuntimeError",
+ "evalue": "Failed to read automaton from true|",
+ "output_type": "pyerr",
+ "traceback": [
+ "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[1;31mStopIteration\u001b[0m Traceback (most recent call last)",
+ "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[1;34m(filename)\u001b[0m\n\u001b[0;32m 158\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 159\u001b[1;33m \u001b[1;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 160\u001b[0m \u001b[1;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
+ "\u001b[1;31mStopIteration\u001b[0m: ",
+ "\nDuring handling of the above exception, another exception occurred:\n",
+ "\u001b[1;31mRuntimeError\u001b[0m Traceback (most recent call last)",
+ "\u001b[1;32m\u001b[0m in \u001b[0;36m\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mspot\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mautomaton\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m'true|'\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m",
+ "\u001b[1;32m/home-ssd/adl/git/spot/wrap/python/spot.py\u001b[0m in \u001b[0;36mautomaton\u001b[1;34m(filename)\u001b[0m\n\u001b[0;32m 159\u001b[0m \u001b[1;32mreturn\u001b[0m \u001b[0mnext\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mautomata\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 160\u001b[0m \u001b[1;32mexcept\u001b[0m \u001b[0mStopIteration\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 161\u001b[1;33m \u001b[1;32mraise\u001b[0m \u001b[0mRuntimeError\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"Failed to read automaton from {}\"\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mformat\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 162\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 163\u001b[0m def translate(formula, output='tgba', pref='small', level='high',\n",
+ "\u001b[1;31mRuntimeError\u001b[0m: Failed to read automaton from true|"
+ ]
+ }
+ ],
+ "prompt_number": 6
+ }
+ ],
+ "metadata": {}
+ }
+ ]
+}
\ No newline at end of file
diff --git a/wrap/python/tests/run.in b/wrap/python/tests/run.in
old mode 100644
new mode 100755
index a6d07c956..0942da19f
--- a/wrap/python/tests/run.in
+++ b/wrap/python/tests/run.in
@@ -32,6 +32,9 @@ modpath='../.libs:@top_builddir@/src/.libs:@top_builddir@/buddy/src/.libs'
# Python 2.6.
pypath='..:../.libs:@srcdir@/..:@srcdir@/../.libs:$PYTHONPATH'
+PATH="@abs_top_builddir@/src/bin:$PATH"
+export PATH
+
test -z "$1" &&
PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec @PYTHON@