From c12b2d63b3d98ae4ea8bec18da437009e78ad6b5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 21 Nov 2014 15:03:11 +0100 Subject: [PATCH] hoa: add support for --ABORT-- * src/hoaparse/parsedecl.hh (hoa_abort): New structure. * src/hoaparse/hoascan.ll: Throw hoa_abort on --ABORT--. * src/hoaparse/hoaparse.yy: Deal with this exception. * src/hoaparse/public.hh: Add a boolean flag to mark aborted automata. * src/bin/autfilt.cc: Report aborted automata. * src/tgbatest/hoaparse.test: Add test case. --- src/bin/autfilt.cc | 8 ++++++++ src/hoaparse/hoaparse.yy | 29 ++++++++++++++++++++--------- src/hoaparse/hoascan.ll | 1 + src/hoaparse/parsedecl.hh | 6 ++++++ src/hoaparse/public.hh | 2 ++ src/tgbatest/hoaparse.test | 29 +++++++++++++++++++++++++++-- 6 files changed, 64 insertions(+), 11 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 49c91db89..196e05c5a 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -331,6 +331,12 @@ namespace return 0; } + int + aborted(const spot::const_hoa_aut_ptr& h, const char* filename) + { + std::cerr << filename << ':' << h->loc << ": aborted input automaton\n"; + return 2; + } int process_file(const char* filename) @@ -351,6 +357,8 @@ namespace err = 2; if (!haut) error(2, 0, "failed to read automaton from %s", filename); + else if (haut->aborted) + err = std::max(err, aborted(haut, filename)); else process_automaton(haut, filename); } diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 061fa3872..fce135d28 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -55,7 +55,6 @@ spot::location state_label_loc; spot::location start_loc; spot::location accset_loc; - spot::location last_loc; spot::acc_cond::mark_t acc_state; spot::acc_cond::mark_t neg_acc_sets = 0U; spot::acc_cond::mark_t pos_acc_sets = 0U; @@ -81,7 +80,7 @@ %parse-param {result_& res} %parse-param {spot::location initial_loc} -%initial-action { @$ = initial_loc; } +%initial-action { @$ = res.h->loc = initial_loc; } %union { @@ -142,7 +141,7 @@ %% hoa: header "--BODY--" body "--END--" { - res.last_loc = @$; + res.h->loc = @$; YYACCEPT; } hoa: ENDOFFILE { YYABORT; } @@ -174,11 +173,11 @@ header: format-version header-items } } -format-version: "HOA:" IDENTIFIER +format-version: "HOA:" { res.h->loc = @1; } IDENTIFIER { - if (*$2 != "v1") + if (*$3 != "v1") error(@$, "unsupported version of the HOA format"); - delete $2; + delete $3; } header-items: | header-items header-item @@ -685,9 +684,21 @@ namespace spot r.env = &env; hoayy::parser parser(error_list, r, last_loc); parser.set_debug_level(debug); - if (parser.parse()) - r.h->aut = nullptr; - last_loc = r.last_loc; + try + { + if (parser.parse()) + r.h->aut = nullptr; + } + catch (const spot::hoa_abort& e) + { + r.h->aborted = true; + // Bison 3.0.2 lacks a += operator for locations. + r.h->loc = r.h->loc + e.pos; + } + last_loc = r.h->loc; + last_loc.step(); + if (r.h->aborted) + return r.h; if (!r.h->aut) return nullptr; if (r.neg_acc_sets) diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll index 9d43fc17e..cb751b183 100644 --- a/src/hoaparse/hoascan.ll +++ b/src/hoaparse/hoascan.ll @@ -65,6 +65,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* "name:" return token::NAME; "properties:" return token::PROPERTIES; "--BODY--" return token::BODY; +"--ABORT--" throw spot::hoa_abort{*yylloc}; "--END--" return token::END; "State:" return token::STATE; [tf{}()\[\]&|!] return *yytext; diff --git a/src/hoaparse/parsedecl.hh b/src/hoaparse/parsedecl.hh index 8eecc8410..232b196a1 100644 --- a/src/hoaparse/parsedecl.hh +++ b/src/hoaparse/parsedecl.hh @@ -34,6 +34,12 @@ namespace spot { int hoayyopen(const std::string& name); void hoayyclose(); + + // This exception is thrown by the lexer when it reads "--ABORT--". + struct hoa_abort + { + spot::location pos; + }; } #endif // SPOT_HOAPARSE_PARSEDECL_HH diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index 7f1941632..19097d026 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -46,6 +46,8 @@ namespace spot // Transition structure of the automaton. // This is encoded as a TGBA without acceptance condition. tgba_digraph_ptr aut; + bool aborted = false; + spot::location loc; }; typedef std::shared_ptr hoa_aut_ptr; diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 1cb30b33c..003d7c91f 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -26,7 +26,7 @@ set -e expecterr() { cat >$1.exp - ../../bin/autfilt $1 2>$1.err && exit 1 + ../../bin/autfilt --hoa $1 2>$1.err >$1.out && exit 1 test $? = 2 cat $1.err diff $1.err $1.exp @@ -390,6 +390,22 @@ EOF cat >input <expected <