alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

improve alternation removal to match G&O construction

Browse source 
When dealternating the VWAA for GFa, our result had two states that
could not be fused by simulation because of unmatched acceptance mark.
With this change, the result can be simplified.

* spot/twaalgos/alternation.cc: Here.
* tests/core/alternating.test, tests/python/alternation.ipynb: Update
test case.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2018-05-30 10:01:52 +02:00
parent 6d9d35c985
commit e87d308eba
4 changed files with 61 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

28
spot/twaalgos/alternation.cc
View file

@ -184,6 +184,7 @@ namespace spot
std::map<int, unsigned> var_to_state_;
std::vector<int> scc_to_var_;
std::map<int, acc_cond::mark_t> var_to_mark_;
std::vector<unsigned> mark_to_state_;
bdd all_vars_;
bdd all_marks_;
bdd all_states_;
@ -223,6 +224,7 @@ namespace spot
unsigned nc = si_.scc_count();
scc_to_var_.reserve(nc);
unsigned mark_pos = has_reject_more_;
mark_to_state_.resize(mark_pos);
bdd all_marks = bddtrue;
for (unsigned s = 0; s < nc; ++s)
{
@ -231,6 +233,7 @@ namespace spot
{
int v = d->register_anonymous_variables(1, this);
scc_to_var_.emplace_back(v);
mark_to_state_.push_back(si_.one_state_of(c));
var_to_mark_.emplace(v, acc_cond::mark_t({mark_pos++}));
bdd bv = bdd_ithvar(v);
all_marks &= bv;
@ -270,7 +273,7 @@ namespace spot
marked && (scc_s == scc_d) && (c == scc_class::reject_more);
dest &= bdd_ithvar(state_to_var_[d] + mark);
if (c == scc_class::reject_1 && scc_s == scc_d)
dest &= bdd_ithvar(scc_to_var_[scc_s]);
dest &= bdd_ithvar(scc_to_var_[scc_d]);
}
res |= e.cond & dest;
}
@ -464,6 +467,29 @@ namespace spot
bdd dest = bdd_existcomp(cube, all_vars_);
v.clear();
acc_cond::mark_t m = bdd_to_state(dest, v);
// if there is no promise "f" is between a state
// that does not have f, and a state that have
// "f", we can add one. Doing so will help later
// simplifications performed by postprocessor. An
// example where this is needed is the VWAA
// generated by ltl[23]ba for GFa. Without the
// next loop, the final TGBA has 2 states instead
// of 1.
for (unsigned m1: (all_marks - m).sets())
{
if (has_reject_more_ && m1 == 0)
continue;
auto& sv = s_to_ss[s];
unsigned ms = mark_to_state_[m1];
if (std::find(v.begin(), v.end(), ms) != v.end())
{
unsigned ms = mark_to_state_[m1];
if (std::find(sv.begin(), sv.end(), ms) == sv.end())
m.set(m1);
}
}
unsigned d = new_state(v, has_mark);
if (has_mark)
m.set(0);