diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index 09cf699f9..079fd9acb 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +// DĂ©veloppement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -67,431 +68,418 @@ namespace spot dump_hash_set(hs, aut, s); return s.str(); } - } - // 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) - { + // From the base automaton and the list of sets, build the minimal + // automaton + static void + build_result(const ta* a, std::list& sets, + tgba_explicit_number* result_tgba, ta_explicit* result) + { + // 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 + // automaton. + hash_map state_num; + std::list::iterator sit; + unsigned num = 0; + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + for (hit = h->begin(); hit != h->end(); ++hit) + state_num[*hit] = num; + ++num; + } - // 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 - // automaton. - hash_map state_num; - std::list::iterator sit; - unsigned num = 0; - for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set::iterator hit; - hash_set* h = *sit; - for (hit = h->begin(); hit != h->end(); ++hit) - state_num[*hit] = num; - ++num; - } + // For each transition in the initial automaton, add the corresponding + // transition in ta. - // For each transition in the initial automaton, add the corresponding - // transition in ta. + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + hit = h->begin(); + const state* src = *hit; + unsigned src_num = state_num[src]; - for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set::iterator hit; - hash_set* h = *sit; - hit = h->begin(); - const state* src = *hit; - unsigned src_num = state_num[src]; + 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) + tgba_condition = a->get_state_condition(src); + bool is_accepting_state = a->is_accepting_state(src); + bool is_livelock_accepting_state = + a->is_livelock_accepting_state(src); - 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) - tgba_condition = a->get_state_condition(src); - 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, + tgba_condition, is_initial_state, + is_accepting_state, + is_livelock_accepting_state); - 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 = result->add_state(new_src); - state_ta_explicit* ta_src = result->add_state(new_src); + if (ta_src != new_src) + { + delete new_src; + } + else if (a->get_artificial_initial_state() != 0) + { + if (a->get_artificial_initial_state() == src) + result->set_artificial_initial_state(new_src); + } + else if (is_initial_state) + { + result->add_to_initial_states_set(new_src); + } - if (ta_src != new_src) - { - delete new_src; - } - else if (a->get_artificial_initial_state() != 0) - { - if (a->get_artificial_initial_state() == src) - result->set_artificial_initial_state(new_src); - } - else if (is_initial_state) - { - result->add_to_initial_states_set(new_src); - } + ta_succ_iterator* succit = a->succ_iter(src); - ta_succ_iterator* succit = a->succ_iter(src); + for (succit->first(); !succit->done(); succit->next()) + { + const state* dst = succit->current_state(); + hash_map::const_iterator i = state_num.find(dst); - for (succit->first(); !succit->done(); succit->next()) - { - const state* dst = succit->current_state(); - hash_map::const_iterator i = state_num.find(dst); + if (i == state_num.end()) // Ignore useless destinations. + continue; - if (i == state_num.end()) // Ignore useless destinations. - continue; + 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) + tgba_condition = a->get_state_condition(dst); + bool is_accepting_state = a->is_accepting_state(dst); + bool is_livelock_accepting_state = + a->is_livelock_accepting_state(dst); - 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) - tgba_condition = a->get_state_condition(dst); - bool is_accepting_state = a->is_accepting_state(dst); - bool is_livelock_accepting_state = a->is_livelock_accepting_state( - dst); + 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* 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 = result->add_state(new_dst); - state_ta_explicit* ta_dst = result->add_state(new_dst); + if (ta_dst != new_dst) + { + delete new_dst; + } + else if (a->get_artificial_initial_state() != 0) + { + if (a->get_artificial_initial_state() == dst) + result->set_artificial_initial_state(new_dst); + } - if (ta_dst != new_dst) - { - delete new_dst; - } - else if (a->get_artificial_initial_state() != 0) - { - if (a->get_artificial_initial_state() == dst) - result->set_artificial_initial_state(new_dst); - } + else if (is_initial_state) + result->add_to_initial_states_set(new_dst); - else if (is_initial_state) - result->add_to_initial_states_set(new_dst); + result->create_transition(ta_src, succit->current_condition(), + succit->current_acceptance_conditions(), + ta_dst); + } + delete succit; + } + } - result->create_transition(ta_src, succit->current_condition(), - succit->current_acceptance_conditions(), ta_dst); + static partition_t + build_partition(const ta* ta_) + { + partition_t cur_run; + partition_t next_run; - } - delete succit; - } + // The list of equivalent states. + partition_t done; - } + std::set states_set = get_states_set(ta_); - partition_t - build_partition(const ta* ta_) - { - partition_t cur_run; - partition_t next_run; + hash_set* I = new hash_set; - // The list of equivalent states. - partition_t done; + // livelock acceptance states + hash_set* G = new hash_set; - std::set states_set = get_states_set(ta_); + // Buchi acceptance states + hash_set* F = new hash_set; - hash_set* I = new hash_set; + // Buchi and livelock acceptance states + hash_set* G_F = new hash_set; - // livelock acceptance states - hash_set* G = new hash_set; + // the other states (non initial and not in G, F and G_F) + hash_set* S = new hash_set; - // Buchi acceptance states - hash_set* F = new hash_set; + std::set::iterator it; - // Buchi and livelock acceptance states - hash_set* G_F = new hash_set; + spot::state* artificial_initial_state = + ta_->get_artificial_initial_state(); - // the other states (non initial and not in G, F and G_F) - hash_set* S = new hash_set; + 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); + } - std::set::iterator it; + hash_map state_set_map; - spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); + // 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_); - for (it = states_set.begin(); it != states_set.end(); ++it) - { - const state* s = (*it); + std::set free_var; + for (unsigned i = set_num; i < set_num + size; ++i) + free_var.insert(i); + std::map used_var; - 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); - } + 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); - else if (ta_->is_livelock_accepting_state(s)) - { - G->insert(s); - } - else - { - S->insert(s); - } + used_var[set_num] = 1; + free_var.erase(set_num); + state_set_map[*i] = set_num; + ++set_num; - } + } + delete I; - hash_map state_set_map; + 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; - // 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_); + } + else + { + delete G; + } - std::set free_var; - for (unsigned i = set_num; i < set_num + size; ++i) - free_var.insert(i); - std::map used_var; + 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; + } - 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); + 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; + } - used_var[set_num] = 1; - free_var.erase(set_num); - state_set_map[*i] = set_num; - ++set_num; + // 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); - } - delete I; + 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(); - 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; + trace + << "processing " << format_hash_set(cur, ta_) << std::endl; - } - else - delete G; + 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); + trace << "+src: " << src << std::endl; + for (si->first(); !si->done(); si->next()) + { + const state* dst = si->current_state(); + hash_map::const_iterator i = state_set_map.find(dst); - 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); - trace - << "+src: " << src << std::endl; - 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 = + assert(i != state_set_map.end()); + bdd current_acceptance_conditions = si->current_acceptance_conditions(); - if (current_acceptance_conditions == bddfalse) - 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; + f |= (bdd_ithvar(i->second) & si->current_condition() + & current_acceptance_conditions); + trace + << "+f: " << bdd_format_accset(ta_->get_dict(), f) + << "\n -bdd_ithvar(i->second): " + << bdd_format_accset(ta_->get_dict(), + bdd_ithvar(i->second)) + << "\n -si->current_condition(): " + << bdd_format_accset(ta_->get_dict(), + si->current_condition()) + << "\n -current_acceptance_conditions: " + << bdd_format_accset(ta_->get_dict(), + current_acceptance_conditions) + << std::endl; + } + delete si; - trace - << " -bdd_ithvar(i->second): " << bdd_format_accset( - ta_->get_dict(), bdd_ithvar(i->second)) << std::endl; + // 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); + } + } - trace - << " -si->current_condition(): " - << bdd_format_accset(ta_->get_dict(), - si->current_condition()) << std::endl; + 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 + { + did_split = true; + 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 + { + 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; - trace - << " -current_acceptance_conditions: " - << bdd_format_accset(ta_->get_dict(), - current_acceptance_conditions) << std::endl; + std::swap(cur_run, next_run); + } - - } - 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 - { - did_split = true; - 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 - { - 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); + 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; + 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; + return done; + } } ta*