Commit c7f4b8e2 authored by Ala-Eddine Ben-Salem's avatar Ala-Eddine Ben-Salem Committed by Alexandre Duret-Lutz
Browse files

Single-pass Testing Automata (STA) optimizations

* src/taalgos/sba2ta.cc, src/taalgos/emptinessta.cc: STA optimizations
parent 782ba001
......@@ -205,9 +205,10 @@ namespace spot
(a_->is_hole_state_in_ta_component(curr))
&& a_->is_livelock_accepting_state(curr);
//may be Buchi accepting scc or livelock accepting state (contains a TA hole and livelock accepting state)
//may be Buchi accepting scc or livelock accepting scc (contains a TA "hole and livelock accepting state")
scc.top().is_accepting = (a_->is_accepting_state(curr)
&& !succ->is_stuttering_transition())
&& (!succ->is_stuttering_transition()
|| a_->is_livelock_accepting_state(curr)))
|| curr_is_livelock_hole_state_in_ta_component;
bool is_stuttering_transition = succ->is_stuttering_transition();
......
......@@ -140,14 +140,8 @@ namespace spot
new state_ta_explicit(ta->get_tgba()->get_init_state(), bddfalse,
false, false, true, 0, true);
state_ta_explicit* artificial_livelock_accepting_state_added = ta->add_state(artificial_livelock_accepting_state);
// unique artificial_livelock_accepting_state
assert(artificial_livelock_accepting_state_added
== artificial_livelock_accepting_state);
add_artificial_livelock_accepting_state(ta,
artificial_livelock_accepting_state_added);
artificial_livelock_accepting_state);
}
......@@ -160,6 +154,13 @@ namespace spot
state_ta_explicit* artificial_livelock_accepting_state)
{
state_ta_explicit* artificial_livelock_accepting_state_added =
testing_automata->add_state(artificial_livelock_accepting_state);
// unique artificial_livelock_accepting_state
assert(artificial_livelock_accepting_state_added
== artificial_livelock_accepting_state);
ta::states_set_t states_set = testing_automata->get_states_set();
ta::states_set_t::iterator it;
......@@ -181,7 +182,7 @@ namespace spot
{
state_ta_explicit* dest = (*it_trans)->dest;
if (dest->is_livelock_accepting_state())
if (dest->is_livelock_accepting_state() && !dest->is_accepting_state())
{
conditions_to_livelock_accepting_states->insert(
(*it_trans)->condition);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment