diff --git a/src/hoaparse/fmterror.cc b/src/hoaparse/fmterror.cc index decad775b..7c66e2aaa 100644 --- a/src/hoaparse/fmterror.cc +++ b/src/hoaparse/fmterror.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -24,8 +24,8 @@ namespace spot { bool format_hoa_parse_errors(std::ostream& os, - const std::string& filename, - hoa_parse_error_list& error_list) + const std::string& filename, + hoa_parse_error_list& error_list) { bool printed = false; spot::hoa_parse_error_list::iterator it; diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 88ff09184..14e185148 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -1612,7 +1612,9 @@ static void fix_properties(result_& r) namespace spot { - hoa_stream_parser::hoa_stream_parser(const std::string& name) + hoa_stream_parser::hoa_stream_parser(const std::string& name, + bool ignore_abort) + : filename_(name), ignore_abort_(ignore_abort) { if (hoayyopen(name)) throw std::runtime_error(std::string("Cannot open file ") + name); @@ -1630,6 +1632,7 @@ namespace spot ltl::environment& env, bool debug) { + restart: result_ r; r.h = std::make_shared(); r.h->aut = make_tgba_digraph(dict); @@ -1652,7 +1655,11 @@ namespace spot last_loc = r.h->loc; last_loc.step(); if (r.h->aborted) - return r.h; + { + if (ignore_abort_) + goto restart; + return r.h; + } if (!r.h->aut) return nullptr; if (r.state_names) @@ -1662,6 +1669,29 @@ namespace spot fix_properties(r); return r.h; }; + + tgba_digraph_ptr + hoa_stream_parser::parse_strict(const bdd_dict_ptr& dict, + ltl::environment& env, + bool debug) + { + hoa_parse_error_list pel; + auto a = parse(pel, dict, env, debug); + + if (!pel.empty()) + { + std::ostringstream s; + if (format_hoa_parse_errors(s, filename_, pel)) + throw parse_error(s.str()); + } + if (!a) + return nullptr; + + if (a->aborted) + throw parse_error("parsing aborted"); + + return a->aut; + } } // Local Variables: diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index 5559cc4d9..ba1a3c6ed 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -60,14 +60,21 @@ namespace spot class SPOT_API hoa_stream_parser { spot::location last_loc; + std::string filename_; + bool ignore_abort_; public: - hoa_stream_parser(const std::string& filename); + hoa_stream_parser(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, ltl::environment& env = ltl::default_environment::instance(), bool debug = false); + // Raises a parse_error on any syntax error + tgba_digraph_ptr parse_strict(const bdd_dict_ptr& dict, + ltl::environment& env = + ltl::default_environment::instance(), + bool debug = false); }; /// \brief Build a spot::tgba_digraph from a HOA file or a neverclaim. diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index 411d1df9a..69c6d7aab 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -123,20 +123,11 @@ namespace spot environment& env = default_environment::instance(), bool debug = false); - - - struct SPOT_API parse_error: public std::runtime_error - { - parse_error(const std::string& s): std::runtime_error(s) - { - } - }; - /// \brief A simple wrapper to parse() and parse_lbt(). /// /// This is mostly meant for interactive use. It first tries parse(); if /// this fails it tries parse_lbt(); and if both fails it returns the errors - /// of the first call to parse() as a std::runtime_error(). + /// of the first call to parse() as a parse_error exception. SPOT_API const formula* parse_formula(const std::string& ltl_string, environment& env = default_environment::instance()); diff --git a/src/misc/common.hh b/src/misc/common.hh index 07a42e0c9..478d34308 100644 --- a/src/misc/common.hh +++ b/src/misc/common.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -109,3 +109,15 @@ // Useful when forwarding methods such as: // auto func(int param) SPOT_RETURN(implem_.func(param)); #define SPOT_RETURN(code) -> decltype(code) { return code; } + + +namespace spot +{ + struct SPOT_API parse_error: public std::runtime_error + { + parse_error(const std::string& s) + : std::runtime_error(s) + { + } + }; +} diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 25dc207bf..1a26386f8 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -80,6 +80,46 @@ formula.__init__ = _formula_str_ctor formula.to_str = _formula_to_str formula.show_ast = _render_formula_as_svg +def _tgba_to_str(a, format='hoa', opt=None): + format = format.lower() + if format == 'hoa': + ostr = ostringstream() + hoa_reachable(ostr, a, opt) + return ostr.str() + if format == 'dot': + ostr = ostringstream() + dotty_reachable(ostr, a, opt) + return ostr.str() + if format == 'spin': + ostr = ostringstream() + never_claim_reachable(ostr, a, opt) + return ostr.str() + if format == 'lbtt': + ostr = ostringstream() + lbtt_reachable(ostr, a, bool(opt)) + return ostr.str() + raise ValueError("unknown string format: " + format) + +def _tgba_save(a, filename, format='hoa', opt=None, append=False): + with open(filename, 'a' if append else 'w') as f: + s = a.to_str(format, opt) + f.write(s) + if s[-1] != '\n': + f.write('\n') + return a + +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 translate(formula, output='tgba', pref='small', level='high', complete=False): """Translate a formula into an automaton. diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index f1b0ea01b..41e1f79f7 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -74,6 +74,7 @@ namespace std { #include #include +#include "misc/common.hh" #include "misc/version.hh" #include "misc/minato.hh" #include "misc/optionmap.hh" @@ -135,6 +136,7 @@ namespace std { #include "tgbaalgos/postproc.hh" #include "tgbaalgos/stutter.hh" #include "tgbaalgos/translate.hh" +#include "tgbaalgos/hoa.hh" #include "hoaparse/public.hh" @@ -182,7 +184,7 @@ using namespace spot; try { $action } - catch (const spot::ltl::parse_error& e) + catch (const spot::parse_error& e) { std::string er("\n"); er += e.what(); @@ -278,6 +280,7 @@ namespace spot { %include "tgbaalgos/postproc.hh" %include "tgbaalgos/stutter.hh" %include "tgbaalgos/translate.hh" +%include "tgbaalgos/hoa.hh" %include "hoaparse/public.hh" diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am index b01bf3ed6..1d1ed3b63 100644 --- a/wrap/python/tests/Makefile.am +++ b/wrap/python/tests/Makefile.am @@ -33,6 +33,7 @@ check_SCRIPTS = run TESTS = \ alarm.py \ automata.ipynb \ + automata-io.ipynb \ bddnqueen.py \ formulas.ipynb \ implies.py \ diff --git a/wrap/python/tests/automata-io.ipynb b/wrap/python/tests/automata-io.ipynb new file mode 100644 index 000000000..1d096d370 --- /dev/null +++ b/wrap/python/tests/automata-io.ipynb @@ -0,0 +1,595 @@ +{ + "metadata": { + "name": "", + "signature": "sha256:8a904efb232462e4b08337adba95ad1f6c71494bad4a9d4b3872cbbb3bec76d6" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "code", + "collapsed": false, + "input": [ + "import os\n", + "from IPython.display import display\n", + "# Note that Spot (loaded by the kernel) will store a copy of\n", + "# the environment variables the first time it reads them, so\n", + "# if you change those variables, the new values will be ignored\n", + "# until you restart the kernel.\n", + "os.environ['SPOT_DOTEXTRA'] = 'size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]'\n", + "os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'\n", + "import spot" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a = spot.translate('a U b')\n", + "for fmt in ('hoa', 'spin', 'dot', 'lbtt'):\n", + " print(a.to_str(fmt))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "HOA: v1\n", + "States: 2\n", + "Start: 1\n", + "AP: 2 \"a\" \"b\"\n", + "acc-name: Buchi\n", + "Acceptance: 1 Inf(0)\n", + "properties: trans-labels explicit-labels state-acc deterministic\n", + "properties: stutter-invariant inherently-weak\n", + "--BODY--\n", + "State: 0 {0}\n", + "[t] 0\n", + "State: 1\n", + "[1] 0\n", + "[0&!1] 1\n", + "--END--\n", + "never {\n", + "T0_init:\n", + " if\n", + " :: ((b)) -> goto accept_all\n", + " :: ((a) && (!(b))) -> goto T0_init\n", + " fi;\n", + "accept_all:\n", + " skip\n", + "}\n", + "\n", + "digraph G {\n", + " rankdir=LR\n", + " node [shape=\"circle\"]\n", + " fontname=\"Lato\"\n", + " node [fontname=\"Lato\"]\n", + " edge [fontname=\"Lato\"]\n", + " size=\"10.2,5\" node[style=filled,fillcolor=\"#ffffaa\"] edge[arrowhead=vee, arrowsize=.7]\n", + " I [label=\"\", style=invis, width=0]\n", + " I -> 1\n", + " 0 [label=<0
\u24ff>]\n", + " 0 -> 0 [label=<1>]\n", + " 1 [label=<1>]\n", + " 1 -> 0 [label=]\n", + " 1 -> 1 [label=]\n", + "}\n", + "\n", + "2 1t\n", + "0 1\n", + "1 -1 \"b\"\n", + "0 -1 & \"a\" ! \"b\"\n", + "-1\n", + "1 0\n", + "1 0 -1 t\n", + "-1\n", + "\n" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "a.save('example.aut').save('example.aut', format='lbtt', append=True)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "0\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f156825d240> >" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "!cat example.aut" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "HOA: v1\r\n", + "States: 2\r\n", + "Start: 1\r\n", + "AP: 2 \"a\" \"b\"\r\n", + "acc-name: Buchi\r\n", + "Acceptance: 1 Inf(0)\r\n", + "properties: trans-labels explicit-labels state-acc deterministic\r\n", + "properties: stutter-invariant inherently-weak\r\n", + "--BODY--\r\n", + "State: 0 {0}\r\n", + "[t] 0\r\n", + "State: 1\r\n", + "[1] 0\r\n", + "[0&!1] 1\r\n", + "--END--\r\n", + "2 1t\r\n", + "0 1\r\n", + "1 -1 \"b\"\r\n", + "0 -1 & \"a\" ! \"b\"\r\n", + "-1\r\n", + "1 0\r\n", + "1 0 -1 t\r\n", + "-1\r\n" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for a in spot.automata('example.aut'):\n", + " display(a)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "0\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f156825d210> >" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\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", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f156825d420> >" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Test `--ABORT--`\n", + "----------------" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "%%file example.aut\n", + "HOA: v1\n", + "States: 2\n", + "Start: 1\n", + "AP: 2 \"a\" \"b\"\n", + "acc-name: Buchi\n", + "Acceptance: 1 Inf(0)\n", + "--BODY--\n", + "State: 0 {0}\n", + "[t] 0\n", + "--ABORT-- /* the previous automaton should be ignored */\n", + "HOA: v1\n", + "States: 2\n", + "Start: 1\n", + "AP: 2 \"a\" \"b\"\n", + "Acceptance: 1 Inf(0)\n", + "--BODY--\n", + "State: 0 {0}\n", + "[t] 0\n", + "State: 1\n", + "[1] 0\n", + "[0&!1] 1\n", + "--END--" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "Overwriting example.aut\n" + ] + } + ], + "prompt_number": 6 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for a in spot.automata('example.aut'):\n", + " display(a)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "0\n", + "\u24ff\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f156825d630> >" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Test syntax errors\n", + "------------------" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "%%file example.aut\n", + "HOA: v1\n", + "States: 2\n", + "Start: 1\n", + "AP: 2 \"a\" \"b\"\n", + "acc-name: Buchi\n", + "Acceptance: 1 Inf(0)\n", + "--BODY--\n", + "State: 0 {0}\n", + "[t] 1\n", + "State: 1\n", + "[t] 1\n", + "--END--\n", + "HOA: v1\n", + "States: 2\n", + "Start: 1\n", + "AP: 2 \"a\" \"b\"\n", + "Acceptance: 1 Inf(0)\n", + "--BODY--\n", + "State: 0 {0}\n", + "[a] 3\n", + "State: 1\n", + "[1] 0\n", + "[0&!1] 1\n", + "--END--" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "Overwriting example.aut\n" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "for a in spot.automata('example.aut'):\n", + " display(a)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "0\n", + "\u24ff\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f156825d510> >" + ] + }, + { + "ename": "SyntaxError", + "evalue": "\nexample.aut:20.2: syntax error, unexpected identifier\nexample.aut:20.1-3: ignoring this invalid label\nexample.aut:20.5: state number is larger than state count...\nexample.aut:14.1-9: ... declared here.\n ()", + "output_type": "pyerr", + "traceback": [ + "\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \nexample.aut:20.2: syntax error, unexpected identifier\nexample.aut:20.1-3: ignoring this invalid label\nexample.aut:20.5: state number is larger than state count...\nexample.aut:14.1-9: ... declared here.\n\n" + ] + } + ], + "prompt_number": 9 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "rm example.aut" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 10 + } + ], + "metadata": {} + } + ] +} \ No newline at end of file