diff --git a/NEWS b/NEWS index a72256700..457ea51ac 100644 --- a/NEWS +++ b/NEWS @@ -174,7 +174,7 @@ New in spot 1.99b (not yet released) - There is a parser for the HOA format (http://adl.github.io/hoaf/) available as a - spot::hoa_stream_parser object or spot::hoa_parse() function. + spot::automaton_stream_parser object or spot::parse_aut() function. The former version is able to parse a stream of automata in order to do batch processing. This format can be output by all tools (since Spot 1.2.5) using the --hoa option, and it can be diff --git a/README b/README index 7c340af58..b79eca2dc 100644 --- a/README +++ b/README @@ -139,7 +139,6 @@ src/ Sources for libspot. man/ Man pages for the above tools. dstarparse/ Parser for the output of ltl2dstar. graph/ Graph representations. - hoaparse/ Parser for HOA automata and Spin's never claims. kripke/ Kripke Structure interface. kripkeparse/ Parser for explicit Kripke. ltlast/ LTL abstract syntax tree (including nodes for ELTL). @@ -147,6 +146,7 @@ src/ Sources for libspot. ltlparse/ Parser for LTL formulae. ltlvisit/ Visitors of LTL formulae. misc/ Miscellaneous support files. + parseaut/ Parser for HOA automata and Spin's never claims. priv/ Private algorithms, used internally but not exported. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. diff --git a/configure.ac b/configure.ac index aa1ae109f..3841858e1 100644 --- a/configure.ac +++ b/configure.ac @@ -202,7 +202,7 @@ AC_CONFIG_FILES([ src/dstarparse/Makefile src/kripke/Makefile src/graph/Makefile - src/hoaparse/Makefile + src/parseaut/Makefile src/ltlast/Makefile src/ltlenv/Makefile src/ltlparse/Makefile diff --git a/doc/org/tut20.org b/doc/org/tut20.org index af3752007..407d79cce 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -123,40 +123,39 @@ State: 4 * C++ Parsing an automaton is almost similar to [[file:tut01.org][parsing an LTL formula]]. The -=hoa_parse()= function (despite the name, it can actually read never -claims, or the LBTT or HOA formats) takes a filename, a reference to a -=hoa_parse_error_list= object to populate (should errors be found) and +=parse_aut()= function takes a filename, a reference to a +=parse_aut_error_list= object to populate (should errors be found) and a BDD dictionary (to be discussed later on this page). It returns a shared pointer to a structure that has two fields: =aborted= is a Boolean telling if the input automaton was voluntarily aborted (a feature of [[file:hoa.org][the HOA format]]), and =aut= is the actual automaton. The -shared pointer returned by =hoa_parse()= might be null (in which case -the the =hoa_parse_error_list= is guaranteed not to be empty), but +shared pointer returned by =parse_aut()= might be null (in which case +the the =parse_aut_error_list= is guaranteed not to be empty), but since the parser performs some error recovery it is likely that an automaton is returned even in the presence of parse errors. #+BEGIN_SRC C++ :results verbatim :exports both #include #include - #include "hoaparse/public.hh" + #include "parseaut/public.hh" #include "twaalgos/hoa.hh" int main() { std::string input = "tut20.never"; - spot::hoa_parse_error_list pel; + spot::parse_aut_error_list pel; spot::bdd_dict_ptr dict = spot::make_bdd_dict(); - spot::hoa_aut_ptr h = hoa_parse(input, pel, dict); - if (spot::format_hoa_parse_errors(std::cerr, input, pel)) + spot::parsed_aut_ptr pa = parse_aut(input, pel, dict); + if (spot::format_parse_aut_errors(std::cerr, input, pel)) return 1; // This cannot occur when reading a never claim, but // it could while reading a HOA file. - if (h->aborted) + if (pa->aborted) { std::cerr << "--ABORT-- read" << '\n'; return 1; } - spot::print_hoa(std::cout, h->aut) << '\n'; + spot::print_hoa(std::cout, pa->aut) << '\n'; return 0; } #+END_SRC @@ -214,11 +213,11 @@ There are actually different C++ interfaces to the automaton parser, depending on your use case. For instance the parser is able to read a stream of automata stored in the same file, so that they could be processed in a loop. For this, you would instanciate a -=hoa_stream_parser= object and call its =parse()= method in a loop. -Each call to this method will either return one automaton, or -=nullptr= if there is no more automaton to read. The =hoa_parse()= -function is actually a simple wrapper that instanciate -=hoa_stream_parser= and calls =parse()= once. +=automaton_stream_parser= object and call its =parse()= method in a +loop. Each call to this method will either return one automaton, or +=nullptr= if there is no more automaton to read. The =parse_aut()= +function is actually a simple convenience wrapper that instanciate +an =automaton_stream_parser= and calls its =parse()= method once. In Python, you can easily iterate over a file containing multiple @@ -284,7 +283,8 @@ print(spot.automaton('spin -f "[]<>p0" |').to_str('lbtt')) : - a string that includes new lines, in which case it is assumed - to describe an automaton, and is passed directly to the parser: + to describe an automaton (or multiple automata) and is + passed directly to the parser: #+BEGIN_SRC python :results output :exports both import spot diff --git a/src/Makefile.am b/src/Makefile.am index efb0babbf..edfdcf75f 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -26,7 +26,7 @@ AUTOMAKE_OPTIONS = subdir-objects # end, after building '.' (since the current directory contains # libspot.la needed by the tests) SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph twa \ - twaalgos ta taalgos kripke kripkeparse dstarparse hoaparse \ + twaalgos ta taalgos kripke kripkeparse dstarparse parseaut \ . bin tests sanity lib_LTLIBRARIES = libspot.la @@ -34,7 +34,7 @@ libspot_la_SOURCES = libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined libspot_la_LIBADD = \ dstarparse/libdstarparse.la \ - hoaparse/libhoaparse.la \ + parseaut/libparseaut.la \ kripke/libkripke.la \ kripkeparse/libkripkeparse.la \ ltlast/libltlast.la \ diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index d408a7202..2ef5a33c0 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -43,7 +43,7 @@ #include "misc/optionmap.hh" #include "misc/timer.hh" #include "misc/random.hh" -#include "hoaparse/public.hh" +#include "parseaut/public.hh" #include "ltlvisit/exclusive.hh" #include "twaalgos/remprop.hh" #include "twaalgos/randomize.hh" @@ -494,7 +494,7 @@ namespace } int - process_automaton(const spot::const_hoa_aut_ptr& haut, + process_automaton(const spot::const_parsed_aut_ptr& haut, const char* filename) { spot::stopwatch sw; @@ -618,7 +618,7 @@ namespace } int - aborted(const spot::const_hoa_aut_ptr& h, const char* filename) + aborted(const spot::const_parsed_aut_ptr& h, const char* filename) { std::cerr << filename << ':' << h->loc << ": aborted input automaton\n"; return 2; @@ -627,8 +627,8 @@ namespace int process_file(const char* filename) { - spot::hoa_parse_error_list pel; - auto hp = spot::hoa_stream_parser(filename); + spot::parse_aut_error_list pel; + auto hp = spot::automaton_stream_parser(filename); int err = 0; @@ -638,7 +638,7 @@ namespace auto haut = hp.parse(pel, opt->dict); if (!haut && pel.empty()) break; - if (spot::format_hoa_parse_errors(std::cerr, filename, pel)) + if (spot::format_parse_aut_errors(std::cerr, filename, pel)) err = 2; if (!haut) error(2, 0, "failed to read automaton from %s", filename); diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 6de83be0f..160ce796c 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -278,7 +278,7 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, int loc, // Time and input automaton for statistics double time, - const spot::const_hoa_aut_ptr& haut) + const spot::const_parsed_aut_ptr& haut) { if (opt_check) { diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index cd24cac7b..c742adc1c 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -24,7 +24,7 @@ #include #include -#include "hoaparse/public.hh" +#include "parseaut/public.hh" #include "twaalgos/stats.hh" #include "twaalgos/sccinfo.hh" @@ -105,7 +105,7 @@ public: /// The \a f argument is not needed if the Formula does not need /// to be output. std::ostream& - print(const spot::const_hoa_aut_ptr& haut, + print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, const spot::ltl::formula* f, const char* filename, int loc, double run_time) @@ -231,7 +231,7 @@ public: int loc = -1, // Time and input automaton for statistics double time = 0.0, - const spot::const_hoa_aut_ptr& haut = nullptr); + const spot::const_parsed_aut_ptr& haut = nullptr); void add_stat(char c, const spot::printable* p); }; diff --git a/src/bin/common_conv.cc b/src/bin/common_conv.cc index 5429fe01c..8d9b3729e 100644 --- a/src/bin/common_conv.cc +++ b/src/bin/common_conv.cc @@ -20,7 +20,7 @@ #include "common_conv.hh" #include #include "error.h" -#include "hoaparse/public.hh" +#include "parseaut/public.hh" int to_int(const char* s) @@ -73,9 +73,9 @@ to_probability(const char* s) spot::twa_graph_ptr read_automaton(const char* filename, spot::bdd_dict_ptr& dict) { - spot::hoa_parse_error_list pel; - auto p = spot::hoa_parse(filename, pel, dict); - if (spot::format_hoa_parse_errors(std::cerr, filename, pel) + spot::parse_aut_error_list pel; + auto p = spot::parse_aut(filename, pel, dict); + if (spot::format_parse_aut_errors(std::cerr, filename, pel) || !p || p->aborted) error(2, 0, "failed to read automaton from %s", filename); return std::move(p->aut); diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index c699997a5..6958c8d99 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -38,7 +38,7 @@ #include "common_file.hh" #include "common_finput.hh" #include "dstarparse/public.hh" -#include "hoaparse/public.hh" +#include "parseaut/public.hh" #include "ltlast/unop.hh" #include "ltlvisit/print.hh" #include "ltlvisit/apcollect.hh" @@ -633,9 +633,9 @@ namespace } case printable_result_filename::Hoa: // Will also read neverclaims { - spot::hoa_parse_error_list pel; + spot::parse_aut_error_list pel; std::string filename = output.val()->name(); - auto aut = spot::hoa_parse(filename, pel, dict); + auto aut = spot::parse_aut(filename, pel, dict); if (!pel.empty()) { status_str = "parse error"; @@ -643,7 +643,7 @@ namespace es = -1; std::ostream& err = global_error(); err << "error: failed to parse the produced automaton.\n"; - spot::format_hoa_parse_errors(err, filename, pel); + spot::format_parse_aut_errors(err, filename, pel); end_error(); res = nullptr; } diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index 7c9009fa1..362a4da8e 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -40,7 +40,7 @@ #include "misc/timer.hh" #include "twaalgos/lbtt.hh" #include "twaalgos/relabel.hh" -#include "hoaparse/public.hh" +#include "parseaut/public.hh" #include "dstarparse/public.hh" const char argp_program_doc[] ="\ @@ -192,15 +192,15 @@ namespace case printable_result_filename::Hoa: { // Will also read neverclaims/LBTT - spot::hoa_parse_error_list pel; + spot::parse_aut_error_list pel; std::string filename = output.val()->name(); - auto aut = spot::hoa_parse(filename, pel, dict); + auto aut = spot::parse_aut(filename, pel, dict); if (!pel.empty()) { problem = true; std::cerr << "error: failed to parse the automaton " "produced by \"" << cmd << "\".\n"; - spot::format_hoa_parse_errors(std::cerr, filename, pel); + spot::format_parse_aut_errors(std::cerr, filename, pel); res = nullptr; } else if (!aut) diff --git a/src/hoaparse/.gitignore b/src/hoaparse/.gitignore deleted file mode 100644 index 2ed9b3c24..000000000 --- a/src/hoaparse/.gitignore +++ /dev/null @@ -1,7 +0,0 @@ -position.hh -hoaparse.cc -hoaparse.output -hoaparse.hh -hoascan.cc -stack.hh -location.hh diff --git a/src/parseaut/.gitignore b/src/parseaut/.gitignore new file mode 100644 index 000000000..9f4528f06 --- /dev/null +++ b/src/parseaut/.gitignore @@ -0,0 +1,7 @@ +position.hh +parseaut.cc +parseaut.output +parseaut.hh +scanaut.cc +stack.hh +location.hh diff --git a/src/hoaparse/Makefile.am b/src/parseaut/Makefile.am similarity index 88% rename from src/hoaparse/Makefile.am rename to src/parseaut/Makefile.am index a8dc390eb..ec4dd50f6 100644 --- a/src/hoaparse/Makefile.am +++ b/src/parseaut/Makefile.am @@ -21,17 +21,17 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT # Disable -Werror because too many versions of flex yield warnings. AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) -hoaparsedir = $(pkgincludedir)/hoaparse +parseautdir = $(pkgincludedir)/parseaut -hoaparse_HEADERS = public.hh +parseaut_HEADERS = public.hh -noinst_LTLIBRARIES = libhoaparse.la +noinst_LTLIBRARIES = libparseaut.la -HOAPARSE_YY = hoaparse.yy -FROM_HOAPARSE_YY_MAIN = hoaparse.cc +HOAPARSE_YY = parseaut.yy +FROM_HOAPARSE_YY_MAIN = parseaut.cc FROM_HOAPARSE_YY_OTHERS = \ stack.hh \ - hoaparse.hh + parseaut.hh FROM_HOAPARSE_YY = $(FROM_HOAPARSE_YY_MAIN) $(FROM_HOAPARSE_YY_OTHERS) @@ -50,8 +50,8 @@ $(FROM_HOAPARSE_YY_OTHERS): $(HOAPARSE_YY) EXTRA_DIST = $(HOAPARSE_YY) -libhoaparse_la_SOURCES = \ +libparseaut_la_SOURCES = \ fmterror.cc \ $(FROM_HOAPARSE_YY) \ - hoascan.ll \ + scanaut.ll \ parsedecl.hh diff --git a/src/hoaparse/fmterror.cc b/src/parseaut/fmterror.cc similarity index 90% rename from src/hoaparse/fmterror.cc rename to src/parseaut/fmterror.cc index 7c66e2aaa..26e504fd0 100644 --- a/src/hoaparse/fmterror.cc +++ b/src/parseaut/fmterror.cc @@ -23,12 +23,12 @@ namespace spot { bool - format_hoa_parse_errors(std::ostream& os, + format_parse_aut_errors(std::ostream& os, const std::string& filename, - hoa_parse_error_list& error_list) + parse_aut_error_list& error_list) { bool printed = false; - spot::hoa_parse_error_list::iterator it; + spot::parse_aut_error_list::iterator it; for (it = error_list.begin(); it != error_list.end(); ++it) { if (filename != "-") diff --git a/src/hoaparse/hoaparse.yy b/src/parseaut/parseaut.yy similarity index 97% rename from src/hoaparse/hoaparse.yy rename to src/parseaut/parseaut.yy index 86ea5f511..c45e5cc14 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/parseaut/parseaut.yy @@ -24,7 +24,7 @@ %name-prefix "hoayy" %debug %error-verbose -%lex-param { spot::hoa_parse_error_list& error_list } +%lex-param { spot::parse_aut_error_list& error_list } %define api.location.type "spot::location" %code requires @@ -68,7 +68,7 @@ bool used = false; spot::location used_loc; }; - spot::hoa_aut_ptr h; + spot::parsed_aut_ptr h; spot::ltl::environment* env; formula_cache fcache; named_tgba_t* namer = nullptr; @@ -127,7 +127,7 @@ } } -%parse-param {spot::hoa_parse_error_list& error_list} +%parse-param {spot::parse_aut_error_list& error_list} %parse-param {result_& res} %parse-param {spot::location initial_loc} @@ -150,7 +150,7 @@ #include "ltlast/constant.hh" #include "ltlparse/public.hh" - /* hoaparse.hh and parsedecl.hh include each other recursively. + /* parseaut.hh and parsedecl.hh include each other recursively. We must ensure that YYSTYPE is declared (by the above %union) before parsedecl.hh uses it. */ #include "parsedecl.hh" @@ -1664,46 +1664,46 @@ static void fix_properties(result_& r) namespace spot { - hoa_stream_parser::hoa_stream_parser(const std::string& name, - bool ignore_abort) + automaton_stream_parser::automaton_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); } - hoa_stream_parser::hoa_stream_parser(int fd, - const std::string& name, - bool ignore_abort) + automaton_stream_parser::automaton_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(const char* data, - const std::string& filename, - bool ignore_abort) + automaton_stream_parser::automaton_stream_parser(const char* data, + const std::string& filename, + bool ignore_abort) : filename_(filename), ignore_abort_(ignore_abort) { hoayystring(data); } - hoa_stream_parser::~hoa_stream_parser() + automaton_stream_parser::~automaton_stream_parser() { hoayyclose(); } - hoa_aut_ptr - hoa_stream_parser::parse(hoa_parse_error_list& error_list, - const bdd_dict_ptr& dict, - ltl::environment& env, - bool debug) + parsed_aut_ptr + automaton_stream_parser::parse(parse_aut_error_list& error_list, + const bdd_dict_ptr& dict, + ltl::environment& env, + bool debug) { restart: result_ r; - r.h = std::make_shared(); + r.h = std::make_shared(); r.h->aut = make_twa_graph(dict); r.env = &env; hoayy::parser parser(error_list, r, last_loc); @@ -1740,17 +1740,17 @@ namespace spot }; twa_graph_ptr - hoa_stream_parser::parse_strict(const bdd_dict_ptr& dict, - ltl::environment& env, - bool debug) + automaton_stream_parser::parse_strict(const bdd_dict_ptr& dict, + ltl::environment& env, + bool debug) { - hoa_parse_error_list pel; + parse_aut_error_list pel; auto a = parse(pel, dict, env, debug); if (!pel.empty()) { std::ostringstream s; - if (format_hoa_parse_errors(s, filename_, pel)) + if (format_parse_aut_errors(s, filename_, pel)) throw parse_error(s.str()); } if (!a) diff --git a/src/hoaparse/parsedecl.hh b/src/parseaut/parsedecl.hh similarity index 94% rename from src/hoaparse/parsedecl.hh rename to src/parseaut/parsedecl.hh index 62eac975c..22efdd68a 100644 --- a/src/hoaparse/parsedecl.hh +++ b/src/parseaut/parsedecl.hh @@ -20,13 +20,13 @@ #pragma once #include -#include "hoaparse.hh" +#include "parseaut.hh" #include "misc/location.hh" # define YY_DECL \ int hoayylex(hoayy::parser::semantic_type *yylval, \ spot::location *yylloc, \ - spot::hoa_parse_error_list& error_list) + spot::parse_aut_error_list& error_list) YY_DECL; namespace spot diff --git a/src/hoaparse/public.hh b/src/parseaut/public.hh similarity index 73% rename from src/hoaparse/public.hh rename to src/parseaut/public.hh index 99261a79d..4fc75efb9 100644 --- a/src/hoaparse/public.hh +++ b/src/parseaut/public.hh @@ -35,17 +35,17 @@ namespace spot #ifndef SWIG /// \brief A parse diagnostic with its location. - typedef std::pair hoa_parse_error; + typedef std::pair parse_aut_error; /// \brief A list of parser diagnostics, as filled by parse. - typedef std::list hoa_parse_error_list; + typedef std::list parse_aut_error_list; #else - // Turn hoa_parse_error_list into an opaque type for Swig. - struct hoa_parse_error_list {}; + // Turn parse_aut_error_list into an opaque type for Swig. + struct parse_aut_error_list {}; #endif /// \brief Temporary encoding of an omega automaton produced by - /// ltl2hoa. - struct SPOT_API hoa_aut + /// the parser. + struct SPOT_API parsed_aut { // Transition structure of the automaton. // This is encoded as a TGBA without acceptance condition. @@ -54,35 +54,36 @@ namespace spot spot::location loc; }; - typedef std::shared_ptr hoa_aut_ptr; - typedef std::shared_ptr const_hoa_aut_ptr; + typedef std::shared_ptr parsed_aut_ptr; + typedef std::shared_ptr const_parsed_aut_ptr; - class SPOT_API hoa_stream_parser + class SPOT_API automaton_stream_parser { spot::location last_loc; std::string filename_; bool ignore_abort_; public: - hoa_stream_parser(const std::string& filename, bool ignore_abort = false); + automaton_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); + automaton_stream_parser(int fd, const std::string& filename, + bool ignore_abort = false); // Read from a buffer - hoa_stream_parser(const char* data, - 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); + automaton_stream_parser(const char* data, + const std::string& filename, + bool ignore_abort = false); + ~automaton_stream_parser(); + parsed_aut_ptr parse(parse_aut_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 twa_graph_ptr parse_strict(const bdd_dict_ptr& dict, - ltl::environment& env = - ltl::default_environment::instance(), - bool debug = false); + ltl::environment& env = + ltl::default_environment::instance(), + bool debug = false); }; /// \brief Build a spot::twa_graph from a HOA file or a neverclaim. @@ -112,16 +113,16 @@ namespace spot /// spot@lrde.epita.fr. /// /// \warning This function is not reentrant. - inline hoa_aut_ptr - hoa_parse(const std::string& filename, - hoa_parse_error_list& error_list, + inline parsed_aut_ptr + parse_aut(const std::string& filename, + parse_aut_error_list& error_list, const bdd_dict_ptr& dict, ltl::environment& env = ltl::default_environment::instance(), bool debug = false) { try { - hoa_stream_parser p(filename); + automaton_stream_parser p(filename); return p.parse(error_list, dict, env, debug); } catch (std::runtime_error& e) @@ -131,16 +132,16 @@ namespace spot } } - /// \brief Format diagnostics produced by spot::hoa_parse. + /// \brief Format diagnostics produced by spot::parse_aut. /// \param os Where diagnostics should be output. /// \param filename The filename that should appear in the diagnostics. /// \param error_list The error list filled by spot::ltl::parse while /// parsing \a ltl_string. /// \return \c true iff any diagnostic was output. SPOT_API bool - format_hoa_parse_errors(std::ostream& os, + format_parse_aut_errors(std::ostream& os, const std::string& filename, - hoa_parse_error_list& error_list); + parse_aut_error_list& error_list); /// @} } diff --git a/src/hoaparse/hoascan.ll b/src/parseaut/scanaut.ll similarity index 97% rename from src/hoaparse/hoascan.ll rename to src/parseaut/scanaut.ll index cecb79160..5d7695d93 100644 --- a/src/hoaparse/hoascan.ll +++ b/src/parseaut/scanaut.ll @@ -25,7 +25,7 @@ %{ #include #include -#include "hoaparse/parsedecl.hh" +#include "parseaut/parsedecl.hh" #include "misc/escape.hh" #define YY_USER_ACTION yylloc->columns(yyleng); @@ -62,7 +62,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* yylval->num = n; if (errno || yylval->num != n) { - error_list.push_back(spot::hoa_parse_error(*yylloc, "value too large")); + error_list.push_back(spot::parse_aut_error(*yylloc, "value too large")); yylval->num = 0; } return end; @@ -96,7 +96,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* if (errno || yylval->num != n) { error_list.push_back( - spot::hoa_parse_error(*yylloc, + spot::parse_aut_error(*yylloc, "value too large")); yylval->num = 0; } @@ -258,7 +258,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* <> { BEGIN(orig_cond); error_list.push_back( - spot::hoa_parse_error(*yylloc, + spot::parse_aut_error(*yylloc, "unclosed comment")); return 0; } @@ -289,7 +289,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* [^\\\"\n\r]+ s.append(yytext, yyleng); <> { error_list.push_back( - spot::hoa_parse_error(*yylloc, + spot::parse_aut_error(*yylloc, "unclosed string")); BEGIN(orig_cond); yylval->str = new std::string(s); @@ -326,7 +326,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* [^()\n\r]+ yylval->str->append(yytext, yyleng); <> { error_list.push_back( - spot::hoa_parse_error(*yylloc, + spot::parse_aut_error(*yylloc, "missing closing parenthese")); yylval->str->append(parent_level, ')'); BEGIN(in_NEVER); diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index b87aaa435..b8bedfc51 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -171,7 +171,7 @@ TESTS_twa = \ nondet.test \ det.test \ neverclaimread.test \ - hoaparse.test \ + parseaut.test \ optba.test \ complete.test \ remfin.test \ diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc index 525e7e17a..a2a5b443d 100644 --- a/src/tests/complementation.cc +++ b/src/tests/complementation.cc @@ -21,7 +21,7 @@ #include #include "twaalgos/dot.hh" #include "twaalgos/hoa.hh" -#include "hoaparse/public.hh" +#include "parseaut/public.hh" #include "twa/twaproduct.hh" #include "twaalgos/gtec/gtec.hh" #include "twaalgos/ltl2tgba_fm.hh" @@ -121,9 +121,9 @@ int main(int argc, char* argv[]) if (print_automaton || print_safra) { spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::hoa_parse_error_list pel; - auto h = spot::hoa_parse(file, pel, dict, env); - if (spot::format_hoa_parse_errors(std::cerr, file, pel)) + spot::parse_aut_error_list pel; + auto h = spot::parse_aut(file, pel, dict, env); + if (spot::format_parse_aut_errors(std::cerr, file, pel)) return 2; spot::twa_graph_ptr a = h->aut; @@ -178,10 +178,10 @@ int main(int argc, char* argv[]) } else { - spot::hoa_parse_error_list pel; + spot::parse_aut_error_list pel; spot::ltl::environment& env(spot::ltl::default_environment::instance()); - auto h = spot::hoa_parse(file, pel, dict, env); - if (spot::format_hoa_parse_errors(std::cerr, file, pel)) + auto h = spot::parse_aut(file, pel, dict, env); + if (spot::format_parse_aut_errors(std::cerr, file, pel)) return 2; a = h->aut; } diff --git a/src/tests/ltl2tgba.cc b/src/tests/ltl2tgba.cc index 840675544..c84c2700b 100644 --- a/src/tests/ltl2tgba.cc +++ b/src/tests/ltl2tgba.cc @@ -40,7 +40,7 @@ #include "twa/twaproduct.hh" #include "twaalgos/reducerun.hh" #include "dstarparse/public.hh" -#include "hoaparse/public.hh" +#include "parseaut/public.hh" #include "twaalgos/dupexp.hh" #include "twaalgos/minimize.hh" #include "taalgos/minimize.hh" @@ -608,9 +608,9 @@ checked_main(int argc, char** argv) tm.start("reading -P's argument"); spot::dstar_parse_error_list pel; - auto daut = spot::hoa_parse(argv[formula_index] + 2, pel, + auto daut = spot::parse_aut(argv[formula_index] + 2, pel, dict, env, debug_opt); - if (spot::format_hoa_parse_errors(std::cerr, + if (spot::format_parse_aut_errors(std::cerr, argv[formula_index] + 2, pel)) return 2; daut->aut->merge_transitions(); @@ -1014,9 +1014,9 @@ checked_main(int argc, char** argv) { spot::dstar_parse_error_list pel; tm.start("parsing hoa"); - auto daut = spot::hoa_parse(input, pel, dict, env, debug_opt); + auto daut = spot::parse_aut(input, pel, dict, env, debug_opt); tm.stop("parsing hoa"); - if (spot::format_hoa_parse_errors(std::cerr, input, pel)) + if (spot::format_parse_aut_errors(std::cerr, input, pel)) return 2; daut->aut->merge_transitions(); a = daut->aut; diff --git a/src/tests/hoaparse.test b/src/tests/parseaut.test similarity index 100% rename from src/tests/hoaparse.test rename to src/tests/parseaut.test diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 02474ba35..883bb7c11 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -567,7 +567,7 @@ EOF # autfilt should complain about the input (we only check the exit # status here, because the actual error messages are tested in -# hoaparse.test) and produce a valid output with the number of states +# parseaut.test) and produce a valid output with the number of states # fixed, and the missing state definitions. $autfilt -H input >output1 && exit 1 diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 43dc972fd..653f888bb 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -587,12 +587,12 @@ elif translator == 'l3': if ret != 0: unbufprint('
ltl3ba exited with error %s
' % ret) finish() - tpel = spot.empty_hoa_parse_error_list() - automaton = spot.hoa_parse(l3file, tpel, dict, env) + tpel = spot.empty_parse_aut_error_list() + automaton = spot.parse_aut(l3file, tpel, dict, env) if tpel: unbufprint('''
failed to read ltl3ba's output
''') unbufprint('
') - err = spot.format_hoa_parse_errors(spot.get_cout(), "output", tpel) + err = spot.format_parse_aut_errors(spot.get_cout(), "output", tpel) unbufprint('
') automaton = 0 finish() diff --git a/wrap/python/spot.py b/wrap/python/spot.py index c08d2a093..ea0afffee 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -176,13 +176,14 @@ def automata(*filenames): if filename[-1] == '|': proc = subprocess.Popen(filename[:-1], shell=True, stdout=subprocess.PIPE) - p = hoa_stream_parser(proc.stdout.fileno(), filename, True) + p = automaton_stream_parser(proc.stdout.fileno(), + filename, True) elif '\n' in filename: proc = None - p = hoa_stream_parser(filename, "", True) + p = automaton_stream_parser(filename, "", True) else: proc = None - p = hoa_stream_parser(filename, True) + p = automaton_stream_parser(filename, True) a = True while a: # This returns None when we reach the end of the file. diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index fb4c74e1a..bcd3f3402 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -39,7 +39,7 @@ // git grep 'typedef.*std::shared_ptr' | grep -v const | // sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g' %shared_ptr(spot::dstar_aut) -%shared_ptr(spot::hoa_aut) +%shared_ptr(spot::parsed_aut) %shared_ptr(spot::fair_kripke) %shared_ptr(spot::kripke) %shared_ptr(spot::kripke_explicit) @@ -143,7 +143,7 @@ namespace std { #include "twaalgos/hoa.hh" #include "twaalgos/dtgbasat.hh" -#include "hoaparse/public.hh" +#include "parseaut/public.hh" #include "ta/ta.hh" #include "ta/tgta.hh" @@ -308,7 +308,7 @@ namespace std { %include "twaalgos/hoa.hh" %include "twaalgos/dtgbasat.hh" -%include "hoaparse/public.hh" +%include "parseaut/public.hh" %include "ta/ta.hh" %include "ta/tgta.hh" @@ -394,10 +394,10 @@ empty_parse_error_list() return l; } -spot::hoa_parse_error_list -empty_hoa_parse_error_list() +spot::parse_aut_error_list +empty_parse_aut_error_list() { - hoa_parse_error_list l; + parse_aut_error_list l; return l; } @@ -467,7 +467,7 @@ __bool__() } -%extend spot::hoa_parse_error_list { +%extend spot::parse_aut_error_list { bool __nonzero__() diff --git a/wrap/python/tests/automata-io.ipynb b/wrap/python/tests/automata-io.ipynb index a08bf0bbd..2bbdaf162 100644 --- a/wrap/python/tests/automata-io.ipynb +++ b/wrap/python/tests/automata-io.ipynb @@ -759,8 +759,8 @@ "\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'example.aut'\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 216\u001b[0m See `spot.automata()` for a list of supported formats.\"\"\"\n\u001b[0;32m 217\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 218\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 219\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 220\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 183\u001b[0m \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 184\u001b[0m \u001b[0mproc\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 185\u001b[1;33m \u001b[0mp\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mhoa_stream_parser\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 186\u001b[0m \u001b[0ma\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 187\u001b[0m \u001b[1;32mwhile\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_impl.py\u001b[0m in \u001b[0;36m__init__\u001b[1;34m(self, *args)\u001b[0m\n\u001b[0;32m 2452\u001b[0m \u001b[0m__repr__\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0m_swig_repr\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 2453\u001b[0m \u001b[1;32mdef\u001b[0m \u001b[0m__init__\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;33m*\u001b[0m\u001b[0margs\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m-> 2454\u001b[1;33m \u001b[0mthis\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0m_spot_impl\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mnew_hoa_stream_parser\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m*\u001b[0m\u001b[0margs\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 2455\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mthis\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mappend\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mthis\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 2456\u001b[0m \u001b[1;32mexcept\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mthis\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mthis\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 183\u001b[0m \u001b[1;32melse\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 184\u001b[0m \u001b[0mproc\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mNone\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m--> 185\u001b[1;33m \u001b[0mp\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mautomaton_stream_parser\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mfilename\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 186\u001b[0m \u001b[0ma\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;32mTrue\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 187\u001b[0m \u001b[1;32mwhile\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_impl.py\u001b[0m in \u001b[0;36m__init__\u001b[1;34m(self, *args)\u001b[0m\n\u001b[0;32m 2452\u001b[0m \u001b[0m__repr__\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0m_swig_repr\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 2453\u001b[0m \u001b[1;32mdef\u001b[0m \u001b[0m__init__\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mself\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;33m*\u001b[0m\u001b[0margs\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m:\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m-> 2454\u001b[1;33m \u001b[0mthis\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0m_spot_impl\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mnew_automaton_stream_parser\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m*\u001b[0m\u001b[0margs\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m 2455\u001b[0m \u001b[1;32mtry\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mthis\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mappend\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mthis\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m 2456\u001b[0m \u001b[1;32mexcept\u001b[0m\u001b[1;33m:\u001b[0m \u001b[0mself\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mthis\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mthis\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n", "\u001b[1;31mRuntimeError\u001b[0m: Cannot open file example.aut" ] } diff --git a/wrap/python/tests/parsetgba.py b/wrap/python/tests/parsetgba.py index c225d320f..58d52e0dc 100755 --- a/wrap/python/tests/parsetgba.py +++ b/wrap/python/tests/parsetgba.py @@ -32,8 +32,8 @@ out = open(filename, 'w+') out.write(contents) out.close() -p = spot.empty_hoa_parse_error_list() -a = spot.hoa_parse(filename, p, spot.make_bdd_dict()) +p = spot.empty_parse_aut_error_list() +a = spot.parse_aut(filename, p, spot.make_bdd_dict()) assert not p