diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index d31adeaa5..faf984456 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -367,6 +367,7 @@ namespace spot const state* src = *hi; bdd f = bddfalse; ta_succ_iterator* si = ta_->succ_iter(src); + trace << "+src: " << src << std::endl; for (si->first(); !si->done(); si->next()) { const state* dst = si->current_state(); @@ -380,7 +381,11 @@ namespace spot = bdd_false_acceptance_condition; f |= (bdd_ithvar(i->second) & si->current_condition() & current_acceptance_conditions); - trace << "--------------f: " << bdd_format_accset(ta_->get_dict(),f) << std::endl;; + trace << "+f: " << bdd_format_accset(ta_->get_dict(),f) << std::endl;; + trace << " -bdd_ithvar(i->second): " << bdd_format_accset(ta_->get_dict(),bdd_ithvar(i->second)) << std::endl;; + trace << " -si->current_condition(): " << bdd_format_accset(ta_->get_dict(),si->current_condition()) << std::endl;; + trace << " -current_acceptance_conditions: " << bdd_format_accset(ta_->get_dict(),current_acceptance_conditions) << std::endl;; + } delete si; @@ -411,6 +416,7 @@ namespace spot } else { + did_split = true; for (; bsi != bdd_map.end(); ++bsi) { hash_set* set = bsi->second; @@ -444,7 +450,6 @@ namespace spot } else { - did_split = true; trace << "set " << format_hash_set(set, ta_) << " should be processed further" << std::endl; diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 8134894af..ec1c0beb0 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -512,7 +512,7 @@ namespace spot == testing_automata->all_acceptance_conditions())) { self_loop_state->set_livelock_accepting_state(true); - self_loop_state->set_accepting_state(true); + if (artificial_livelock_accepting_state != 0) self_loop_state->set_accepting_state(true); }