diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 852a09dd8..8a6b6314b 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -292,17 +292,10 @@ namespace SPOT_UNREACHABLE(); } - int - process_file(const char* filename) + process_automaton(const spot::const_hoa_aut_ptr& haut, + const char* filename) { - spot::hoa_parse_error_list pel; - auto haut = spot::hoa_parse(filename, pel, spot::make_bdd_dict()); - if (spot::format_hoa_parse_errors(std::cerr, filename, pel)) - return 2; - if (!haut) - error(2, 0, "failed to read automaton from %s", filename); - spot::stopwatch sw; sw.start(); auto aut = post.run(haut->aut, nullptr); @@ -337,6 +330,32 @@ namespace flush_cout(); return 0; } + + + int + process_file(const char* filename) + { + spot::hoa_parse_error_list pel; + auto b = spot::make_bdd_dict(); + auto hp = spot::hoa_stream_parser(filename); + + int err = 0; + + for (;;) + { + auto haut = hp.parse(pel, b); + if (!haut && pel.empty()) + break; + if (spot::format_hoa_parse_errors(std::cerr, filename, pel)) + err = 2; + if (!haut) + error(0, 0, "failed to read automaton from %s", filename); + else + process_automaton(haut, filename); + } + + return err; + } }; } diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 5708f6efa..7f3cd712d 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -95,6 +95,7 @@ %token ANAME "alias name"; %token STRING "string"; %token INT "integer"; +%token ENDOFFILE 0 "end of file" %left '|' %left '&' @@ -114,7 +115,8 @@ %printer { debug_stream() << $$; } %% -hoa: header "--BODY--" body "--END--" +hoa: header "--BODY--" body "--END--" { YYACCEPT; } +hoa: ENDOFFILE { YYABORT; } string_opt: | STRING BOOLEAN: 't' | 'f' @@ -464,19 +466,23 @@ hoayy::parser::error(const location_type& location, namespace spot { - hoa_aut_ptr - hoa_parse(const std::string& name, - hoa_parse_error_list& error_list, - const bdd_dict_ptr& dict, - ltl::environment& env, - bool debug) + hoa_stream_parser::hoa_stream_parser(const std::string& name) { if (hoayyopen(name)) - { - error_list.emplace_back(spot::location(), - std::string("Cannot open file ") + name); - return 0; - } + throw std::runtime_error(std::string("Cannot open file ") + name); + } + + hoa_stream_parser::~hoa_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) + { result_ r; r.h = std::make_shared(); r.h->aut = make_tgba_digraph(dict); @@ -485,10 +491,8 @@ namespace spot parser.set_debug_level(debug); if (parser.parse()) r.h->aut = nullptr; - hoayyclose(); if (!r.h->aut) return nullptr; - if (r.start != -1) r.h->aut->set_init_state(r.start); else @@ -498,7 +502,7 @@ namespace spot r.h->aut->set_init_state(r.h->aut->new_state()); } return r.h; - } + }; } // Local Variables: diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index 02fbee6dd..2d97b6e2b 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -51,7 +51,19 @@ namespace spot typedef std::shared_ptr hoa_aut_ptr; typedef std::shared_ptr const_hoa_aut_ptr; - /// \brief Build a spot::tgba_digraph from ltl2hoa's output. + class SPOT_API hoa_stream_parser + { + public: + hoa_stream_parser(const std::string& filename); + ~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); + }; + + /// \brief Build a spot::tgba_digraph from a HOA file. /// \param filename The name of the file to parse. /// \param error_list A list that will be filled with /// parse errors that occured during parsing. @@ -63,17 +75,29 @@ namespace spot /// 0 if the file could not be opened. /// /// Note that the parser usually tries to recover from errors. It can - /// return an non zero value even if it encountered error during the + /// return a non zero value even if it encountered error during the /// parsing of \a filename. If you want to make sure \a filename /// was parsed succesfully, check \a error_list for emptiness. /// /// \warning This function is not reentrant. - SPOT_API hoa_aut_ptr + inline hoa_aut_ptr hoa_parse(const std::string& filename, hoa_parse_error_list& error_list, const bdd_dict_ptr& dict, ltl::environment& env = ltl::default_environment::instance(), - bool debug = false); + bool debug = false) + { + try + { + hoa_stream_parser p(filename); + return p.parse(error_list, dict, env, debug); + } + catch (std::runtime_error& e) + { + error_list.emplace_back(spot::location(), e.what()); + return nullptr; + } + } /// \brief Format diagnostics produced by spot::hoa_parse. /// \param os Where diagnostics should be output.