diff --git a/src/graph/ngraph.hh b/src/graph/ngraph.hh index f68d02c42..684fc42f2 100644 --- a/src/graph/ngraph.hh +++ b/src/graph/ngraph.hh @@ -78,10 +78,36 @@ namespace spot } /// \brief Give an alternate name to a state. - /// \return true iff the newname was already used. + /// \return true iff the newname state was already existing + /// (in this case the existing newname state will be merged + /// with state s: the newname will be unreachable and without + /// successors.) bool alias_state(state s, name newname) { - return !name_to_state.emplace(newname, s).second; + auto p = name_to_state.emplace(newname, s); + if (!p.second) + { + // The state already exists. Change its number. + auto old = p.first->second; + p.first->second = s; + // Add the successor of OLD to those of S. + auto& trans = g_.transitions(); + auto& states = g_.states(); + trans[states[s].succ_tail].next_succ = states[old].succ; + states[s].succ_tail = states[old].succ_tail; + states[old].succ = 0; + states[old].succ_tail = 0; + // Remove all references to old in transitions: + unsigned tend = trans.size(); + for (unsigned t = 1; t < tend; ++t) + { + if (trans[t].src == old) + trans[t].src = s; + if (trans[t].dst == old) + trans[t].dst = s; + } + } + return !p.second; } state get_state(name n) const diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 6ce680731..187bb4401 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -88,6 +88,7 @@ bool accept_all_needed = false; bool accept_all_seen = false; + bool aliased_states = false; std::map labels; ~result_() @@ -732,6 +733,10 @@ never: "never" { res.namer = res.h->aut->create_namer(); unsigned n = res.namer->new_state("accept_all"); res.h->aut->new_acc_transition(n, n, bddtrue); } + // If we aliased existing state, we have some unreachable + // states to remove. + if (res.aliased_states) + res.h->aut->purge_unreachable_states(); } nc-states: @@ -742,12 +747,6 @@ nc-states: nc-one-ident: IDENTIFIER ':' { - unsigned n = res.namer->new_state(*$1); - if (res.labels.empty()) - { - // The first state is initial. - res.start.emplace_back(@$, n); - } auto r = res.labels.insert(std::make_pair(*$1, @1)); if (!r.second) { @@ -759,9 +758,19 @@ nc-one-ident: IDENTIFIER ':' } nc-ident-list: nc-one-ident + { + unsigned n = res.namer->new_state(*$1); + if (res.start.empty()) + { + // The first state is initial. + res.start.emplace_back(@$, n); + } + $$ = $1; + } | nc-ident-list nc-one-ident { - res.namer->alias_state(res.namer->get_state(*$1), *$2); + res.aliased_states |= + res.namer->alias_state(res.namer->get_state(*$1), *$2); // Keep any identifier that starts with accept. if (strncmp("accept", $1->c_str(), 6)) { @@ -791,10 +800,9 @@ nc-state: if (*$1 == "accept_all") res.accept_all_seen = true; - res.namer->new_transition(*$1, *$1, bddtrue, - !strncmp("accept", $1->c_str(), 6) ? - res.h->aut->acc().all_sets() : - spot::acc_cond::mark_t(0U)); + auto acc = !strncmp("accept", $1->c_str(), 6) ? + res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U); + res.namer->new_transition(*$1, *$1, bddtrue, acc); delete $1; } | nc-ident-list { delete $1; } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 94cdf78c2..4f5dc7858 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -31,12 +31,15 @@ if :: (p1 && p0) -> goto T1 fi; T1: +T1b: /* alias */ if -:: (p1 && (! p0)) -> goto accept_all -:: !(p1) -> goto T1 +:: (p1 && (! p0)) -> goto alias2 +:: !(p1) -> goto T1b :: ! (p1) -> goto T2_init fi; +alias1: accept_all: +alias2: skip } EOF