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

ltl2aa: finish SERE aut merging with rhs outedges

Browse source
This commit is contained in:
Antoine Martin 2022-09-16 03:41:30 +02:00
parent 87c99cb38f
commit 88914c58c7
3 changed files with 38 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

21
spot/twaalgos/alternation.cc
View file

@ -36,7 +36,7 @@ namespace spot
aut_->get_dict()->unregister_all_my_variables(this);
}
bdd outedge_combiner::operator()(unsigned st)
bdd outedge_combiner::operator()(unsigned st, const std::vector<unsigned>& dst_filter)
{
const auto& dict = aut_->get_dict();
bdd res = bddtrue;
@ -45,6 +45,21 @@ namespace spot
bdd res2 = bddfalse;
for (auto& e: aut_->out(d1))
{
// handle edge filtering
if (!dst_filter.empty())
{
// if any edge destination is an accepting state in the SERE
// automaton, handle the edge, otherwise skip it
auto univ_dests = aut_->univ_dests(e.dst);
if (std::all_of(univ_dests.begin(), univ_dests.end(),
[&](unsigned dst)
{
return std::find(dst_filter.begin(), dst_filter.end(), dst)
== dst_filter.end();
}))
continue;
}
bdd out = bddtrue;
for (unsigned d: aut_->univ_dests(e.dst))
{
@ -63,7 +78,9 @@ namespace spot
}
res2 |= e.cond & out;
}
res &= res2;
if (res2 != bddfalse)
res &= res2;
}
return res;
}

2
spot/twaalgos/alternation.hh
View file

@ -54,7 +54,7 @@ namespace spot
public:
outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u);
~outedge_combiner();
bdd operator()(unsigned st);
bdd operator()(unsigned st, const std::vector<unsigned>& dst_filter = std::vector<unsigned>());
void new_dests(unsigned st, bdd out) const;
};

20
spot/twaalgos/translate_aa.cc
View file

@ -274,8 +274,7 @@ namespace spot
case op::UConcat:
{
// FIXME: combine out edges with rhs !
//unsigned rhs_init = recurse(f[1]);
unsigned rhs_init = recurse(f[1]);
const auto& dict = aut_->get_dict();
twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], dict);
@ -286,6 +285,7 @@ namespace spot
bdd vars = bddtrue;
bdd aps = sere_aut->ap_vars();
std::vector<unsigned> univ_dest;
std::vector<unsigned> acc_states;
// registers a state in various maps and returns the index of the
// anonymous bdd var representing that state
@ -300,6 +300,9 @@ namespace spot
old_to_new.emplace(st, new_st);
var_to_state.emplace(v, new_st);
if (sere_aut->state_is_accepting(st))
acc_states.push_back(new_st);
vars &= bdd_ithvar(v);
}
@ -345,9 +348,22 @@ namespace spot
}
}
for (unsigned st = 0; st < ns; ++st)
{
auto it = old_to_new.find(st);
assert(it != old_to_new.end());
unsigned new_st = it->second;
bdd comb = bddtrue;
comb &= oe_(new_st, acc_states);
comb &= oe_(rhs_init);
oe_.new_dests(new_st, comb);
}
auto it = old_to_new.find(sere_aut->get_init_state_number());
assert(it != old_to_new.end());
//aut_->merge_edges();
return it->second;
}