diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index c014d3250..b9c214263 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -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(); diff --git a/src/taalgos/sba2ta.cc b/src/taalgos/sba2ta.cc index 8f5138467..64ccaa646 100644 --- a/src/taalgos/sba2ta.cc +++ b/src/taalgos/sba2ta.cc @@ -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);