From a13d2c8fc7a8d7cdafb68380086730083c235b9f Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Thu, 22 Dec 2011 22:56:05 +0100 Subject: [PATCH] BUG FIX in TA construction and minimization * src/taalgos/tgba2ta.cc: BUG FIX in TA construction * src/taalgos/minimize.cc: BUG FIX in TA minimization (did_split Flag) --- src/taalgos/minimize.cc | 9 +++++++-- src/taalgos/tgba2ta.cc | 2 +- 2 files changed, 8 insertions(+), 3 deletions(-) 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); }