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

Improving efficiency of unsplit_2step

Browse source 
* spot/twaalgos/synthesis.cc: Here
This commit is contained in:
philipp 2021-07-16 13:51:50 +02:00
parent 9669806cd0
commit 31d6dc33e7
1 changed files with 25 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

38
spot/twaalgos/synthesis.cc
View file

@ -301,13 +301,14 @@ namespace spot
return split; return split;
} }
twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut) twa_graph_ptr
unsplit_2step(const const_twa_graph_ptr& aut)
{ {
constexpr unsigned unseen_mark = std::numeric_limits<unsigned>::max();
twa_graph_ptr out = make_twa_graph(aut->get_dict()); twa_graph_ptr out = make_twa_graph(aut->get_dict());
out->copy_acceptance_of(aut); out->copy_acceptance_of(aut);
out->copy_ap_of(aut); out->copy_ap_of(aut);
out->new_states(aut->num_states());
out->set_init_state(aut->get_init_state_number());
// split_2step is not guaranteed to produce // split_2step is not guaranteed to produce
// states that alternate between env and player do to do_simplify // states that alternate between env and player do to do_simplify
@ -316,15 +317,23 @@ namespace spot
throw std::runtime_error("unsplit requires the named prop " throw std::runtime_error("unsplit requires the named prop "
"state-player as set by split_2step"); "state-player as set by split_2step");
std::vector<bool> seen(aut->num_states(), false); std::vector<unsigned> state_map(aut->num_states(), unseen_mark);
auto seen = [&](unsigned s){return state_map[s] != unseen_mark; };
auto map_s = [&](unsigned s)
{
if (!seen(s))
state_map[s] = out->new_state();
return state_map[s];
};
std::deque<unsigned> todo; std::deque<unsigned> todo;
todo.push_back(aut->get_init_state_number()); todo.push_back(aut->get_init_state_number());
seen[aut->get_init_state_number()] = true; map_s(aut->get_init_state_number());
while (!todo.empty()) while (!todo.empty())
{ {
unsigned cur = todo.front(); unsigned cur = todo.front();
unsigned cur_m = map_s(cur);
todo.pop_front(); todo.pop_front();
seen[cur] = true;
for (const auto& i : aut->out(cur)) for (const auto& i : aut->out(cur))
{ {
@ -338,21 +347,24 @@ namespace spot
auto out_cont = aut->out(cur); auto out_cont = aut->out(cur);
return (++(out_cont.begin()) == out_cont.end()); return (++(out_cont.begin()) == out_cont.end());
})()); })());
out->new_edge(cur, i.dst, i.cond, i.acc); if (!seen(i.dst))
if (!seen[i.dst])
todo.push_back(i.dst); todo.push_back(i.dst);
out->new_edge(cur_m, map_s(i.dst), i.cond, i.acc);
continue; // Done with cur continue; // Done with cur
} }
for (const auto& o : aut->out(i.dst)) for (const auto& o : aut->out(i.dst))
{ {
out->new_edge(cur, o.dst, i.cond & o.cond, i.acc | o.acc); if (!seen(o.dst))
if (!seen[o.dst])
todo.push_back(o.dst); todo.push_back(o.dst);
out->new_edge(cur_m, map_s(o.dst),
i.cond & o.cond, i.acc | o.acc);
} }
} }
} }
out->merge_edges(); out->set_init_state(map_s(aut->get_init_state_number()));
out->merge_states(); // Try to set outputs
if (bdd* outptr = aut->get_named_prop<bdd>("synthesis-outputs"))
out->set_named_prop("synthesis-outputs", new bdd(*outptr));
return out; return out;
} }