From 69678152b6bea76398c5dc64c08bd9c8684539c2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Nov 2014 19:44:56 +0100 Subject: [PATCH] hoa: add support for unlabeled transitions * src/hoaparse/hoaparse.yy: Here. * src/tgbatest/hoaparse.test: Add tests. --- src/hoaparse/hoaparse.yy | 106 +++++++++++++++++++++++++++---------- src/tgbatest/hoaparse.test | 106 +++++++++++++++++++++++++++++++++++++ 2 files changed, 185 insertions(+), 27 deletions(-) diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index f4758e8a9..cbac5cf7e 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -45,6 +45,8 @@ spot::hoa_aut_ptr h; spot::ltl::environment* env; std::vector ap; + std::vector guards; + std::vector::const_iterator cur_guard; spot::location states_loc; spot::location ap_loc; spot::location state_label_loc; @@ -59,7 +61,6 @@ bdd state_label; bdd cur_label; bool has_state_label = false; - bool has_trans_label = false; bool ignore_more_ap = false; // Set to true after the first "AP:" // line has been read. bool ignore_acc = false; // Set to true in case of missing @@ -92,6 +93,8 @@ We must ensure that YYSTYPE is declared (by the above %union) before parsedecl.hh uses it. */ #include "parsedecl.hh" + + static void fill_guards(result_& res); } %token HOA "HOA:" @@ -446,7 +449,16 @@ state-num: INT } states: | states state -state: state-name edges +state: state-name labeled-edges + | state-name unlabeled-edges + { + if (!res.has_state_label) + { + if (res.cur_guard != res.guards.end()) + error(@$, "not enough transitions for this state"); + res.cur_guard = res.guards.begin(); + } + } state-name: "State:" state-label_opt state-num string_opt acc-sig_opt { res.cur_state = $3; @@ -461,19 +473,14 @@ state-label_opt: { res.has_state_label = false; } | label { res.has_state_label = true; res.state_label_loc = @1; res.state_label = res.cur_label; } -trans-label_opt: { res.has_trans_label = false; } - | label +trans-label: label { if (res.has_state_label) { error(@1, "cannot label this transition because..."); error(res.state_label_loc, "... the state is already labeled."); - res.has_trans_label = false; - } - else - { - res.has_trans_label = true; + res.cur_label = res.state_label; } } @@ -503,27 +510,72 @@ acc-sets: else $$ = $1 | res.h->aut->acc().mark($2); } -edges: | edges edge -edge: trans-label_opt state-num acc-sig_opt - { - bdd cond = bddfalse; - if (res.has_state_label) - cond = res.state_label; - else if (res.has_trans_label) - cond = res.cur_label; - else - error(@$, "unlabeled transitions are not yet supported"); - res.h->aut->new_transition(res.cur_state, $2, cond, - $3 | res.acc_state); - } - | trans-label_opt state-conj-2 acc-sig_opt - { - error(@2, "alternation is not yet supported"); - YYABORT; - } +labeled-edges: | labeled-edges labeled-edge +labeled-edge: trans-label state-num acc-sig_opt + { + res.h->aut->new_transition(res.cur_state, $2, + res.cur_label, $3 | res.acc_state); + } + | trans-label state-conj-2 acc-sig_opt + { + error(@2, "alternation is not yet supported"); + YYABORT; + } + +/* We never have zero unlabeled edges, these are considered as zero + labeled edges. */ +unlabeled-edges: unlabeled-edge | unlabeled-edges unlabeled-edge +unlabeled-edge: state-num acc-sig_opt + { + bdd cond; + if (res.has_state_label) + { + cond = res.state_label; + } + else + { + if (res.guards.empty()) + fill_guards(res); + if (res.cur_guard == res.guards.end()) + { + error(@$, "too many transition for this state, " + "ignoring this one"); + cond = bddfalse; + } + else + { + cond = *res.cur_guard++; + } + } + res.h->aut->new_transition(res.cur_state, $1, + cond, $2 | res.acc_state); + } + | state-conj-2 acc-sig_opt + { + error(@1, "alternation is not yet supported"); + YYABORT; + } %% +static void fill_guards(result_& r) +{ + spot::bdd_dict_ptr d = r.h->aut->get_dict(); + unsigned nap = r.ap.size(); + + int* vars = new int[nap]; + for (unsigned i = 0; i < nap; ++i) + vars[i] = r.ap[nap - 1 - i]; + + // build the 2^nap possible guards + r.guards.reserve(1U << nap); + for (size_t i = 0; i < (1U << nap); ++i) + r.guards.push_back(bdd_ibuildcube(i, nap, vars)); + r.cur_guard = r.guards.begin(); + + delete[] vars; +} + void hoayy::parser::error(const location_type& location, const std::string& message) diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 7a5ac2d39..11f9e8e38 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -32,6 +32,15 @@ expecterr() diff $1.err $1.exp } +expectok() +{ + cat >$1.exp + ../../bin/autfilt --hoa $1 >$1.out + test $? = 0 + cat $1.out + diff $1.out $1.exp +} + cat >input <input <input<input<input<