diff --git a/src/ta/ta.cc b/src/ta/ta.cc index fc6fab0b4..ded4f5675 100644 --- a/src/ta/ta.cc +++ b/src/ta/ta.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement // de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -78,5 +78,3 @@ namespace spot } - - diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 83ecb22ce..853a0d76c 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement // de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -103,15 +103,15 @@ namespace spot { Sgi::hash_map >::const_iterator i = - transitions_by_condition.find(condition.id()); + transitions_by_condition.find(condition.id()); if (i == transitions_by_condition.end()) { - return 0; + return 0; } else { - return i->second; + return i->second; } } @@ -128,8 +128,8 @@ namespace spot if (transitions_condition == 0) { - transitions_condition = new transitions; - transitions_by_condition[(t->condition).id()] = transitions_condition; + transitions_condition = new transitions; + transitions_by_condition[(t->condition).id()] = transitions_condition; } transitions_condition->push_back(t); @@ -188,7 +188,7 @@ namespace spot int state_ta_explicit::compare(const spot::state* other) const { - const state_ta_explicit* o = dynamic_cast (other); + const state_ta_explicit* o = down_cast (other); assert(o); int compare_value = tgba_state_->compare(o->tgba_state_); @@ -219,37 +219,37 @@ namespace spot if (trans != 0) for (it_trans = trans->begin(); it_trans != trans->end();) - { - state_ta_explicit* dest = (*it_trans)->dest; - bool is_stuttering_transition = (get_tgba_condition() - == (dest)->get_tgba_condition()); - bool dest_is_livelock_accepting = dest->is_livelock_accepting_state(); + { + state_ta_explicit* dest = (*it_trans)->dest; + bool is_stuttering_transition = (get_tgba_condition() + == (dest)->get_tgba_condition()); + bool dest_is_livelock_accepting = dest->is_livelock_accepting_state(); - //Before deleting stuttering transitions, propaged back livelock and initial state's properties - if (is_stuttering_transition) - { - if (dest_is_livelock_accepting) - set_livelock_accepting_state(true); - if (dest->is_initial_state()) - set_initial_state(true); - } + //Before deleting stuttering transitions, propaged back livelock and initial state's properties + if (is_stuttering_transition) + { + if (dest_is_livelock_accepting) + set_livelock_accepting_state(true); + if (dest->is_initial_state()) + set_initial_state(true); + } - //remove hole successors states - state_ta_explicit::transitions* dest_trans = - (dest)->get_transitions(); - bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); - if (is_stuttering_transition || (dest_trans_empty - && (!dest_is_livelock_accepting))) - { - get_transitions((*it_trans)->condition)->remove(*it_trans); - delete (*it_trans); - it_trans = trans->erase(it_trans); - } - else - { - it_trans++; - } - } + //remove hole successors states + state_ta_explicit::transitions* dest_trans = + (dest)->get_transitions(); + bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); + if (is_stuttering_transition || (dest_trans_empty + && (!dest_is_livelock_accepting))) + { + get_transitions((*it_trans)->condition)->remove(*it_trans); + delete (*it_trans); + it_trans = trans->erase(it_trans); + } + else + { + it_trans++; + } + } } @@ -262,18 +262,18 @@ namespace spot // they are not cloned. if (trans != 0) for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) - { - delete *it_trans; - } + { + delete *it_trans; + } delete trans; get_tgba_state()->destroy(); Sgi::hash_map >::iterator i = - transitions_by_condition.begin(); + transitions_by_condition.begin(); while (i != transitions_by_condition.end()) { - delete i->second; - ++i; + delete i->second; + ++i; } } @@ -293,10 +293,10 @@ namespace spot ta::states_set_t::iterator it; for (it = states_set_.begin(); it != states_set_.end(); it++) { - state_ta_explicit* s = dynamic_cast (*it); + state_ta_explicit* s = down_cast (*it); - s->free_transitions(); - delete s; + s->free_transitions(); + delete s; } get_dict()->unregister_all_my_variables(this); delete tgba_; @@ -306,17 +306,17 @@ namespace spot ta_explicit::add_state(state_ta_explicit* s) { std::pair add_state_to_ta = - states_set_.insert(s); + states_set_.insert(s); - return dynamic_cast (*add_state_to_ta.first); + return static_cast (*add_state_to_ta.first); } void ta_explicit::add_to_initial_states_set(state* state) { - state_ta_explicit * s = dynamic_cast (state); - + state_ta_explicit * s = down_cast (state); + assert(s); s->set_initial_state(true); initial_states_set_.insert(s); @@ -326,7 +326,8 @@ namespace spot void ta_explicit::delete_stuttering_and_hole_successors(spot::state* s) { - state_ta_explicit * state = dynamic_cast (s); + state_ta_explicit * state = down_cast (s); + assert(state); state->delete_stuttering_and_hole_successors(); if (state->is_initial_state()) add_to_initial_states_set(state); @@ -354,35 +355,39 @@ namespace spot ta_explicit::get_state_condition(const spot::state* initial_state) const { const state_ta_explicit* sta = - dynamic_cast (initial_state); + down_cast (initial_state); + assert(sta); return sta->get_tgba_condition(); } bool ta_explicit::is_accepting_state(const spot::state* s) const { - const state_ta_explicit* sta = dynamic_cast (s); + const state_ta_explicit* sta = down_cast (s); + assert(sta); return sta->is_accepting_state(); } bool ta_explicit::is_initial_state(const spot::state* s) const { - const state_ta_explicit* sta = dynamic_cast (s); + const state_ta_explicit* sta = down_cast (s); + assert(sta); return sta->is_initial_state(); } bool ta_explicit::is_livelock_accepting_state(const spot::state* s) const { - const state_ta_explicit* sta = dynamic_cast (s); + const state_ta_explicit* sta = down_cast (s); + assert(sta); return sta->is_livelock_accepting_state(); } ta_succ_iterator* ta_explicit::succ_iter(const spot::state* state) const { - const state_ta_explicit* s = dynamic_cast (state); + const state_ta_explicit* s = down_cast (state); assert(s); return new ta_explicit_succ_iterator(s); } @@ -390,7 +395,7 @@ namespace spot ta_succ_iterator* ta_explicit::succ_iter(const spot::state* state, bdd condition) const { - const state_ta_explicit* s = dynamic_cast (state); + const state_ta_explicit* s = down_cast (state); assert(s); return new ta_explicit_succ_iterator(s, condition); } @@ -410,14 +415,14 @@ namespace spot std::string ta_explicit::format_state(const spot::state* s) const { - const state_ta_explicit* sta = dynamic_cast (s); + const state_ta_explicit* sta = down_cast (s); assert(sta); if (sta->get_tgba_condition() == bddtrue) return tgba_->format_state(sta->get_tgba_state()); return tgba_->format_state(sta->get_tgba_state()) + "\n" - + bdd_format_formula(get_dict(), sta->get_tgba_condition()); + + bdd_format_formula(get_dict(), sta->get_tgba_condition()); } @@ -428,26 +433,26 @@ namespace spot for (it = states_set_.begin(); it != states_set_.end(); it++) { - const state_ta_explicit* source = - dynamic_cast (*it); + const state_ta_explicit* source = + static_cast (*it); - state_ta_explicit::transitions* trans = source->get_transitions(); - state_ta_explicit::transitions::iterator it_trans; + state_ta_explicit::transitions* trans = source->get_transitions(); + state_ta_explicit::transitions::iterator it_trans; - if (trans != 0) - for (it_trans = trans->begin(); it_trans != trans->end();) - { - if (source->get_tgba_condition() - == ((*it_trans)->dest)->get_tgba_condition()) - { - delete *it_trans; - it_trans = trans->erase(it_trans); - } - else - { - it_trans++; - } - } + if (trans != 0) + for (it_trans = trans->begin(); it_trans != trans->end();) + { + if (source->get_tgba_condition() + == ((*it_trans)->dest)->get_tgba_condition()) + { + delete *it_trans; + it_trans = trans->erase(it_trans); + } + else + { + it_trans++; + } + } } } diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index d849e4bfa..51710649b 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -31,7 +31,7 @@ namespace spot state_ta_product::state_ta_product(const state_ta_product& o) : state(), ta_state_(o.get_ta_state()), kripke_state_( - o.get_kripke_state()->clone()) + o.get_kripke_state()->clone()) { } @@ -44,7 +44,7 @@ namespace spot int state_ta_product::compare(const state* other) const { - const state_ta_product* o = dynamic_cast (other); + const state_ta_product* o = down_cast (other); assert(o); int res = ta_state_->compare(o->get_ta_state()); if (res != 0) @@ -91,9 +91,9 @@ namespace spot ta_succ_it_->next(); if (ta_succ_it_->done()) { - delete ta_succ_it_; - ta_succ_it_ = 0; - kripke_succ_it_->next(); + delete ta_succ_it_; + ta_succ_it_ = 0; + kripke_succ_it_->next(); } } @@ -111,9 +111,9 @@ namespace spot // done().) if (kripke_succ_it_->done()) { - delete kripke_succ_it_; - kripke_succ_it_ = 0; - return; + delete kripke_succ_it_; + kripke_succ_it_ = 0; + return; } next_non_stuttering_(); @@ -126,8 +126,8 @@ namespace spot current_state_ = 0; if (is_stuttering_transition()) { - ta_succ_it_ = 0; - kripke_succ_it_->next(); + ta_succ_it_ = 0; + kripke_succ_it_->next(); } else step_(); @@ -144,34 +144,34 @@ namespace spot while (!done()) { - state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); - bdd dc = kripke_->state_condition(kripke_succ_it_current_state); + state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); + bdd dc = kripke_->state_condition(kripke_succ_it_current_state); - is_stuttering_transition_ = (sc == dc); - if (is_stuttering_transition_) - { - //if stuttering transition, the TA automata stays in the same state - current_state_ = new state_ta_product(source_->get_ta_state(), - kripke_succ_it_current_state); - current_condition_ = bddtrue; - return; - } + is_stuttering_transition_ = (sc == dc); + if (is_stuttering_transition_) + { + //if stuttering transition, the TA automata stays in the same state + current_state_ = new state_ta_product(source_->get_ta_state(), + kripke_succ_it_current_state); + current_condition_ = bddtrue; + return; + } - if (ta_succ_it_ == 0){ - current_condition_ = bdd_setxor(sc, dc); - ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), current_condition_); - ta_succ_it_->first(); - } + if (ta_succ_it_ == 0){ + current_condition_ = bdd_setxor(sc, dc); + ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), current_condition_); + ta_succ_it_->first(); + } - if (!ta_succ_it_->done()) - { - current_state_ = new state_ta_product(ta_succ_it_->current_state(), - kripke_succ_it_current_state); - return; - } + if (!ta_succ_it_->done()) + { + current_state_ = new state_ta_product(ta_succ_it_->current_state(), + kripke_succ_it_current_state); + return; + } - kripke_succ_it_current_state->destroy(); - step_(); + kripke_succ_it_current_state->destroy(); + step_(); } } @@ -227,7 +227,7 @@ namespace spot ta_product::ta_product(const ta* testing_automata, const kripke* kripke_structure) : dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_( - kripke_structure) + kripke_structure) { assert(dict_ == kripke_structure->get_dict()); dict_->register_all_variables_of(&ta_, this); @@ -252,19 +252,19 @@ namespace spot for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++) { - state* kripke_init_state = kripke_->get_init_state(); - if ((kripke_->state_condition(kripke_init_state)) - == (ta_->get_state_condition(*it))) - { - state_ta_product* stp = new state_ta_product((*it), - kripke_init_state); + state* kripke_init_state = kripke_->get_init_state(); + if ((kripke_->state_condition(kripke_init_state)) + == (ta_->get_state_condition(*it))) + { + state_ta_product* stp = new state_ta_product((*it), + kripke_init_state); - initial_states_set.insert(stp); - } - else - { - kripke_init_state->destroy(); - } + initial_states_set.insert(stp); + } + else + { + kripke_init_state->destroy(); + } } @@ -274,7 +274,7 @@ namespace spot ta_succ_iterator_product* ta_product::succ_iter(const state* s) const { - const state_ta_product* stp = dynamic_cast (s); + const state_ta_product* stp = down_cast (s); assert(s); return new ta_succ_iterator_product(stp, ta_, kripke_); @@ -289,16 +289,17 @@ namespace spot std::string ta_product::format_state(const state* state) const { - const state_ta_product* s = dynamic_cast (state); + const state_ta_product* s = down_cast (state); assert(s); return kripke_->format_state(s->get_kripke_state()) + " * \n" - + ta_->format_state(s->get_ta_state()); + + ta_->format_state(s->get_ta_state()); } bool ta_product::is_accepting_state(const spot::state* s) const { - const state_ta_product* stp = dynamic_cast (s); + const state_ta_product* stp = down_cast (s); + assert(stp); return ta_->is_accepting_state(stp->get_ta_state()); } @@ -306,7 +307,8 @@ namespace spot bool ta_product::is_livelock_accepting_state(const spot::state* s) const { - const state_ta_product* stp = dynamic_cast (s); + const state_ta_product* stp = down_cast (s); + assert(stp); return ta_->is_livelock_accepting_state(stp->get_ta_state()); } @@ -314,21 +316,23 @@ namespace spot bool ta_product::is_initial_state(const spot::state* s) const { - const state_ta_product* stp = dynamic_cast (s); + const state_ta_product* stp = down_cast (s); + assert(stp); state* ta_s = stp->get_ta_state(); state* kr_s = stp->get_kripke_state(); return (ta_->is_initial_state(ta_s)) - && ((kripke_->get_init_state())->compare(kr_s) == 0) - && ((kripke_->state_condition(kr_s)) - == (ta_->get_state_condition(ta_s))); + && ((kripke_->get_init_state())->compare(kr_s) == 0) + && ((kripke_->state_condition(kr_s)) + == (ta_->get_state_condition(ta_s))); } bdd ta_product::get_state_condition(const spot::state* s) const { - const state_ta_product* stp = dynamic_cast (s); + const state_ta_product* stp = down_cast (s); + assert(stp); state* ta_s = stp->get_ta_state(); return ta_->get_state_condition(ta_s); } @@ -337,7 +341,8 @@ namespace spot ta_product::free_state(const spot::state* s) const { - const state_ta_product* stp = dynamic_cast (s); + const state_ta_product* stp = down_cast (s); + assert(stp); ta_->free_state(stp->get_ta_state()); delete stp; diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 16798a194..2c52bb3ed 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -1,8 +1,5 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement +// Copyright (C) 2010, 2011 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. // // This file is part of Spot, a model checking library. // @@ -57,7 +54,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(); ///< Heap of visited states. + numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. // * num: the number of visited nodes. Used to set the order of each // visited node, @@ -74,7 +71,7 @@ namespace spot std::stack init_set; Sgi::hash_map - colour; + colour; trace << "PASS 1" << std::endl; @@ -84,7 +81,7 @@ namespace spot //const std::string BLACK = "BK"; Sgi::hash_map, - state_ptr_hash, state_ptr_equal> liveset; + state_ptr_hash, state_ptr_equal> liveset; std::stack livelock_roots; @@ -92,233 +89,233 @@ namespace spot ta::states_set_t::const_iterator it; for (it = init_states_set.begin(); it != init_states_set.end(); it++) { - state* init_state = (*it); - init_set.push(init_state); - //colour[init_state] = WHITE; + state* init_state = (*it); + init_set.push(init_state); + //colour[init_state] = WHITE; } while (!init_set.empty()) { - // Setup depth-first search from initial states. + // Setup depth-first search from initial states. - { - state* init = dynamic_cast (init_set.top()); - init_set.pop(); + { + state* init = init_set.top(); + init_set.pop(); - numbered_state_heap::state_index_p h_init = h->find(init); + numbered_state_heap::state_index_p h_init = h->find(init); - if (h_init.first) - continue; + if (h_init.first) + continue; - h->insert(init, ++num); - scc.push(num); + h->insert(init, ++num); + scc.push(num); - ta_succ_iterator* iter = a_->succ_iter(init); - iter->first(); - todo.push(pair_state_iter(init, iter)); - //colour[init] = GREY; - inc_depth(); + ta_succ_iterator* iter = a_->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); + //colour[init] = GREY; + inc_depth(); - //push potential root of live-lock accepting cycle - if (a_->is_livelock_accepting_state(init)) - livelock_roots.push(init); + //push potential root of live-lock accepting cycle + if (a_->is_livelock_accepting_state(init)) + livelock_roots.push(init); - } + } - while (!todo.empty()) - { + while (!todo.empty()) + { - state* curr = todo.top().first; + state* curr = todo.top().first; - // We are looking at the next successor in SUCC. - ta_succ_iterator* succ = todo.top().second; + // We are looking at the next successor in SUCC. + ta_succ_iterator* succ = todo.top().second; - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. - // Backtrack TODO. - todo.pop(); - dec_depth(); - trace - << "PASS 1 : backtrack" << std::endl; + // Backtrack TODO. + todo.pop(); + dec_depth(); + trace + << "PASS 1 : backtrack" << std::endl; - // fill rem with any component removed, - numbered_state_heap::state_index_p spi = - h->index(curr->clone()); - assert(spi.first); + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = + h->index(curr->clone()); + assert(spi.first); - scc.rem().push_front(curr); - inc_depth(); + 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); + // set the h value of the Backtracked state to negative value. + // colour[curr] = BLUE; + *spi.second = -std::abs(*spi.second); - // Backtrack livelock_roots. - if (!livelock_roots.empty() && !livelock_roots.top()->compare( - curr)) - livelock_roots.pop(); + // Backtrack livelock_roots. + if (!livelock_roots.empty() && !livelock_roots.top()->compare( + curr)) + livelock_roots.pop(); - // 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(!scc.empty()); - if (scc.top().index == std::abs(*spi.second)) - { - // removing states - std::list::iterator i; + // 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(!scc.empty()); + if (scc.top().index == std::abs(*spi.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 (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; - } - dec_depth(scc.rem().size()); - scc.pop(); - } + } + dec_depth(scc.rem().size()); + scc.pop(); + } - delete succ; - // Do not delete CURR: it is a key in H. - continue; - } + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } - // We have a successor to look at. - inc_transitions(); - trace - << "PASS 1: transition" << std::endl; - // Fetch the values destination state we are interested in... - state* dest = succ->current_state(); + // We have a successor to look at. + inc_transitions(); + trace + << "PASS 1: transition" << std::endl; + // Fetch the values destination state we are interested in... + state* dest = succ->current_state(); - //may be Buchi accepting scc - scc.top().is_accepting = a_->is_accepting_state(curr) - && !succ->is_stuttering_transition(); + //may be Buchi accepting scc + scc.top().is_accepting = a_->is_accepting_state(curr) + && !succ->is_stuttering_transition(); - bool is_stuttering_transition = succ->is_stuttering_transition(); + bool is_stuttering_transition = succ->is_stuttering_transition(); - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // 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); + // 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) - { - // Number it, stack it, and register its successors - // for later processing. - h->insert(dest, ++num); - scc.push(num); + // Is this a new state? + if (!spi.first) + { + // Number it, stack it, and register its successors + // for later processing. + h->insert(dest, ++num); + scc.push(num); - ta_succ_iterator* iter = a_->succ_iter(dest); - iter->first(); - todo.push(pair_state_iter(dest, iter)); - //colour[dest] = GREY; - inc_depth(); + ta_succ_iterator* iter = a_->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + //colour[dest] = GREY; + inc_depth(); - //push potential root of live-lock accepting cycle - if (a_->is_livelock_accepting_state(dest) - && !is_stuttering_transition) - livelock_roots.push(dest); + //push potential root of live-lock accepting cycle + if (a_->is_livelock_accepting_state(dest) + && !is_stuttering_transition) + livelock_roots.push(dest); - continue; - } + continue; + } - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - continue; + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; - // Now this is the most interesting case. We have reached a - // state S1 which is already part of a non-dead SSCC. Any such - // non-dead SSCC has necessarily been crossed by our path to - // this state: there is a state S2 in our path which belongs - // to this SSCC too. We are going to merge all states between - // this S1 and S2 into this SSCC. - // - // This merge is easy to do because the order of the SSCC in - // 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); - std::list rem; - bool acc = false; + // Now this is the most interesting case. We have reached a + // state S1 which is already part of a non-dead SSCC. Any such + // non-dead SSCC has necessarily been crossed by our path to + // this state: there is a state S2 in our path which belongs + // to this SSCC too. We are going to merge all states between + // this S1 and S2 into this SSCC. + // + // This merge is easy to do because the order of the SSCC in + // 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); + std::list rem; + bool acc = false; - while (threshold < scc.top().index) - { - assert(!scc.empty()); + while (threshold < scc.top().index) + { + assert(!scc.empty()); - acc |= scc.top().is_accepting; + acc |= scc.top().is_accepting; - rem.splice(rem.end(), scc.rem()); - scc.pop(); + rem.splice(rem.end(), scc.rem()); + scc.pop(); - } - // Note that we do not always have - // threshold == scc.top().index - // after this loop, the SSCC whose index is threshold might have - // been merged with a lower SSCC. + } + // Note that we do not always have + // threshold == scc.top().index + // after this loop, the SSCC whose index is threshold might have + // been merged with a lower SSCC. - // Accumulate all acceptance conditions into the merged SSCC. - scc.top().is_accepting |= acc; + // Accumulate all acceptance conditions into the merged SSCC. + scc.top().is_accepting |= acc; - scc.rem().splice(scc.rem().end(), rem); - if (scc.top().is_accepting) - { - clear(h, todo, init_set); - trace - << "PASS 1: SUCCESS" << std::endl; - return true; - } + scc.rem().splice(scc.rem().end(), rem); + if (scc.top().is_accepting) + { + clear(h, todo, init_set); + trace + << "PASS 1: SUCCESS" << std::endl; + return true; + } - //ADDLINKS - if (!is_full_2_pass_ && a_->is_livelock_accepting_state(curr) - && is_stuttering_transition) - { - trace - << "PASS 1: heuristic livelock detection " << std::endl; - const state* dest = spi.first; - std::set liveset_dest = - liveset[dest]; + //ADDLINKS + if (!is_full_2_pass_ && a_->is_livelock_accepting_state(curr) + && is_stuttering_transition) + { + trace + << "PASS 1: heuristic livelock detection " << std::endl; + const state* dest = spi.first; + std::set liveset_dest = + liveset[dest]; - std::set liveset_curr = - liveset[curr]; + std::set liveset_curr = + liveset[curr]; - int h_livelock_root = 0; - if (!livelock_roots.empty()) - h_livelock_root = *(h->find((livelock_roots.top()))).second; + int h_livelock_root = 0; + if (!livelock_roots.empty()) + h_livelock_root = *(h->find((livelock_roots.top()))).second; - if (heuristic_livelock_detection(dest, h, h_livelock_root, - liveset_curr)) - { - clear(h, todo, init_set); - return true; - } + if (heuristic_livelock_detection(dest, h, h_livelock_root, + liveset_curr)) + { + clear(h, todo, init_set); + 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, init_set); - 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, init_set); + return true; + } - } + } - } - } + } + } } @@ -329,21 +326,21 @@ namespace spot bool ta_check::heuristic_livelock_detection(const state * u, numbered_state_heap* h, int h_livelock_root, std::set liveset_curr) + state_ptr_less_than> liveset_curr) { numbered_state_heap::state_index_p hu = h->find(u); if (*hu.second > 0) // colour[u] == GREY { - if (*hu.second >= h_livelock_root) - { - trace - << "PASS 1: heuristic livelock detection SUCCESS" << std::endl; - return true; - } + if (*hu.second >= h_livelock_root) + { + trace + << "PASS 1: heuristic livelock detection SUCCESS" << std::endl; + return true; + } - liveset_curr.insert(u); + liveset_curr.insert(u); } return false; @@ -361,7 +358,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(); ///< Heap of visited states. + numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. // * num: the number of visited nodes. Used to set the order of each // visited node, @@ -387,8 +384,8 @@ namespace spot ta::states_set_t::const_iterator it; for (it = init_states_set.begin(); it != init_states_set.end(); it++) { - state* init_state = (*it); - init_set.push(init_state); + state* init_state = (*it); + init_set.push(init_state); } @@ -396,180 +393,180 @@ namespace spot while (!init_set.empty()) { - // Setup depth-first search from initial states. - { - state* init = init_set.top(); - init_set.pop(); - numbered_state_heap::state_index_p h_init = h->find(init); + // Setup depth-first search from initial states. + { + state* init = init_set.top(); + init_set.pop(); + numbered_state_heap::state_index_p h_init = h->find(init); - if (h_init.first) - continue; + if (h_init.first) + continue; - h->insert(init, ++num); - sscc.push(num); - sscc.top().is_accepting = t->is_livelock_accepting_state(init); - ta_succ_iterator* iter = t->succ_iter(init); - iter->first(); - todo.push(pair_state_iter(init, iter)); - inc_depth(); + h->insert(init, ++num); + sscc.push(num); + sscc.top().is_accepting = t->is_livelock_accepting_state(init); + ta_succ_iterator* iter = t->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); + inc_depth(); - } + } - while (!todo.empty()) - { + while (!todo.empty()) + { - state* curr = todo.top().first; + state* curr = todo.top().first; - // We are looking at the next successor in SUCC. - ta_succ_iterator* succ = todo.top().second; + // We are looking at the next successor in SUCC. + ta_succ_iterator* succ = todo.top().second; - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. - // Backtrack TODO. - todo.pop(); - dec_depth(); - trace - << "PASS 2 : backtrack" << std::endl; + // Backtrack TODO. + todo.pop(); + dec_depth(); + trace + << "PASS 2 : backtrack" << std::endl; - // fill rem with any component removed, - numbered_state_heap::state_index_p spi = - h->index(curr->clone()); - assert(spi.first); + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = + h->index(curr->clone()); + assert(spi.first); - sscc.rem().push_front(curr); - inc_depth(); + sscc.rem().push_front(curr); + inc_depth(); - // 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) - { - // removing states - std::list::iterator i; + // 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) + { + // 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; - } - dec_depth(sscc.rem().size()); - sscc.pop(); - } + 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; + } + dec_depth(sscc.rem().size()); + sscc.pop(); + } - delete succ; - // Do not delete CURR: it is a key in H. + delete succ; + // Do not delete CURR: it is a key in H. - continue; - } + continue; + } - // We have a successor to look at. - inc_transitions(); - trace - << "PASS 2 : transition" << std::endl; - // Fetch the values destination state we are interested in... - state* dest = succ->current_state(); + // We have a successor to look at. + inc_transitions(); + trace + << "PASS 2 : transition" << std::endl; + // Fetch the values destination state we are interested in... + state* dest = succ->current_state(); - bool is_stuttering_transition = succ->is_stuttering_transition(); - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. + bool is_stuttering_transition = succ->is_stuttering_transition(); + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. - numbered_state_heap::state_index_p spi = h->find(dest); + numbered_state_heap::state_index_p spi = h->find(dest); - // Is this a new state? - if (!spi.first) - { + // Is this a new state? + if (!spi.first) + { - // Are we going to a new state through a stuttering transition? + // Are we going to a new state through a stuttering transition? - if (!is_stuttering_transition) - { - init_set.push(dest); - continue; - } + if (!is_stuttering_transition) + { + init_set.push(dest); + continue; + } - // Number it, stack it, and register its successors - // for later processing. - h->insert(dest, ++num); - sscc.push(num); - sscc.top().is_accepting = t->is_livelock_accepting_state(dest); + // Number it, stack it, and register its successors + // for later processing. + h->insert(dest, ++num); + sscc.push(num); + sscc.top().is_accepting = t->is_livelock_accepting_state(dest); - ta_succ_iterator* iter = t->succ_iter(dest); - iter->first(); - todo.push(pair_state_iter(dest, iter)); - inc_depth(); - continue; - } + ta_succ_iterator* iter = t->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + inc_depth(); + continue; + } - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - continue; + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; - //self loop state - if (!curr->compare(spi.first)) - { - state * self_loop_state = (curr); + //self loop state + if (!curr->compare(spi.first)) + { + state * self_loop_state = (curr); - if (t->is_livelock_accepting_state(self_loop_state)) - { - clear(h, todo, init_set); - trace - << "PASS 2: SUCCESS" << std::endl; - return true; - } + if (t->is_livelock_accepting_state(self_loop_state)) + { + clear(h, todo, init_set); + trace + << "PASS 2: SUCCESS" << std::endl; + return true; + } - } + } - // Now this is the most interesting case. We have reached a - // state S1 which is already part of a non-dead SSCC. Any such - // non-dead SSCC has necessarily been crossed by our path to - // this state: there is a state S2 in our path which belongs - // to this SSCC too. We are going to merge all states between - // this S1 and S2 into this SSCC. - // - // This merge is easy to do because the order of the SSCC in - // 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; - std::list rem; - bool acc = false; + // Now this is the most interesting case. We have reached a + // state S1 which is already part of a non-dead SSCC. Any such + // non-dead SSCC has necessarily been crossed by our path to + // this state: there is a state S2 in our path which belongs + // to this SSCC too. We are going to merge all states between + // this S1 and S2 into this SSCC. + // + // This merge is easy to do because the order of the SSCC in + // 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; + std::list rem; + bool acc = false; - while (threshold < sscc.top().index) - { - assert(!sscc.empty()); + while (threshold < sscc.top().index) + { + assert(!sscc.empty()); - acc |= sscc.top().is_accepting; + acc |= sscc.top().is_accepting; - rem.splice(rem.end(), sscc.rem()); - sscc.pop(); + rem.splice(rem.end(), sscc.rem()); + sscc.pop(); - } - // Note that we do not always have - // threshold == sscc.top().index - // after this loop, the SSCC whose index is threshold might have - // been merged with a lower SSCC. + } + // Note that we do not always have + // threshold == sscc.top().index + // after this loop, the SSCC whose index is threshold might have + // been merged with a lower SSCC. - // Accumulate all acceptance conditions into the merged SSCC. - sscc.top().is_accepting |= acc; + // Accumulate all acceptance conditions into the merged SSCC. + sscc.top().is_accepting |= acc; - sscc.rem().splice(sscc.rem().end(), rem); - if (sscc.top().is_accepting) - { - clear(h, todo, init_set); - trace - << "PASS 2: SUCCESS" << std::endl; - return true; - } - } + sscc.rem().splice(sscc.rem().end(), rem); + if (sscc.top().is_accepting) + { + clear(h, todo, init_set); + trace + << "PASS 2: SUCCESS" << std::endl; + return true; + } + } } clear(h, todo, init_set); @@ -585,16 +582,16 @@ namespace spot while (!init_states.empty()) { - a_->free_state(init_states.top()); - init_states.pop(); + a_->free_state(init_states.top()); + init_states.pop(); } // Release all iterators in TODO. while (!todo.empty()) { - delete todo.top().second; - todo.pop(); - dec_depth(); + delete todo.top().second; + todo.pop(); + dec_depth(); } delete h; } @@ -607,7 +604,7 @@ namespace spot //TODO sscc; os << scc.size() << " strongly connected components in search stack" - << std::endl; + << std::endl; os << transitions() << " transitions explored" << std::endl; os << max_depth() << " items max in DFS search stack" << std::endl; return os; diff --git a/src/taalgos/sba2ta.cc b/src/taalgos/sba2ta.cc index 7bf4e9a79..3f492daaa 100644 --- a/src/taalgos/sba2ta.cc +++ b/src/taalgos/sba2ta.cc @@ -50,70 +50,70 @@ namespace spot bdd satone_tgba_condition; while ((satone_tgba_condition = bdd_satoneset(tgba_condition, - atomic_propositions_set_, bddtrue)) != bddfalse) + atomic_propositions_set_, bddtrue)) != bddfalse) { - tgba_condition -= satone_tgba_condition; - state_ta_explicit* init_state = new state_ta_explicit( - tgba_init_state->clone(), satone_tgba_condition, true, - tgba_->state_is_accepting(tgba_init_state)); - state_ta_explicit* is = ta->add_state(init_state); - assert(is == init_state); - ta->add_to_initial_states_set(is); - todo.push(init_state); + tgba_condition -= satone_tgba_condition; + state_ta_explicit* init_state = new state_ta_explicit( + tgba_init_state->clone(), satone_tgba_condition, true, + tgba_->state_is_accepting(tgba_init_state)); + state_ta_explicit* is = ta->add_state(init_state); + assert(is == init_state); + ta->add_to_initial_states_set(is); + todo.push(init_state); } tgba_init_state->destroy(); while (!todo.empty()) { - state_ta_explicit* source = todo.top(); - todo.pop(); + state_ta_explicit* source = todo.top(); + todo.pop(); - tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter( - source->get_tgba_state()); - for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next()) - { - const state* tgba_state = tgba_succ_it->current_state(); - bdd tgba_condition = tgba_succ_it->current_condition(); - bdd satone_tgba_condition; - while ((satone_tgba_condition = bdd_satoneset(tgba_condition, - atomic_propositions_set_, bddtrue)) != bddfalse) - { + tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter( + source->get_tgba_state()); + for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next()) + { + const state* tgba_state = tgba_succ_it->current_state(); + bdd tgba_condition = tgba_succ_it->current_condition(); + bdd satone_tgba_condition; + while ((satone_tgba_condition = bdd_satoneset(tgba_condition, + atomic_propositions_set_, bddtrue)) != bddfalse) + { - tgba_condition -= satone_tgba_condition; + tgba_condition -= satone_tgba_condition; - bdd all_props = bddtrue; - bdd dest_condition; - if (satone_tgba_condition == source->get_tgba_condition()) - while ((dest_condition = bdd_satoneset(all_props, - atomic_propositions_set_, bddtrue)) != bddfalse) - { - all_props -= dest_condition; - state_ta_explicit* new_dest = new state_ta_explicit( - tgba_state->clone(), dest_condition, false, - tgba_->state_is_accepting(tgba_state)); + bdd all_props = bddtrue; + bdd dest_condition; + if (satone_tgba_condition == source->get_tgba_condition()) + while ((dest_condition = bdd_satoneset(all_props, + atomic_propositions_set_, bddtrue)) != bddfalse) + { + all_props -= dest_condition; + state_ta_explicit* new_dest = new state_ta_explicit( + tgba_state->clone(), dest_condition, false, + tgba_->state_is_accepting(tgba_state)); - state_ta_explicit* dest = ta->add_state(new_dest); + state_ta_explicit* dest = ta->add_state(new_dest); - if (dest != new_dest) - { - // the state dest already exists in the testing automata - new_dest->get_tgba_state()->destroy(); - delete new_dest; - } - else - { - todo.push(dest); - } + if (dest != new_dest) + { + // the state dest already exists in the testing automata + new_dest->get_tgba_state()->destroy(); + delete new_dest; + } + else + { + todo.push(dest); + } - ta->create_transition(source, bdd_setxor( - source->get_tgba_condition(), - dest->get_tgba_condition()), dest); - } + ta->create_transition(source, bdd_setxor( + source->get_tgba_condition(), + dest->get_tgba_condition()), dest); + } - } - tgba_state->destroy(); - } - delete tgba_succ_it; + } + tgba_state->destroy(); + } + delete tgba_succ_it; } @@ -138,7 +138,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(); ///< Heap of visited states. + numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. // * num: the number of visited nodes. Used to set the order of each // visited node, @@ -158,196 +158,197 @@ namespace spot 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 = down_cast (*it); - init_set.push(init_state); + state* init_state = down_cast (*it); + init_set.push(init_state); } while (!init_set.empty()) { - // Setup depth-first search from initial states. - { - state_ta_explicit* init = - down_cast (init_set.top()); - init_set.pop(); - state_ta_explicit* init_clone = init->clone(); - numbered_state_heap::state_index_p h_init = h->find(init_clone); + // Setup depth-first search from initial states. + { + state_ta_explicit* init = + down_cast (init_set.top()); + init_set.pop(); + state_ta_explicit* init_clone = init->clone(); + numbered_state_heap::state_index_p h_init = h->find(init_clone); - if (h_init.first) - continue; + if (h_init.first) + continue; - h->insert(init_clone, ++num); - sscc.push(num); - 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)); + h->insert(init_clone, ++num); + sscc.push(num); + 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)); - } + } - while (!todo.empty()) - { + while (!todo.empty()) + { - state* curr = todo.top().first; + state* curr = todo.top().first; - numbered_state_heap::state_index_p spi = h->find(curr->clone()); - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - { - todo.pop(); - continue; - } + numbered_state_heap::state_index_p spi = h->find(curr->clone()); + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + { + todo.pop(); + continue; + } - // We are looking at the next successor in SUCC. - tgba_succ_iterator* succ = todo.top().second; + // We are looking at the next successor in SUCC. + tgba_succ_iterator* succ = todo.top().second; - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. - // Backtrack TODO. - todo.pop(); + // Backtrack TODO. + todo.pop(); - // fill rem with any component removed, - numbered_state_heap::state_index_p spi = - h->index(curr->clone()); - assert(spi.first); + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = + h->index(curr->clone()); + assert(spi.first); - sscc.rem().push_front(curr); + 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) - { - // removing states - std::list::iterator i; - bool is_livelock_accepting_sscc = (sscc.top().is_accepting - && (sscc.rem().size() > 1)); - 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; - if (is_livelock_accepting_sscc) - {//if it is an accepting sscc - //add the state to G (=the livelock-accepting states set) + // 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) + { + // removing states + std::list::iterator i; + bool is_livelock_accepting_sscc = (sscc.top().is_accepting + && (sscc.rem().size() > 1)); + 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; + if (is_livelock_accepting_sscc) + {//if it is an accepting sscc + //add the state to G (=the livelock-accepting states set) - state_ta_explicit * livelock_accepting_state = - down_cast (*i); + state_ta_explicit * livelock_accepting_state = + down_cast (*i); - livelock_accepting_state->set_livelock_accepting_state( - true); + livelock_accepting_state->set_livelock_accepting_state( + true); - } + } - } + } - sscc.pop(); + sscc.pop(); - } + } - // automata reduction - testing_automata->delete_stuttering_and_hole_successors(curr); - delete succ; - // Do not delete CURR: it is a key in H. - continue; - } + // automata reduction + testing_automata->delete_stuttering_and_hole_successors(curr); + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } - // Fetch the values destination state we are interested in... - state* dest = succ->current_state(); + // Fetch the values destination state we are interested in... + state* dest = succ->current_state(); - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. - // Are we going to a new state through a stuttering transition? - bool is_stuttering_transition = - testing_automata->get_state_condition(curr) - == testing_automata->get_state_condition(dest); - state* dest_clone = dest->clone(); - spi = h->find(dest_clone); + // Are we going to a new state through a stuttering transition? + bool is_stuttering_transition = + testing_automata->get_state_condition(curr) + == testing_automata->get_state_condition(dest); + state* dest_clone = dest->clone(); + spi = h->find(dest_clone); - // Is this a new state? - if (!spi.first) - { - if (!is_stuttering_transition) - { - init_set.push(dest); - dest_clone->destroy(); - continue; - } + // Is this a new state? + if (!spi.first) + { + if (!is_stuttering_transition) + { + init_set.push(dest); + dest_clone->destroy(); + continue; + } - // Number it, stack it, and register its successors - // for later processing. - h->insert(dest_clone, ++num); - sscc.push(num); - sscc.top().is_accepting = testing_automata->is_accepting_state( - dest); + // Number it, stack it, and register its successors + // for later processing. + h->insert(dest_clone, ++num); + sscc.push(num); + sscc.top().is_accepting = testing_automata->is_accepting_state( + dest); - tgba_succ_iterator* iter = testing_automata->succ_iter(dest); - iter->first(); - todo.push(pair_state_iter(dest, iter)); - continue; - } + tgba_succ_iterator* iter = testing_automata->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + continue; + } - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - continue; + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; - if (!curr->compare(dest)) - { - state_ta_explicit * self_loop_state = - dynamic_cast (curr); + if (!curr->compare(dest)) + { + state_ta_explicit * self_loop_state = + down_cast (curr); + assert(self_loop_state); - if (testing_automata->is_accepting_state(self_loop_state)) - self_loop_state->set_livelock_accepting_state(true); + if (testing_automata->is_accepting_state(self_loop_state)) + self_loop_state->set_livelock_accepting_state(true); - } + } - // Now this is the most interesting case. We have reached a - // state S1 which is already part of a non-dead SSCC. Any such - // non-dead SSCC has necessarily been crossed by our path to - // this state: there is a state S2 in our path which belongs - // to this SSCC too. We are going to merge all states between - // this S1 and S2 into this SSCC. - // - // This merge is easy to do because the order of the SSCC in - // 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; - std::list rem; - bool acc = false; + // Now this is the most interesting case. We have reached a + // state S1 which is already part of a non-dead SSCC. Any such + // non-dead SSCC has necessarily been crossed by our path to + // this state: there is a state S2 in our path which belongs + // to this SSCC too. We are going to merge all states between + // this S1 and S2 into this SSCC. + // + // This merge is easy to do because the order of the SSCC in + // 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; + std::list rem; + bool acc = false; - while (threshold < sscc.top().index) - { - assert(!sscc.empty()); + while (threshold < sscc.top().index) + { + assert(!sscc.empty()); - acc |= sscc.top().is_accepting; + acc |= sscc.top().is_accepting; - rem.splice(rem.end(), sscc.rem()); - sscc.pop(); + rem.splice(rem.end(), sscc.rem()); + sscc.pop(); - } - // Note that we do not always have - // threshold == sscc.top().index - // after this loop, the SSCC whose index is threshold might have - // been merged with a lower SSCC. + } + // Note that we do not always have + // threshold == sscc.top().index + // after this loop, the SSCC whose index is threshold might have + // been merged with a lower SSCC. - // Accumulate all acceptance conditions into the merged SSCC. - sscc.top().is_accepting |= acc; + // Accumulate all acceptance conditions into the merged SSCC. + sscc.top().is_accepting |= acc; - sscc.rem().splice(sscc.rem().end(), rem); + sscc.rem().splice(sscc.rem().end(), rem); - } + } } delete h;