From 782ba0010bae5197fe23a14d000995acde95c580 Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Tue, 17 May 2011 23:41:45 +0200 Subject: [PATCH] Add a new form of TA with a Single-pass emptiness check (STA) * src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,src/ta/taproduct.hh, src/taalgos/dotty.cc, src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh, src/taalgos/minimize.cc, src/taalgos/reachiter.cc, src/taalgos/sba2ta.cc, src/taalgos/sba2ta.hh, src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc: Impacts of the implementation of a new variant of TA, called STA, which involve a Single-pass emptiness check. The new options (-in and -lv) added to build the new variants of TA allow to add two artificial states: 1- an initial artificial state to have an unique initial state (-in) 2- a livelock artificial state which has no successors in order to obtain the new form of TA which requires only a Single-pass emptiness- check: STA (-lv). --- src/ta/ta.cc | 88 ++--- src/ta/ta.hh | 4 + src/ta/taexplicit.cc | 198 +++++++---- src/ta/taexplicit.hh | 33 +- src/ta/taproduct.cc | 50 ++- src/ta/taproduct.hh | 19 + src/taalgos/dotty.cc | 19 +- src/taalgos/emptinessta.cc | 709 +++++++++++++++++++------------------ src/taalgos/emptinessta.hh | 8 +- src/taalgos/minimize.cc | 47 ++- src/taalgos/reachiter.cc | 19 +- src/taalgos/sba2ta.cc | 508 +++++++++++++++----------- src/taalgos/sba2ta.hh | 11 +- src/tgbatest/ltl2ta.test | 181 ++++++++++ src/tgbatest/ltl2tgba.cc | 41 ++- 15 files changed, 1224 insertions(+), 711 deletions(-) create mode 100755 src/tgbatest/ltl2ta.test diff --git a/src/ta/ta.cc b/src/ta/ta.cc index ded4f5675..3d33d5a8e 100644 --- a/src/ta/ta.cc +++ b/src/ta/ta.cc @@ -19,62 +19,64 @@ // 02111-1307, USA. - #include "ta.hh" namespace spot { - + spot::state* + ta::get_artificial_initial_state() const + { + return 0; + } scc_stack_ta::connected_component::connected_component(int i) - { - index = i; - is_accepting = false; - } + { + index = i; + is_accepting = false; + } - scc_stack_ta::connected_component& - scc_stack_ta::top() - { - return s.front(); - } + scc_stack_ta::connected_component& + scc_stack_ta::top() + { + return s.front(); + } - const scc_stack_ta::connected_component& - scc_stack_ta::top() const - { - return s.front(); - } + const scc_stack_ta::connected_component& + scc_stack_ta::top() const + { + return s.front(); + } - void - scc_stack_ta::pop() - { - // assert(rem().empty()); - s.pop_front(); - } + void + scc_stack_ta::pop() + { + // assert(rem().empty()); + s.pop_front(); + } - void - scc_stack_ta::push(int index) - { - s.push_front(connected_component(index)); - } + void + scc_stack_ta::push(int index) + { + s.push_front(connected_component(index)); + } - std::list& - scc_stack_ta::rem() - { - return top().rem; - } + std::list& + scc_stack_ta::rem() + { + return top().rem; + } - size_t - scc_stack_ta::size() const - { - return s.size(); - } - - bool - scc_stack_ta::empty() const - { - return s.empty(); - } + size_t + scc_stack_ta::size() const + { + return s.size(); + } + bool + scc_stack_ta::empty() const + { + return s.empty(); + } } diff --git a/src/ta/ta.hh b/src/ta/ta.hh index 7e0753946..caa9fe9df 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -49,6 +49,9 @@ namespace spot virtual const states_set_t get_initial_states_set() const = 0; + virtual spot::state* + get_artificial_initial_state() const = 0; + virtual ta_succ_iterator* succ_iter(const spot::state* s) const = 0; @@ -67,6 +70,7 @@ namespace spot virtual bool is_livelock_accepting_state(const spot::state* s) const = 0; + virtual bool is_initial_state(const spot::state* s) const = 0; diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 853a0d76c..1882c3bb1 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -64,7 +64,8 @@ namespace spot bool ta_explicit_succ_iterator::done() const { - return transitions_ == 0 || i_ == transitions_->end(); + return transitions_ == 0 || transitions_->empty() || i_ + == transitions_->end(); } state* @@ -103,15 +104,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; } } @@ -122,17 +123,32 @@ namespace spot if (transitions_ == 0) transitions_ = new transitions; - transitions_->push_back(t); - transitions* transitions_condition = get_transitions(t->condition); 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); + state_ta_explicit::transitions::iterator it_trans; + bool transition_found = false; + + for (it_trans = transitions_condition->begin(); (it_trans + != transitions_condition->end() && !transition_found); it_trans++) + { + transition_found = ((*it_trans)->dest == t->dest); + } + + if (!transition_found) + { + transitions_condition->push_back(t); + transitions_->push_back(t); + } + else + { + delete t; + } } @@ -185,6 +201,13 @@ namespace spot is_initial_state_ = is_initial_state; } + bool + state_ta_explicit::is_hole_state() const + { + state_ta_explicit::transitions* trans = get_transitions(); + return trans == 0 || trans->empty(); + } + int state_ta_explicit::compare(const spot::state* other) const { @@ -196,7 +219,16 @@ namespace spot if (compare_value != 0) return compare_value; - return tgba_condition_.id() - o->tgba_condition_.id(); + compare_value = tgba_condition_.id() - o->tgba_condition_.id(); + + // if (compare_value != 0) + // return compare_value; + // + // //unique artificial_livelock_accepting_state + // if (o->is_the_artificial_livelock_accepting_state()) + // return is_the_artificial_livelock_accepting_state(); + + return compare_value; } size_t @@ -219,37 +251,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 +294,17 @@ 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; } } @@ -282,10 +313,17 @@ namespace spot // ta_explicit - ta_explicit::ta_explicit(const tgba* tgba_) : - tgba_(tgba_) + ta_explicit::ta_explicit(const tgba* tgba_, + state_ta_explicit* artificial_initial_state) : + tgba_(tgba_), artificial_initial_state_(artificial_initial_state) { get_dict()->register_all_variables_of(&tgba_, this); + if (artificial_initial_state != 0) + { + state_ta_explicit* is = add_state(artificial_initial_state); + assert(is == artificial_initial_state); + } + } ta_explicit::~ta_explicit() @@ -293,10 +331,11 @@ namespace spot ta::states_set_t::iterator it; for (it = states_set_.begin(); it != states_set_.end(); it++) { - state_ta_explicit* s = down_cast (*it); + state_ta_explicit* s = down_cast (*it); - s->free_transitions(); - delete s; + s->free_transitions(); + s->get_tgba_state()->destroy(); + delete s; } get_dict()->unregister_all_my_variables(this); delete tgba_; @@ -306,20 +345,26 @@ 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 static_cast (*add_state_to_ta.first); } void - ta_explicit::add_to_initial_states_set(state* state) + ta_explicit::add_to_initial_states_set(state* state, bdd condition) { state_ta_explicit * s = down_cast (state); assert(s); s->set_initial_state(true); - - initial_states_set_.insert(s); + if (condition == bddfalse) + condition = get_state_condition(s); + std::pair add_state = + initial_states_set_.insert(s); + if (get_artificial_initial_state() != 0) + if (add_state.second) + create_transition((state_ta_explicit*) get_artificial_initial_state(), + condition, s); } @@ -329,7 +374,8 @@ namespace spot 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); + if (state->is_initial_state()) + add_to_initial_states_set(state); } @@ -355,7 +401,7 @@ namespace spot ta_explicit::get_state_condition(const spot::state* initial_state) const { const state_ta_explicit* sta = - down_cast (initial_state); + down_cast (initial_state); assert(sta); return sta->get_tgba_condition(); } @@ -422,7 +468,7 @@ namespace spot 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()); } @@ -433,26 +479,26 @@ namespace spot for (it = states_set_.begin(); it != states_set_.end(); it++) { - const state_ta_explicit* source = - static_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/taexplicit.hh b/src/ta/taexplicit.hh index cb0744d42..1bcce96fd 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -41,7 +41,8 @@ namespace spot class ta_explicit : public ta { public: - ta_explicit(const tgba* tgba_); + ta_explicit(const tgba* tgba_, state_ta_explicit* artificial_initial_state = + 0); const tgba* get_tgba() const; @@ -50,7 +51,7 @@ namespace spot add_state(state_ta_explicit* s); void - add_to_initial_states_set(state* s); + add_to_initial_states_set(state* s, bdd condition = bddfalse); void create_transition(state_ta_explicit* source, bdd condition, @@ -91,9 +92,28 @@ namespace spot virtual void free_state(const spot::state* s) const; + spot::state* + get_artificial_initial_state() const + { + return (spot::state*) artificial_initial_state_; + } + + void + set_artificial_initial_state(state_ta_explicit* s) + { + artificial_initial_state_ = s; + + } + virtual void delete_stuttering_and_hole_successors(spot::state* s); + ta::states_set_t + get_states_set() + { + return states_set_; + } + private: // Disallow copy. ta_explicit(const ta_explicit& other); @@ -103,6 +123,7 @@ namespace spot ta::states_set_t states_set_; ta::states_set_t initial_states_set_; const tgba* tgba_; + state_ta_explicit* artificial_initial_state_; }; @@ -122,7 +143,8 @@ namespace spot state_ta_explicit(const state* tgba_state, const bdd tgba_condition, bool is_initial_state = false, bool is_accepting_state = false, - bool is_livelock_accepting_state = false, transitions* trans = 0) : + bool is_livelock_accepting_state = false, transitions* trans = 0, + bool is_the_artificial_livelock_accepting_state = false) : tgba_state_(tgba_state), tgba_condition_(tgba_condition), is_initial_state_(is_initial_state), is_accepting_state_( is_accepting_state), is_livelock_accepting_state_( @@ -164,10 +186,15 @@ namespace spot is_livelock_accepting_state() const; void set_livelock_accepting_state(bool is_livelock_accepting_state); + bool is_initial_state() const; void set_initial_state(bool is_initial_state); + + bool + is_hole_state() const; + void delete_stuttering_and_hole_successors(); diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index bce8fe137..067e71303 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -1,4 +1,4 @@ -// Copykripke_structure (C) 2010 Laboratoire de Recherche et Developpement +// Copyright (C) 2010 Laboratoire de Recherche et Developpement // de l Epita (LRDE). // // @@ -87,7 +87,7 @@ namespace spot delete ta_succ_it_; delete kripke_succ_it_; if (kripke_current_dest_state != 0) - kripke_current_dest_state->destroy(); + kripke_current_dest_state->destroy(); } void @@ -116,7 +116,7 @@ namespace spot else { kripke_current_dest_state->destroy(); - kripke_current_dest_state = 0; + kripke_current_dest_state = 0; kripke_succ_it_->next(); } @@ -138,7 +138,7 @@ namespace spot == kripke_current_dest_condition); if (is_stuttering_transition_) { - current_condition_ = bddtrue; + current_condition_ = bddfalse; } else { @@ -174,7 +174,7 @@ namespace spot step_(); if (!done()) - next_non_stuttering_(); + next_non_stuttering_(); } @@ -274,7 +274,7 @@ namespace spot { //build initial states set - const ta::states_set_t ta_init_states_set = ta_->get_initial_states_set(); + ta::states_set_t ta_init_states_set; ta::states_set_t::const_iterator it; ta::states_set_t initial_states_set; @@ -282,10 +282,29 @@ namespace spot bdd kripke_init_state_condition = kripke_->state_condition( kripke_init_state); + spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); + + if (artificial_initial_state != 0) + { + ta_succ_iterator* ta_init_it_ = ta_->succ_iter( + artificial_initial_state, kripke_init_state_condition); + for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next()) + { + ta_init_states_set.insert(ta_init_it_->current_state()); + } + delete ta_init_it_; + + } + else + { + ta_init_states_set = ta_->get_initial_states_set(); + } + for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++) { - if (kripke_init_state_condition == (ta_->get_state_condition(*it))) + if ((artificial_initial_state != 0) || (kripke_init_state_condition + == ta_->get_state_condition(*it))) { state_ta_product* stp = new state_ta_product((*it), kripke_init_state->clone()); @@ -341,6 +360,13 @@ namespace spot return ta_->is_livelock_accepting_state(stp->get_ta_state()); } + spot::state* + ta_product::get_artificial_initial_state() const + { + return 0; + } + + //TODO BUG FIX bool ta_product::is_initial_state(const spot::state* s) const { @@ -356,6 +382,16 @@ namespace spot == (ta_->get_state_condition(ta_s))); } + bool + ta_product::is_hole_state_in_ta_component(const spot::state* s) const + { + const state_ta_product* stp = down_cast (s); + ta_succ_iterator* ta_succ_iter = get_ta()->succ_iter(stp->get_ta_state()); + bool is_hole_state = ta_succ_iter->done(); + delete ta_succ_iter; + return is_hole_state; + } + bdd ta_product::get_state_condition(const spot::state* s) const { diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh index e79df4bc5..f5a975480 100644 --- a/src/ta/taproduct.hh +++ b/src/ta/taproduct.hh @@ -164,15 +164,34 @@ namespace spot virtual bool is_livelock_accepting_state(const spot::state* s) const; + virtual spot::state* + get_artificial_initial_state() const; + virtual bool is_initial_state(const spot::state* s) const; + virtual bool + is_hole_state_in_ta_component(const spot::state* s) const; + + virtual bdd get_state_condition(const spot::state* s) const; virtual void free_state(const spot::state* s) const; + const ta* + get_ta() const + { + return ta_; + } + + const kripke* + get_kripke() const + { + return kripke_; + } + private: bdd_dict* dict_; const ta* ta_; diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index c28885728..251cbe48d 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -43,10 +43,24 @@ namespace spot os_ << "digraph G {" << std::endl; int n = 0; - const ta::states_set_t init_states_set = - t_automata_->get_initial_states_set(); + + spot::state* artificial_initial_state = + t_automata_->get_artificial_initial_state(); + + ta::states_set_t init_states_set; + ta::states_set_t::const_iterator it; + if (artificial_initial_state != 0) + { + init_states_set.insert(artificial_initial_state); + + } + else + { + init_states_set = t_automata_->get_initial_states_set(); + } + for (it = (init_states_set.begin()); it != init_states_set.end(); it++) { // cout << (*it).first << " => " << (*it).second << endl; @@ -60,6 +74,7 @@ namespace spot + "\"]" << std::endl; } + } void diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index 2c52bb3ed..c014d3250 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -18,7 +18,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -// #define TRACE +//#define TRACE #include #ifdef TRACE @@ -34,7 +34,7 @@ namespace spot { - ta_check::ta_check(const ta* a, option_map o) : + ta_check::ta_check(const ta_product* a, option_map o) : a_(a), o_(o) { is_full_2_pass_ = o.get("is_full_2_pass", 0); @@ -46,7 +46,7 @@ namespace spot } bool - ta_check::check() + ta_check::check(bool disable_second_pass) { // We use five main data in this algorithm: @@ -54,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, @@ -71,276 +71,291 @@ namespace spot std::stack init_set; Sgi::hash_map - colour; + colour; trace << "PASS 1" << std::endl; - //const std::string WHITE = "W"; - //const std::string GREY = "G"; - //const std::string BLUE = "B"; - //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; + bool livelock_acceptance_states_not_found = true; + const ta::states_set_t init_states_set = a_->get_initial_states_set(); + 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); } while (!init_set.empty()) { - // Setup depth-first search from initial states. + // Setup depth-first search from initial states. - { - state* init = 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)); - //push potential root of live-lock accepting cycle - if (a_->is_livelock_accepting_state(init)) - livelock_roots.push(init); + inc_depth(); - } + //push potential root of live-lock accepting cycle + if (a_->is_livelock_accepting_state(init)) + livelock_roots.push(init); - while (!todo.empty()) - { + } - state* curr = todo.top().first; + while (!todo.empty()) + { - // We are looking at the next successor in SUCC. - ta_succ_iterator* succ = todo.top().second; + state* curr = todo.top().first; - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. + // 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. - // 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); + if (a_->is_livelock_accepting_state(curr)) + { + livelock_acceptance_states_not_found = false; + trace + << "PASS 1 : livelock accepting state found" << std::endl; - 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); + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = + h->index(curr->clone()); + assert(spi.first); - // Backtrack livelock_roots. - if (!livelock_roots.empty() && !livelock_roots.top()->compare( - curr)) - livelock_roots.pop(); + scc.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(!scc.empty()); - if (scc.top().index == std::abs(*spi.second)) - { - // removing states - std::list::iterator i; + // set the h value of the Backtracked state to negative value. + // colour[curr] = BLUE; + *spi.second = -std::abs(*spi.second); - 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; + // Backtrack livelock_roots. + if (!livelock_roots.empty() && !livelock_roots.top()->compare( + curr)) + livelock_roots.pop(); - } - dec_depth(scc.rem().size()); - scc.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; - delete succ; - // Do not delete CURR: it is a key in H. - continue; - } + 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; - // 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(); + } + dec_depth(scc.rem().size()); + scc.pop(); + } - //may be Buchi accepting scc - scc.top().is_accepting = a_->is_accepting_state(curr) - && !succ->is_stuttering_transition(); + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } - bool is_stuttering_transition = succ->is_stuttering_transition(); + // 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(); - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. + bool curr_is_livelock_hole_state_in_ta_component = + (a_->is_hole_state_in_ta_component(curr)) + && a_->is_livelock_accepting_state(curr); - // Are we going to a new state? - numbered_state_heap::state_index_p spi = h->find(dest); + //may be Buchi accepting scc or livelock accepting state (contains a TA hole and livelock accepting state) + scc.top().is_accepting = (a_->is_accepting_state(curr) + && !succ->is_stuttering_transition()) + || curr_is_livelock_hole_state_in_ta_component; - // 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); + bool is_stuttering_transition = succ->is_stuttering_transition(); - ta_succ_iterator* iter = a_->succ_iter(dest); - iter->first(); - todo.push(pair_state_iter(dest, iter)); - //colour[dest] = GREY; - inc_depth(); + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. - //push potential root of live-lock accepting cycle - if (a_->is_livelock_accepting_state(dest) - && !is_stuttering_transition) - livelock_roots.push(dest); + // Are we going to a new state? + numbered_state_heap::state_index_p spi = h->find(dest); - continue; - } + // 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); - // If we have reached a dead component, ignore it. - if (*spi.second == -1) - continue; + ta_succ_iterator* iter = a_->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + //colour[dest] = GREY; + inc_depth(); - // 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; + //push potential root of live-lock accepting cycle + if (a_->is_livelock_accepting_state(dest) + && !is_stuttering_transition) + livelock_roots.push(dest); - while (threshold < scc.top().index) - { - assert(!scc.empty()); + continue; + } - acc |= scc.top().is_accepting; + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; - rem.splice(rem.end(), scc.rem()); - scc.pop(); + // 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; - } - // 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. + while (threshold < scc.top().index) + { + assert(!scc.empty()); - // Accumulate all acceptance conditions into the merged SSCC. - scc.top().is_accepting |= acc; + acc |= scc.top().is_accepting; - 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; - } + rem.splice(rem.end(), scc.rem()); + scc.pop(); - //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]; + } + // 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. - std::set liveset_curr = - liveset[curr]; + // Accumulate all acceptance conditions into the merged SSCC. + scc.top().is_accepting |= acc; - int h_livelock_root = 0; - if (!livelock_roots.empty()) - h_livelock_root = *(h->find((livelock_roots.top()))).second; + 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; + } - if (heuristic_livelock_detection(dest, h, h_livelock_root, - liveset_curr)) - { - clear(h, todo, init_set); - 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]; - 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 liveset_curr = + liveset[curr]; - } + 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; + } + + 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; + } + + } + + } + } } clear(h, todo, init_set); + + if (disable_second_pass || livelock_acceptance_states_not_found) + return false; + return livelock_detection(a_); } 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; @@ -358,7 +373,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, @@ -378,195 +393,191 @@ namespace spot // * init: the set of the depth-first search initial states std::stack init_set; - - const ta::states_set_t init_states_set = a_->get_initial_states_set(); 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); } - 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); @@ -582,16 +593,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; } @@ -604,7 +615,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/emptinessta.hh b/src/taalgos/emptinessta.hh index 3ca7f5fd3..9e1861f71 100644 --- a/src/taalgos/emptinessta.hh +++ b/src/taalgos/emptinessta.hh @@ -24,7 +24,7 @@ #ifndef SPOT_TAALGOS_EMPTINESS_HH # define SPOT_TAALGOS_EMPTINESS_HH -#include "ta/ta.hh" +#include "ta/taproduct.hh" #include "misc/optionmap.hh" #include "tgbaalgos/gtec/nsheap.hh" #include "tgbaalgos/emptiness_stats.hh" @@ -43,13 +43,13 @@ namespace spot class ta_check : public ec_statistics { public: - ta_check(const ta* a, option_map o = option_map()); + ta_check(const ta_product* a, option_map o = option_map()); virtual ~ta_check(); /// Check whether the automaton's language is empty. virtual bool - check(); + check(bool disable_second_pass = false); virtual bool livelock_detection(const ta* t); @@ -75,7 +75,7 @@ namespace spot heuristic_livelock_detection(const state * stuttering_succ, numbered_state_heap* h, int h_livelock_root, std::set liveset_curr); - const ta* a_; ///< The automaton. + const ta_product* a_; ///< The automaton. option_map o_; ///< The options bool is_full_2_pass_; diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index e2a4d6e5d..c531e5142 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -106,7 +106,7 @@ namespace spot state* tgba_state = tgba->add_state(src_num); bdd tgba_condition = bddtrue; bool is_initial_state = a->is_initial_state(src); - if (is_initial_state) + if ((a->get_artificial_initial_state() == 0) && is_initial_state) tgba_condition = a->get_state_condition(src); bool is_accepting_state = a->is_accepting_state(src); bool is_livelock_accepting_state = a->is_livelock_accepting_state(src); @@ -120,10 +120,16 @@ namespace spot if (ta_src != new_src) { new_src->destroy(); - tgba_state->destroy(); + } + else if (a->get_artificial_initial_state() != 0) + { + if (a->get_artificial_initial_state() == src) + ta->set_artificial_initial_state(new_src); } else if (is_initial_state) - ta->add_to_initial_states_set(new_src); + { + ta->add_to_initial_states_set(new_src); + } ta_succ_iterator* succit = a->succ_iter(src); @@ -138,7 +144,7 @@ namespace spot state* tgba_state = tgba->add_state(i->second); bdd tgba_condition = bddtrue; is_initial_state = a->is_initial_state(dst); - if (is_initial_state) + if ((a->get_artificial_initial_state() == 0) && is_initial_state) tgba_condition = a->get_state_condition(dst); bool is_accepting_state = a->is_accepting_state(dst); bool is_livelock_accepting_state = a->is_livelock_accepting_state( @@ -153,8 +159,13 @@ namespace spot if (ta_dst != new_dst) { new_dst->destroy(); - tgba_state->destroy(); } + else if (a->get_artificial_initial_state() != 0) + { + if (a->get_artificial_initial_state() == dst) + ta->set_artificial_initial_state(new_dst); + } + else if (is_initial_state) ta->add_to_initial_states_set(new_dst); @@ -196,11 +207,17 @@ namespace spot std::set::iterator it; + spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); + for (it = states_set.begin(); it != states_set.end(); it++) { const state* s = (*it); - if (ta_->is_initial_state(s)) + if (s == artificial_initial_state) + { + I->insert(s); + } + else if (artificial_initial_state == 0 && ta_->is_initial_state(s)) { I->insert(s); } @@ -254,12 +271,13 @@ namespace spot } } - delete I; - - if (!G->empty()) + delete I; + + if (!G->empty()) { unsigned s = G->size(); - unsigned num = ++set_num; + unsigned num = set_num; + set_num++; used_var[num] = s; free_var.erase(num); if (s > 1) @@ -276,7 +294,8 @@ namespace spot if (!F->empty()) { unsigned s = F->size(); - unsigned num = ++set_num; + unsigned num = set_num; + set_num++; used_var[num] = s; free_var.erase(num); if (s > 1) @@ -292,7 +311,8 @@ namespace spot if (!G_F->empty()) { unsigned s = G_F->size(); - unsigned num = ++set_num; + unsigned num = set_num; + set_num++; used_var[num] = s; free_var.erase(num); if (s > 1) @@ -308,7 +328,8 @@ namespace spot if (!S->empty()) { unsigned s = S->size(); - unsigned num = ++set_num; + unsigned num = set_num; + set_num++; used_var[num] = s; free_var.erase(num); if (s > 1) diff --git a/src/taalgos/reachiter.cc b/src/taalgos/reachiter.cc index 85cd01321..5a9de8199 100644 --- a/src/taalgos/reachiter.cc +++ b/src/taalgos/reachiter.cc @@ -51,10 +51,23 @@ namespace spot { int n = 0; start(); - const ta::states_set_t init_states_set = - t_automata_->get_initial_states_set(); + + spot::state* artificial_initial_state = + t_automata_->get_artificial_initial_state(); + + ta::states_set_t init_states_set; + ta::states_set_t::const_iterator it; + if (artificial_initial_state != 0) + { + init_states_set.insert(artificial_initial_state); + } + else + { + init_states_set = t_automata_->get_initial_states_set(); + } + for (it = init_states_set.begin(); it != init_states_set.end(); it++) { state* init_state = (*it); @@ -89,7 +102,7 @@ namespace spot { if (ws) process_link(tn, s->second, si); - t_automata_->free_state(current); + t_automata_->free_state(current); } } delete si; diff --git a/src/taalgos/sba2ta.cc b/src/taalgos/sba2ta.cc index 3f492daaa..8f5138467 100644 --- a/src/taalgos/sba2ta.cc +++ b/src/taalgos/sba2ta.cc @@ -29,6 +29,7 @@ #include "tgbaalgos/gtec/nsheap.hh" #include #include "sba2ta.hh" +#include "taalgos/statessetbuilder.hh" using namespace std; @@ -36,93 +37,193 @@ namespace spot { ta* - sba_to_ta(const tgba_sba_proxy* tgba_, bdd atomic_propositions_set_) + sba_to_ta(const tgba_sba_proxy* tgba_, bdd atomic_propositions_set_, + bool artificial_initial_state_mode, + bool artificial_livelock_accepting_state_mode) { - ta_explicit* ta = new spot::ta_explicit(tgba_); - + ta_explicit* ta; std::stack todo; // build Initial states set: state* tgba_init_state = tgba_->get_init_state(); + if (artificial_initial_state_mode) + { + state_ta_explicit* ta_init_state = new state_ta_explicit( + tgba_init_state->clone(), bddtrue, true); + + ta = new spot::ta_explicit(tgba_, ta_init_state); + } + else + { + ta = new spot::ta_explicit(tgba_); + } + 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) + 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* 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_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; } compute_livelock_acceptance_states(ta); + if (artificial_livelock_accepting_state_mode) + { + + state_ta_explicit* artificial_livelock_accepting_state = + new state_ta_explicit(ta->get_tgba()->get_init_state(), bddfalse, + false, false, true, 0, true); + + state_ta_explicit* artificial_livelock_accepting_state_added = ta->add_state(artificial_livelock_accepting_state); + + // unique artificial_livelock_accepting_state + assert(artificial_livelock_accepting_state_added + == artificial_livelock_accepting_state); + + add_artificial_livelock_accepting_state(ta, + artificial_livelock_accepting_state_added); + + } return ta; } + void + add_artificial_livelock_accepting_state(ta_explicit* testing_automata, + state_ta_explicit* artificial_livelock_accepting_state) + { + + ta::states_set_t states_set = testing_automata->get_states_set(); + ta::states_set_t::iterator it; + + std::set* conditions_to_livelock_accepting_states = + new std::set; + + for (it = states_set.begin(); it != states_set.end(); it++) + { + + state_ta_explicit* source = static_cast (*it); + + conditions_to_livelock_accepting_states->clear(); + + 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 (dest->is_livelock_accepting_state()) + { + conditions_to_livelock_accepting_states->insert( + (*it_trans)->condition); + + } + + //remove hole successors states + state_ta_explicit::transitions* dest_trans = + (dest)->get_transitions(); + bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); + if (dest_trans_empty) + { + source->get_transitions((*it_trans)->condition)->remove( + *it_trans); + delete (*it_trans); + it_trans = trans->erase(it_trans); + } + else + { + it_trans++; + } + } + + if (conditions_to_livelock_accepting_states != 0) + { + std::set::iterator it_conditions; + for (it_conditions + = conditions_to_livelock_accepting_states->begin(); it_conditions + != conditions_to_livelock_accepting_states->end(); it_conditions++) + { + + testing_automata->create_transition(source, (*it_conditions), + artificial_livelock_accepting_state); + + } + } + + } + delete conditions_to_livelock_accepting_states; + + } + namespace { typedef std::pair pair_state_iter; @@ -138,7 +239,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,201 +259,200 @@ 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 = (*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); - // automata reduction - testing_automata->delete_stuttering_and_hole_successors(curr); - 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; + } - // 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 = - down_cast (curr); - assert(self_loop_state); + 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; } - } diff --git a/src/taalgos/sba2ta.hh b/src/taalgos/sba2ta.hh index b6d97855f..56617d3c2 100644 --- a/src/taalgos/sba2ta.hh +++ b/src/taalgos/sba2ta.hh @@ -31,13 +31,18 @@ #include "misc/bddlt.hh" #include "ta/taexplicit.hh" - namespace spot { - ta* sba_to_ta(const tgba_sba_proxy* tgba_to_convert, bdd atomic_propositions_set); + ta* + sba_to_ta(const tgba_sba_proxy* tgba_to_convert, bdd atomic_propositions_set, bool artificial_initial_state_mode = true, + bool artificial_livelock_accepting_state_mode = false); + void + compute_livelock_acceptance_states(ta_explicit* testing_automata); - void compute_livelock_acceptance_states(ta_explicit* testing_automata); + void + add_artificial_livelock_accepting_state(ta_explicit* testing_automata, + state_ta_explicit* artificial_livelock_accepting_state); } diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test new file mode 100755 index 000000000..f4182146f --- /dev/null +++ b/src/tgbatest/ltl2ta.test @@ -0,0 +1,181 @@ +#!/bin/sh +# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs + +set -e + +check () +{ + run 0 ../ltl2tgba -TA "$1" + run 0 ../ltl2tgba -TM "$1" +} + +# We don't check the output, but just running these might be enough to +# trigger assertions. + +check a +check 'a U b' +check 'F a' +check 'a & b & c' +check 'a | b | (c U (d & (g U (h ^ i))))' +check 'a & (b U !a) & (b U !a)' +check 'Fa & b & GFc & Gd' +check 'Fa & a & GFc & Gc' +check 'Fc & (a | b) & GF(a | b) & Gc' +check 'a R (b R c)' +check '(a U b) U (c U d)' + +check '((Gp2)U(F(1)))&(p1 R(p2 R p0))' + + + +# Make sure 'a U (b U c)' has 21 states and 144 transitions, +# before and after degeneralization. +for opt in -TA; do + ../ltl2tgba -ks $opt -in 'a U (b U c)' > stdout + grep 'transitions: 144$' stdout + grep 'states: 21$' stdout +done + + +for opt in -TM; do + ../ltl2tgba -ks $opt -in 'a U (b U c)' > stdout + grep 'transitions: 69$' stdout + grep 'states: 10$' stdout +done + + + +for opt in -TM; do + ../ltl2tgba -ks $opt '!(Ga U b)' > stdout + grep 'transitions: 15$' stdout + grep 'states: 5$' stdout +done + +# Make sure 'Ga U b' has 6 states and 12 transitions, +# before and after degeneralization. +for opt in -TM; do + ../ltl2tgba -ks $opt 'Ga U b' > stdout + grep 'transitions: 13$' stdout + grep 'states: 6$' stdout +done + + +# Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' +# has 21 states and 96 transitions, before minimization. +f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' + +../ltl2tgba -ks -TA "$f" > stdout +grep 'transitions: 96$' stdout +grep 'states: 21$' stdout + +# Note: after minimization with -TM. +# has 20 states and 89 transitions, after minimization. +../ltl2tgba -ks -TM "$f" > stdout +grep 'transitions: 89$' stdout +grep 'states: 20$' stdout + + +# Make sure 'GFa & GFb & GFc & GFd & GFe & GFf' +# has 448 states and 28224 transitions. +f='GFa & GFb & GFc & GFd & GFe & GFg' +../ltl2tgba -ks -TA -x "$f" > stdout +grep 'transitions: 28351$' stdout +grep 'states: 449$' stdout + + +# Make sure 'GFa & GFb & GFc & GFd & GFe & GFf' +# has 290 states and 18527 transitions with artificial livelock state. + +f='GFa & GFb & GFc & GFd & GFe & GFg' +../ltl2tgba -ks -TM -x -lv "$f" > stdout +grep 'transitions: 18527$' stdout +grep 'states: 290$' stdout + + +#tests with artificial livelock state: +run 0 ../ltl2tgba -ks -TA -lv "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout +grep 'transitions: 920$' stdout +grep 'states: 78$' stdout + +run 0 ../ltl2tgba -TM -ks -lv "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout +grep 'transitions: 458$' stdout +grep 'states: 28$' stdout + + + +run 0 ../ltl2tgba -TM -ks -in -R3f -x "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 521$' stdout +grep 'states: 43$' stdout + + +run 0 ../ltl2tgba -TM -ks -lv -R3f -x "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 645$' stdout +grep 'states: 45$' stdout + + +run 0 ../ltl2tgba -TM -ks "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +grep 'transitions: 2779$' stdout +grep 'states: 127$' stdout + + +run 0 ../ltl2tgba -TM -ks -lv "G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" >stdout +grep 'transitions: 3105$' stdout +grep 'states: 128$' stdout + + + +run 0 ../ltl2tgba -TM -ks "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 536$' stdout +grep 'states: 37$' stdout + + +run 0 ../ltl2tgba -TM -ks -lv -in "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 612$' stdout +grep 'states: 37$' stdout + + +run 0 ../ltl2tgba -TM -ks -in -R3 -x "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 464$' stdout +grep 'states: 36$' stdout + +run 0 ../ltl2tgba -TM -ks -lv -R3 -x "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 575$' stdout +grep 'states: 38$' stdout + + +run 0 ../ltl2tgba -TA -ks -lv "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 876$' stdout +grep 'states: 56$' stdout + + +run 0 ../ltl2tgba -TM -ks -lv "FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" >stdout +grep 'transitions: 631$' stdout +grep 'states: 38$' stdout + + + +echo '.................. OK' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index abaca0e40..26e7095bc 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -68,6 +68,7 @@ #include "taalgos/sba2ta.hh" #include "taalgos/dotty.hh" +#include "taalgos/stats.hh" std::string ltl_defs() @@ -285,6 +286,12 @@ syntax(char* prog) << std::endl << std::endl << " -TM Translate an LTL formula into a minimal Testing automata" + << std::endl + << std::endl + << " -lv Translate an LTL formula into a Testing automata with an artificial livelock accepting state" + << std::endl + << std::endl + << " -in Translate an LTL formula into a Testing automata without artificial initial state" << std::endl; @@ -347,6 +354,8 @@ main(int argc, char** argv) bool reduction_dir_sim = false; spot::tgba* temp_dir_sim = 0; bool ta_opt = false; + bool opt_with_artificial_livelock = false; + bool opt_with_artificial_initial_state = true; for (;;) @@ -684,6 +693,14 @@ main(int argc, char** argv) ta_opt = true; opt_minimize = true; } + else if (!strcmp(argv[formula_index], "-lv")) + { + opt_with_artificial_livelock = true; + } + else if (!strcmp(argv[formula_index], "-in")) + { + opt_with_artificial_initial_state = false; + } else if (!strcmp(argv[formula_index], "-taa")) { translation = TransTAA; @@ -979,7 +996,7 @@ main(int argc, char** argv) const spot::tgba* degeneralized = 0; spot::tgba* minimized = 0; - if (opt_minimize) + if (opt_minimize && !ta_opt) { tm.start("obligation minimization"); minimized = minimize_obligation(a, f); @@ -1094,12 +1111,28 @@ main(int argc, char** argv) } delete aps; - spot::ta* testing_automata = sba_to_ta(degeneralized, atomic_props_set_bdd); + spot::ta* testing_automata = sba_to_ta(degeneralized, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock); if (opt_minimize) testing_automata = minimize_ta(testing_automata); - spot::dotty_reachable(std::cout, testing_automata); - delete testing_automata; + if (output != -1) + { + tm.start("producing output"); + switch (output) + { + case 0: + spot::dotty_reachable(std::cout, testing_automata); + break; + case 12: + stats_reachable(testing_automata).dump(std::cout); + break; + default: + assert(!"unknown output option"); + } + tm.stop("producing output"); + } + delete testing_automata; output = -1; + } spot::tgba* product_degeneralized = 0;