From ed27dab306065a309f381341829eef92ea9be301 Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Fri, 25 Nov 2011 10:16:49 +0100 Subject: [PATCH] Add an implementation of TGTA minimization * src/ta/taexplicit.cc, src/ta/taexplicit.hh: Bug fix TGTA * src/taalgos/minimize.cc,src/taalgos/minimize.hh: TGTA minimization * src/taalgos/tgba2ta.cc: add a TGTA minimization command (uses -Rm) * src/taalgos/minimize.cc, src/taalgos/minimize.hh (minimize_tgbta): New function. * src/taalgos/tgba2ta.cc: Set livelock-accepting flag of TGTA states to false so they can be merged with other states. * src/ta/taexplicit.cc (hash): Use id. * src/ta/taexplicit.hh: Cosmetics. --- src/ta/taexplicit.cc | 4 +- src/ta/taexplicit.hh | 4 +- src/taalgos/minimize.cc | 660 +++++++++++++++++++++------------------- src/taalgos/minimize.hh | 4 + src/taalgos/tgba2ta.cc | 3 +- 5 files changed, 360 insertions(+), 315 deletions(-) diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 18a5e77f5..9132c4c0a 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -266,7 +266,9 @@ namespace spot size_t state_ta_explicit::hash() const { - return wang32_hash(tgba_state_->hash()); + //return wang32_hash(tgba_state_->hash()); + return wang32_hash(tgba_state_->hash()) ^ wang32_hash(tgba_condition_.id()); + } state_ta_explicit* diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index bde2b3f68..93c3a956d 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -176,11 +176,11 @@ namespace spot virtual state_ta_explicit* clone() const; - virtual - void destroy() const + virtual void destroy() const { } + virtual ~state_ta_explicit() { diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index dc43aec0e..d31adeaa5 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -34,7 +34,7 @@ #include "ltlast/allnodes.hh" #include "misc/hash.hh" #include "misc/bddlt.hh" -#include "ta/taproduct.hh" +#include "ta/tgbtaexplicit.hh" #include "taalgos/statessetbuilder.hh" #include "tgba/tgbaexplicit.hh" #include "tgba/bddprint.hh" @@ -44,6 +44,7 @@ namespace spot typedef Sgi::hash_set hash_set; typedef Sgi::hash_map hash_map; + typedef std::list partition_t; namespace { @@ -70,13 +71,10 @@ namespace spot } } - // From the base automaton and the list of sets, build the minimal - // tgbaulting automaton - ta* - build_result(const ta* a, std::list& sets) + // From the base automaton and the list of sets, build the minimal automaton + void + build_result(const ta* a, std::list& sets, tgba_explicit_number* result_tgba, ta_explicit* result) { - tgba_explicit_number* tgba = new tgba_explicit_number(a->get_dict()); - ta_explicit* ta = new ta_explicit(tgba, a->all_acceptance_conditions()); // For each set, create a state in the tgbaulting automaton. // For a state s, state_num[s] is the number of the state in the minimal @@ -104,7 +102,7 @@ namespace spot const state* src = *hit; unsigned src_num = state_num[src]; - state* tgba_state = tgba->add_state(src_num); + state* tgba_state = result_tgba->add_state(src_num); bdd tgba_condition = bddtrue; bool is_initial_state = a->is_initial_state(src); if ((a->get_artificial_initial_state() == 0) && is_initial_state) @@ -112,24 +110,24 @@ namespace spot bool is_accepting_state = a->is_accepting_state(src); bool is_livelock_accepting_state = a->is_livelock_accepting_state(src); - state_ta_explicit* new_src = new state_ta_explicit(tgba_state->clone(), + state_ta_explicit* new_src = new state_ta_explicit(tgba_state, tgba_condition, is_initial_state, is_accepting_state, is_livelock_accepting_state); - state_ta_explicit* ta_src = ta->add_state(new_src); + state_ta_explicit* ta_src = result->add_state(new_src); if (ta_src != new_src) { - new_src->destroy(); + delete new_src; } else if (a->get_artificial_initial_state() != 0) { if (a->get_artificial_initial_state() == src) - ta->set_artificial_initial_state(new_src); + result->set_artificial_initial_state(new_src); } else if (is_initial_state) { - ta->add_to_initial_states_set(new_src); + result->add_to_initial_states_set(new_src); } ta_succ_iterator* succit = a->succ_iter(src); @@ -142,7 +140,7 @@ namespace spot if (i == state_num.end()) // Ignore useless destinations. continue; - state* tgba_state = tgba->add_state(i->second); + state* tgba_state = result_tgba->add_state(i->second); bdd tgba_condition = bddtrue; is_initial_state = a->is_initial_state(dst); if ((a->get_artificial_initial_state() == 0) && is_initial_state) @@ -151,341 +149,381 @@ namespace spot bool is_livelock_accepting_state = a->is_livelock_accepting_state( dst); - state_ta_explicit* new_dst = new state_ta_explicit(tgba_state->clone(), + state_ta_explicit* new_dst = new state_ta_explicit(tgba_state, tgba_condition, is_initial_state, is_accepting_state, is_livelock_accepting_state); - state_ta_explicit* ta_dst = ta->add_state(new_dst); + state_ta_explicit* ta_dst = result->add_state(new_dst); if (ta_dst != new_dst) { - new_dst->destroy(); + delete new_dst; } else if (a->get_artificial_initial_state() != 0) { if (a->get_artificial_initial_state() == dst) - ta->set_artificial_initial_state(new_dst); + result->set_artificial_initial_state(new_dst); } else if (is_initial_state) - ta->add_to_initial_states_set(new_dst); + result->add_to_initial_states_set(new_dst); - ta->create_transition(ta_src, succit->current_condition(), succit->current_acceptance_conditions(), ta_dst); + result->create_transition(ta_src, succit->current_condition(), succit->current_acceptance_conditions(), ta_dst); } delete succit; } - return ta; + + } + + partition_t build_partition(const ta* ta_){ + partition_t cur_run; + partition_t next_run; + + // The list of equivalent states. + partition_t done; + + std::set states_set = get_states_set(ta_); + + hash_set* I = new hash_set; + + // livelock acceptance states + hash_set* G = new hash_set; + + // Buchi acceptance states + hash_set* F = new hash_set; + + // Buchi and livelock acceptance states + hash_set* G_F = new hash_set; + + // the other states (non initial and not in G, F and G_F) + hash_set* S = new hash_set; + + std::set::iterator it; + + spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); + + for (it = states_set.begin(); it != states_set.end(); it++) + { + const state* s = (*it); + + if (s == artificial_initial_state) + { + I->insert(s); + } + else if (artificial_initial_state == 0 && ta_->is_initial_state(s)) + { + I->insert(s); + } + else if (ta_->is_livelock_accepting_state(s) + && ta_->is_accepting_state(s)) + { + G_F->insert(s); + } + else if (ta_->is_accepting_state(s)) + { + F->insert(s); + } + + else if (ta_->is_livelock_accepting_state(s)) + { + G->insert(s); + } + else + { + S->insert(s); + } + + } + + hash_map state_set_map; + + // Size of ta_ + unsigned size = states_set.size() + 6; + // Use bdd variables to number sets. set_num is the first variable + // available. + unsigned set_num = ta_->get_dict()->register_anonymous_variables(size, ta_); + + std::set free_var; + for (unsigned i = set_num; i < set_num + size; ++i) + free_var.insert(i); + std::map used_var; + + { + + for (hash_set::const_iterator i = I->begin(); i != I->end(); ++i) + { + hash_set* cI = new hash_set; + cI->insert(*i); + done.push_back(cI); + + used_var[set_num] = 1; + free_var.erase(set_num); + state_set_map[*i] = set_num; + set_num++; + + } + + } + delete I; + + if (!G->empty()) + { + unsigned s = G->size(); + unsigned num = set_num; + set_num++; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(G); + else + done.push_back(G); + for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i) + state_set_map[*i] = num; + + } + else + delete G; + + if (!F->empty()) + { + unsigned s = F->size(); + unsigned num = set_num; + set_num++; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(F); + else + done.push_back(F); + for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i) + state_set_map[*i] = num; + } + else + delete F; + + if (!G_F->empty()) + { + unsigned s = G_F->size(); + unsigned num = set_num; + set_num++; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(G_F); + else + done.push_back(G_F); + for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i) + state_set_map[*i] = num; + } + else + delete G_F; + + if (!S->empty()) + { + unsigned s = S->size(); + unsigned num = set_num; + set_num++; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(S); + else + done.push_back(S); + for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i) + state_set_map[*i] = num; + } + else + delete S; + + // A bdd_states_map is a list of formulae (in a BDD form) associated with a + // destination set of states. + typedef std::map bdd_states_map; + + bool did_split = true; + unsigned num = set_num; + set_num++; + used_var[num] = 1; + free_var.erase(num); + bdd bdd_false_acceptance_condition = bdd_ithvar(num); + + while (did_split) + { + did_split = false; + while (!cur_run.empty()) + { + // Get a set to process. + hash_set* cur = cur_run.front(); + cur_run.pop_front(); + + trace + << "processing " << format_hash_set(cur, ta_) << std::endl; + + hash_set::iterator hi; + bdd_states_map bdd_map; + for (hi = cur->begin(); hi != cur->end(); ++hi) + { + const state* src = *hi; + bdd f = bddfalse; + ta_succ_iterator* si = ta_->succ_iter(src); + for (si->first(); !si->done(); si->next()) + { + const state* dst = si->current_state(); + hash_map::const_iterator i = state_set_map.find(dst); + + assert(i != state_set_map.end()); + bdd current_acceptance_conditions = + si->current_acceptance_conditions(); + if (current_acceptance_conditions == bddfalse) + current_acceptance_conditions + = 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;; + } + delete si; + + // Have we already seen this formula ? + bdd_states_map::iterator bsi = bdd_map.find(f); + if (bsi == bdd_map.end()) + { + // No, create a new set. + hash_set* new_set = new hash_set; + new_set->insert(src); + bdd_map[f] = new_set; + } + else + { + // Yes, add the current state to the set. + bsi->second->insert(src); + } + } + + bdd_states_map::iterator bsi = bdd_map.begin(); + if (bdd_map.size() == 1) + { + // The set was not split. + trace + << "set " << format_hash_set(bsi->second, ta_) + << " was not split" << std::endl; + next_run.push_back(bsi->second); + } + else + { + for (; bsi != bdd_map.end(); ++bsi) + { + hash_set* set = bsi->second; + // Free the number associated to these states. + unsigned num = state_set_map[*set->begin()]; + assert(used_var.find(num) != used_var.end()); + unsigned left = (used_var[num] -= set->size()); + // Make sure LEFT does not become negative (hence bigger + // than SIZE when read as unsigned) + assert(left < size); + if (left == 0) + { + used_var.erase(num); + free_var.insert(num); + } + // Pick a free number + assert(!free_var.empty()); + num = *free_var.begin(); + free_var.erase(free_var.begin()); + used_var[num] = set->size(); + for (hash_set::iterator hit = set->begin(); hit + != set->end(); ++hit) + state_set_map[*hit] = num; + // Trivial sets can't be splitted any further. + if (set->size() == 1) + { + trace + << "set " << format_hash_set(set, ta_) + << " is minimal" << std::endl; + done.push_back(set); + } + else + { + did_split = true; + trace + << "set " << format_hash_set(set, ta_) + << " should be processed further" << std::endl; + next_run.push_back(set); + } + } + } + delete cur; + } + if (did_split) + trace + << "splitting did occur during this pass." << std::endl; + //elsetrace << "splitting did not occur during this pass." << std::endl; + std::swap(cur_run, next_run); + } + + done.splice(done.end(), cur_run); + + #ifdef TRACE + trace << "Final partition: "; + for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) + trace << format_hash_set(*i, ta_) << " "; + trace << std::endl; + #endif + + return done; } ta* minimize_ta(const ta* ta_) { - typedef std::list partition_t; - partition_t cur_run; - partition_t next_run; + tgba_explicit_number* tgba = new tgba_explicit_number(ta_->get_dict()); - // The list of equivalent states. - partition_t done; + ta_explicit* res = new ta_explicit(tgba, ta_->all_acceptance_conditions()); - std::set states_set = get_states_set(ta_); - hash_set* I = new hash_set; + partition_t partition = build_partition(ta_); - // livelock acceptance states - hash_set* G = new hash_set; - // Buchi acceptance states - hash_set* F = new hash_set; - // Buchi and livelock acceptance states - hash_set* G_F = new hash_set; - - // the other states (non initial and not in G, F and G_F) - hash_set* S = new hash_set; - - std::set::iterator it; - - spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); - - for (it = states_set.begin(); it != states_set.end(); it++) - { - const state* s = (*it); - - if (s == artificial_initial_state) - { - I->insert(s); - } - else if (artificial_initial_state == 0 && ta_->is_initial_state(s)) - { - I->insert(s); - } - else if (ta_->is_livelock_accepting_state(s) - && ta_->is_accepting_state(s)) - { - G_F->insert(s); - } - else if (ta_->is_accepting_state(s)) - { - F->insert(s); - } - - else if (ta_->is_livelock_accepting_state(s)) - { - G->insert(s); - } - else - { - S->insert(s); - } - - } - - hash_map state_set_map; - - // Size of ta_ - unsigned size = states_set.size() + 6; - // Use bdd variables to number sets. set_num is the first variable - // available. - unsigned set_num = ta_->get_dict()->register_anonymous_variables(size, ta_); - - std::set free_var; - for (unsigned i = set_num; i < set_num + size; ++i) - free_var.insert(i); - std::map used_var; - - { - - for (hash_set::const_iterator i = I->begin(); i != I->end(); ++i) - { - hash_set* cI = new hash_set; - cI->insert(*i); - done.push_back(cI); - - used_var[set_num] = 1; - free_var.erase(set_num); - state_set_map[*i] = set_num; - set_num++; - - } - - } - delete I; - - if (!G->empty()) - { - unsigned s = G->size(); - unsigned num = set_num; - set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(G); - else - done.push_back(G); - for (hash_set::const_iterator i = G->begin(); i != G->end(); ++i) - state_set_map[*i] = num; - - } - else - delete G; - - if (!F->empty()) - { - unsigned s = F->size(); - unsigned num = set_num; - set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(F); - else - done.push_back(F); - for (hash_set::const_iterator i = F->begin(); i != F->end(); ++i) - state_set_map[*i] = num; - } - else - delete F; - - if (!G_F->empty()) - { - unsigned s = G_F->size(); - unsigned num = set_num; - set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(G_F); - else - done.push_back(G_F); - for (hash_set::const_iterator i = G_F->begin(); i != G_F->end(); ++i) - state_set_map[*i] = num; - } - else - delete G_F; - - if (!S->empty()) - { - unsigned s = S->size(); - unsigned num = set_num; - set_num++; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(S); - else - done.push_back(S); - for (hash_set::const_iterator i = S->begin(); i != S->end(); ++i) - state_set_map[*i] = num; - } - else - delete S; - - // A bdd_states_map is a list of formulae (in a BDD form) associated with a - // destination set of states. - typedef std::map bdd_states_map; - - bool did_split = true; - unsigned num = set_num; - set_num++; - used_var[num] = 1; - free_var.erase(num); - bdd bdd_false_acceptance_condition = bdd_ithvar(num); - - while (did_split) - { - did_split = false; - while (!cur_run.empty()) - { - // Get a set to process. - hash_set* cur = cur_run.front(); - cur_run.pop_front(); - - trace - << "processing " << format_hash_set(cur, ta_) << std::endl; - - hash_set::iterator hi; - bdd_states_map bdd_map; - for (hi = cur->begin(); hi != cur->end(); ++hi) - { - const state* src = *hi; - bdd f = bddfalse; - ta_succ_iterator* si = ta_->succ_iter(src); - for (si->first(); !si->done(); si->next()) - { - const state* dst = si->current_state(); - hash_map::const_iterator i = state_set_map.find(dst); - - assert(i != state_set_map.end()); - bdd current_acceptance_conditions = - si->current_acceptance_conditions(); - if (current_acceptance_conditions == bddfalse) - current_acceptance_conditions - = 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;; - } - delete si; - - // Have we already seen this formula ? - bdd_states_map::iterator bsi = bdd_map.find(f); - if (bsi == bdd_map.end()) - { - // No, create a new set. - hash_set* new_set = new hash_set; - new_set->insert(src); - bdd_map[f] = new_set; - } - else - { - // Yes, add the current state to the set. - bsi->second->insert(src); - } - } - - bdd_states_map::iterator bsi = bdd_map.begin(); - if (bdd_map.size() == 1) - { - // The set was not split. - trace - << "set " << format_hash_set(bsi->second, ta_) - << " was not split" << std::endl; - next_run.push_back(bsi->second); - } - else - { - for (; bsi != bdd_map.end(); ++bsi) - { - hash_set* set = bsi->second; - // Free the number associated to these states. - unsigned num = state_set_map[*set->begin()]; - assert(used_var.find(num) != used_var.end()); - unsigned left = (used_var[num] -= set->size()); - // Make sure LEFT does not become negative (hence bigger - // than SIZE when read as unsigned) - assert(left < size); - if (left == 0) - { - used_var.erase(num); - free_var.insert(num); - } - // Pick a free number - assert(!free_var.empty()); - num = *free_var.begin(); - free_var.erase(free_var.begin()); - used_var[num] = set->size(); - for (hash_set::iterator hit = set->begin(); hit - != set->end(); ++hit) - state_set_map[*hit] = num; - // Trivial sets can't be splitted any further. - if (set->size() == 1) - { - trace - << "set " << format_hash_set(set, ta_) - << " is minimal" << std::endl; - done.push_back(set); - } - else - { - did_split = true; - trace - << "set " << format_hash_set(set, ta_) - << " should be processed further" << std::endl; - next_run.push_back(set); - } - } - } - delete cur; - } - if (did_split) - trace - << "splitting did occur during this pass." << std::endl; - //elsetrace << "splitting did not occur during this pass." << std::endl; - std::swap(cur_run, next_run); - } - - done.splice(done.end(), cur_run); - -#ifdef TRACE - trace << "Final partition: "; - for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) - trace << format_hash_set(*i, ta_) << " "; - trace << std::endl; -#endif - - // Build the tgbault. - ta* res = build_result(ta_, done); + // Build the ta automata result. + build_result(ta_, partition, tgba, res); // Free all the allocated memory. std::list::iterator itdone; - for (itdone = done.begin(); itdone != done.end(); ++itdone) + for (itdone = partition.begin(); itdone != partition.end(); ++itdone) delete *itdone; //delete ta_; return res; } + tgbta* + minimize_tgbta(const tgbta* tgbta_) + { + + tgba_explicit_number* tgba = new tgba_explicit_number(tgbta_->get_dict()); + + tgbta_explicit* res = new tgbta_explicit(tgba, tgbta_->all_acceptance_conditions(),0); + + const ta_explicit* tgbta = dynamic_cast (tgbta_); + + partition_t partition = build_partition(tgbta); + + + + // Build the tgbault. + build_result(tgbta, partition,tgba, res); + + // Free all the allocated memory. + std::list::iterator itdone; + for (itdone = partition.begin(); itdone != partition.end(); ++itdone) + delete *itdone; + //delete ta_; + + return res; + } + + + } diff --git a/src/taalgos/minimize.hh b/src/taalgos/minimize.hh index 547214e2c..1fc97fdd1 100644 --- a/src/taalgos/minimize.hh +++ b/src/taalgos/minimize.hh @@ -22,6 +22,7 @@ # define SPOT_TAALGOS_MINIMIZE_HH # include "ta/ta.hh" +# include "ta/tgbta.hh" # include "ta/taexplicit.hh" namespace spot @@ -30,6 +31,9 @@ namespace spot ta* minimize_ta(const ta* ta_); + tgbta* + minimize_tgbta(const tgbta* tgbta_); + /// @} } diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 134c6d8fe..ffdab7f53 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -586,8 +586,9 @@ namespace spot << "***tgba_to_tgbta: POST if (state->is_livelock_accepting_state()) ... create_transition ***" << std::endl; + } else { + state->set_livelock_accepting_state(false); } - //state->set_livelock_accepting_state(false); } if (state->compare(tgbta->get_artificial_initial_state()))