diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 277dec58f..6d63a6a9a 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -276,6 +276,9 @@ namespace spot std::list rem; bool acc = false; + trace + << "***PASS 1: CYCLE***" << std::endl; + while (threshold < scc.top().index) { assert(!scc.empty()); @@ -306,15 +309,23 @@ namespace spot if (is_accepting_sscc) { - clear(h, todo, init_set); trace - << "PASS 1: SUCCESS" << std::endl; + << "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " << a_->is_livelock_accepting_state(curr) << std::endl; trace << "PASS 1: scc.top().condition : " << bdd_format_accset(a_->get_dict(), scc.top().condition) << std::endl; trace - << "PASS 1: a_->all_acceptance_conditions() : " << bdd_format_accset(a_->get_dict(), - a_->all_acceptance_conditions()) << std::endl; + << "PASS 1: a_->all_acceptance_conditions() : " << (scc.top().condition == a_->all_acceptance_conditions()) << std::endl; + + trace + << "PASS 1: bddtrue : " << (a_->all_acceptance_conditions()== + bddtrue) << std::endl; + + trace + << "PASS 1: bddfalse : " << (a_->all_acceptance_conditions()== + bddfalse) << std::endl; + + clear(h, todo, init_set); return true; } diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 0bdb34aa0..41db794e6 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -18,6 +18,17 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#define TRACE + +#include +#ifdef TRACE +#define trace std::clog +#else +#define trace while (0) std::clog +#endif + + + #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "tgba/formula2bdd.hh" @@ -441,6 +452,9 @@ namespace spot if (*spi.second == -1) continue; + trace + << "***compute_livelock_acceptance_states: CYCLE***" << std::endl; + if (!curr->compare(dest)) { state_ta_explicit * self_loop_state = @@ -449,6 +463,8 @@ namespace spot if (testing_automata->is_accepting_state(self_loop_state)) self_loop_state->set_livelock_accepting_state(true); + trace + << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" << std::endl; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 33a0d3005..336bae24d 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1136,7 +1136,9 @@ main(int argc, char** argv) } delete testing_automata_nm; - delete testing_automata; + //delete testing_automata; + a = 0; + degeneralized = 0; output = -1; }