diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy index d2e7de0ee..53b789e0d 100644 --- a/src/dstarparse/dstarparse.yy +++ b/src/dstarparse/dstarparse.yy @@ -38,12 +38,9 @@ { typedef std::map map_t; - enum dstar_type { Rabin, Streett }; - struct result_ { spot::parsed_aut_ptr d; - dstar_type type; spot::ltl::environment* env; std::vector guards; std::vector::const_iterator cur_guard; @@ -128,13 +125,13 @@ opt_eols: | opt_eols EOL auttype: DRA { - result.type = Rabin; + result.d->type = spot::parsed_aut_type::DRA; result.plus = 1; result.minus = 0; } | DSA { - result.type = Streett; + result.d->type = spot::parsed_aut_type::DSA; result.plus = 0; result.minus = 1; } @@ -189,9 +186,9 @@ sizes: result.accpair_count = $4; result.accpair_count_seen = true; result.d->aut->set_acceptance(2 * $4, - result.type == Rabin ? - spot::acc_cond::acc_code::rabin($4) : - spot::acc_cond::acc_code::streett($4)); + result.d->type == spot::parsed_aut_type::DRA + ? spot::acc_cond::acc_code::rabin($4) + : spot::acc_cond::acc_code::streett($4)); } | sizes STATES opt_eols NUMBER opt_eols { diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index 9427509af..8d55f55a1 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -246,10 +246,9 @@ aut: aut-1 { res.h->loc = @$; YYACCEPT; } | ENDOFFILE { YYABORT; } | error ENDOFFILE { YYABORT; } -aut-1: hoa - | never - | lbtt - +aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; } + | never { res.h->type = spot::parsed_aut_type::NeverClaim; } + | lbtt { res.h->type = spot::parsed_aut_type::LBTT; } /**********************************************************************/ /* Rules for HOA */ diff --git a/src/parseaut/public.hh b/src/parseaut/public.hh index 4fc75efb9..a98a4e1b7 100644 --- a/src/parseaut/public.hh +++ b/src/parseaut/public.hh @@ -43,6 +43,8 @@ namespace spot struct parse_aut_error_list {}; #endif + enum class parsed_aut_type { HOA, NeverClaim, LBTT, DRA, DSA, Unknown }; + /// \brief Temporary encoding of an omega automaton produced by /// the parser. struct SPOT_API parsed_aut @@ -52,6 +54,7 @@ namespace spot twa_graph_ptr aut; bool aborted = false; spot::location loc; + parsed_aut_type type = parsed_aut_type::Unknown; }; typedef std::shared_ptr parsed_aut_ptr;