diff --git a/src/ta/Makefile.am b/src/ta/Makefile.am index 9a9850143..11de1047b 100644 --- a/src/ta/Makefile.am +++ b/src/ta/Makefile.am @@ -25,8 +25,11 @@ tadir = $(pkgincludedir)/ta ta_HEADERS = \ ta.hh \ + taproduct.hh \ taexplicit.hh - + noinst_LTLIBRARIES = libta.la libta_la_SOURCES = \ + ta.cc \ + taproduct.cc \ taexplicit.cc diff --git a/src/ta/ta.cc b/src/ta/ta.cc new file mode 100644 index 000000000..fc6fab0b4 --- /dev/null +++ b/src/ta/ta.cc @@ -0,0 +1,82 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// 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. + + + +#include "ta.hh" + +namespace spot +{ + + + + scc_stack_ta::connected_component::connected_component(int i) + { + index = i; + is_accepting = false; + } + + 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(); + } + + void + scc_stack_ta::pop() + { + // assert(rem().empty()); + s.pop_front(); + } + + void + scc_stack_ta::push(int index) + { + s.push_front(connected_component(index)); + } + + 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(); + } + + +} + + diff --git a/src/ta/ta.hh b/src/ta/ta.hh index 244d8a213..7e0753946 100644 --- a/src/ta/ta.hh +++ b/src/ta/ta.hh @@ -46,29 +46,35 @@ namespace spot typedef std::set states_set_t; - virtual const states_set_t* - get_initial_states_set() const = 0; + virtual const states_set_t + get_initial_states_set() const = 0; virtual ta_succ_iterator* - succ_iter(const spot::state* s) const = 0; + succ_iter(const spot::state* s) const = 0; + + virtual ta_succ_iterator* + succ_iter(const spot::state* s, bdd condition) const = 0; virtual bdd_dict* - get_dict() const = 0; + get_dict() const = 0; virtual std::string - format_state(const spot::state* s) const = 0; + format_state(const spot::state* s) const = 0; virtual bool - is_accepting_state(const spot::state* s) const = 0; + is_accepting_state(const spot::state* s) const = 0; virtual bool - is_livelock_accepting_state(const spot::state* s) const = 0; + is_livelock_accepting_state(const spot::state* s) const = 0; virtual bool - is_initial_state(const spot::state* s) const = 0; + is_initial_state(const spot::state* s) const = 0; virtual bdd - get_state_condition(const spot::state* s) const = 0; + get_state_condition(const spot::state* s) const = 0; + + virtual void + free_state(const spot::state* s) const = 0; }; @@ -93,6 +99,8 @@ namespace spot virtual bdd current_condition() const = 0; + virtual bool + is_stuttering_transition() const = 0; bdd current_acceptance_conditions() const @@ -103,7 +111,7 @@ namespace spot }; // A stack of Strongly-Connected Components - class sscc_stack + class scc_stack_ta { public: struct connected_component @@ -116,8 +124,6 @@ namespace spot bool is_accepting; - bool is_initial; - std::list rem; }; diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index ace94522b..12aedad34 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -28,22 +28,31 @@ #include "tgba/bddprint.hh" - namespace spot { //////////////////////////////////////// // ta_explicit_succ_iterator - ta_explicit_succ_iterator::ta_explicit_succ_iterator(const state_ta_explicit* s) + ta_explicit_succ_iterator::ta_explicit_succ_iterator( + const state_ta_explicit* s) : + source_(s) { transitions_ = s->get_transitions(); } + ta_explicit_succ_iterator::ta_explicit_succ_iterator( + const state_ta_explicit* s, bdd condition) : + source_(s) + { + transitions_ = s->get_transitions(condition); + } + void ta_explicit_succ_iterator::first() { - i_ = transitions_->begin(); + if (transitions_ != 0) + i_ = transitions_->begin(); } void @@ -55,7 +64,7 @@ namespace spot bool ta_explicit_succ_iterator::done() const { - return i_ == transitions_->end(); + return transitions_ == 0 || i_ == transitions_->end(); } state* @@ -73,8 +82,11 @@ namespace spot return (*i_)->condition; } - - + bool + ta_explicit_succ_iterator::is_stuttering_transition() const + { + return source_->get_tgba_condition() == ((*i_)->dest)->get_tgba_condition(); + } //////////////////////////////////////// // state_ta_explicit @@ -85,16 +97,44 @@ namespace spot return transitions_; } + // return transitions filtred by condition + state_ta_explicit::transitions* + state_ta_explicit::get_transitions(bdd condition) const + { - void - state_ta_explicit::add_transition(state_ta_explicit::transition* t){ - if(transitions_ == 0) - transitions_= new transitions; + Sgi::hash_map >::const_iterator i = + transitions_by_condition.find(condition.id()); - transitions_->push_back(t); + if (i == transitions_by_condition.end()) + { + return 0; + } + else + { + return i->second; + } } + void + state_ta_explicit::add_transition(state_ta_explicit::transition* t) + { + 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->push_back(t); + + } const state* state_ta_explicit::get_tgba_state() const @@ -133,7 +173,8 @@ namespace spot } void - state_ta_explicit::set_livelock_accepting_state(bool is_livelock_accepting_state) + state_ta_explicit::set_livelock_accepting_state( + bool is_livelock_accepting_state) { is_livelock_accepting_state_ = is_livelock_accepting_state; } @@ -170,54 +211,71 @@ namespace spot return new state_ta_explicit(*this); } - sscc_stack::connected_component::connected_component(int i) + void + state_ta_explicit::delete_stuttering_and_hole_successors() { - index = i; - is_accepting = false; - is_initial = false; - } + state_ta_explicit::transitions* trans = get_transitions(); + state_ta_explicit::transitions::iterator it_trans; - sscc_stack::connected_component& - sscc_stack::top() - { - return s.front(); - } + 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(); + + //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++; + } + } - const sscc_stack::connected_component& - sscc_stack::top() const - { - return s.front(); } void - sscc_stack::pop() + state_ta_explicit::free_transitions() { - // assert(rem().empty()); - s.pop_front(); - } + state_ta_explicit::transitions* trans = get_transitions(); + state_ta_explicit::transitions::iterator it_trans; + // We don't destroy the transitions in the state's destructor because + // they are not cloned. + if (trans != 0) + for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) + { + delete *it_trans; + } + delete trans; + delete get_tgba_state(); - void - sscc_stack::push(int index) - { - s.push_front(connected_component(index)); - } + Sgi::hash_map >::iterator i = + transitions_by_condition.begin(); + while (i != transitions_by_condition.end()) + { + delete i->second; + ++i; + } - std::list& - sscc_stack::rem() - { - return top().rem; - } - - size_t - sscc_stack::size() const - { - return s.size(); - } - - bool - sscc_stack::empty() const - { - return s.empty(); } //////////////////////////////////////// @@ -227,6 +285,7 @@ namespace spot ta_explicit::ta_explicit(const tgba* tgba_) : tgba_(tgba_) { + get_dict()->register_all_variables_of(&tgba_, this); } ta_explicit::~ta_explicit() @@ -234,20 +293,13 @@ namespace spot ta::states_set_t::iterator it; for (it = states_set_.begin(); it != states_set_.end(); it++) { - const state_ta_explicit* s = dynamic_cast (*it); - state_ta_explicit::transitions* trans = s->get_transitions(); - state_ta_explicit::transitions::iterator it_trans; - // We don't destroy the transitions in the state's destructor because - // they are not cloned. - for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) - { - delete *it_trans; - } - delete trans; - delete s->get_tgba_state(); + state_ta_explicit* s = dynamic_cast (*it); + + s->free_transitions(); delete s; } - + get_dict()->unregister_all_my_variables(this); + delete tgba_; } state_ta_explicit* @@ -256,24 +308,33 @@ namespace spot std::pair add_state_to_ta = states_set_.insert(s); - if (is_initial_state(*add_state_to_ta.first)) - initial_states_set_.insert(*add_state_to_ta.first); - return dynamic_cast (*add_state_to_ta.first); } - state_ta_explicit* - ta_explicit::add_initial_state(state_ta_explicit* s) + void + ta_explicit::add_to_initial_states_set(state* state) { + state_ta_explicit * s = dynamic_cast (state); + s->set_initial_state(true); - return add_state(s); + initial_states_set_.insert(s); } void - ta_explicit::create_transition(state_ta_explicit* source, bdd condition, state_ta_explicit* dest) + ta_explicit::delete_stuttering_and_hole_successors(spot::state* s) + { + state_ta_explicit * state = dynamic_cast (s); + state->delete_stuttering_and_hole_successors(); + if (state->is_initial_state()) add_to_initial_states_set(state); + + } + + void + ta_explicit::create_transition(state_ta_explicit* source, bdd condition, + state_ta_explicit* dest) { state_ta_explicit::transition* t = new state_ta_explicit::transition; t->dest = dest; @@ -282,17 +343,18 @@ namespace spot } - const ta::states_set_t* + const ta::states_set_t ta_explicit::get_initial_states_set() const { - return &initial_states_set_; + return initial_states_set_; } bdd ta_explicit::get_state_condition(const spot::state* initial_state) const { - const state_ta_explicit* sta = dynamic_cast (initial_state); + const state_ta_explicit* sta = + dynamic_cast (initial_state); return sta->get_tgba_condition(); } @@ -325,6 +387,14 @@ namespace spot return new ta_explicit_succ_iterator(s); } + ta_succ_iterator* + ta_explicit::succ_iter(const spot::state* state, bdd condition) const + { + const state_ta_explicit* s = dynamic_cast (state); + assert(s); + return new ta_explicit_succ_iterator(s, condition); + } + bdd_dict* ta_explicit::get_dict() const { @@ -342,6 +412,10 @@ namespace spot { const state_ta_explicit* sta = dynamic_cast (s); assert(sta); + + if (sta->get_tgba_condition() == bddtrue) + return tgba_->format_state(sta->get_tgba_state()); + return tgba_->format_state(sta->get_tgba_state()) + "\n" + bdd_format_formula(get_dict(), sta->get_tgba_condition()); @@ -354,26 +428,33 @@ namespace spot for (it = states_set_.begin(); it != states_set_.end(); it++) { - const state_ta_explicit* source = dynamic_cast (*it); + const state_ta_explicit* source = + dynamic_cast (*it); state_ta_explicit::transitions* trans = source->get_transitions(); state_ta_explicit::transitions::iterator it_trans; - 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++; + } + } } } + void + ta_explicit::free_state(const spot::state*) const + { + } + } diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index f6258bc7b..cb0744d42 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -37,8 +37,6 @@ namespace spot class ta_explicit_succ_iterator; class ta_explicit; - - /// ta_explicit explicit representa_explicittion of a Testing Automata_explicit class ta_explicit : public ta { @@ -51,23 +49,27 @@ namespace spot state_ta_explicit* add_state(state_ta_explicit* s); - state_ta_explicit* - add_initial_state(state_ta_explicit* s); + void + add_to_initial_states_set(state* s); void - create_transition(state_ta_explicit* source, bdd condition, state_ta_explicit* dest); + create_transition(state_ta_explicit* source, bdd condition, + state_ta_explicit* dest); void delete_stuttering_transitions(); // ta interface virtual ~ta_explicit(); - virtual const states_set_t* + virtual const states_set_t get_initial_states_set() const; virtual ta_succ_iterator* succ_iter(const spot::state* s) const; + virtual ta_succ_iterator* + succ_iter(const spot::state* s, bdd condition) const; + virtual bdd_dict* get_dict() const; @@ -86,6 +88,12 @@ namespace spot virtual bdd get_state_condition(const spot::state* s) const; + virtual void + free_state(const spot::state* s) const; + + virtual void + delete_stuttering_and_hole_successors(spot::state* s); + private: // Disallow copy. ta_explicit(const ta_explicit& other); @@ -137,6 +145,10 @@ namespace spot transitions* get_transitions() const; + // return transitions filtred by condition + transitions* + get_transitions(bdd condition) const; + void add_transition(transition* t); @@ -156,6 +168,11 @@ namespace spot is_initial_state() const; void set_initial_state(bool is_initial_state); + void + delete_stuttering_and_hole_successors(); + + void + free_transitions(); private: const state* tgba_state_; @@ -164,6 +181,7 @@ namespace spot bool is_accepting_state_; bool is_livelock_accepting_state_; transitions* transitions_; + Sgi::hash_map > transitions_by_condition; }; @@ -173,6 +191,8 @@ namespace spot public: ta_explicit_succ_iterator(const state_ta_explicit* s); + ta_explicit_succ_iterator(const state_ta_explicit* s, bdd condition); + virtual void first(); virtual void @@ -185,11 +205,13 @@ namespace spot virtual bdd current_condition() const; - + virtual bool + is_stuttering_transition() const; private: state_ta_explicit::transitions* transitions_; state_ta_explicit::transitions::const_iterator i_; + const state_ta_explicit* source_; }; } diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc new file mode 100644 index 000000000..d977aff3d --- /dev/null +++ b/src/ta/taproduct.cc @@ -0,0 +1,346 @@ +// Copykripke_structure (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// +// 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. + +#include "taproduct.hh" +#include +#include "misc/hashfunc.hh" + +namespace spot +{ + + //////////////////////////////////////////////////////////// + // state_ta_product + + state_ta_product::state_ta_product(const state_ta_product& o) : + state(), ta_state_(o.get_ta_state()), kripke_state_( + o.get_kripke_state()->clone()) + { + } + + state_ta_product::~state_ta_product() + { + //see ta_product::free_state() method + delete kripke_state_; + } + + int + state_ta_product::compare(const state* other) const + { + const state_ta_product* o = dynamic_cast (other); + assert(o); + int res = ta_state_->compare(o->get_ta_state()); + if (res != 0) + return res; + return kripke_state_->compare(o->get_kripke_state()); + } + + size_t + state_ta_product::hash() const + { + // We assume that size_t is 32-bit wide. + return wang32_hash(ta_state_->hash()) ^ wang32_hash(kripke_state_->hash()); + } + + state_ta_product* + state_ta_product::clone() const + { + return new state_ta_product(*this); + } + + //////////////////////////////////////////////////////////// + // ta_succ_iterator_product + ta_succ_iterator_product::ta_succ_iterator_product(const state_ta_product* s, + const ta* t, const kripke* k) : + source_(s), ta_(t), kripke_(k) + { + kripke_succ_it_ = k->succ_iter(s->get_kripke_state()); + current_state_ = 0; + } + + ta_succ_iterator_product::~ta_succ_iterator_product() + { + // ta_->free_state(current_state_); + delete current_state_; + current_state_ = 0; + delete ta_succ_it_; + delete kripke_succ_it_; + } + + void + ta_succ_iterator_product::step_() + { + if (!ta_succ_it_->done()) + ta_succ_it_->next(); + if (ta_succ_it_->done()) + { + delete ta_succ_it_; + ta_succ_it_ = 0; + kripke_succ_it_->next(); + } + } + + void + ta_succ_iterator_product::first() + { + if (!kripke_succ_it_) + return; + + ta_succ_it_ = 0; + kripke_succ_it_->first(); + // If one of the two successor sets is empty initially, we reset + // kripke_succ_it_, so that done() can detect this situation easily. (We + // choose to reset kripke_succ_it_ because this variable is already used by + // done().) + if (kripke_succ_it_->done()) + { + delete kripke_succ_it_; + kripke_succ_it_ = 0; + return; + } + + next_non_stuttering_(); + } + + void + ta_succ_iterator_product::next() + { + delete current_state_; + current_state_ = 0; + if (is_stuttering_transition()) + { + ta_succ_it_ = 0; + kripke_succ_it_->next(); + } + else + step_(); + + if (!done()) + next_non_stuttering_(); + } + + void + ta_succ_iterator_product::next_non_stuttering_() + { + + bdd sc = kripke_->state_condition(source_->get_kripke_state()); + + while (!done()) + { + state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); + bdd dc = kripke_->state_condition(kripke_succ_it_current_state); + + is_stuttering_transition_ = (sc == dc); + if (is_stuttering_transition_) + { + //if stuttering transition, the TA automata stays in the same state + current_state_ = new state_ta_product(source_->get_ta_state(), + kripke_succ_it_current_state); + current_condition_ = bddtrue; + return; + } + + if (ta_succ_it_ == 0){ + current_condition_ = bdd_setxor(sc, dc); + ta_succ_it_ = ta_->succ_iter(source_->get_ta_state(), current_condition_); + ta_succ_it_->first(); + } + + if (!ta_succ_it_->done()) + { + current_state_ = new state_ta_product(ta_succ_it_->current_state(), + kripke_succ_it_current_state); + return; + } + + delete kripke_succ_it_current_state; + step_(); + } + } + + bool + ta_succ_iterator_product::done() const + { + return !kripke_succ_it_ || kripke_succ_it_->done(); + } + + state_ta_product* + ta_succ_iterator_product::current_state() const + { + //assert(!done()); + //if stuttering transition, the TA automata stays in the same state + // if (is_stuttering_transition()) + // return new state_ta_product(source_->get_ta_state(), + // kripke_succ_it_->current_state()); + // + // return new state_ta_product(ta_succ_it_->current_state(), + // kripke_succ_it_->current_state()); + return current_state_->clone(); + } + + bool + ta_succ_iterator_product::is_stuttering_transition() const + { + // assert(!done()); + // bdd sc = kripke_->state_condition(source_->get_kripke_state()); + // state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); + // bdd dc = kripke_->state_condition(kripke_succ_it_current_state); + // delete kripke_succ_it_current_state; + + return is_stuttering_transition_; + } + + bdd + ta_succ_iterator_product::current_condition() const + { + // assert(!done()); + // bdd sc = kripke_->state_condition(source_->get_kripke_state()); + // state * kripke_succ_it_current_state = kripke_succ_it_->current_state(); + // bdd dc = kripke_->state_condition(kripke_succ_it_current_state); + // delete kripke_succ_it_current_state; + // return bdd_setxor(sc, dc); + + return current_condition_; + } + + //////////////////////////////////////////////////////////// + // ta_product + + + ta_product::ta_product(const ta* testing_automata, + const kripke* kripke_structure) : + dict_(testing_automata->get_dict()), ta_(testing_automata), kripke_( + kripke_structure) + { + assert(dict_ == kripke_structure->get_dict()); + dict_->register_all_variables_of(&ta_, this); + dict_->register_all_variables_of(&kripke_, this); + + } + + ta_product::~ta_product() + { + dict_->unregister_all_my_variables(this); + } + + const ta::states_set_t + ta_product::get_initial_states_set() const + { + //build initial states set + + const ta::states_set_t ta_init_states_set = ta_->get_initial_states_set(); + ta::states_set_t::const_iterator it; + + ta::states_set_t initial_states_set; + + for (it = ta_init_states_set.begin(); it != ta_init_states_set.end(); it++) + { + state* kripke_init_state = kripke_->get_init_state(); + if ((kripke_->state_condition(kripke_init_state)) + == (ta_->get_state_condition(*it))) + { + state_ta_product* stp = new state_ta_product((*it), + kripke_init_state); + + initial_states_set.insert(stp); + } + else + { + delete kripke_init_state; + } + + } + + return initial_states_set; + } + + ta_succ_iterator_product* + ta_product::succ_iter(const state* s) const + { + const state_ta_product* stp = dynamic_cast (s); + assert(s); + + return new ta_succ_iterator_product(stp, ta_, kripke_); + } + + bdd_dict* + ta_product::get_dict() const + { + return dict_; + } + + std::string + ta_product::format_state(const state* state) const + { + const state_ta_product* s = dynamic_cast (state); + assert(s); + return kripke_->format_state(s->get_kripke_state()) + " * \n" + + ta_->format_state(s->get_ta_state()); + } + + bool + ta_product::is_accepting_state(const spot::state* s) const + { + const state_ta_product* stp = dynamic_cast (s); + + return ta_->is_accepting_state(stp->get_ta_state()); + } + + bool + ta_product::is_livelock_accepting_state(const spot::state* s) const + { + const state_ta_product* stp = dynamic_cast (s); + + return ta_->is_livelock_accepting_state(stp->get_ta_state()); + } + + bool + ta_product::is_initial_state(const spot::state* s) const + { + const state_ta_product* stp = dynamic_cast (s); + + state* ta_s = stp->get_ta_state(); + state* kr_s = stp->get_kripke_state(); + + return (ta_->is_initial_state(ta_s)) + && ((kripke_->get_init_state())->compare(kr_s) == 0) + && ((kripke_->state_condition(kr_s)) + == (ta_->get_state_condition(ta_s))); + } + + bdd + ta_product::get_state_condition(const spot::state* s) const + { + const state_ta_product* stp = dynamic_cast (s); + state* ta_s = stp->get_ta_state(); + return ta_->get_state_condition(ta_s); + } + + void + ta_product::free_state(const spot::state* s) const + { + + const state_ta_product* stp = dynamic_cast (s); + ta_->free_state(stp->get_ta_state()); + delete stp; + + } + +} diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh new file mode 100644 index 000000000..9ab38995c --- /dev/null +++ b/src/ta/taproduct.hh @@ -0,0 +1,180 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// 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. + +#ifndef SPOT_TA_TAPRODUCT_HH +# define SPOT_TA_TAPRODUCT_HH + +#include "ta.hh" +#include "kripke/kripke.hh" + +namespace spot +{ + + /// \brief A state for spot::ta_product. + /// + /// This state is in fact a pair of state: the state from the ta + /// automaton and that of Kripke structure. + class state_ta_product : public state + { + public: + /// \brief Constructor + /// \param ta_state The state from the ta automaton. + /// \param kripke_state_ The state from Kripke structure. + + state_ta_product(state* ta_state, state* kripke_state) : + ta_state_(ta_state), kripke_state_(kripke_state) + { + } + + /// Copy constructor + state_ta_product(const state_ta_product& o); + + virtual + ~state_ta_product(); + + state* + get_ta_state() const + { + return ta_state_; + } + + state* + get_kripke_state() const + { + return kripke_state_; + } + + virtual int + compare(const state* other) const; + virtual size_t + hash() const; + virtual state_ta_product* + clone() const; + + private: + state* ta_state_; ///< State from the ta automaton. + state* kripke_state_; ///< State from the kripke structure. + }; + + /// \brief Iterate over the successors of a product computed on the fly. + class ta_succ_iterator_product : public ta_succ_iterator + { + public: + ta_succ_iterator_product(const state_ta_product* s, const ta* t, const kripke* k); + + virtual + ~ta_succ_iterator_product(); + + // iteration + void + first(); + void + next(); + bool + done() const; + + // inspection + state_ta_product* + current_state() const; + bdd + current_condition() const; + + bool + is_stuttering_transition() const; + + private: + //@{ + /// Internal routines to advance to the next successor. + void + step_(); + void + next_non_stuttering_(); + //@} + + protected: + const state_ta_product* source_; + const ta* ta_; + const kripke* kripke_; + ta_succ_iterator* ta_succ_it_; + tgba_succ_iterator* kripke_succ_it_; + state_ta_product* current_state_; + bdd current_condition_; + bool is_stuttering_transition_; + + }; + + /// \brief A lazy product. (States are computed on the fly.) + class ta_product : public ta + { + public: + ta_product(const ta* testing_automata, const kripke* kripke_structure); + + virtual + ~ta_product(); + + virtual const states_set_t + get_initial_states_set() const; + + virtual ta_succ_iterator_product* + succ_iter(const spot::state* s) const; + + virtual ta_succ_iterator_product* + succ_iter(const spot::state* s, bdd condition) const { + + if(condition == bddtrue) return succ_iter(s); + //TODO + return 0; + } + + virtual bdd_dict* + get_dict() const; + + virtual std::string + format_state(const spot::state* s) const; + + virtual bool + is_accepting_state(const spot::state* s) const; + + virtual bool + is_livelock_accepting_state(const spot::state* s) const; + + virtual bool + is_initial_state(const spot::state* s) const; + + virtual bdd + get_state_condition(const spot::state* s) const; + + virtual void + free_state(const spot::state* s) const; + + private: + bdd_dict* dict_; + const ta* ta_; + const kripke* kripke_; + + // Disallow copy. + ta_product(const ta_product&); + ta_product& + operator=(const ta_product&); + }; + +} + +#endif // SPOT_TA_TAPRODUCT_HH diff --git a/src/taalgos/Makefile.am b/src/taalgos/Makefile.am index 7340c8268..f82b98c42 100644 --- a/src/taalgos/Makefile.am +++ b/src/taalgos/Makefile.am @@ -27,11 +27,14 @@ taalgosdir = $(pkgincludedir)/taalgos taalgos_HEADERS = \ sba2ta.hh \ dotty.hh \ - reachiter.hh + reachiter.hh \ + stats.hh \ + emptinessta.hh noinst_LTLIBRARIES = libtaalgos.la libtaalgos_la_SOURCES = \ sba2ta.cc \ dotty.cc \ - reachiter.cc - + reachiter.cc \ + stats.cc \ + emptinessta.cc diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index 14e95174d..c28885728 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -43,11 +43,11 @@ namespace spot os_ << "digraph G {" << std::endl; int n = 0; - const ta::states_set_t* init_states_set = + const ta::states_set_t init_states_set = t_automata_->get_initial_states_set(); ta::states_set_t::const_iterator it; - for (it = (init_states_set->begin()); it != init_states_set->end(); it++) + for (it = (init_states_set.begin()); it != init_states_set.end(); it++) { // cout << (*it).first << " => " << (*it).second << endl; @@ -99,7 +99,7 @@ namespace spot } void - process_link(int in, int out, const tgba_succ_iterator* si) + process_link(int in, int out, const ta_succ_iterator* si) { os_ << " " << in << " -> " << out << " [label=\""; diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc new file mode 100644 index 000000000..16798a194 --- /dev/null +++ b/src/taalgos/emptinessta.cc @@ -0,0 +1,619 @@ +// Copyright (C) 2008 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// 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. + +// #define TRACE + +#include +#ifdef TRACE +#define trace std::clog +#else +#define trace while (0) std::clog +#endif + +#include "emptinessta.hh" +#include "misc/memusage.hh" +#include + +namespace spot +{ + + ta_check::ta_check(const ta* a, option_map o) : + a_(a), o_(o) + { + is_full_2_pass_ = o.get("is_full_2_pass", 0); + } + + ta_check::~ta_check() + { + + } + + bool + ta_check::check() + { + + // We use five main data in this algorithm: + + // * 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 = 1; + + // * todo: the depth-first search stack. This holds pairs of the + // form (STATE, ITERATOR) where ITERATOR is a ta_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; + + Sgi::hash_map + 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; + + std::stack livelock_roots; + + 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; + + } + + while (!init_set.empty()) + { + // Setup depth-first search from initial states. + + { + state* init = dynamic_cast (init_set.top()); + init_set.pop(); + + numbered_state_heap::state_index_p h_init = h->find(init); + + if (h_init.first) + continue; + + 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(); + + //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; + + // 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; + + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = + h->index(curr->clone()); + assert(spi.first); + + scc.rem().push_front(curr); + inc_depth(); + + // set the h value of the Backtracked state to negative value. + // colour[curr] = BLUE; + *spi.second = -std::abs(*spi.second); + + // Backtrack livelock_roots. + if (!livelock_roots.empty() && !livelock_roots.top()->compare( + curr)) + livelock_roots.pop(); + + // When backtracking the root of an SSCC, we must also + // remove that SSCC from the ROOT stacks. We must + // discard from H all reachable states from this SSCC. + assert(!scc.empty()); + if (scc.top().index == std::abs(*spi.second)) + { + // removing states + std::list::iterator i; + + for (i = scc.rem().begin(); i != scc.rem().end(); ++i) + { + numbered_state_heap::state_index_p spi = h->index( + (*i)->clone()); + assert(spi.first->compare(*i) == 0); + assert(*spi.second != -1); + *spi.second = -1; + //colour[*i] = BLACK; + + } + dec_depth(scc.rem().size()); + scc.pop(); + } + + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } + + // We have a successor to look at. + inc_transitions(); + trace + << "PASS 1: transition" << std::endl; + // Fetch the values destination state we are interested in... + state* dest = succ->current_state(); + + //may be Buchi accepting scc + scc.top().is_accepting = a_->is_accepting_state(curr) + && !succ->is_stuttering_transition(); + + bool is_stuttering_transition = succ->is_stuttering_transition(); + + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. + + // Are we going to a new state? + numbered_state_heap::state_index_p spi = h->find(dest); + + // Is this a new state? + if (!spi.first) + { + // Number it, stack it, and register its successors + // for later processing. + h->insert(dest, ++num); + scc.push(num); + + ta_succ_iterator* iter = a_->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + //colour[dest] = GREY; + inc_depth(); + + //push potential root of live-lock accepting cycle + if (a_->is_livelock_accepting_state(dest) + && !is_stuttering_transition) + livelock_roots.push(dest); + + continue; + } + + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; + + // Now this is the most interesting case. We have reached a + // state S1 which is already part of a non-dead SSCC. Any such + // non-dead SSCC has necessarily been crossed by our path to + // this state: there is a state S2 in our path which belongs + // to this SSCC too. We are going to merge all states between + // this S1 and S2 into this SSCC. + // + // This merge is easy to do because the order of the SSCC in + // ROOT is ascending: we just have to merge all SSCCs from the + // top of ROOT that have an index greater to the one of + // the SSCC of S2 (called the "threshold"). + int threshold = std::abs(*spi.second); + std::list rem; + bool acc = false; + + while (threshold < scc.top().index) + { + assert(!scc.empty()); + + acc |= scc.top().is_accepting; + + rem.splice(rem.end(), scc.rem()); + scc.pop(); + + } + // Note that we do not always have + // threshold == scc.top().index + // after this loop, the SSCC whose index is threshold might have + // been merged with a lower SSCC. + + // Accumulate all acceptance conditions into the merged SSCC. + scc.top().is_accepting |= acc; + + scc.rem().splice(scc.rem().end(), rem); + if (scc.top().is_accepting) + { + clear(h, todo, init_set); + trace + << "PASS 1: SUCCESS" << std::endl; + return true; + } + + //ADDLINKS + if (!is_full_2_pass_ && a_->is_livelock_accepting_state(curr) + && is_stuttering_transition) + { + trace + << "PASS 1: heuristic livelock detection " << std::endl; + const state* dest = spi.first; + std::set liveset_dest = + liveset[dest]; + + std::set liveset_curr = + liveset[curr]; + + 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); + 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) + { + 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; + } + + liveset_curr.insert(u); + } + + return false; + + } + + bool + ta_check::livelock_detection(const ta* t) + { + // We use five main data in this algorithm: + + // * sscc: a stack of strongly stuttering-connected components (SSCC) + + + // * 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, + + trace + << "PASS 2" << std::endl; + + 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; + + + + 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); + + + } + + + 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); + + 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(); + + } + + while (!todo.empty()) + { + + state* curr = todo.top().first; + + // 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 2 : backtrack" << std::endl; + + // 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(); + + // 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(); + } + + delete succ; + // Do not delete CURR: it is a key in H. + + 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(); + + 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); + + // Is this a new state? + if (!spi.first) + { + + // Are we going to a new state through a stuttering transition? + + 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); + + 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; + + //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; + } + + } + + // 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()); + + acc |= sscc.top().is_accepting; + + 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. + + // 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; + } + } + + } + clear(h, todo, init_set); + return false; + } + + void + ta_check::clear(numbered_state_heap* h, std::stack todo, + std::stack init_states) + { + + set_states(states() + h->size()); + + while (!init_states.empty()) + { + 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 h; + } + + std::ostream& + ta_check::print_stats(std::ostream& os) const + { + // ecs_->print_stats(os); + os << states() << " unique states visited" << std::endl; + + //TODO sscc; + os << scc.size() << " strongly connected components in search stack" + << 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 new file mode 100644 index 000000000..3ca7f5fd3 --- /dev/null +++ b/src/taalgos/emptinessta.hh @@ -0,0 +1,94 @@ +// Copyright (C) 2008 Laboratoire de Recherche et Development de +// l'Epita (LRDE). +// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// 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. + +#ifndef SPOT_TAALGOS_EMPTINESS_HH +# define SPOT_TAALGOS_EMPTINESS_HH + +#include "ta/ta.hh" +#include "misc/optionmap.hh" +#include "tgbaalgos/gtec/nsheap.hh" +#include "tgbaalgos/emptiness_stats.hh" +#include + +namespace spot +{ + + namespace + { + typedef std::pair pair_state_iter; + } + /// \brief An implementation of the ta emptiness-check algorithm. + /// + /// See the documentation for spot::ta. + class ta_check : public ec_statistics + { + public: + ta_check(const ta* a, option_map o = option_map()); + virtual + ~ta_check(); + + /// Check whether the automaton's language is empty. + virtual bool + check(); + + virtual bool + livelock_detection(const ta* t); + + virtual std::ostream& + print_stats(std::ostream& os) const; + + /// \brief Return the status of the emptiness-check. + /// + /// When check() succeed, the status should be passed along + /// to spot::counter_example. + /// + /// This status should not be deleted, it is a pointer + /// to a member of this class that will be deleted when + /// the ta object is deleted. + // const tgba_check_status* result() const; + + protected: + void + clear(numbered_state_heap* h, std::stack todo, std::stack< + spot::state*> init_set); + bool + heuristic_livelock_detection(const state * stuttering_succ, + numbered_state_heap* h, int h_livelock_root, std::set liveset_curr); + const ta* a_; ///< The automaton. + option_map o_; ///< The options + + bool is_full_2_pass_; + + // * scc: a stack of strongly connected components (SCC) + scc_stack_ta scc; + + // * sscc: a stack of strongly stuttering-connected components (SSCC) + scc_stack_ta sscc; + + }; + +/// @} +} + +#endif // SPOT_TAALGOS_EMPTINESS_HH diff --git a/src/taalgos/reachiter.cc b/src/taalgos/reachiter.cc index 88fb44b58..85cd01321 100644 --- a/src/taalgos/reachiter.cc +++ b/src/taalgos/reachiter.cc @@ -42,7 +42,7 @@ namespace spot // Advance the iterator before deleting the "key" pointer. const state* ptr = s->first; ++s; - delete ptr; + t_automata_->free_state(ptr); } } @@ -51,13 +51,13 @@ namespace spot { int n = 0; start(); - const ta::states_set_t* init_states_set = + const ta::states_set_t init_states_set = t_automata_->get_initial_states_set(); ta::states_set_t::const_iterator it; - for (it = init_states_set->begin(); it != init_states_set->end(); it++) + for (it = init_states_set.begin(); it != init_states_set.end(); it++) { - state* init_state = (*it)->clone(); + state* init_state = (*it); if (want_state(init_state)) add_state(init_state); seen[init_state] = ++n; @@ -69,11 +69,11 @@ namespace spot { assert(seen.find(t) != seen.end()); int tn = seen[t]; - tgba_succ_iterator* si = t_automata_->succ_iter(t); + ta_succ_iterator* si = t_automata_->succ_iter(t); process_state(t, tn); for (si->first(); !si->done(); si->next()) { - const state* current = si->current_state()->clone(); + const state* current = si->current_state(); seen_map::const_iterator s = seen.find(current); bool ws = want_state(current); if (s == seen.end()) @@ -89,7 +89,7 @@ namespace spot { if (ws) process_link(tn, s->second, si); - delete current; + t_automata_->free_state(current); } } delete si; @@ -119,7 +119,7 @@ namespace spot } void - ta_reachable_iterator::process_link(int, int, const tgba_succ_iterator*) + ta_reachable_iterator::process_link(int, int, const ta_succ_iterator*) { } diff --git a/src/taalgos/reachiter.hh b/src/taalgos/reachiter.hh index 32c6702e8..f2280f4e6 100644 --- a/src/taalgos/reachiter.hh +++ b/src/taalgos/reachiter.hh @@ -92,7 +92,7 @@ namespace spot /// spot::ta_reachable_iterator instance and destroyed when the /// instance is destroyed. virtual void - process_link(int in, int out, const tgba_succ_iterator* si); + process_link(int in, int out, const ta_succ_iterator* si); protected: diff --git a/src/taalgos/sba2ta.cc b/src/taalgos/sba2ta.cc index 307a741c2..7dc205bec 100644 --- a/src/taalgos/sba2ta.cc +++ b/src/taalgos/sba2ta.cc @@ -30,7 +30,6 @@ #include #include "sba2ta.hh" - using namespace std; namespace spot @@ -42,26 +41,32 @@ namespace spot ta_explicit* ta = new spot::ta_explicit(tgba_); - // build I set: - bdd init_condition; - bdd all_props = bddtrue; - ta::states_set_t todo; + std::stack todo; - while ((init_condition = bdd_satoneset(all_props, atomic_propositions_set_, - bddtrue)) != bddfalse) + // 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) { - all_props -= init_condition; - state_ta_explicit* init_state = new state_ta_explicit((tgba_->get_init_state()), - init_condition, true); - ta->add_initial_state(init_state); - todo.insert(init_state); + tgba_condition -= satone_tgba_condition; + state_ta_explicit* init_state = new state_ta_explicit( + tgba_init_state->clone(), satone_tgba_condition, true, + tgba_->state_is_accepting(tgba_init_state)); + state_ta_explicit* is = ta->add_state(init_state); + assert(is == init_state); + ta->add_to_initial_states_set(is); + todo.push(init_state); } + delete tgba_init_state; while (!todo.empty()) { - ta::states_set_t::iterator todo_it = todo.begin(); - state_ta_explicit* source = dynamic_cast (*todo_it); - todo.erase(todo_it); + state_ta_explicit* source = todo.top(); + todo.pop(); tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter( source->get_tgba_state()); @@ -75,26 +80,35 @@ namespace spot { tgba_condition -= satone_tgba_condition; - state_ta_explicit* new_dest = new state_ta_explicit(tgba_state->clone(), - satone_tgba_condition, false, tgba_->state_is_accepting( - tgba_state)); - 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 = new state_ta_explicit( + tgba_state->clone(), dest_condition, false, + tgba_->state_is_accepting(tgba_state)); - if (dest != new_dest) - { - // the state dest already exists in the testing automata - delete new_dest->get_tgba_state(); - delete new_dest; - } - else - { - todo.insert(dest); - } + state_ta_explicit* dest = ta->add_state(new_dest); - ta->create_transition(source, bdd_setxor( - source->get_tgba_condition(), dest->get_tgba_condition()), - dest); + if (dest != new_dest) + { + // the state dest already exists in the testing automata + delete new_dest->get_tgba_state(); + delete new_dest; + } + else + { + todo.push(dest); + } + + ta->create_transition(source, bdd_setxor( + source->get_tgba_condition(), + dest->get_tgba_condition()), dest); + } } delete tgba_state; @@ -105,8 +119,6 @@ namespace spot compute_livelock_acceptance_states(ta); - ta->delete_stuttering_transitions(); - return ta; } @@ -121,7 +133,7 @@ namespace spot { // We use five main data in this algorithm: // * sscc: a stack of strongly stuttering-connected components (SSCC) - sscc_stack sscc; + scc_stack_ta sscc; // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) @@ -140,23 +152,24 @@ namespace spot std::stack todo; // * init: the set of the depth-first search initial states - ta::states_set_t init_set; + std::stack init_set; ta::states_set_t::const_iterator it; - for (it = (testing_automata->get_initial_states_set())->begin(); it != (testing_automata->get_initial_states_set())->end(); 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.insert(init_state); + state* init_state = dynamic_cast (*it); + init_set.push(init_state); } while (!init_set.empty()) { - // Setup depth-first search from an initial state. + // Setup depth-first search from initial states. { - ta::states_set_t::iterator init_set_it = init_set.begin(); - state_ta_explicit* init = dynamic_cast (*init_set_it); - init_set.erase(init_set_it); + state_ta_explicit* init = + dynamic_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); @@ -165,8 +178,8 @@ namespace spot h->insert(init_clone, ++num); sscc.push(num); - sscc.top().is_accepting = testing_automata->is_accepting_state(init); - sscc.top().is_initial = testing_automata->is_initial_state(init); + 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)); @@ -176,11 +189,19 @@ namespace spot while (!todo.empty()) { + 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; + } + // We are looking at the next successor in SUCC. tgba_succ_iterator* succ = todo.top().second; - state* curr = todo.top().first; - // If there is no more successor, backtrack. if (succ->done()) { @@ -190,7 +211,8 @@ namespace spot todo.pop(); // fill rem with any component removed, - numbered_state_heap::state_index_p spi = h->index(curr->clone()); + numbered_state_heap::state_index_p spi = + h->index(curr->clone()); assert(spi.first); sscc.rem().push_front(curr); @@ -207,8 +229,9 @@ namespace spot && (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); + 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) @@ -223,34 +246,14 @@ namespace spot } - if (sscc.top().is_initial) - {//if it is an initial sscc - //add the state to I (=the initial states set) - - state_ta_explicit * initial_state = - dynamic_cast (*i); - - testing_automata->add_initial_state(initial_state); - } } - is_livelock_accepting_sscc = testing_automata->is_livelock_accepting_state( - *sscc.rem().begin()); sscc.pop(); - if (is_livelock_accepting_sscc && !sscc.empty()) - { - sscc.top().is_accepting = true; - state_ta_explicit * livelock_accepting_state = - dynamic_cast (todo.top().first); - livelock_accepting_state->set_livelock_accepting_state( - true); - - } - if (sscc.top().is_initial && !sscc.empty()) - sscc.top().is_initial = true; } + // automata reduction + testing_automata->delete_stuttering_and_hole_successors(curr); delete succ; // Do not delete CURR: it is a key in H. continue; @@ -266,17 +269,18 @@ namespace spot // 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); + bool is_stuttering_transition = + testing_automata->get_state_condition(curr) + == testing_automata->get_state_condition(dest); state* dest_clone = dest->clone(); - numbered_state_heap::state_index_p spi = h->find(dest_clone); + spi = h->find(dest_clone); // Is this a new state? if (!spi.first) { if (!is_stuttering_transition) { - init_set.insert(dest); + init_set.push(dest); delete dest_clone; continue; } @@ -285,8 +289,9 @@ namespace spot // for later processing. h->insert(dest_clone, ++num); sscc.push(num); - sscc.top().is_accepting = testing_automata->is_accepting_state(dest); - sscc.top().is_initial = testing_automata->is_initial_state(dest); + 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)); @@ -299,7 +304,8 @@ namespace spot if (!curr->compare(dest)) { - state_ta_explicit * self_loop_state = dynamic_cast (curr); + state_ta_explicit * self_loop_state = + dynamic_cast (curr); if (testing_automata->is_accepting_state(self_loop_state)) self_loop_state->set_livelock_accepting_state(true); @@ -320,13 +326,12 @@ namespace spot int threshold = *spi.second; std::list rem; bool acc = false; - bool init = false; + while (threshold < sscc.top().index) { assert(!sscc.empty()); acc |= sscc.top().is_accepting; - init |= sscc.top().is_initial; rem.splice(rem.end(), sscc.rem()); sscc.pop(); @@ -339,7 +344,6 @@ namespace spot // Accumulate all acceptance conditions into the merged SSCC. sscc.top().is_accepting |= acc; - sscc.top().is_initial |= init; sscc.rem().splice(sscc.rem().end(), rem); diff --git a/src/taalgos/stats.cc b/src/taalgos/stats.cc new file mode 100644 index 000000000..7c7255133 --- /dev/null +++ b/src/taalgos/stats.cc @@ -0,0 +1,79 @@ +// Copyright (C) 2008 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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. + +#include +#include "ta/ta.hh" +#include "stats.hh" +#include "reachiter.hh" + +namespace spot +{ + namespace + { + class stats_bfs : public ta_reachable_iterator_breadth_first + { + public: + stats_bfs(const ta* a, ta_statistics& s) : + ta_reachable_iterator_breadth_first(a), s_(s) + { + } + + void + process_state(const state* s, int) + { + ++s_.states; + if (t_automata_->is_accepting_state(s) + || t_automata_->is_livelock_accepting_state(s)) + ++s_.acceptance_states; + } + + void + process_link(int, int, const ta_succ_iterator*) + { + ++s_.transitions; + } + + private: + ta_statistics& s_; + }; + } // anonymous + + + std::ostream& + ta_statistics::dump(std::ostream& out) const + { + out << "transitions: " << transitions << std::endl; + out << "states: " << states << std::endl; + return out; + } + + ta_statistics + stats_reachable(const ta* t) + { + ta_statistics s = + { 0, 0, 0}; + stats_bfs d(t, s); + d.run(); + return s; + } +} diff --git a/src/taalgos/stats.hh b/src/taalgos/stats.hh new file mode 100644 index 000000000..f7c6a99a0 --- /dev/null +++ b/src/taalgos/stats.hh @@ -0,0 +1,51 @@ +// Copyright (C) 2008 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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. + +#ifndef SPOT_TAALGOS_STATS_HH +# define SPOT_TAALGOS_STATS_HH + +#include "ta/ta.hh" +#include + +namespace spot +{ + + /// \addtogroup ta_misc + /// @{ + + struct ta_statistics + { + unsigned transitions; + unsigned states; + unsigned acceptance_states; + + std::ostream& dump(std::ostream& out) const; + }; + + /// \brief Compute statistics for an automaton. + ta_statistics stats_reachable(const ta* t); + + /// @} +} + +#endif // SPOT_TAALGOS_STATS_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7c6b5fe5d..3d0a074d5 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1061,13 +1061,11 @@ main(int argc, char** argv) } - const spot::tgba* product_degeneralized = 0; - if (ta_opt) { - spot::tgba_sba_proxy* degeneralized_new = 0; - spot::tgba_sba_proxy* degeneralized = - dynamic_cast (a); + const spot::tgba_sba_proxy* degeneralized_new = 0; + const spot::tgba_sba_proxy* degeneralized = + dynamic_cast (a); if (degeneralized == 0) degeneralized_new = degeneralized = new spot::tgba_sba_proxy(a); @@ -1092,6 +1090,7 @@ main(int argc, char** argv) output = -1; } + spot::tgba* product_degeneralized = 0; if (system) { @@ -1120,6 +1119,7 @@ main(int argc, char** argv) } } + if (echeck_inst && (a->number_of_acceptance_conditions() < echeck_inst->min_acceptance_conditions()))