From 236742aed850e9031b4398fd1a2385818d27e8be Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 2 Feb 2006 13:46:04 +0000 Subject: [PATCH] * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check): Reorganize this function so that syntactically there is only one loop over the successors, and not two. Call reintroduce the call to couvreur99_check_shy::state_index(), needed by SSP, and suppress that to index_and_insert introduced on 2004-12-29. Also split the "group" option in two: "group" and "group2". "group2" is the equivalent of the older "group", while the new "group" is weaker and faster. (couvreur99_check_shy::state_index): Change prototype as needed by the algorithm. * src/tgbaalgos/gtec/gtec.hh: Adjust. * src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc (index_and_insert): Remove. * iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust to new prototype. * bench/emptchk/README, bench/emptchk/algorithms: Adjust references to group/group2. --- ChangeLog | 20 +++ bench/emptchk/README | 4 +- bench/emptchk/algorithms | 2 + iface/gspn/ssp.cc | 25 ++- src/tgbaalgos/gtec/gtec.cc | 318 ++++++++++++++++------------------- src/tgbaalgos/gtec/gtec.hh | 18 +- src/tgbaalgos/gtec/nsheap.cc | 15 +- src/tgbaalgos/gtec/nsheap.hh | 9 +- 8 files changed, 197 insertions(+), 214 deletions(-) diff --git a/ChangeLog b/ChangeLog index 3cc4cc144..63fb82594 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2006-02-02 Alexandre Duret-Lutz + + * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check): + Reorganize this function so that syntactically there is only one + loop over the successors, and not two. Call reintroduce the call + to couvreur99_check_shy::state_index(), needed by SSP, and + suppress that to index_and_insert introduced on 2004-12-29. Also + split the "group" option in two: "group" and "group2". "group2" + is the equivalent of the older "group", while the new "group" is + weaker and faster. + (couvreur99_check_shy::state_index): Change prototype as needed by + the algorithm. + * src/tgbaalgos/gtec/gtec.hh: Adjust. + * src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc + (index_and_insert): Remove. + * iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust + to new prototype. + * bench/emptchk/README, bench/emptchk/algorithms: Adjust references + to group/group2. + 2006-01-30 Alexandre Duret-Lutz * NEWS, configure.ac: Bump version to 0.3a. diff --git a/bench/emptchk/README b/bench/emptchk/README index d3e89aa29..66baf0633 100644 --- a/bench/emptchk/README +++ b/bench/emptchk/README @@ -194,9 +194,11 @@ This directory contains: Cou99 Cou99(shy !group) Cou99(shy group) + Cou99(shy group2) > Cou99(poprem) # called `Cou99' in the paper > Cou99(poprem shy !group) # called `Cou99 Shy-' in the paper - > Cou99(poprem shy group) # called `Cou99 Shy' in the paper + Cou99(poprem shy group) + > Cou99(poprem shy group2) # called `Cou99 Shy' in the paper > CVWY90 > GV04 > SE05 diff --git a/bench/emptchk/algorithms b/bench/emptchk/algorithms index f2f3085cc..201d038fb 100644 --- a/bench/emptchk/algorithms +++ b/bench/emptchk/algorithms @@ -1,9 +1,11 @@ Cou99 Cou99(shy !group) Cou99(shy group) +Cou99(shy group2) Cou99(poprem) Cou99(poprem shy !group) Cou99(poprem shy group) +Cou99(poprem shy group2) GV04 CVWY90 SE05 diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc index 4f1c09e11..2fa8e61dc 100644 --- a/iface/gspn/ssp.cc +++ b/iface/gspn/ssp.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -916,7 +916,7 @@ namespace spot option_map(), numbered_state_heap_ssp_factory_semi::instance()) { - } + } protected: @@ -924,7 +924,7 @@ namespace spot // children to the list of children of that older state. We cannot // to this by sub-classing numbered_state_heap since TODO is not // available. So we override find_state() instead. - virtual int* + virtual numbered_state_heap::state_index_p find_state(const state* s) { typedef numbered_state_heap_ssp_semi::hash_type hash_type; @@ -979,11 +979,22 @@ namespace spot } } } + + state_index_p res; if (i == h.end()) - return 0; - if (i->first != s) - delete s; - return &i->second; + { + res.first = 0; + res.second = 0; + } + else + { + res.first = i->first; + res.second = &i->second; + + if (s != i->first) + delete s; + } + return res; } }; diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 2a06d4c50..0bac3495b 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// 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. // // This file is part of Spot, a model checking library. // @@ -288,6 +288,20 @@ namespace spot ////////////////////////////////////////////////////////////////////// + couvreur99_check_shy::todo_item::todo_item(const state* s, int n, + couvreur99_check_shy* shy) + : s(s), n(n) + { + tgba_succ_iterator* iter = shy->ecs_->aut->succ_iter(s); + for (iter->first(); !iter->done(); iter->next(), shy->inc_transitions()) + { + q.push_back(successor(iter->current_acceptance_conditions(), + iter->current_state())); + shy->inc_depth(); + } + delete iter; + } + couvreur99_check_shy::couvreur99_check_shy(const tgba* a, option_map o, const numbered_state_heap_factory* @@ -295,11 +309,15 @@ namespace spot : couvreur99_check(a, o, nshf), num(1) { group_ = o.get("group", 1); + group2_ = o.get("group2", 0); + group_ |= group2_; // Setup depth-first search from the initial state. - todo.push_back(todo_item(0, 0)); - todo.back().q.push_front(successor(bddtrue, ecs_->aut->get_init_state())); - inc_depth(2); + const state* i = ecs_->aut->get_init_state(); + ecs_->h->insert(i, ++num); + ecs_->root.push(num); + todo.push_back(todo_item(i, num, this)); + inc_depth(1); } couvreur99_check_shy::~couvreur99_check_shy() @@ -334,9 +352,12 @@ namespace spot emptiness_check_result* couvreur99_check_shy::check() { + // Position in the loop seeking known successors. + succ_queue::iterator pos = todo.back().q.begin(); + for (;;) { - assert(ecs_->root.size() == arc.size()); + assert(ecs_->root.size() == 1 + arc.size()); // Get the successors of the current state. succ_queue& queue = todo.back().q; @@ -361,6 +382,8 @@ namespace spot return 0; } + pos = todo.back().q.begin(); + // If poprem is used, fill rem with any component removed, // so that remove_component() does not have to traverse // the SCC again. @@ -386,193 +409,138 @@ namespace spot continue; } - // Pick one successor off the list. - successor succ = queue.front(); - queue.pop_front(); - dec_depth(); + // We always make a first pass over the successors of a state + // to check whether it contains some state we have already seen. + // This way we hope to merge the most SCCs before stacking new + // states. + // + // So are we checking for known states ? If yes, POS tells us + // which state we are considering. Otherwise just pick the + // first one. + succ_queue::iterator old; + if (pos == queue.end()) + old = queue.begin(); + else + old = pos++; + successor succ = *old; - int& n = ecs_->h->index_and_insert(succ.s); - // Skip dead states. - if (n == -1) - continue; - // If it is known, it is necessarily in the current condition. - if (n != 0) + numbered_state_heap::state_index_p sip = find_state(succ.s); + int* i = sip.second; + + if (!i) { - assert(n >= ecs_->root.top().index); - ecs_->root.top().condition |= succ.acc; - - // Have we found all acceptance conditions? - if (ecs_->root.top().condition - == ecs_->aut->all_acceptance_conditions()) - { - // Use this state to start the computation of an accepting - // cycle. - ecs_->cycle_seed = succ.s; - // We have found an accepting SCC. Clean up TODO. - clear_todo(); - set_states(ecs_->states()); - return new couvreur99_check_result(ecs_, options()); - } - + // It's a new state. + // If we are seeking known states, just skip it. + if (pos != queue.end()) + continue; + // Otherwise, number it and stack it so we recurse. + queue.erase(old); + dec_depth(); + ecs_->h->insert(succ.s, ++num); + ecs_->root.push(num); + arc.push(succ.acc); + todo.push_back(todo_item(succ.s, num, this)); + pos = todo.back().q.begin(); + inc_depth(); continue; } - // It is a new state. Number it, and stack it. - n = ++num; - ecs_->root.push(num); - arc.push(succ.acc); - todo.push_back(todo_item(succ.s, num)); - inc_depth(); - succ_queue* new_queue = &todo.back().q; - tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s); - succ_queue::iterator merge_end; - bool merged = false; - for (iter->first(); !iter->done(); iter->next(), inc_transitions()) + queue.erase(old); + dec_depth(); + + // Skip dead states. + if (*i == -1) + continue; + + // Now this is the most interesting case. We have + // reached a state S1 which is already part of a + // non-dead SCC. Any such non-dead SCC has + // necessarily been crossed by our path to this + // state: there is a state S2 in our path which + // belongs to this SCC too. We are going to merge + // all states between this S1 and S2 into this + // SCC. + // + // This merge is easy to do because the order of + // the SCC in 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 = *i; + std::list rem; + bdd acc = succ.acc; + while (threshold < ecs_->root.top().index) { - const state* dest = iter->current_state(); - bdd acc = iter->current_acceptance_conditions(); - - numbered_state_heap::state_index_p sip = ecs_->h->find(dest); - int* i = sip.second; - // Add new states to the queue. - if (!i) - { - new_queue->push_back(successor(acc, dest)); - inc_depth(); - continue; - } - // Skip dead states. - if (*i == -1) - continue; - - // Now this is the most interesting case. We have - // reached a state S1 which is already part of a - // non-dead SCC. Any such non-dead SCC has - // necessarily been crossed by our path to this - // state: there is a state S2 in our path which - // belongs to this SCC too. We are going to merge - // all states between this S1 and S2 into this - // SCC. - // - // This merge is easy to do because the order of - // the SCC in 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 = *i; - std::list rem; - while (threshold < ecs_->root.top().index) - { - assert(!ecs_->root.empty()); - assert(!arc.empty()); - acc |= ecs_->root.top().condition; - acc |= arc.top(); - rem.splice(rem.end(), ecs_->root.rem()); - ecs_->root.pop(); - arc.pop(); - } - // Note that we do not always have - // threshold == ecs_->root.top().index - // after this loop, the SCC whose index is threshold - // might have been merged with a lower SCC. - - // Accumulate all acceptance conditions into the - // merged SCC. - ecs_->root.top().condition |= acc; - ecs_->root.rem().splice(ecs_->root.rem().end(), rem); - - // Have we found all acceptance conditions? - if (ecs_->root.top().condition - == ecs_->aut->all_acceptance_conditions()) - { - // Use this state to start the computation of an accepting - // cycle. - ecs_->cycle_seed = sip.first; - - // We have found an accepting SCC. Clean up TODO. - clear_todo(); - set_states(ecs_->states()); - delete iter; - return new couvreur99_check_result(ecs_, options()); - } - // Group the pending successors of formed SCC if requested. - if (group_) - { - assert(todo.back().s); - while (ecs_->root.top().index < todo.back().n) - { - todo_list::reverse_iterator prev = todo.rbegin(); - todo_list::reverse_iterator last = prev++; - if (!merged) - { - merge_end = last->q.begin(); - merged = true; - } - prev->q.splice(prev->q.end(), last->q); - - 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); - // Don't change the stack depth, since - // we are just moving the state from TODO to REM. - } - else - { - dec_depth(); - } - todo.pop_back(); - } - new_queue = &todo.back().q; - } + assert(!ecs_->root.empty()); + assert(!arc.empty()); + acc |= ecs_->root.top().condition; + acc |= arc.top(); + rem.splice(rem.end(), ecs_->root.rem()); + ecs_->root.pop(); + arc.pop(); } - delete iter; - if (merged) + // Note that we do not always have + // threshold == ecs_->root.top().index + // after this loop, the SCC whose index is threshold + // might have been merged with a lower SCC. + + // Accumulate all acceptance conditions into the + // merged SCC. + ecs_->root.top().condition |= acc; + ecs_->root.rem().splice(ecs_->root.rem().end(), rem); + + // Have we found all acceptance conditions? + if (ecs_->root.top().condition + == ecs_->aut->all_acceptance_conditions()) { - succ_queue::iterator q = new_queue->begin(); - while (q != merge_end && q != new_queue->end()) + // Use this state to start the computation of an accepting + // cycle. + ecs_->cycle_seed = sip.first; + + // We have found an accepting SCC. Clean up TODO. + clear_todo(); + set_states(ecs_->states()); + return new couvreur99_check_result(ecs_, options()); + } + // Group the pending successors of formed SCC if requested. + if (group_) + { + assert(todo.back().s); + while (ecs_->root.top().index < todo.back().n) { - numbered_state_heap::state_index_p sip = ecs_->h->find(q->s); - succ_queue::iterator old = q++; - int* i = sip.second; - // Skip new states. - if (!i) - continue; - bdd acc = old->acc; - // Delete other states. - new_queue->erase(old); - dec_depth(); - // Delete dead states. - if (*i == -1) - continue; + todo_list::reverse_iterator prev = todo.rbegin(); + todo_list::reverse_iterator last = prev++; + // If group2 is used we insert the last->q in front + // of prev->q so that the states in prev->q are checked + // for existence again after we have done with the states + // of last->q. Otherwise we just append to the end. + prev->q.splice(group2_ ? prev->q.begin() : prev->q.end(), + last->q); - // Merge existing states. - assert(n >= ecs_->root.top().index); - ecs_->root.top().condition |= acc; - - // Have we found all acceptance conditions? - if (ecs_->root.top().condition - == ecs_->aut->all_acceptance_conditions()) + if (poprem_) { - // Use this state to start the computation of an accepting - // cycle. - ecs_->cycle_seed = sip.first; - // We have found an accepting SCC. Clean up TODO. - clear_todo(); - set_states(ecs_->states()); - return new couvreur99_check_result(ecs_, options()); + numbered_state_heap::state_index_p spi = + ecs_->h->index(todo.back().s); + assert(spi.first); + ecs_->root.rem().push_front(spi.first); + // Don't change the stack depth, since + // we are just moving the state from TODO to REM. } + else + { + dec_depth(); + } + todo.pop_back(); } + pos = todo.back().q.begin(); } } } - int* + numbered_state_heap::state_index_p couvreur99_check_shy::find_state(const state* s) { - return ecs_->h->find(s).second; + return ecs_->h->find(s); } emptiness_check* diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index c2f3a45ac..12267567e 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// 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. // // This file is part of Spot, a model checking library. // @@ -222,11 +222,8 @@ namespace spot { const state* s; int n; - succ_queue q; - todo_item(const state* s, int n) - : s(s), n(n) - { - } + succ_queue q; // Unprocessed successors of S + todo_item(const state* s, int n, couvreur99_check_shy* shy); }; typedef std::list todo_list; @@ -237,6 +234,9 @@ namespace spot // Whether successors should be grouped for states in the same // SCC. bool group_; + // If the "group2" option is set (it implies "group"), we + // reprocess the successor states of SCC that have been merged. + bool group2_; /// \brief find the SCC number of a unprocessed state. /// @@ -246,7 +246,7 @@ namespace spot /// 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 int* find_state(const state* s); + 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 index 502a84094..4089a8c0e 100644 --- a/src/tgbaalgos/gtec/nsheap.cc +++ b/src/tgbaalgos/gtec/nsheap.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -150,19 +150,6 @@ namespace spot h[s] = index; } - int& - numbered_state_heap_hash_map::index_and_insert(const state*& s) - { - std::pair r - = h.insert(hash_type::value_type(s, 0)); - if (!r.second) - { - delete s; - s = r.first->first; - } - return r.first->second; - } - int numbered_state_heap_hash_map::size() const { diff --git a/src/tgbaalgos/gtec/nsheap.hh b/src/tgbaalgos/gtec/nsheap.hh index 796c46d5b..509d0ef3c 100644 --- a/src/tgbaalgos/gtec/nsheap.hh +++ b/src/tgbaalgos/gtec/nsheap.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// 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. // @@ -89,12 +89,6 @@ namespace spot /// Add a new state \a s with index \a index virtual void insert(const state* s, int index) = 0; - /// \brief Get the index of a state, and insert that state if it is missing. - /// - /// If a clone of \a s is already in the hash table, \a s will be deleted - /// and replaced by the address of the clone used. - virtual int& index_and_insert(const state*& s) = 0; - /// The number of stored states. virtual int size() const = 0; @@ -120,7 +114,6 @@ namespace spot 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 int& index_and_insert(const state*& s); virtual void insert(const state* s, int index); virtual int size() const;