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

tra2tba: Make result state-based if possible

Browse source 
* spot/twaalgos/remfin.cc: Create state-based result.
This commit is contained in:
xlauko 2017-07-13 11:19:45 +02:00 • committed by Alexandre Duret-Lutz
parent d45b60a4e5
commit 71b08b034a
1 changed files with 19 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

36
spot/twaalgos/remfin.cc
View file

@ -84,6 +84,23 @@ namespace spot
return scc_mark; return scc_mark;
} }
// Transforms automaton from transition based acceptance to state based
// acceptance.
void make_state_acc(twa_graph_ptr & aut)
{
unsigned nst = aut->num_states();
for (unsigned s = 0; s < nst; ++s)
{
acc_cond::mark_t acc = 0U;
for (auto& t: aut->out(s))
acc |= t.acc;
for (auto& t: aut->out(s))
t.acc = acc;
}
aut->prop_state_acc(true);
}
// Check whether the SCC contains non-accepting cycles. // Check whether the SCC contains non-accepting cycles.
// //
// A cycle is accepting (in a Rabin automaton) if there exists an // A cycle is accepting (in a Rabin automaton) if there exists an
@ -341,26 +358,11 @@ namespace spot
res->prop_universal(deterministic); res->prop_universal(deterministic);
res->purge_dead_states(); res->purge_dead_states();
res->merge_edges(); res->merge_edges();
if (!aut_pairs.infs())
make_state_acc(res);
return res; return res;
} }
// Transforms automaton from transition based acceptance to state based
// acceptance.
void make_state_acc(twa_graph_ptr & aut)
{
unsigned nst = aut->num_states();
for (unsigned s = 0; s < nst; ++s)
{
acc_cond::mark_t acc = 0U;
for (auto& t: aut->out(s))
acc |= t.acc;
for (auto& t: aut->out(s))
t.acc = acc;
}
aut->prop_state_acc(true);
}
// If the DNF is // If the DNF is
// Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) | // Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) |
// Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4) // Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4)