diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index e9b561265..fb619caf4 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -1,5 +1,5 @@ // -*- coding utf-8 -*- -// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -49,531 +49,515 @@ namespace spot namespace { typedef std::pair pair_state_iter; - } - void - transform_to_single_pass_automaton(ta_explicit* testing_automata, - state_ta_explicit* artificial_livelock_accepting_state = 0) - { + static void + transform_to_single_pass_automaton + (ta_explicit* testing_automata, + state_ta_explicit* artificial_livelock_acc_state = 0) + { - if (artificial_livelock_accepting_state != 0) - { - state_ta_explicit* artificial_livelock_accepting_state_added = - testing_automata->add_state(artificial_livelock_accepting_state); + if (artificial_livelock_acc_state != 0) + { + state_ta_explicit* artificial_livelock_acc_state_added = + testing_automata->add_state(artificial_livelock_acc_state); - // unique artificial_livelock_accepting_state - assert(artificial_livelock_accepting_state_added - == artificial_livelock_accepting_state); - artificial_livelock_accepting_state->set_livelock_accepting_state(true); - artificial_livelock_accepting_state->free_transitions(); - } + // unique artificial_livelock_acc_state + assert(artificial_livelock_acc_state_added + == artificial_livelock_acc_state); + artificial_livelock_acc_state->set_livelock_accepting_state(true); + artificial_livelock_acc_state->free_transitions(); + } + ta::states_set_t states_set = testing_automata->get_states_set(); + ta::states_set_t::iterator it; - - ta::states_set_t states_set = testing_automata->get_states_set(); - ta::states_set_t::iterator it; - - state_ta_explicit::transitions* transitions_to_livelock_states = + state_ta_explicit::transitions* transitions_to_livelock_states = new state_ta_explicit::transitions; - for (it = states_set.begin(); it != states_set.end(); ++it) - { + for (it = states_set.begin(); it != states_set.end(); ++it) + { + state_ta_explicit* source = static_cast (*it); - state_ta_explicit* source = static_cast (*it); + transitions_to_livelock_states->clear(); - transitions_to_livelock_states->clear(); + 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();) + { + state_ta_explicit* dest = (*it_trans)->dest; - if (trans != 0) - for (it_trans = trans->begin(); it_trans != trans->end();) - { - state_ta_explicit* dest = (*it_trans)->dest; - - state_ta_explicit::transitions* dest_trans = + state_ta_explicit::transitions* dest_trans = (dest)->get_transitions(); - bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); + bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); + //select transitions where a destination is a livelock state + // which isn't a Buchi accepting state and has successors + if (dest->is_livelock_accepting_state() + && (!dest->is_accepting_state()) && (!dest_trans_empty)) + transitions_to_livelock_states->push_front(*it_trans); + // optimization to have, after minimization, an unique + // livelock state which has no successors + if (dest->is_livelock_accepting_state() && (dest_trans_empty)) + dest->set_accepting_state(false); - //select transitions where a destination is a livelock state - // which isn't a Buchi accepting state and has successors - if (dest->is_livelock_accepting_state() - && (!dest->is_accepting_state()) && (!dest_trans_empty)) - { - transitions_to_livelock_states->push_front(*it_trans); + ++it_trans; + } - } + if (transitions_to_livelock_states != 0) + { + state_ta_explicit::transitions::iterator it_trans; - //optimization to have, after - // minimization, an unique livelock state which has no successors - if (dest->is_livelock_accepting_state() && (dest_trans_empty)) - { - dest->set_accepting_state(false); + for (it_trans = transitions_to_livelock_states->begin(); + it_trans != transitions_to_livelock_states->end(); + ++it_trans) + { + if (artificial_livelock_acc_state != 0) + { + testing_automata->create_transition + (source, + (*it_trans)->condition, + (*it_trans)->acceptance_conditions, + artificial_livelock_acc_state, true); + } + else + { + testing_automata->create_transition + (source, + (*it_trans)->condition, + (*it_trans)->acceptance_conditions, + ((*it_trans)->dest)->stuttering_reachable_livelock, + true); + } + } + } + } + delete transitions_to_livelock_states; - } - - ++it_trans; - - } - - if (transitions_to_livelock_states != 0) - { - state_ta_explicit::transitions::iterator it_trans; - - for (it_trans = transitions_to_livelock_states->begin(); - it_trans != transitions_to_livelock_states->end(); ++it_trans) - { - if (artificial_livelock_accepting_state != 0) - { - testing_automata->create_transition(source, - (*it_trans)->condition, - (*it_trans)->acceptance_conditions, - artificial_livelock_accepting_state, true); - } - else - { - testing_automata->create_transition(source, - (*it_trans)->condition, - (*it_trans)->acceptance_conditions, - ((*it_trans)->dest)->stuttering_reachable_livelock, - true); - } - - } - } - - } - delete transitions_to_livelock_states; - - for (it = states_set.begin(); it != states_set.end(); ++it) - { - - state_ta_explicit* state = static_cast (*it); - state_ta_explicit::transitions* state_trans = + for (it = states_set.begin(); it != states_set.end(); ++it) + { + state_ta_explicit* state = static_cast (*it); + state_ta_explicit::transitions* state_trans = (state)->get_transitions(); - bool state_trans_empty = state_trans == 0 || state_trans->empty(); - - if (state->is_livelock_accepting_state() - && (!state->is_accepting_state()) && (!state_trans_empty)) - state->set_livelock_accepting_state(false); - } - - } - -void -compute_livelock_acceptance_states(ta_explicit* testing_automata, - bool single_pass_emptiness_check, - state_ta_explicit* artificial_livelock_accepting_state) -{ - // We use five main data in this algorithm: - // * sscc: a stack of strongly stuttering-connected components (SSCC) - scc_stack_ta sscc; - - // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; - - // * 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. - - // * num: the number of visited nodes. Used to set the order of each - // visited node, - int num = 0; - - // * todo: the depth-first search stack. This holds pairs of the - // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator - // over the successors of STATE. In our use, ITERATOR should - // always be freed when TODO is popped, but STATE should not because - // it is also used as a key in H. - std::stack todo; - - // * 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); + bool state_trans_empty = state_trans == 0 || state_trans->empty(); + if (state->is_livelock_accepting_state() + && (!state->is_accepting_state()) && (!state_trans_empty)) + state->set_livelock_accepting_state(false); + } } - while (!init_set.empty()) + static void + compute_livelock_acceptance_states(ta_explicit* testing_automata, + bool single_pass_emptiness_check, + state_ta_explicit* + artificial_livelock_acc_state) { - // Setup depth-first search from initial states. + // We use five main data in this algorithm: + // * sscc: a stack of strongly stuttering-connected components (SSCC) + scc_stack_ta sscc; - { - state_ta_explicit* init = + // * arc, a stack of acceptance conditions between each of these SCC, + std::stack arc; + + // * 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. + + // * num: the number of visited nodes. Used to set the order of each + // visited node, + int num = 0; + + // * todo: the depth-first search stack. This holds pairs of the + // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator + // over the successors of STATE. In our use, ITERATOR should + // always be freed when TODO is popped, but STATE should not because + // it is also used as a key in H. + std::stack todo; + + // * 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); + } + + 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; - numbered_state_heap::state_index_p h_init = h->find(init_clone); + 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_init.first) + continue; - h->insert(init_clone, ++num); - sscc.push(num); - arc.push(bddfalse); - sscc.top().is_accepting + h->insert(init_clone, ++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)); + tgba_succ_iterator* iter = testing_automata->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); + } - } + while (!todo.empty()) + { + state* curr = todo.top().first; + + numbered_state_heap::state_index_p spi = h->find(curr); + // 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; + + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. + + // Backtrack TODO. + todo.pop(); + + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = h->index(curr); + assert(spi.first); + + 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.rem().size() > 1) + && ((sscc.top().is_accepting) + || (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) + { + numbered_state_heap::state_index_p spi = + h->index((*i)); + 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) + trace << "*** sscc.size() > 1: states: ***" + << testing_automata->format_state(*i) + << std::endl; + state_ta_explicit * livelock_accepting_state = + down_cast (*i); + + livelock_accepting_state-> + set_livelock_accepting_state(true); + + if (single_pass_emptiness_check) + { + livelock_accepting_state + ->set_accepting_state(true); + livelock_accepting_state + ->stuttering_reachable_livelock + = livelock_accepting_state; + } + } + } + + assert(!arc.empty()); + sscc.pop(); + arc.pop(); + + } + + // 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(); + + bdd acc_cond = succ->current_acceptance_conditions(); + // ... 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; + 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; + } + + // Number it, stack it, and register its successors + // for later processing. + h->insert(dest_clone, ++num); + sscc.push(num); + arc.push(acc_cond); + 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; + } + + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; + + trace << "***compute_livelock_acceptance_states: CYCLE***\n"; + + 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) + || (acc_cond + == testing_automata->all_acceptance_conditions())) + { + self_loop_state->set_livelock_accepting_state(true); + if (single_pass_emptiness_check) + { + self_loop_state->set_accepting_state(true); + self_loop_state->stuttering_reachable_livelock + = self_loop_state; + } + } + + trace + << "***compute_livelock_acceptance_states: CYCLE: " + << "self_loop_state***\n"; + } + + // 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()); + assert(!arc.empty()); + acc |= sscc.top().is_accepting; + acc_cond |= sscc.top().condition; + acc_cond |= arc.top(); + rem.splice(rem.end(), sscc.rem()); + sscc.pop(); + arc.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. + + // Accumulate all acceptance conditions into the merged SSCC. + sscc.top().is_accepting |= acc; + sscc.top().condition |= acc_cond; + + sscc.rem().splice(sscc.rem().end(), rem); + + } + + } + delete h; + + if ((artificial_livelock_acc_state != 0) + || single_pass_emptiness_check) + transform_to_single_pass_automaton(testing_automata, + artificial_livelock_acc_state); + } + + ta_explicit* + build_ta(ta_explicit* ta, bdd atomic_propositions_set_, bool degeneralized, + bool single_pass_emptiness_check, + bool artificial_livelock_state_mode) + { + + std::stack todo; + const tgba* tgba_ = ta->get_tgba(); + const sba* sba_ = down_cast(tgba_); + assert(!degeneralized || sba_); + + // build Initial states set: + state* tgba_init_state = tgba_->get_init_state(); + + bdd tgba_condition = tgba_->support_conditions(tgba_init_state); + + bdd satone_tgba_condition; + while ((satone_tgba_condition = bdd_satoneset(tgba_condition, + atomic_propositions_set_, + bddtrue)) != bddfalse) + { + tgba_condition -= satone_tgba_condition; + state_ta_explicit* init_state; + if (degeneralized) + { + init_state = new + state_ta_explicit(tgba_init_state->clone(), + satone_tgba_condition, true, + sba_->state_is_accepting(tgba_init_state)); + } + else + { + init_state = new + state_ta_explicit(tgba_init_state->clone(), + satone_tgba_condition, true, false); + } + + state_ta_explicit* s = ta->add_state(init_state); + assert(s == init_state); + ta->add_to_initial_states_set(s); + + todo.push(init_state); + } + tgba_init_state->destroy(); while (!todo.empty()) - { + { + state_ta_explicit* source = todo.top(); + todo.pop(); - state* curr = todo.top().first; - - numbered_state_heap::state_index_p spi = h->find(curr); - // 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; - - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. - - // Backtrack TODO. - todo.pop(); - - // fill rem with any component removed, - numbered_state_heap::state_index_p spi = h->index(curr); - assert(spi.first); - - 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.rem().size() > 1) - && ((sscc.top().is_accepting) || (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) - { - numbered_state_heap::state_index_p spi = h->index((*i)); - 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) - trace << "*** sscc.size() > 1: states: ***" - << testing_automata->format_state(*i) - << std::endl; - state_ta_explicit * livelock_accepting_state = - down_cast (*i); - - livelock_accepting_state-> - set_livelock_accepting_state(true); - - if (single_pass_emptiness_check) - { - livelock_accepting_state - ->set_accepting_state(true); - livelock_accepting_state - ->stuttering_reachable_livelock - = livelock_accepting_state; - } - } - } - - assert(!arc.empty()); - sscc.pop(); - arc.pop(); - - } - - // 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(); - - bdd acc_cond = succ->current_acceptance_conditions(); - // ... 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; - 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; - } - - // Number it, stack it, and register its successors - // for later processing. - h->insert(dest_clone, ++num); - sscc.push(num); - arc.push(acc_cond); - 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; - } - - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - continue; - - trace - << "***compute_livelock_acceptance_states: CYCLE***" << std::endl; - - 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) - || (acc_cond - == testing_automata->all_acceptance_conditions())) - { - self_loop_state->set_livelock_accepting_state(true); - if (single_pass_emptiness_check) - { - self_loop_state->set_accepting_state(true); - self_loop_state->stuttering_reachable_livelock - = self_loop_state; - } - - } - - trace - << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" - << std::endl; - - } - - // 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()); - assert(!arc.empty()); - acc |= sscc.top().is_accepting; - acc_cond |= sscc.top().condition; - acc_cond |= arc.top(); - rem.splice(rem.end(), sscc.rem()); - sscc.pop(); - arc.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. - - // Accumulate all acceptance conditions into the merged SSCC. - sscc.top().is_accepting |= acc; - sscc.top().condition |= acc_cond; - - sscc.rem().splice(sscc.rem().end(), rem); - - } - - } - delete h; - - if ((artificial_livelock_accepting_state != 0) - || single_pass_emptiness_check) - transform_to_single_pass_automaton(testing_automata, - artificial_livelock_accepting_state); - -} - - ta_explicit* - build_ta(ta_explicit* ta, bdd atomic_propositions_set_, bool degeneralized, - bool single_pass_emptiness_check, bool artificial_livelock_state_mode) - { - - std::stack todo; - const tgba* tgba_ = ta->get_tgba(); - const sba* sba_ = down_cast(tgba_); - assert(!degeneralized || sba_); - - // build Initial states set: - state* tgba_init_state = tgba_->get_init_state(); - - bdd tgba_condition = tgba_->support_conditions(tgba_init_state); - - bdd satone_tgba_condition; - while ((satone_tgba_condition = bdd_satoneset(tgba_condition, - atomic_propositions_set_, bddtrue)) != bddfalse) - { - tgba_condition -= satone_tgba_condition; - state_ta_explicit* init_state; - if (degeneralized) - { - init_state = - new state_ta_explicit(tgba_init_state->clone(), - satone_tgba_condition, true, - sba_->state_is_accepting(tgba_init_state)); - } - else - { - init_state = - new state_ta_explicit(tgba_init_state->clone(), - satone_tgba_condition, true, false); - } - - state_ta_explicit* s = ta->add_state(init_state); - assert(s == init_state); - ta->add_to_initial_states_set(s); - - todo.push(init_state); - } - tgba_init_state->destroy(); - - while (!todo.empty()) - { - 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 tgba_acceptance_conditions = + 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 tgba_acceptance_conditions = tgba_succ_it->current_acceptance_conditions(); - bdd satone_tgba_condition; - while ((satone_tgba_condition = bdd_satoneset(tgba_condition, - atomic_propositions_set_, bddtrue)) != bddfalse) - { + 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; + if (degeneralized) + { + new_dest = new state_ta_explicit + (tgba_state->clone(), + dest_condition, + false, + sba_->state_is_accepting(tgba_state)); + } + else + { + new_dest = new state_ta_explicit + (tgba_state->clone(), + dest_condition, false, false); + } + state_ta_explicit* dest = ta->add_state(new_dest); - 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; - if (degeneralized) - { - new_dest = new state_ta_explicit - (tgba_state->clone(), - dest_condition, - false, - sba_->state_is_accepting(tgba_state)); + if (dest != new_dest) + { + // the state dest already exists in the automaton + new_dest->get_tgba_state()->destroy(); + delete new_dest; + } + else + { + todo.push(dest); + } - } - else - { - new_dest = new state_ta_explicit - (tgba_state->clone(), dest_condition, false, false); - } - state_ta_explicit* dest = ta->add_state(new_dest); + bdd cs = bdd_setxor(source->get_tgba_condition(), + dest->get_tgba_condition()); + ta->create_transition(source, cs, + tgba_acceptance_conditions, dest); + } + } + tgba_state->destroy(); + } + delete tgba_succ_it; + } - if (dest != new_dest) - { - // the state dest already exists in the automaton - new_dest->get_tgba_state()->destroy(); - delete new_dest; - } - else - { - todo.push(dest); - } + state_ta_explicit* artificial_livelock_acc_state = 0; - ta->create_transition(source, bdd_setxor( - source->get_tgba_condition(), - dest->get_tgba_condition()), - tgba_acceptance_conditions, dest); + trace << "*** build_ta: artificial_livelock_acc_state_mode = ***" + << artificial_livelock_state_mode << std::endl; - } - - } - tgba_state->destroy(); - } - delete tgba_succ_it; - - } - - state_ta_explicit* artificial_livelock_accepting_state = 0; - - trace << "*** build_ta: artificial_livelock_accepting_state_mode = ***" - << artificial_livelock_state_mode << std::endl; - - if (artificial_livelock_state_mode) - { - single_pass_emptiness_check = true; - artificial_livelock_accepting_state = new state_ta_explicit( - ta->get_tgba()->get_init_state(), bddtrue, false, false, true, 0); - trace - << "*** build_ta: artificial_livelock_accepting_state = ***" - << artificial_livelock_accepting_state << std::endl; - - } - - compute_livelock_acceptance_states(ta, single_pass_emptiness_check, - artificial_livelock_accepting_state); - - return ta; + if (artificial_livelock_state_mode) + { + single_pass_emptiness_check = true; + artificial_livelock_acc_state = + new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue, + false, false, true, 0); + trace + << "*** build_ta: artificial_livelock_acc_state = ***" + << artificial_livelock_acc_state << std::endl; + } + compute_livelock_acceptance_states(ta, single_pass_emptiness_check, + artificial_livelock_acc_state); + return ta; + } } ta_explicit* @@ -616,7 +600,6 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, if (state->is_accepting_state()) { - state_ta_explicit::transitions* trans = state->get_transitions(); state_ta_explicit::transitions::iterator it_trans; @@ -625,23 +608,18 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, { (*it_trans)->acceptance_conditions = ta->all_acceptance_conditions(); - } state->set_accepting_state(false); } - } - - return ta; } tgta_explicit* tgba_to_tgta(const tgba* tgba_, bdd atomic_propositions_set_) { - state* tgba_init_state = tgba_->get_init_state(); state_ta_explicit* artificial_init_state = new state_ta_explicit( tgba_init_state->clone(), bddfalse, true); @@ -681,14 +659,12 @@ compute_livelock_acceptance_states(ta_explicit* testing_automata, state_ta_explicit::transitions* trans = state->get_transitions(); if (state->is_livelock_accepting_state()) { - bool trans_empty = (trans == 0 || trans->empty()); if (trans_empty || state->is_accepting_state()) { ta->create_transition(state, bdd_stutering_transition, ta->all_acceptance_conditions(), state); } - } if (state->compare(ta->get_artificial_initial_state()))