diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 4a8ff3d1e..535dd9398 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -604,6 +604,39 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, // build ta automata: build_ta(ta, atomic_propositions_set_, degeneralized, single_pass_emptiness_check, artificial_livelock_state_mode); + + // (degeneralized=true) => TA + if (degeneralized) + return ta; + + // (degeneralized=false) => GTA + // adapt a GTA to remove acceptance conditions from states + ta::states_set_t states_set = ta->get_states_set(); + ta::states_set_t::iterator it; + for (it = states_set.begin(); it != states_set.end(); it++) + { + state_ta_explicit* state = static_cast (*it); + + if (state->is_accepting_state()) + { + + state_ta_explicit::transitions* trans = state->get_transitions(); + state_ta_explicit::transitions::iterator it_trans; + + for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) + { + (*it_trans)->acceptance_conditions + = ta->all_acceptance_conditions(); + + } + + state->set_accepting_state(false); + } + + } + + + return ta; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 4858fe514..25a578e44 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1174,7 +1174,7 @@ main(int argc, char** argv) { case 0: spot::dotty_reachable(std::cout, - dynamic_cast(a)); + dynamic_cast(a)->get_ta()); break; case 12: stats_reachable(a).dump(std::cout);