Commit d0525871 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

neverclaim: fix parsing of aliased states

* src/graph/ngraph.hh (alias_states): Deal with the case
of aliasing two existing states.
* src/hoaparse/hoaparse.yy: Fix handling of aliased states.
* src/tgbatest/neverclaimread.test: Augment test case.
parent e1bba500
......@@ -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
......
......@@ -88,6 +88,7 @@
bool accept_all_needed = false;
bool accept_all_seen = false;
bool aliased_states = false;
std::map<std::string, spot::location> labels;
~result_()
......@@ -732,6 +733,10 @@ never: "never" { res.namer = res.h->aut->create_namer<std::string>();
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; }
......
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment