diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index c97fb24b0..b86f519da 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -58,8 +58,7 @@ namespace spot // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) - numbered_state_heap* h = - numbered_state_heap_hash_map_factory::instance()->build(); + hash_type h; // * num: the number of visited nodes. Used to set the order of each // visited node, @@ -107,13 +106,13 @@ namespace spot state_ta_product* init = new state_ta_product( (ta_init_it_->current_state()), kripke_init_state->clone()); - numbered_state_heap::state_index_p h_init = h->find(init); + if (!h.insert(std::make_pair(init, num + 1)).second) + { + init->destroy(); + continue; + } - if (h_init.first) - continue; - - h->insert(init, ++num); - scc.push(num); + scc.push(++num); arc.push(bddfalse); ta_succ_iterator_product* iter = a_->succ_iter(init); @@ -143,29 +142,25 @@ namespace spot // Backtrack TODO. todo.pop(); dec_depth(); - trace - << "PASS 1 : backtrack" << std::endl; + trace << "PASS 1 : backtrack\n"; if (a_->is_livelock_accepting_state(curr) && !a_->is_accepting_state(curr)) { livelock_acceptance_states_not_found = false; - trace - << "PASS 1 : livelock accepting state found" << std::endl; - + trace << "PASS 1 : livelock accepting state found\n"; } // fill rem with any component removed, - numbered_state_heap::state_index_p spi = - h->index(curr->clone()); - assert(spi.first); + auto i = h.find(curr); + assert(i != h.end()); scc.rem().push_front(curr); inc_depth(); // set the h value of the Backtracked state to negative value. // colour[curr] = BLUE; - *spi.second = -std::abs(*spi.second); + i->second = -std::abs(i->second); // Backtrack livelock_roots. if (activate_heuristic && !livelock_roots.empty() @@ -176,21 +171,11 @@ namespace spot // remove that SSCC from the ROOT stacks. We must // discard from H all reachable states from this SSCC. assert(!scc.empty()); - if (scc.top().index == std::abs(*spi.second)) + if (scc.top().index == std::abs(i->second)) { // removing states - std::list::iterator i; - - for (i = scc.rem().begin(); i != scc.rem().end(); ++i) - { - numbered_state_heap::state_index_p spi = h->index( - (*i)->clone()); - assert(spi.first->compare(*i) == 0); - assert(*spi.second != -1); - *spi.second = -1; - //colour[*i] = BLACK; - - } + for (auto j: scc.rem()) + h[j] = -1; //colour[*i] = BLACK; dec_depth(scc.rem().size()); scc.pop(); assert(!arc.empty()); @@ -205,8 +190,7 @@ namespace spot // We have a successor to look at. inc_transitions(); - trace - << "PASS 1: transition" << std::endl; + trace << "PASS 1: transition\n"; // Fetch the values destination state we are interested in... state* dest = succ->current_state(); @@ -232,15 +216,12 @@ namespace spot // We do not need SUCC from now on. // Are we going to a new state? - numbered_state_heap::state_index_p spi = h->find(dest); - - // Is this a new state? - if (!spi.first) + auto p = h.insert(std::make_pair(dest, num + 1)); + if (p.second) { // Number it, stack it, and register its successors // for later processing. - h->insert(dest, ++num); - scc.push(num); + scc.push(++num); arc.push(acc_cond); ta_succ_iterator_product* iter = a_->succ_iter(dest); @@ -258,7 +239,7 @@ namespace spot } // If we have reached a dead component, ignore it. - if (*spi.second == -1) + if (p.first->second == -1) continue; // Now this is the most interesting case. We have reached a @@ -272,12 +253,11 @@ namespace spot // ROOT is ascending: we just have to merge all SSCCs from the // top of ROOT that have an index greater to the one of // the SSCC of S2 (called the "threshold"). - int threshold = std::abs(*spi.second); + int threshold = std::abs(p.first->second); std::list rem; bool acc = false; - trace - << "***PASS 1: CYCLE***" << std::endl; + trace << "***PASS 1: CYCLE***\n"; while (threshold < scc.top().index) { @@ -310,15 +290,15 @@ namespace spot if (is_accepting_sscc) { trace - << "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " - << a_->is_livelock_accepting_state(curr) << std::endl; + << "PASS 1: SUCCESS: a_->is_livelock_accepting_state(curr): " + << a_->is_livelock_accepting_state(curr) << '\n'; trace << "PASS 1: scc.top().condition : " << bdd_format_accset(a_->get_dict(), scc.top().condition) - << std::endl; + << '\n'; trace << "PASS 1: a_->all_acceptance_conditions() : " - << (a_->all_acceptance_conditions()) << std::endl; + << (a_->all_acceptance_conditions()) << '\n'; trace << ("PASS 1 CYCLE and (scc.top().condition == " "a_->all_acceptance_conditions()) : ") @@ -326,12 +306,12 @@ namespace spot == a_->all_acceptance_conditions()) << std::endl; trace - << "PASS 1: bddtrue : " << (a_->all_acceptance_conditions() - == bddtrue) << std::endl; + << "PASS 1: bddtrue: " << (a_->all_acceptance_conditions() + == bddtrue) << '\n'; trace - << "PASS 1: bddfalse : " << (a_->all_acceptance_conditions() - == bddfalse) << std::endl; + << "PASS 1: bddfalse: " << (a_->all_acceptance_conditions() + == bddfalse) << '\n'; clear(h, todo, ta_init_it_); return true; @@ -341,9 +321,8 @@ namespace spot if (activate_heuristic && a_->is_livelock_accepting_state(curr) && is_stuttering_transition) { - trace - << "PASS 1: heuristic livelock detection " << std::endl; - const state* dest = spi.first; + trace << "PASS 1: heuristic livelock detection \n"; + const state* dest = p.first->first; std::set liveset_dest = liveset[dest]; @@ -352,28 +331,23 @@ namespace spot int h_livelock_root = 0; if (!livelock_roots.empty()) - h_livelock_root = *(h->find((livelock_roots.top()))).second; + h_livelock_root = h[livelock_roots.top()]; if (heuristic_livelock_detection(dest, h, h_livelock_root, - liveset_curr)) + liveset_curr)) { clear(h, todo, ta_init_it_); return true; } std::set::const_iterator it; - for (it = liveset_dest.begin(); it != liveset_dest.end(); ++it) - { - const state* succ = (*it); - if (heuristic_livelock_detection(succ, h, h_livelock_root, - liveset_curr)) - { - clear(h, todo, ta_init_it_); - return true; - } - - } - + for (const state* succ: liveset_dest) + if (heuristic_livelock_detection(succ, h, h_livelock_root, + liveset_curr)) + { + clear(h, todo, ta_init_it_); + return true; + } } } @@ -389,26 +363,23 @@ namespace spot bool ta_check::heuristic_livelock_detection(const state * u, - numbered_state_heap* h, int h_livelock_root, std::set liveset_curr) { - numbered_state_heap::state_index_p hu = h->find(u); + int hu = h[u]; - if (*hu.second > 0) // colour[u] == GREY + if (hu > 0) // colour[u] == GREY { - if (*hu.second >= h_livelock_root) + if (hu >= h_livelock_root) { - trace - << "PASS 1: heuristic livelock detection SUCCESS" << std::endl; + trace << "PASS 1: heuristic livelock detection SUCCESS\n"; return true; } liveset_curr.insert(u); } - return false; - } bool @@ -421,8 +392,7 @@ namespace spot // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) - numbered_state_heap* h = - numbered_state_heap_hash_map_factory::instance()->build(); + hash_type h; // * num: the number of visited nodes. Used to set the order of each // visited node, @@ -448,7 +418,6 @@ namespace spot { state* init_state = (*it); ta_init_it_.push(init_state); - } while (!ta_init_it_.empty()) @@ -457,19 +426,19 @@ namespace spot { state* init = ta_init_it_.front(); ta_init_it_.pop(); - numbered_state_heap::state_index_p h_init = h->find(init); - if (h_init.first) - continue; + if (!h.insert(std::make_pair(init, num + 1)).second) + { + init->destroy(); + continue; + } - h->insert(init, ++num); sscc.push(num); sscc.top().is_accepting = t->is_livelock_accepting_state(init); ta_succ_iterator_product* iter = t->succ_iter(init); iter->first(); todo.emplace(init, iter); inc_depth(); - } while (!todo.empty()) @@ -488,13 +457,11 @@ namespace spot // Backtrack TODO. todo.pop(); dec_depth(); - trace - << "PASS 2 : backtrack" << std::endl; + trace << "PASS 2 : backtrack\n"; // fill rem with any component removed, - numbered_state_heap::state_index_p spi = - h->index(curr->clone()); - assert(spi.first); + auto i = h.find(curr); + assert(i != h.end()); sscc.rem().push_front(curr); inc_depth(); @@ -503,19 +470,11 @@ namespace spot // remove that SSCC from the ROOT stacks. We must // discard from H all reachable states from this SSCC. assert(!sscc.empty()); - if (sscc.top().index == *spi.second) + if (sscc.top().index == i->second) { // removing states - std::list::iterator i; - - for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) - { - numbered_state_heap::state_index_p spi = h->index( - (*i)->clone()); - assert(spi.first->compare(*i) == 0); - assert(*spi.second != -1); - *spi.second = -1; - } + for (auto j: sscc.rem()) + h[j] = -1; dec_depth(sscc.rem().size()); sscc.pop(); } @@ -528,8 +487,7 @@ namespace spot // We have a successor to look at. inc_transitions(); - trace - << "PASS 2 : transition" << std::endl; + trace << "PASS 2 : transition\n"; // Fetch the values destination state we are interested in... state* dest = succ->current_state(); @@ -539,10 +497,10 @@ namespace spot succ->next(); // We do not need SUCC from now on. - numbered_state_heap::state_index_p spi = h->find(dest); + auto i = h.find(dest); // Is this a new state? - if (!spi.first) + if (i == h.end()) { // Are we going to a new state through a stuttering transition? @@ -555,7 +513,7 @@ namespace spot // Number it, stack it, and register its successors // for later processing. - h->insert(dest, ++num); + h[dest] = ++num; sscc.push(num); sscc.top().is_accepting = t->is_livelock_accepting_state(dest); @@ -565,24 +523,26 @@ namespace spot inc_depth(); continue; } + else + { + dest->destroy(); + } // If we have reached a dead component, ignore it. - if (*spi.second == -1) + if (i->second == -1) continue; //self loop state - if (!curr->compare(spi.first)) + if (!curr->compare(i->first)) { - state * self_loop_state = (curr); + state* self_loop_state = curr; if (t->is_livelock_accepting_state(self_loop_state)) { clear(h, todo, ta_init_it_); - trace - << "PASS 2: SUCCESS" << std::endl; + trace << "PASS 2: SUCCESS\n"; return true; } - } // Now this is the most interesting case. We have reached a @@ -596,7 +556,7 @@ namespace spot // ROOT is ascending: we just have to merge all SSCCs from the // top of ROOT that have an index greater to the one of // the SSCC of S2 (called the "threshold"). - int threshold = *spi.second; + int threshold = i->second; std::list rem; bool acc = false; @@ -634,11 +594,11 @@ namespace spot } void - ta_check::clear(numbered_state_heap* h, std::stack todo, + ta_check::clear(hash_type& h, std::stack todo, std::queue init_states) { - set_states(states() + h->size()); + set_states(states() + h.size()); while (!init_states.empty()) { @@ -653,15 +613,14 @@ namespace spot todo.pop(); dec_depth(); } - delete h; } void - ta_check::clear(numbered_state_heap* h, std::stack todo, + ta_check::clear(hash_type& h, std::stack todo, spot::ta_succ_iterator* init_states_it) { - set_states(states() + h->size()); + set_states(states() + h.size()); delete init_states_it; @@ -672,7 +631,6 @@ namespace spot todo.pop(); dec_depth(); } - delete h; } std::ostream& diff --git a/src/taalgos/emptinessta.hh b/src/taalgos/emptinessta.hh index 733b93da8..6db9bb376 100644 --- a/src/taalgos/emptinessta.hh +++ b/src/taalgos/emptinessta.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2008, 2012, 2013, 2014 Laboratoire de Recherche et // Dévelopment de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -25,7 +25,6 @@ #include "ta/taproduct.hh" #include "misc/optionmap.hh" -#include "tgbaalgos/gtec/nsheap.hh" #include "tgbaalgos/emptiness_stats.hh" #include #include @@ -87,6 +86,8 @@ namespace spot /// See the paper cited above. class SPOT_API ta_check : public ec_statistics { + typedef std::unordered_map hash_type; public: ta_check(const ta_product* a, option_map o = option_map()); virtual @@ -126,18 +127,18 @@ namespace spot protected: void - clear(numbered_state_heap* h, std::stack todo, std::queue< + clear(hash_type& h, std::stack todo, std::queue< spot::state*> init_set); void - clear(numbered_state_heap* h, std::stack todo, + clear(hash_type& h, std::stack todo, spot::ta_succ_iterator* init_states_it); /// the heuristic for livelock-accepting runs detection, it's described /// in the paper cited above bool heuristic_livelock_detection(const state * stuttering_succ, - numbered_state_heap* h, int h_livelock_root, std::set liveset_curr); const ta_product* a_; ///< The automaton. diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index fb619caf4..3fc3cd0a1 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -1,6 +1,6 @@ // -*- coding utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -35,7 +35,6 @@ #include "ltlvisit/tostring.hh" #include #include "tgba/bddprint.hh" -#include "tgbaalgos/gtec/nsheap.hh" #include #include "tgba2ta.hh" #include "taalgos/statessetbuilder.hh" @@ -164,9 +163,9 @@ namespace spot // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) - numbered_state_heap* h = - numbered_state_heap_hash_map_factory::instance()->build(); - ///< Heap of visited states. + typedef std::unordered_map hash_type; + hash_type h; ///< Heap of visited states. // * num: the number of visited nodes. Used to set the order of each // visited node, @@ -182,13 +181,8 @@ namespace spot // * init: the set of the depth-first search initial states std::stack init_set; - ta::states_set_t::const_iterator it; - ta::states_set_t init_states = testing_automata->get_initial_states_set(); - for (it = init_states.begin(); it != init_states.end(); ++it) - { - state* init_state = (*it); - init_set.push(init_state); - } + for (state* s: testing_automata->get_initial_states_set()) + init_set.push(s); while (!init_set.empty()) { @@ -196,31 +190,31 @@ namespace spot { state_ta_explicit* init = - down_cast (init_set.top()); + down_cast (init_set.top()); init_set.pop(); - state_ta_explicit* init_clone = init; - numbered_state_heap::state_index_p h_init = h->find(init_clone); - if (h_init.first) - continue; + if (!h.insert(std::make_pair(init, num + 1)).second) + { + init->destroy(); + continue; + } - h->insert(init_clone, ++num); - sscc.push(num); + sscc.push(++num); arc.push(bddfalse); sscc.top().is_accepting = testing_automata->is_accepting_state(init); tgba_succ_iterator* iter = testing_automata->succ_iter(init); iter->first(); - todo.push(pair_state_iter(init, iter)); + todo.emplace(init, iter); } while (!todo.empty()) { state* curr = todo.top().first; - numbered_state_heap::state_index_p spi = h->find(curr); + auto i = h.find(curr); // If we have reached a dead component, ignore it. - if (*spi.second == -1) + if (i != h.end() && i->second == -1) { todo.pop(); continue; @@ -238,16 +232,14 @@ namespace spot todo.pop(); // fill rem with any component removed, - numbered_state_heap::state_index_p spi = h->index(curr); - assert(spi.first); - + assert(i != h.end()); sscc.rem().push_front(curr); // When backtracking the root of an SSCC, we must also // remove that SSCC from the ROOT stacks. We must // discard from H all reachable states from this SSCC. assert(!sscc.empty()); - if (sscc.top().index == *spi.second) + if (sscc.top().index == i->second) { // removing states std::list::iterator i; @@ -256,25 +248,20 @@ namespace spot || (sscc.top().condition == testing_automata->all_acceptance_conditions())); - trace << "*** sscc.size() = ***" - << sscc.size() << std::endl; - for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) + trace << "*** sscc.size() = ***" << sscc.size() << '\n'; + for (auto j: sscc.rem()) { - numbered_state_heap::state_index_p spi = - h->index((*i)); - assert(spi.first->compare(*i) == 0); - assert(*spi.second != -1); - *spi.second = -1; + h[j] = -1; if (is_livelock_accepting_sscc) { // if it is an accepting sscc add the state to // G (=the livelock-accepting states set) trace << "*** sscc.size() > 1: states: ***" - << testing_automata->format_state(*i) - << std::endl; - state_ta_explicit * livelock_accepting_state = - down_cast (*i); + << testing_automata->format_state(j) + << '\n'; + state_ta_explicit* livelock_accepting_state = + down_cast(j); livelock_accepting_state-> set_livelock_accepting_state(true); @@ -317,22 +304,21 @@ namespace spot bool is_stuttering_transition = testing_automata->get_state_condition(curr) == testing_automata->get_state_condition(dest); - state* dest_clone = dest; - spi = h->find(dest_clone); + auto id = h.find(dest); // Is this a new state? - if (!spi.first) + if (id == h.end()) { if (!is_stuttering_transition) { init_set.push(dest); - dest_clone->destroy(); + dest->destroy(); continue; } // Number it, stack it, and register its successors // for later processing. - h->insert(dest_clone, ++num); + h[dest] = ++num; sscc.push(num); arc.push(acc_cond); sscc.top().is_accepting = @@ -340,17 +326,18 @@ namespace spot tgba_succ_iterator* iter = testing_automata->succ_iter(dest); iter->first(); - todo.push(pair_state_iter(dest, iter)); + todo.emplace(dest, iter); continue; } + dest->destroy(); // If we have reached a dead component, ignore it. - if (*spi.second == -1) + if (id->second == -1) continue; trace << "***compute_livelock_acceptance_states: CYCLE***\n"; - if (!curr->compare(dest)) + if (!curr->compare(id->first)) { state_ta_explicit * self_loop_state = down_cast (curr); @@ -385,7 +372,7 @@ namespace spot // ROOT is ascending: we just have to merge all SSCCs from the // top of ROOT that have an index greater to the one of // the SSCC of S2 (called the "threshold"). - int threshold = *spi.second; + int threshold = id->second; std::list rem; bool acc = false; @@ -415,7 +402,6 @@ namespace spot } } - delete h; if ((artificial_livelock_acc_state != 0) || single_pass_emptiness_check) diff --git a/src/tgbaalgos/gtec/Makefile.am b/src/tgbaalgos/gtec/Makefile.am index 4bd9dc403..0d2835da8 100644 --- a/src/tgbaalgos/gtec/Makefile.am +++ b/src/tgbaalgos/gtec/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement +## Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Developpement ## de l'Epita (LRDE). ## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -29,7 +29,6 @@ gtec_HEADERS = \ ce.hh \ explscc.hh \ gtec.hh \ - nsheap.hh \ sccstack.hh \ status.hh @@ -38,6 +37,5 @@ libgtec_la_SOURCES = \ ce.cc \ explscc.cc \ gtec.cc \ - nsheap.cc \ sccstack.cc \ status.cc diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 7c7704bb9..4c42b236e 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -47,17 +48,15 @@ namespace spot filter(const state* s) { r->inc_ars_prefix_states(); - numbered_state_heap::state_index_p sip = ecs->h->find(s); + auto i = ecs->h.find(s); + s->destroy(); // Ignore unknown states ... - if (!sip.first) - { - s->destroy(); - return 0; - } + if (i == ecs->h.end()) + return nullptr; // ... as well as dead states. - if (*sip.second == -1) - return 0; - return sip.first; + if (i->second == -1) + return nullptr; + return i->first; } bool @@ -83,14 +82,11 @@ namespace spot unsigned couvreur99_check_result::acss_states() const { - unsigned count = 0; int scc_root = ecs_->root.top().index; - - numbered_state_heap_const_iterator* i = ecs_->h->iterator(); - for (i->first(); !i->done(); i->next()) - if (i->get_index() >= scc_root) + unsigned count = 0; + for (auto i: ecs_->h) + if (i.second >= scc_root) ++count; - delete i; return count; } @@ -190,18 +186,16 @@ namespace spot virtual const state* filter(const state* s) { - numbered_state_heap::state_index_p sip = ecs->h->find(s); + auto i = ecs->h.find(s); + s->destroy(); // Ignore unknown states. - if (!sip.first) - { - s->destroy(); - return 0; - } + if (i == ecs->h.end()) + return 0; // Stay in the final SCC. - if (*sip.second < scc_root) + if (i->second < scc_root) return 0; r->inc_ars_cycle_states(); - return sip.first; + return i->first; } virtual bool diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 0fc7b1ea9..caf2f17fa 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -40,14 +40,12 @@ namespace spot typedef std::pair pair_state_iter; } - couvreur99_check::couvreur99_check(const tgba* a, - option_map o, - const numbered_state_heap_factory* nshf) + couvreur99_check::couvreur99_check(const tgba* a, option_map o) : emptiness_check(a, o), removed_components(0) { poprem_ = o.get("poprem", 1); - ecs_ = new couvreur99_check_status(a, nshf); + ecs_ = new couvreur99_check_status(a); stats["removed components"] = static_cast (&couvreur99_check::get_removed_components); @@ -85,14 +83,8 @@ namespace spot { assert(!ecs_->root.rem().empty()); dec_depth(ecs_->root.rem().size()); - std::list::iterator i; - for (i = ecs_->root.rem().begin(); i != ecs_->root.rem().end(); ++i) - { - numbered_state_heap::state_index_p spi = ecs_->h->index(*i); - assert(spi.first == *i); - assert(*spi.second != -1); - *spi.second = -1; - } + for (auto i: ecs_->root.rem()) + ecs_->h[i] = -1; // ecs_->root.rem().clear(); return; } @@ -106,10 +98,7 @@ namespace spot // (FROM should be in H, otherwise it means all reachable // states from FROM have already been removed and there is no // point in calling remove_component.) - numbered_state_heap::state_index_p spi = ecs_->h->index(from); - assert(spi.first == from); - assert(*spi.second != -1); - *spi.second = -1; + ecs_->h[from] = -1; tgba_succ_iterator* i = ecs_->aut->succ_iter(from); for (;;) @@ -121,20 +110,14 @@ namespace spot inc_transitions(); state* s = i->current_state(); - numbered_state_heap::state_index_p spi = ecs_->h->index(s); + auto j = ecs_->h.find(s); + assert(j != ecs_->h.end()); + s->destroy(); - // This state is not necessary in H, because if we were - // doing inclusion checking during the emptiness-check - // (redefining find()), the index `s' can be included in a - // larger state and will not be found by index(). We can - // safely ignore such states. - if (!spi.first) - continue; - - if (*spi.second != -1) + if (j->second != -1) { - *spi.second = -1; - to_remove.push(ecs_->aut->succ_iter(spi.first)); + j->second = -1; + to_remove.push(ecs_->aut->succ_iter(j->first)); } } while (i->next()); @@ -168,7 +151,7 @@ namespace spot // Setup depth-first search from the initial state. { state* init = ecs_->aut->get_init_state(); - ecs_->h->insert(init, 1); + ecs_->h[init] = 1; ecs_->root.push(1); arc.push(bddfalse); tgba_succ_iterator* iter = ecs_->aut->succ_iter(init); @@ -197,18 +180,18 @@ namespace spot // If poprem is used, fill rem with any component removed, // so that remove_component() does not have to traverse // the SCC again. - numbered_state_heap::state_index_p spi = ecs_->h->index(curr); - assert(spi.first); + auto i = ecs_->h.find(curr); + assert(i != ecs_->h.end()); if (poprem_) { - ecs_->root.rem().push_front(spi.first); + ecs_->root.rem().push_front(i->first); inc_depth(); } // When backtracking the root of an SCC, we must also // remove that SCC from the ARC/ROOT stacks. We must // discard from H all reachable states from this SCC. assert(!ecs_->root.empty()); - if (ecs_->root.top().index == *spi.second) + if (ecs_->root.top().index == i->second) { assert(!arc.empty()); arc.pop(); @@ -232,13 +215,12 @@ namespace spot // We do not need SUCC from now on. // Are we going to a new state? - numbered_state_heap::state_index_p spi = ecs_->h->find(dest); - if (!spi.first) + auto p = ecs_->h.insert(std::make_pair(dest, num + 1)); + if (p.second) { - // Yes. Number it, stack it, and register its successors - // for later processing. - ecs_->h->insert(dest, ++num); - ecs_->root.push(num); + // Yes. Bump number, stack the stack, and register its + // successors for later processing. + ecs_->root.push(++num); arc.push(acc); tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest); iter->first(); @@ -246,9 +228,10 @@ namespace spot inc_depth(); continue; } + dest->destroy(); // If we have reached a dead component, ignore it. - if (*spi.second == -1) + if (p.first->second == -1) continue; // Now this is the most interesting case. We have reached a @@ -262,7 +245,7 @@ namespace spot // ROOT is ascending: we just have to merge all SCCs from the // top of ROOT that have an index greater to the one of // the SCC of S2 (called the "threshold"). - int threshold = *spi.second; + int threshold = p.first->second; std::list rem; while (threshold < ecs_->root.top().index) { @@ -296,7 +279,7 @@ namespace spot } // Use this state to start the computation of an accepting // cycle. - ecs_->cycle_seed = spi.first; + ecs_->cycle_seed = p.first->first; set_states(ecs_->states()); return new couvreur99_check_result(ecs_, options()); } @@ -336,20 +319,16 @@ namespace spot } } - couvreur99_check_shy::couvreur99_check_shy(const tgba* a, - option_map o, - const numbered_state_heap_factory* - nshf) - : couvreur99_check(a, o, nshf), num(1) + couvreur99_check_shy::couvreur99_check_shy(const tgba* a, option_map o) + : couvreur99_check(a, o), num(1) { group_ = o.get("group", 1); group2_ = o.get("group2", 0); group_ |= group2_; - onepass_ = o.get("onepass", 0); // Setup depth-first search from the initial state. const state* i = ecs_->aut->get_init_state(); - ecs_->h->insert(i, ++num); + ecs_->h[i] = ++num; ecs_->root.push(num); todo.emplace_back(i, num, this); inc_depth(1); @@ -367,15 +346,13 @@ namespace spot while (!todo.empty()) { succ_queue& queue = todo.back().q; - for (succ_queue::iterator q = queue.begin(); - q != queue.end(); ++q) + for (auto& q: queue) { - // Destroy the state if it is a clone of a - // state in the heap... - numbered_state_heap::state_index_p spi = ecs_->h->index(q->s); - // ... or if it is an unknown state. - if (spi.first == 0) - q->s->destroy(); + // Destroy the state if it is a clone of a state in the + // heap or if it is an unknown state. + auto i = ecs_->h.find(q.s); + if (i == ecs_->h.end() || i->first != q.s) + q.s->destroy(); } dec_depth(todo.back().q.size() + 1); todo.pop_back(); @@ -387,21 +364,21 @@ namespace spot void couvreur99_check_shy::dump_queue(std::ostream& os) { - os << "--- TODO ---" << std::endl; + os << "--- TODO ---\n"; unsigned pos = 0; - for (todo_list::const_iterator ti = todo.begin(); ti != todo.end(); ++ti) + for (auto& ti: todo) { ++pos; - os << '#' << pos << " s:" << ti->s << " n:" << ti->n + os << '#' << pos << " s:" << ti.s << " n:" << ti.n << " q:{"; - for (succ_queue::const_iterator qi = ti->q.begin(); qi != ti->q.end();) + for (auto qi = ti.q.begin(); qi != ti.q.end();) { os << qi->s; ++qi; - if (qi != ti->q.end()) + if (qi != ti.q.end()) os << ", "; } - os << '}' << std::endl; + os << "}\n"; } } @@ -450,9 +427,10 @@ namespace spot // the SCC again. if (poprem_) { - numbered_state_heap::state_index_p spi = ecs_->h->index(curr); - assert(spi.first); - ecs_->root.rem().push_front(spi.first); + auto i = ecs_->h.find(curr); + assert(i != ecs_->h.end()); + assert(i->first == curr); + ecs_->root.rem().push_front(i->first); inc_depth(); } @@ -479,35 +457,31 @@ namespace spot // which state we are considering. Otherwise just pick the // first one. succ_queue::iterator old; - if (onepass_) - pos = queue.end(); if (pos == queue.end()) old = queue.begin(); else old = pos; - successor succ = *old; - // Beware: the implementation of find_state in ifage/gspn/ssp.cc - // uses POS and modifies QUEUE. - numbered_state_heap::state_index_p sip = find_state(succ.s); if (pos != queue.end()) ++pos; - int* i = sip.second; + //int* i = sip.second; - trace << "picked state " << succ.s << std::endl; + successor succ = *old; + trace << "picked state " << succ.s << '\n'; + auto i = ecs_->h.find(succ.s); - if (!i) + if (i == ecs_->h.end()) { // It's a new state. // If we are seeking known states, just skip it. if (pos != queue.end()) continue; - trace << "new state" << std::endl; + trace << "new state\n"; // Otherwise, number it and stack it so we recurse. queue.erase(old); dec_depth(); - ecs_->h->insert(succ.s, ++num); + ecs_->h[succ.s] = ++num; ecs_->root.push(num); arc.push(succ.acc); todo.emplace_back(succ.s, num, this); @@ -516,17 +490,20 @@ namespace spot continue; } + // It's an known state. Use i->first from now on. + succ.s->destroy(); + queue.erase(old); dec_depth(); // Skip dead states. - if (*i == -1) + if (i->second == -1) { - trace << "dead state" << std::endl; + trace << "dead state\n"; continue; } - trace << "merging..." << std::endl; + trace << "merging...\n"; // Now this is the most interesting case. We have // reached a state S1 which is already part of a @@ -542,7 +519,7 @@ namespace spot // merge all SCCs from the top of ROOT that have // an index greater to the one of the SCC of S2 // (called the "threshold"). - int threshold = *i; + int threshold = i->second; std::list rem; bdd acc = succ.acc; while (threshold < ecs_->root.top().index) @@ -571,7 +548,7 @@ namespace spot { // Use this state to start the computation of an accepting // cycle. - ecs_->cycle_seed = sip.first; + ecs_->cycle_seed = i->first; // We have found an accepting SCC. Clean up TODO. clear_todo(); @@ -595,10 +572,11 @@ namespace spot if (poprem_) { - numbered_state_heap::state_index_p spi = - ecs_->h->index(todo.back().s); - assert(spi.first); - ecs_->root.rem().push_front(spi.first); + const state* s = todo.back().s; + auto i = ecs_->h.find(s); + assert(i != ecs_->h.end()); + assert(i->first == s); + ecs_->root.rem().push_front(i->first); // Don't change the stack depth, since // we are just moving the state from TODO to REM. } @@ -613,20 +591,12 @@ namespace spot } } - numbered_state_heap::state_index_p - couvreur99_check_shy::find_state(const state* s) - { - return ecs_->h->find(s); - } - emptiness_check* - couvreur99(const tgba* a, - option_map o, - const numbered_state_heap_factory* nshf) + couvreur99(const tgba* a, option_map o) { if (o.get("shy")) - return new couvreur99_check_shy(a, o, nshf); - return new couvreur99_check(a, o, nshf); + return new couvreur99_check_shy(a, o); + return new couvreur99_check(a, o); } } diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index 44d33f23c..dc5de0e7e 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -137,10 +137,7 @@ namespace spot /// choosing a successor. Otherwise, only the successor of the /// topmost state on the DFS stack are considered. SPOT_API emptiness_check* - couvreur99(const tgba* a, - option_map options = option_map(), - const numbered_state_heap_factory* nshf - = numbered_state_heap_hash_map_factory::instance()); + couvreur99(const tgba* a, option_map options = option_map()); /// \brief An implementation of the Couvreur99 emptiness-check algorithm. @@ -149,10 +146,7 @@ namespace spot class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics { public: - couvreur99_check(const tgba* a, - option_map o = option_map(), - const numbered_state_heap_factory* nshf - = numbered_state_heap_hash_map_factory::instance()); + couvreur99_check(const tgba* a, option_map o = option_map()); virtual ~couvreur99_check(); /// Check whether the automaton's language is empty. @@ -194,10 +188,7 @@ namespace spot class SPOT_API couvreur99_check_shy : public couvreur99_check { public: - couvreur99_check_shy(const tgba* a, - option_map o = option_map(), - const numbered_state_heap_factory* nshf - = numbered_state_heap_hash_map_factory::instance()); + couvreur99_check_shy(const tgba* a, option_map o = option_map()); virtual ~couvreur99_check_shy(); virtual emptiness_check_result* check(); @@ -247,20 +238,6 @@ namespace spot // If the "group2" option is set (it implies "group"), we // reprocess the successor states of SCC that have been merged. bool group2_; - // If the onepass option is true, do only one pass. This cancels - // all the "shyness" of the algorithm, but we need the framework - // of the implementation when working with GreatSPN. - bool onepass_; - - /// \brief find the SCC number of a unprocessed state. - /// - /// Sometimes we want to modify some of the above structures when - /// looking up a new state. This happens for instance when find() - /// must perform inclusion checking and add new states to process - /// to TODO during this step. (Because TODO must be known, - /// sub-classing spot::numbered_state_heap is not enough.) Then - /// overriding this method is the way to go. - virtual numbered_state_heap::state_index_p find_state(const state* s); }; diff --git a/src/tgbaalgos/gtec/nsheap.cc b/src/tgbaalgos/gtec/nsheap.cc deleted file mode 100644 index ff615ba45..000000000 --- a/src/tgbaalgos/gtec/nsheap.cc +++ /dev/null @@ -1,182 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "nsheap.hh" - -namespace spot -{ - namespace - { - class numbered_state_heap_hash_map_const_iterator: - public numbered_state_heap_const_iterator - { - public: - numbered_state_heap_hash_map_const_iterator - (const numbered_state_heap_hash_map::hash_type& h) - : numbered_state_heap_const_iterator(), h(h) - { - } - - ~numbered_state_heap_hash_map_const_iterator() - { - } - - virtual void - first() - { - i = h.begin(); - } - - virtual void - next() - { - ++i; - } - - virtual bool - done() const - { - return i == h.end(); - } - - virtual const state* - get_state() const - { - return i->first; - } - - virtual int - get_index() const - { - return i->second; - } - - private: - numbered_state_heap_hash_map::hash_type::const_iterator i; - const numbered_state_heap_hash_map::hash_type& h; - }; - } // anonymous - - numbered_state_heap_hash_map::~numbered_state_heap_hash_map() - { - // Free keys in H. - hash_type::iterator i = h.begin(); - while (i != h.end()) - { - // Advance the iterator before deleting the key. - const state* s = i->first; - ++i; - s->destroy(); - } - } - - numbered_state_heap::state_index - numbered_state_heap_hash_map::find(const state* s) const - { - state_index res; - hash_type::const_iterator i = h.find(s); - - if (i == h.end()) - { - res.first = 0; - res.second = 0; - } - else - { - res.first = i->first; - res.second = i->second; - - if (s != i->first) - s->destroy(); - } - return res; - } - - numbered_state_heap::state_index_p - numbered_state_heap_hash_map::find(const state* s) - { - state_index_p res; - hash_type::iterator i = h.find(s); - - if (i == h.end()) - { - res.first = 0; - res.second = 0; - } - else - { - res.first = i->first; - res.second = &i->second; - - if (s != i->first) - s->destroy(); - } - return res; - } - - numbered_state_heap::state_index - numbered_state_heap_hash_map::index(const state* s) const - { - return this->numbered_state_heap_hash_map::find(s); - } - - numbered_state_heap::state_index_p - numbered_state_heap_hash_map::index(const state* s) - { - return this->numbered_state_heap_hash_map::find(s); - } - - void - numbered_state_heap_hash_map::insert(const state* s, int index) - { - h[s] = index; - } - - int - numbered_state_heap_hash_map::size() const - { - return h.size(); - } - - numbered_state_heap_const_iterator* - numbered_state_heap_hash_map::iterator() const - { - return new numbered_state_heap_hash_map_const_iterator(h); - } - - numbered_state_heap_hash_map_factory::numbered_state_heap_hash_map_factory() - : numbered_state_heap_factory() - { - } - - numbered_state_heap_hash_map* - numbered_state_heap_hash_map_factory::build() const - { - return new numbered_state_heap_hash_map(); - } - - const numbered_state_heap_hash_map_factory* - numbered_state_heap_hash_map_factory::instance() - { - static numbered_state_heap_hash_map_factory f; - return &f; - } -} diff --git a/src/tgbaalgos/gtec/nsheap.hh b/src/tgbaalgos/gtec/nsheap.hh deleted file mode 100644 index eb6401bad..000000000 --- a/src/tgbaalgos/gtec/nsheap.hh +++ /dev/null @@ -1,148 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Development de -// l'Epita (LRDE). -// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#ifndef SPOT_TGBAALGOS_GTEC_NSHEAP_HH -# define SPOT_TGBAALGOS_GTEC_NSHEAP_HH - -# include "tgba/state.hh" -# include "misc/hash.hh" - -namespace spot -{ - /// Iterator on numbered_state_heap objects. - class SPOT_API numbered_state_heap_const_iterator - { - public: - virtual ~numbered_state_heap_const_iterator() {} - - //@{ - /// Iteration - virtual void first() = 0; - virtual void next() = 0; - virtual bool done() const = 0; - //@} - - //@{ - /// Inspection - virtual const state* get_state() const = 0; - virtual int get_index() const = 0; - //@} - }; - - /// Keep track of a large quantity of indexed states. - class SPOT_API numbered_state_heap - { - public: - typedef std::pair state_index_p; - typedef std::pair state_index; - - virtual ~numbered_state_heap() {} - //@{ - /// \brief Is state in the heap? - /// - /// Returns a pair (0,0) if \a s is not in the heap. - /// or a pair (p, i) if there is a clone \a p of \a s \a i - /// in the heap with index. If \a s is in the heap and is different - /// from \a p it will be freed. - /// - /// These functions are called by the algorithm to check whether a - /// successor is a new state to explore or an already visited - /// state. - /// - /// These functions can be redefined to search for more - /// than an equal match. For example we could redefine - /// it to check state inclusion. - virtual state_index find(const state* s) const = 0; - virtual state_index_p find(const state* s) = 0; - //@} - - //@{ - /// \brief Return the index of an existing state. - /// - /// This is mostly similar to find(), except it will - /// be called for state which we know are already in - /// the heap, or for state which may not be in the - /// heap but for which it is always OK to do equality - /// checks. - virtual state_index index(const state* s) const = 0; - virtual state_index_p index(const state* s) = 0; - //@} - - /// Add a new state \a s with index \a index - virtual void insert(const state* s, int index) = 0; - - /// The number of stored states. - virtual int size() const = 0; - - /// Return an iterator on the states/indexes pairs. - virtual numbered_state_heap_const_iterator* iterator() const = 0; - }; - - /// Abstract factory for numbered_state_heap - class SPOT_API numbered_state_heap_factory - { - public: - virtual ~numbered_state_heap_factory() {} - virtual numbered_state_heap* build() const = 0; - }; - - /// A straightforward implementation of numbered_state_heap with a hash map. - class SPOT_API numbered_state_heap_hash_map : public numbered_state_heap - { - public: - virtual ~numbered_state_heap_hash_map(); - - virtual state_index find(const state* s) const; - virtual state_index_p find(const state* s); - virtual state_index index(const state* s) const; - virtual state_index_p index(const state* s); - - virtual void insert(const state* s, int index); - virtual int size() const; - - virtual numbered_state_heap_const_iterator* iterator() const; - - typedef std::unordered_map hash_type; - protected: - hash_type h; ///< Map of visited states. - }; - - /// \brief Factory for numbered_state_heap_hash_map. - /// - /// This class is a singleton. Retrieve the instance using instance(). - class SPOT_API numbered_state_heap_hash_map_factory: - public numbered_state_heap_factory - { - public: - virtual numbered_state_heap_hash_map* build() const; - - /// Get the unique instance of this class. - static const numbered_state_heap_hash_map_factory* instance(); - protected: - virtual ~numbered_state_heap_hash_map_factory() {} - numbered_state_heap_hash_map_factory(); - }; - -} - -#endif // SPOT_TGBAALGOS_GTEC_NSHEAP_HH diff --git a/src/tgbaalgos/gtec/status.cc b/src/tgbaalgos/gtec/status.cc index f7ec41ea8..9869105da 100644 --- a/src/tgbaalgos/gtec/status.cc +++ b/src/tgbaalgos/gtec/status.cc @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -22,31 +25,34 @@ namespace spot { - couvreur99_check_status::couvreur99_check_status - (const tgba* aut, - const numbered_state_heap_factory* nshf) - : aut(aut), - h(nshf->build()) + couvreur99_check_status::couvreur99_check_status(const tgba* aut) + : aut(aut) { } couvreur99_check_status::~couvreur99_check_status() { - delete h; + hash_type::iterator i = h.begin(); + while (i != h.end()) + { + // Advance the iterator before deleting the key. + const state* s = i->first; + ++i; + s->destroy(); + } } void couvreur99_check_status::print_stats(std::ostream& os) const { - os << h->size() << " unique states visited" << std::endl; + os << h.size() << " unique states visited" << std::endl; os << root.size() - << " strongly connected components in search stack" - << std::endl; + << " strongly connected components in search stack\n"; } int couvreur99_check_status::states() const { - return h->size(); + return h.size(); } } diff --git a/src/tgbaalgos/gtec/status.hh b/src/tgbaalgos/gtec/status.hh index 77f294f9f..971401eef 100644 --- a/src/tgbaalgos/gtec/status.hh +++ b/src/tgbaalgos/gtec/status.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -24,7 +24,6 @@ # define SPOT_TGBAALGOS_GTEC_STATUS_HH #include "sccstack.hh" -#include "nsheap.hh" #include "tgba/tgba.hh" #include @@ -38,13 +37,17 @@ namespace spot class SPOT_API couvreur99_check_status { public: - couvreur99_check_status(const tgba* aut, - const numbered_state_heap_factory* nshf); + couvreur99_check_status(const tgba* aut); + ~couvreur99_check_status(); const tgba* aut; scc_stack root; - numbered_state_heap* h; ///< Heap of visited states. + + typedef std::unordered_map hash_type; + hash_type h; + const state* cycle_seed; /// Output statistics about this object.