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

ltl2aa: factorize self-loop creation

Browse source
This commit is contained in:
Antoine Martin 2022-07-07 17:57:05 +02:00
parent e4bfebf36f
commit 43ed07d283
1 changed files with 26 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

63
spot/twaalgos/translate_aa.cc
View file

@ -43,6 +43,29 @@ namespace spot
internal::univ_dest_mapper<twa_graph::graph_t> uniq_; internal::univ_dest_mapper<twa_graph::graph_t> uniq_;
outedge_combiner oe_; outedge_combiner oe_;
void add_self_loop(twa_graph::edge_storage_t const& e,
unsigned init_state,
acc_cond::mark_t acc)
{
if (e.dst == accepting_sink_)
{
// avoid creating a univ_dests vector if the only dest is an
// accepting sink, which can be simplified, only keeping the self
// loop
aut_->new_edge(init_state, init_state, e.cond, acc);
return;
}
auto dests = aut_->univ_dests(e);
std::vector<unsigned> new_dests(dests.begin(), dests.end());
new_dests.push_back(init_state);
unsigned dst = uniq_.new_univ_dests(new_dests.begin(),
new_dests.end());
aut_->new_edge(init_state, dst, e.cond, acc);
}
unsigned recurse(formula f) unsigned recurse(formula f)
{ {
switch (f.kind()) switch (f.kind())
@ -134,18 +157,7 @@ namespace spot
std::vector<unsigned> new_dests; std::vector<unsigned> new_dests;
for (auto& e : aut_->out(lhs_init)) for (auto& e : aut_->out(lhs_init))
{ add_self_loop(e, init_state, acc);
auto dests = aut_->univ_dests(e);
std::copy(dests.begin(), dests.end(),
std::back_inserter(new_dests));
new_dests.push_back(init_state);
unsigned dest = uniq_.new_univ_dests(new_dests.begin(),
new_dests.end());
aut_->new_edge(init_state, dest, e.cond, acc);
new_dests.clear();
}
for (auto& e : aut_->out(rhs_init)) for (auto& e : aut_->out(rhs_init))
{ {
@ -173,20 +185,8 @@ namespace spot
unsigned lhs_init = recurse(f[0]); unsigned lhs_init = recurse(f[0]);
unsigned rhs_init = recurse(f[1]); unsigned rhs_init = recurse(f[1]);
std::vector<unsigned> new_dests;
for (auto& e : aut_->out(rhs_init)) for (auto& e : aut_->out(rhs_init))
{ add_self_loop(e, init_state, acc);
auto dests = aut_->univ_dests(e);
std::copy(dests.begin(), dests.end(),
std::back_inserter(new_dests));
new_dests.push_back(init_state);
unsigned dst = uniq_.new_univ_dests(new_dests.begin(),
new_dests.end());
aut_->new_edge(init_state, dst, e.cond, acc);
new_dests.clear();
}
std::vector<unsigned> dsts; std::vector<unsigned> dsts;
for (const auto& lhs_e : aut_->out(lhs_init)) for (const auto& lhs_e : aut_->out(lhs_init))
@ -253,18 +253,7 @@ namespace spot
// the product of edges // the product of edges
std::vector<unsigned> new_dests; std::vector<unsigned> new_dests;
for (auto& e : aut_->out(sub_init)) for (auto& e : aut_->out(sub_init))
{ add_self_loop(e, init_state, {});
auto dests = aut_->univ_dests(e);
std::copy(dests.begin(), dests.end(),
std::back_inserter(new_dests));
new_dests.push_back(init_state);
unsigned dst = uniq_.new_univ_dests(new_dests.begin(),
new_dests.end());
aut_->new_edge(init_state, dst, e.cond, {});
new_dests.clear();
}
return init_state; return init_state;
} }