From a15aac2845814cff1e44f6924efab714f1a8373e Mon Sep 17 00:00:00 2001 From: Pierre PARUTTO Date: Tue, 6 Mar 2012 00:13:15 +0100 Subject: [PATCH] Revamp tgbaexplicit.hh * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: Factor most of the code in an explicit_graph that inherits from type. The tgba_explicit type now inherits from explicit_graph. * src/ltlvisit/contain.cc, src/neverparse/neverclaimparse.yy src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc, src/tgbaalgos/sccfilter.cc, src/tgbaparse/tgbaparse.yy, src/tgbatest/complementation.cc, src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Replace tgba_explicit* by the actual type used. * src/tgbatest/explicit2.cc: New file. * src/tgbatest/Makefile.am: Add it. --- src/ltlvisit/contain.cc | 8 +- src/neverparse/neverclaimparse.yy | 4 +- src/tgba/tgbaexplicit.cc | 350 +----------- src/tgba/tgbaexplicit.hh | 872 ++++++++++++++++++++---------- src/tgba/tgbareduc.cc | 57 +- src/tgba/tgbareduc.hh | 4 +- src/tgbaalgos/cutscc.cc | 2 +- src/tgbaalgos/dupexp.cc | 6 +- src/tgbaalgos/dupexp.hh | 4 +- src/tgbaalgos/emptiness.cc | 9 +- src/tgbaalgos/ltl2tgba_fm.cc | 8 +- src/tgbaalgos/ltl2tgba_fm.hh | 13 +- src/tgbaalgos/minimize.cc | 2 +- src/tgbaalgos/powerset.cc | 2 +- src/tgbaalgos/randomgraph.cc | 13 +- src/tgbaalgos/sccfilter.cc | 8 +- src/tgbaparse/tgbaparse.yy | 2 +- src/tgbatest/Makefile.am | 2 + src/tgbatest/complementation.cc | 2 +- src/tgbatest/explicit.cc | 2 +- src/tgbatest/explicit2.cc | 126 +++++ src/tgbatest/explprod.cc | 4 +- src/tgbatest/ltl2tgba.cc | 2 +- src/tgbatest/mixprod.cc | 2 +- src/tgbatest/powerset.cc | 4 +- src/tgbatest/tgbaread.cc | 4 +- src/tgbatest/tripprod.cc | 6 +- 27 files changed, 810 insertions(+), 708 deletions(-) create mode 100644 src/tgbatest/explicit2.cc diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 0c0dc87d5..cc727154e 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -132,9 +132,11 @@ namespace spot if (i != translated_.end()) return &i->second; - const tgba_explicit* e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, - branching_postponement_, - fair_loop_approx_); + const tgba_explicit_formula* e = + ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, + branching_postponement_, + fair_loop_approx_); + record_& r = translated_[f->clone()]; r.translation = e; return &r; diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index a849cdb1a..5f7bdfda9 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -120,7 +120,7 @@ ident_list: state: ident_list "skip" { - spot::tgba_explicit::transition* t = result->create_transition(*$1, *$1); + spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1); bool acc = !strncmp("accept", $1->c_str(), 6); if (acc) result->add_acceptance_condition(t, @@ -135,7 +135,7 @@ state: bool acc = !strncmp("accept", $1->c_str(), 6); for (it = $3->begin(); it != $3->end(); ++it) { - spot::tgba_explicit::transition* t = + spot::state_explicit_string::transition* t = result->create_transition(*$1,*it->second); result->add_condition(t, it->first); diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index e305c526b..55f33937b 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -1,8 +1,5 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement +// Copyright (C) 2012 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. // @@ -21,348 +18,13 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include -#include "ltlast/atomic_prop.hh" -#include "ltlast/constant.hh" #include "tgbaexplicit.hh" -#include "tgba/formula2bdd.hh" -#include "misc/bddop.hh" -#include -#include "ltlvisit/tostring.hh" +#include "ltlast/constant.hh" namespace spot { - - //////////////////////////////////////// - // tgba_explicit_succ_iterator - - tgba_explicit_succ_iterator::tgba_explicit_succ_iterator - (const state_explicit::transitions_t* s, bdd all_acc) - : s_(s), all_acceptance_conditions_(all_acc) - { - } - - void - tgba_explicit_succ_iterator::first() - { - i_ = s_->begin(); - } - - void - tgba_explicit_succ_iterator::next() - { - ++i_; - } - - bool - tgba_explicit_succ_iterator::done() const - { - return i_ == s_->end(); - } - - state_explicit* - tgba_explicit_succ_iterator::current_state() const - { - assert(!done()); - return const_cast(i_->dest); - } - - bdd - tgba_explicit_succ_iterator::current_condition() const - { - assert(!done()); - return i_->condition; - } - - bdd - tgba_explicit_succ_iterator::current_acceptance_conditions() const - { - assert(!done()); - return i_->acceptance_conditions & all_acceptance_conditions_; - } - - - //////////////////////////////////////// - // state_explicit - - int - state_explicit::compare(const spot::state* other) const - { - const state_explicit* o = down_cast(other); - assert(o); - // Do not simply return "o - this", it might not fit in an int. - if (o < this) - return -1; - if (o > this) - return 1; - return 0; - } - - size_t - state_explicit::hash() const - { - return - reinterpret_cast(this) - static_cast(0); - } - - - //////////////////////////////////////// - // tgba_explicit - - - tgba_explicit::tgba_explicit(bdd_dict* dict) - : dict_(dict), init_(0), all_acceptance_conditions_(bddfalse), - neg_acceptance_conditions_(bddtrue), - all_acceptance_conditions_computed_(false) - { - } - - tgba_explicit::~tgba_explicit() - { - dict_->unregister_all_my_variables(this); - } - - tgba_explicit::transition* - tgba_explicit::create_transition(state* source, const state* dest) - { - transition t; - t.dest = dest; - t.condition = bddtrue; - t.acceptance_conditions = bddfalse; - state_explicit::transitions_t::iterator i = - source->successors.insert(source->successors.end(), t); - return &*i; - } - void - tgba_explicit::add_condition(transition* t, const ltl::formula* f) - { - t->condition &= formula_to_bdd(f, dict_, this); - f->destroy(); - } - - void - tgba_explicit::add_conditions(transition* t, bdd f) - { - dict_->register_propositions(f, this); - t->condition &= f; - } - - void - tgba_explicit::copy_acceptance_conditions_of(const tgba *a) - { - assert(neg_acceptance_conditions_ == bddtrue); - assert(all_acceptance_conditions_computed_ == false); - bdd f = a->neg_acceptance_conditions(); - dict_->register_acceptance_variables(f, this); - neg_acceptance_conditions_ = f; - } - - void - tgba_explicit::set_acceptance_conditions(bdd acc) - { - assert(neg_acceptance_conditions_ == bddtrue); - assert(all_acceptance_conditions_computed_ == false); - dict_->register_acceptance_variables(bdd_support(acc), this); - neg_acceptance_conditions_ = compute_neg_acceptance_conditions(acc); - all_acceptance_conditions_computed_ = true; - all_acceptance_conditions_ = acc; - } - - bool - tgba_explicit::has_acceptance_condition(const ltl::formula* f) const - { - return dict_->is_registered_acceptance_variable(f, this); - } - - bdd - tgba_explicit::get_acceptance_condition(const ltl::formula* f) - { - bdd_dict::fv_map::iterator i = dict_->acc_map.find(f); - assert(has_acceptance_condition(f)); - /* If this second assert fails and the first doesn't, - things are badly broken. This has already happened. */ - assert(i != dict_->acc_map.end()); - f->destroy(); - bdd v = bdd_ithvar(i->second); - v &= bdd_exist(neg_acceptance_conditions_, v); - return v; - } - - void - tgba_explicit::add_acceptance_condition(transition* t, const ltl::formula* f) - { - bdd c = get_acceptance_condition(f); - t->acceptance_conditions |= c; - } - - void - tgba_explicit::add_acceptance_conditions(transition* t, bdd f) - { - bdd sup = bdd_support(f); - dict_->register_acceptance_variables(sup, this); - while (sup != bddtrue) - { - neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup)); - sup = bdd_high(sup); - } - t->acceptance_conditions |= f; - } - - state* - tgba_explicit::get_init_state() const - { - // Fix empty automata by adding a lone initial state. - if (!init_) - const_cast(this)->add_default_init(); - return init_; - } - - tgba_succ_iterator* - tgba_explicit::succ_iter(const spot::state* state, - const spot::state* global_state, - const tgba* global_automaton) const - { - const state_explicit* s = down_cast(state); - assert(s); - (void) global_state; - (void) global_automaton; - return new tgba_explicit_succ_iterator(&s->successors, - all_acceptance_conditions()); - } - - bdd - tgba_explicit::compute_support_conditions(const spot::state* in) const - { - const state_explicit* s = down_cast(in); - assert(s); - const state_explicit::transitions_t& st = s->successors; - - bdd res = bddfalse; - state_explicit::transitions_t::const_iterator i; - for (i = st.begin(); i != st.end(); ++i) - res |= i->condition; - return res; - } - - bdd - tgba_explicit::compute_support_variables(const spot::state* in) const - { - const state_explicit* s = down_cast(in); - assert(s); - const state_explicit::transitions_t& st = s->successors; - - bdd res = bddtrue; - state_explicit::transitions_t::const_iterator i; - for (i = st.begin(); i != st.end(); ++i) - res &= bdd_support(i->condition); - return res; - } - - bdd_dict* - tgba_explicit::get_dict() const - { - return dict_; - } - - bdd - tgba_explicit::all_acceptance_conditions() const - { - if (!all_acceptance_conditions_computed_) - { - all_acceptance_conditions_ = - compute_all_acceptance_conditions(neg_acceptance_conditions_); - all_acceptance_conditions_computed_ = true; - } - return all_acceptance_conditions_; - } - - bdd - tgba_explicit::neg_acceptance_conditions() const - { - return neg_acceptance_conditions_; - } - - tgba_explicit_string::~tgba_explicit_string() - { - ns_map::iterator i; - for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) - { - // Do not erase the same state twice. (Because of possible aliases.) - if (state_name_map_.erase(i->second)) - { - delete i->second; - } - } - } - - tgba_explicit::state* - tgba_explicit_string::add_default_init() - { - return add_state("empty"); - } - - std::string - tgba_explicit_string::format_state(const spot::state* s) const - { - const state_explicit* se = down_cast(s); - assert(se); - sn_map::const_iterator i = state_name_map_.find(se); - assert(i != state_name_map_.end()); - return i->second; - } - - tgba_explicit_formula::~tgba_explicit_formula() - { - ns_map::iterator i = name_state_map_.begin(); - while (i != name_state_map_.end()) - { - // Advance the iterator before deleting the formula. - const ltl::formula* s = i->first; - delete i->second; - ++i; - s->destroy(); - } - } - - tgba_explicit::state* tgba_explicit_formula::add_default_init() - { - return add_state(ltl::constant::true_instance()); - } - - std::string - tgba_explicit_formula::format_state(const spot::state* s) const - { - const state_explicit* se = down_cast(s); - assert(se); - sn_map::const_iterator i = state_name_map_.find(se); - assert(i != state_name_map_.end()); - return ltl::to_string(i->second); - } - - tgba_explicit_number::~tgba_explicit_number() - { - ns_map::iterator i = name_state_map_.begin(); - while (i != name_state_map_.end()) - { - delete i->second; - ++i; - } - } - - tgba_explicit::state* tgba_explicit_number::add_default_init() - { - return add_state(0); - } - - std::string - tgba_explicit_number::format_state(const spot::state* s) const - { - const state_explicit* se = down_cast(s); - assert(se); - sn_map::const_iterator i = state_name_map_.find(se); - assert(i != state_name_map_.end()); - std::stringstream ss; - ss << i->second; - return ss.str(); - } + const std::string state_explicit_string::default_val("empty"); + const int state_explicit_number::default_val(0); + const ltl::formula* + state_explicit_formula::default_val(ltl::constant::true_instance()); } diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index a8f3df0c4..f3c1a3837 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// -*- encoding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita. +// Copyright (C) 2003, 2004, 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. // @@ -24,21 +25,48 @@ #ifndef SPOT_TGBA_TGBAEXPLICIT_HH # define SPOT_TGBA_TGBAEXPLICIT_HH -#include "misc/hash.hh" +#include #include + #include "tgba.hh" +#include "tgba/formula2bdd.hh" +#include "misc/hash.hh" +#include "misc/bddop.hh" #include "ltlast/formula.hh" -#include +#include "ltlvisit/tostring.hh" namespace spot { - // Forward declarations. See below. - class state_explicit; - class tgba_explicit_succ_iterator; - class tgba_explicit; + ///misc + template + struct destroy_key + { + void destroy(T t) + { + (void) t; + } + }; - /// States used by spot::tgba_explicit. + template<> + struct destroy_key + { + void destroy(const ltl::formula* t) + { + t->destroy(); + } + }; + + class tba: public tgba + { + public: + /// A State in a TBA (Transition based Buchi Automaton) is accepting + /// iff all outgoing transitions are accepting. + virtual bool is_accepting(const spot::state* s) = 0; + }; + + /// States used by spot::explicit_graph implementation /// \ingroup tgba_representation + template class state_explicit: public spot::state { public: @@ -46,12 +74,35 @@ namespace spot { } - virtual int compare(const spot::state* other) const; - virtual size_t hash() const; - - virtual state_explicit* clone() const + state_explicit(const Label& l): + label_(l) { - return const_cast(this); + } + + virtual ~state_explicit() + { + } + + void destroy() const + { + } + + typedef Label Label_t; + typedef label_hash label_hash_t; + + struct transition + { + bdd condition; + bdd acceptance_conditions; + const state_explicit* dest; + }; + + typedef std::list transitions_t; + transitions_t successors; + + const Label& label() const + { + return label_; } bool empty() const @@ -59,347 +110,600 @@ namespace spot return successors.empty(); } - virtual - void destroy() const + virtual int compare(const state* other) const { + const state_explicit* s = + down_cast*>(other); + assert (s); + + // Do not simply return "o - this", it might not fit in an int. + if (s < this) + return -1; + if (s > this) + return 1; + return 0; } - /// Explicit transitions. - struct transition - { - bdd condition; - bdd acceptance_conditions; - const state_explicit* dest; - }; - - typedef std::list transitions_t; - transitions_t successors; - private: - state_explicit(const state_explicit& other); - state_explicit& operator=(const state_explicit& other); - - virtual ~state_explicit() + virtual size_t hash() const { + return + reinterpret_cast(this) - static_cast(0); } - friend class tgba_explicit_string; - friend class tgba_explicit_formula; - friend class tgba_explicit_number; - }; - - /// Explicit representation of a spot::tgba. - /// \ingroup tgba_representation - class tgba_explicit: public tgba - { - public: - typedef state_explicit state; - typedef state_explicit::transition transition; - - tgba_explicit(bdd_dict* dict); - - /// Add a default initial state. - virtual state* add_default_init() = 0; - - transition* - create_transition(state* source, const state* dest); - - void add_condition(transition* t, const ltl::formula* f); - /// This assumes that all variables in \a f are known from dict. - void add_conditions(transition* t, bdd f); - - /// \brief Copy the acceptance conditions of a tgba. - /// - /// If used, this function should be called before creating any - /// transition. - void copy_acceptance_conditions_of(const tgba *a); - - /// The the acceptance conditions. - void set_acceptance_conditions(bdd acc); - - bool has_acceptance_condition(const ltl::formula* f) const; - void add_acceptance_condition(transition* t, const ltl::formula* f); - /// This assumes that all acceptance conditions in \a f are known from dict. - void add_acceptance_conditions(transition* t, bdd f); - - // tgba interface - virtual ~tgba_explicit(); - virtual spot::state* get_init_state() const; - virtual tgba_succ_iterator* - succ_iter(const spot::state* local_state, - const spot::state* global_state = 0, - const tgba* global_automaton = 0) const; - virtual bdd_dict* get_dict() const; - - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - - virtual std::string format_state(const spot::state* s) const = 0; + virtual state_explicit* + clone() const + { + return const_cast*>(this); + } protected: - virtual bdd compute_support_conditions(const spot::state* state) const; - virtual bdd compute_support_variables(const spot::state* state) const; - - bdd get_acceptance_condition(const ltl::formula* f); - - bdd_dict* dict_; - state_explicit* init_; - mutable bdd all_acceptance_conditions_; - bdd neg_acceptance_conditions_; - mutable bool all_acceptance_conditions_computed_; - - private: - // Disallow copy. - tgba_explicit(const tgba_explicit& other); - tgba_explicit& operator=(const tgba_explicit& other); + Label label_; }; + ///states labeled by an int + /// \ingroup tgba_representation + class state_explicit_number: + public state_explicit > + { + public: + state_explicit_number() + : state_explicit >() + { + } + state_explicit_number(int label) + : state_explicit >(label) + { + } + + virtual void destroy() + { + } + + static const int default_val; + static std::string to_string(int l) + { + std::stringstream ss; + ss << l; + return ss.str(); + } + }; + + /// States labeled by a string + /// \ingroup tgba_representation + class state_explicit_string: + public state_explicit + { + public: + state_explicit_string(): + state_explicit() + { + } + + state_explicit_string(const std::string& label) + : state_explicit(label) + { + } + + virtual void destroy() + { + } + + static const std::string default_val; + static std::string to_string(const std::string& l) + { + return l; + } + }; + + /// States labeled by a formula + /// \ingroup tgba_representation + class state_explicit_formula: + public state_explicit + { + public: + state_explicit_formula(): + state_explicit() + { + } + + state_explicit_formula(const ltl::formula* label) + : state_explicit(label) + { + } + + virtual void destroy() + { + } + + static const ltl::formula* default_val; + static std::string to_string(const ltl::formula* l) + { + return ltl::to_string(l); + } + }; /// Successor iterators used by spot::tgba_explicit. /// \ingroup tgba_representation + template class tgba_explicit_succ_iterator: public tgba_succ_iterator { public: - tgba_explicit_succ_iterator(const state_explicit::transitions_t* s, - bdd all_acc); + tgba_explicit_succ_iterator(const State* start, + bdd all_acc) + : start_(start), + all_acceptance_conditions_(all_acc) + { + } - virtual void first(); - virtual void next(); - virtual bool done() const; + virtual void first() + { + it_ = start_->successors.begin(); + } - virtual state_explicit* current_state() const; - virtual bdd current_condition() const; - virtual bdd current_acceptance_conditions() const; + virtual void next() + { + ++it_; + } + + virtual bool done() const + { + return it_ == start_->successors.end(); + } + + virtual State* current_state() const + { + assert(!done()); + + //ugly but I can't see any other wayout + const State* res = down_cast(it_->dest); + assert(res); + + return + const_cast(res); + } + + virtual bdd current_condition() const + { + assert(!done()); + return it_->condition; + } + + virtual bdd current_acceptance_conditions() const + { + assert(!done()); + return it_->acceptance_conditions & all_acceptance_conditions_; + } private: - const state_explicit::transitions_t* s_; - state_explicit::transitions_t::const_iterator i_; + const State* start_; + typename State::transitions_t::const_iterator it_; bdd all_acceptance_conditions_; }; - /// A tgba_explicit instance with states labeled by a given type. - template - class tgba_explicit_labelled: public tgba_explicit + /// Graph implementation for automata representation + /// \ingroup tgba_representation + template + class explicit_graph: public Type { protected: - typedef label label_t; - typedef Sgi::hash_map ns_map; - typedef Sgi::hash_map > sn_map; - ns_map name_state_map_; - sn_map state_name_map_; + typedef Sgi::hash_map ls_map; + typedef Sgi::hash_map > sl_map; + typedef typename State::transition transition; + public: - tgba_explicit_labelled(bdd_dict* dict) : tgba_explicit(dict) {}; - - bool has_state(const label& name) + explicit_graph(bdd_dict* dict) + : ls_(), + sl_(), + init_(0), + dict_(dict) { - return name_state_map_.find(name) != name_state_map_.end(); } - const label& get_label(const state_explicit* s) const + State* add_default_init() { - typename sn_map::const_iterator i = state_name_map_.find(s); - assert(i != state_name_map_.end()); - return i->second; - } - - const label& get_label(const spot::state* s) const - { - const state_explicit* se = down_cast(s); - assert(se); - return get_label(se); - } - - /// Return the state_explicit for \a name, creating the state if - /// it does not exist. - state* add_state(const label& name) - { - typename ns_map::iterator i = name_state_map_.find(name); - if (i == name_state_map_.end()) - { - state_explicit* s = new state_explicit; - name_state_map_[name] = s; - state_name_map_[s] = name; - - // The first state we add is the inititial state. - // It can also be overridden with set_init_state(). - if (!init_) - init_ = s; - - return s; - } - return i->second; - } - - state* - set_init_state(const label& state) - { - state_explicit* s = add_state(state); - init_ = s; - return s; - } - - - transition* - create_transition(state* source, const state* dest) - { - return tgba_explicit::create_transition(source, dest); + return add_state(State::default_val); } transition* - create_transition(const label& source, const label& dest) + create_transition(State* source, const State* dest) + { + transition t; + + t.dest = dest; + t.condition = bddtrue; + t.acceptance_conditions = bddfalse; + + typename State::transitions_t::iterator i = + source->successors.insert(source->successors.end(), t); + + return &*i; + } + + transition* + create_transition(const typename State::Label_t& source, + const typename State::Label_t& dest) { // It's important that the source be created before the // destination, so the first source encountered becomes the // default initial state. - state* s = add_state(source); - return tgba_explicit::create_transition(s, add_state(dest)); + State* s = add_state(source); + return create_transition(s, add_state(dest)); + } + + transition* + get_transition(const tgba_explicit_succ_iterator* si) + { + return const_cast(&(*(si->i_))); + } + + void add_condition(transition* t, const ltl::formula* f) + { + t->condition &= formula_to_bdd(f, dict_, this); + f->destroy(); + } + + /// This assumes that all variables in \a f are known from dict. + void add_conditions(transition* t, bdd f) + { + dict_->register_propositions(f, this); + t->condition &= f; + } + + bool has_acceptance_condition(const ltl::formula* f) const + { + return dict_->is_registered_acceptance_variable(f, this); + } + + //old tgba explicit labelled interface + bool has_state(const typename State::Label_t& name) + { + return ls_.find(name) != ls_.end(); + } + + const typename State::Label_t& get_label(const State* s) const + { + typename sl_map::const_iterator i = sl_.find(s); + assert(i != sl_.end()); + return i->second; + } + + const typename State::Label_t& get_label(const spot::state* s) const + { + const State* se = down_cast(s); + assert(se); + return get_label(se); + } + + transition* + create_trainsition(const typename State::Label_t& source, + const typename State::Label_t& dest) + { + // It's important that the source be created before the + // destination, so the first source encountered becomes the + // default initial state. + State* s = add_state(source); + return create_transition(s, add_state(dest)); } void complement_all_acceptance_conditions() { - bdd all = all_acceptance_conditions(); - typename ns_map::iterator i; - for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) + bdd all = this->all_acceptance_conditions(); + typename ls_map::iterator i; + for (i = ls_.begin(); i != ls_.end(); ++i) { - state_explicit::transitions_t::iterator i2; - for (i2 = i->second->successors.begin(); - i2 != i->second->successors.end(); ++i2) - { - i2->acceptance_conditions = all - i2->acceptance_conditions; - } + typename State::transitions_t::iterator i2; + for (i2 = i->second.successors.begin(); + i2 != i->second.successors.end(); ++i2) + i2->acceptance_conditions = all - i2->acceptance_conditions; } } + void + merge_transitions() + { + typename ls_map::iterator i; + for (i = ls_.begin(); i != ls_.end(); ++i) + { + typename State::transitions_t::iterator t1; + for (t1 = i->second.successors.begin(); + t1 != i->second.successors.end(); ++t1) + { + bdd acc = t1->acceptance_conditions; + const state_explicit* dest = t1->dest; + + // Find another transition with the same destination and + // acceptance conditions. + typename State::transitions_t::iterator t2 = t1; + ++t2; + while (t2 != i->second.successors.end()) + { + typename State::transitions_t::iterator t2copy = t2++; + if (t2copy->acceptance_conditions == acc && t2copy->dest == dest) + { + t1->condition |= t2copy->condition; + i->second.successors.erase(t2copy); + } + } + } + } + } + + /// Return the state_explicit for \a name, creating the state if + /// it does not exist. + State* add_state(const typename State::Label_t& name) + { + typename ls_map::iterator i = ls_.find(name); + if (i == ls_.end()) + { + State s(name); + ls_[name] = s; + sl_[&ls_[name]] = name; + + // The first state we add is the inititial state. + // It can also be overridden with set_init_state(). + if (!init_) + init_ = &ls_[name]; + + return &(ls_[name]); + } + return &(i->second); + } + + State* + set_init_state(const typename State::Label_t& state) + { + State* s = add_state(state); + init_ = s; + return s; + } + + // tgba interface + virtual ~explicit_graph() + { + typename ls_map::iterator i = ls_.begin(); + + while (i != ls_.end()) + { + typename State::Label_t s = i->first; + + // Do not erase the same state twice(Because of possible aliases). + if (sl_.erase(&(i->second))) + i->second.destroy(); + + ++i; + destroy_key dest; + dest.destroy(s); + } + } + + virtual State* get_init_state() const + { + if (!init_) + const_cast*>(this)->add_default_init(); + + return init_; + } + + virtual tgba_explicit_succ_iterator* + succ_iter(const spot::state* state, + const spot::state* global_state = 0, + const tgba* global_automaton = 0) const + { + const State* s = down_cast(state); + assert(s); + + (void) global_state; + (void) global_automaton; + + return + new tgba_explicit_succ_iterator(s, + this + ->all_acceptance_conditions()); + } + + //no need? + virtual std::string format_state(const spot::state* state) const + { + const State* se = down_cast(state); + assert(se); + typename sl_map::const_iterator i = sl_.find(se); + assert(i != sl_.end()); + return State::to_string(i->second); + } + + /// old implementation in tgba_explicit_string + /// Create an alias for a state. Any reference to \a alias_name + /// will act as a reference to \a real_name. + void add_state_alias(const typename State::Label_t& alias, + const typename State::Label_t& real) + { + ls_[alias] = *(add_state(real)); + } + + protected: + + ls_map ls_; + sl_map sl_; + State* init_; + + bdd_dict* dict_; + }; + + template + class tgba_explicit: public explicit_graph + { + protected: + typedef typename State::transition transition; + public: + typedef State state; + + tgba_explicit(bdd_dict* dict): + explicit_graph(dict), + all_acceptance_conditions_(bddfalse), + all_acceptance_conditions_computed_(false), + neg_acceptance_conditions_(bddtrue) + { + } + + /// \brief Copy the acceptance conditions of a tgba. + /// + /// If used, this function should be called before creating any + /// transition. + void copy_acceptance_conditions_of(const tgba *a) + { + assert(neg_acceptance_conditions_ == bddtrue); + assert(all_acceptance_conditions_computed_ == false); + bdd f = a->neg_acceptance_conditions(); + this->dict_->register_acceptance_variables(f, this); + neg_acceptance_conditions_ = f; + } + + /// The acceptance conditions. + void set_acceptance_conditions(bdd acc) + { + assert(neg_acceptance_conditions_ == bddtrue); + assert(all_acceptance_conditions_computed_ == false); + + this->dict_->register_acceptance_variables(bdd_support(acc), this); + neg_acceptance_conditions_ = compute_neg_acceptance_conditions(acc); + all_acceptance_conditions_computed_ = true; + all_acceptance_conditions_ = acc; + } + + void add_acceptance_condition(transition* t, const ltl::formula* f) + { + bdd c = get_acceptance_condition(f); + t->acceptance_conditions |= c; + } + + /// This assumes that all acceptance conditions in \a f are known from + /// dict. + void add_acceptance_conditions(transition* t, bdd f) + { + bdd sup = bdd_support(f); + this->dict_->register_acceptance_variables(sup, this); + while (sup != bddtrue) + { + neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup)); + sup = bdd_high(sup); + } + t->acceptance_conditions |= f; + } + + /// tgba interface + virtual ~tgba_explicit() + { + this->dict_->unregister_all_my_variables(this); + // These have already been destroyed by subclasses. + // Prevent destroying by tgba::~tgba. + this->last_support_conditions_input_ = 0; + this->last_support_variables_input_ = 0; + + } + + virtual bdd all_acceptance_conditions() const + { + if (!all_acceptance_conditions_computed_) + { + all_acceptance_conditions_ = + compute_all_acceptance_conditions(neg_acceptance_conditions_); + all_acceptance_conditions_computed_ = true; + } + return all_acceptance_conditions_; + } + + virtual bdd_dict* get_dict() const + { + return this->dict_; + } + + virtual bdd neg_acceptance_conditions() const + { + return neg_acceptance_conditions_; + } + void declare_acceptance_condition(const ltl::formula* f) { - int v = dict_->register_acceptance_variable(f, this); + int v = this->dict_->register_acceptance_variable(f, this); f->destroy(); bdd neg = bdd_nithvar(v); neg_acceptance_conditions_ &= neg; // Append neg to all acceptance conditions. - typename ns_map::iterator i; - for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) + typename explicit_graph::ls_map::iterator i; + for (i = this->ls_.begin(); i != this->ls_.end(); ++i) { - state_explicit::transitions_t::iterator i2; - for (i2 = i->second->successors.begin(); - i2 != i->second->successors.end(); ++i2) + typename State::transitions_t::iterator i2; + for (i2 = i->second.successors.begin(); + i2 != i->second.successors.end(); ++i2) i2->acceptance_conditions &= neg; } all_acceptance_conditions_computed_ = false; } + protected: - void - merge_transitions() + bdd get_acceptance_condition(const ltl::formula* f) { - typename ns_map::iterator i; - for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i) - { - state_explicit::transitions_t::iterator t1; - for (t1 = i->second->successors.begin(); - t1 != i->second->successors.end(); ++t1) - { - bdd acc = t1->acceptance_conditions; - const state* dest = t1->dest; - - // Find another transition with the same destination and - // acceptance conditions. - state_explicit::transitions_t::iterator t2 = t1; - ++t2; - while (t2 != i->second->successors.end()) - { - state_explicit::transitions_t::iterator t2copy = t2++; - if (t2copy->acceptance_conditions == acc - && t2copy->dest == dest) - { - t1->condition |= t2copy->condition; - i->second->successors.erase(t2copy); - } - } - } - } + bdd_dict::fv_map::iterator i = this->dict_->acc_map.find(f); + assert(this->has_acceptance_condition(f)); + f->destroy(); + bdd v = bdd_ithvar(i->second); + v &= bdd_exist(neg_acceptance_conditions_, v); + return v; } - - virtual - ~tgba_explicit_labelled() + virtual bdd compute_support_conditions(const spot::state* in) const { - // These have already been destroyed by subclasses. - // Prevent destroying by tgba::~tgba. - last_support_conditions_input_ = 0; - last_support_variables_input_ = 0; + const State* s = down_cast(in); + assert(s); + const typename State::transitions_t& st = s->successors; + + bdd res = bddfalse; + + typename State::transitions_t::const_iterator i; + for (i = st.begin(); i != st.end(); ++i) + res |= i->condition; + + return res; } - }; - -#ifndef SWIG - class tgba_explicit_string: - public tgba_explicit_labelled - { - public: - tgba_explicit_string(bdd_dict* dict): - tgba_explicit_labelled(dict) - {}; - virtual ~tgba_explicit_string(); - virtual state* add_default_init(); - virtual std::string format_state(const spot::state* s) const; - - /// Create an alias for a state. Any reference to \a alias_name - /// will act as a reference to \a real_name. - virtual - void add_state_alias(const std::string& alias_name, - const std::string& real_name) + virtual bdd compute_support_variables(const spot::state* in) const { - name_state_map_[alias_name] = add_state(real_name); + const State* s = down_cast(in); + assert(s); + const typename State::transitions_t& st = s->successors; + + bdd res = bddtrue; + + typename State::transitions_t::const_iterator i; + for (i = st.begin(); i != st.end(); ++i) + res &= bdd_support(i->condition); + + return res; } - }; -#else - class tgba_explicit_string: public tgba - { - }; -#endif -#ifndef SWIG - class tgba_explicit_formula: - public tgba_explicit_labelled - { - public: - tgba_explicit_formula(bdd_dict* dict): - tgba_explicit_labelled(dict) - {}; - virtual ~tgba_explicit_formula(); - virtual state* add_default_init(); - virtual std::string format_state(const spot::state* s) const; - }; -#else - class tgba_explicit_formula: public tgba - { - }; -#endif + mutable bdd all_acceptance_conditions_; + mutable bool all_acceptance_conditions_computed_; + bdd neg_acceptance_conditions_; -#ifndef SWIG - class tgba_explicit_number: - public tgba_explicit_labelled > - { - public: - tgba_explicit_number(bdd_dict* dict): - tgba_explicit_labelled >(dict) - {}; - virtual ~tgba_explicit_number(); - virtual state* add_default_init(); - virtual std::string format_state(const spot::state* s) const; + private: + // Disallow copy. + tgba_explicit(const tgba_explicit& other); + tgba_explicit& operator=(const tgba_explicit& other); }; -#else - class tgba_explicit_number: public tgba - { - }; -#endif + + + typedef tgba_explicit tgba_explicit_string; + typedef tgba_explicit tgba_explicit_formula; + typedef tgba_explicit tgba_explicit_number; } #endif // SPOT_TGBA_TGBAEXPLICIT_HH diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc index a014302ed..4ef9b6894 100644 --- a/src/tgba/tgbareduc.cc +++ b/src/tgba/tgbareduc.cc @@ -148,15 +148,15 @@ namespace spot } } - tgba_explicit::transition* + tgba_explicit_string::transition* tgba_reduc::create_transition(const spot::state* source, const spot::state* dest) { const std::string ss = aut_->format_state(source); const std::string sd = aut_->format_state(dest); - tgba_explicit::state* s = tgba_explicit_string::add_state(ss); - tgba_explicit::state* d = tgba_explicit_string::add_state(sd); + state_explicit_string* s = tgba_explicit_string::add_state(ss); + state_explicit_string* d = tgba_explicit_string::add_state(sd); transition t; t.dest = d; @@ -175,7 +175,7 @@ namespace spot t.condition = bddtrue; t.acceptance_conditions = bddfalse; - state_explicit::transitions_t::iterator is + state_explicit_string::transitions_t::iterator is = s->successors.insert(s->successors.end(), t); return &*is; } @@ -190,10 +190,10 @@ namespace spot bdd cond_simul; bdd acc_simul; std::list ltmp; - const tgba_explicit::state* s1 = - name_state_map_[tgba_explicit_string::format_state(s)]; - const tgba_explicit::state* s2 = - name_state_map_[tgba_explicit_string::format_state(simul)]; + const state_explicit_string* s1 = + &(ls_[tgba_explicit_string::format_state(s)]); + const state_explicit_string* s2 = + &(ls_[tgba_explicit_string::format_state(simul)]); sp_map::iterator i = state_predecessor_map_.find(s1); if (i == state_predecessor_map_.end()) // 0 predecessor @@ -205,7 +205,7 @@ namespace spot { // We check if simul belong to the successor of p, // as s belong too. - for (state_explicit::transitions_t::iterator + for (state_explicit_string::transitions_t::iterator j = (*p)->successors.begin(); j != (*p)->successors.end(); ++j) if (j->dest == s2) // simul belong to the successor of p. @@ -221,7 +221,7 @@ namespace spot continue; // for all successor of p, a predecessor of s and simul. - for (state_explicit::transitions_t::iterator + for (state_explicit_string::transitions_t::iterator j = (*p)->successors.begin(); j != (*p)->successors.end(); ++j) { @@ -233,7 +233,7 @@ namespace spot ((!j->acceptance_conditions) | acc_simul) == bddtrue)) { // We can redirect transition leading to s on simul. - j->dest = const_cast(s2); + j->dest = const_cast(s2); // We memorize that we have to remove p // of the predecessor of s. @@ -273,19 +273,20 @@ namespace spot // merge_state => NO PREDECESSOR. But it can be have some // predecessor in state_predecessor_map_. - ns_map::iterator k = - name_state_map_.find(tgba_explicit_string::format_state(s)); - if (k == name_state_map_.end()) // 0 predecessor + ls_map::iterator k = + ls_.find(tgba_explicit_string::format_state(s)); + if (k == ls_.end()) // 0 predecessor return; - tgba_explicit::state* st = - name_state_map_[tgba_explicit_string::format_state(s)]; + state_explicit_string* st = + &(ls_[tgba_explicit_string::format_state(s)]); // for all successor q of s, we remove s of the predecessor of q. // Note that the initial node can't be removed. - for (state_explicit::transitions_t::iterator j = + for (state_explicit_string::transitions_t::iterator j = st->successors.begin(); j != st->successors.end(); ++j) - this->remove_predecessor_state(j->dest, st); + this->remove_predecessor_state(down_cast + (j->dest), st); sp_map::iterator i = state_predecessor_map_.find(st); @@ -297,7 +298,7 @@ namespace spot p != (i->second)->end(); ++p) { // for all transition of p, a predecessor of s. - for (state_explicit::transitions_t::iterator + for (state_explicit_string::transitions_t::iterator j = (*p)->successors.begin(); j != (*p)->successors.end();) { @@ -321,11 +322,11 @@ namespace spot void tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2) { - const tgba_explicit::state* s1 = - name_state_map_[tgba_explicit_string::format_state(sim1)]; - const tgba_explicit::state* s2 = - name_state_map_[tgba_explicit_string::format_state(sim2)]; - const tgba_explicit::state* stmp = s1; + const state_explicit_string* s1 = + &(ls_[tgba_explicit_string::format_state(sim1)]); + const state_explicit_string* s2 = + &(ls_[tgba_explicit_string::format_state(sim2)]); + const state_explicit_string* stmp = s1; const spot::state* simtmp = sim1; // if sim1 is the init state, we remove sim2. @@ -354,7 +355,7 @@ namespace spot p != (i->second)->end(); ++p) { // for all successor of p, a predecessor of s1. - for (state_explicit::transitions_t::iterator + for (state_explicit_string::transitions_t::iterator j = (*p)->successors.begin(); j != (*p)->successors.end(); ++j) { @@ -362,7 +363,7 @@ namespace spot if (j->dest == s1) { // ... make it s2. - j->dest = const_cast(s2); + j->dest = const_cast(s2); } } } @@ -373,7 +374,7 @@ namespace spot // leaving s1 (possible when the simulation is delayed). Since s2 // simulates s1, s2 has some labels that imply these of s1, so we // can put the acceptance conditions on its arcs. - for (state_explicit::transitions_t::const_iterator + for (state_explicit_string::transitions_t::const_iterator j = s1->successors.begin(); j != s1->successors.end(); ++j) { @@ -381,7 +382,7 @@ namespace spot t.dest = j->dest; t.condition = j->condition; t.acceptance_conditions = j->acceptance_conditions; - const_cast(s2)->successors.push_back(t); + const_cast(s2)->successors.push_back(t); } // We remove all the predecessor of s1. diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh index a07963a56..dd53be3ec 100644 --- a/src/tgba/tgbareduc.hh +++ b/src/tgba/tgbareduc.hh @@ -75,9 +75,9 @@ namespace spot void display_scc(std::ostream& os); protected: - typedef Sgi::hash_map*, - ptr_hash > sp_map; + ptr_hash > sp_map; sp_map state_predecessor_map_; // Interface of tgba_reachable_iterator_breadth_first diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc index 5001e1b67..417604b96 100644 --- a/src/tgbaalgos/cutscc.cc +++ b/src/tgbaalgos/cutscc.cc @@ -74,7 +74,7 @@ namespace spot { dst->destroy(); } - tgba_explicit::transition* t = + state_explicit_string::transition* t = sub_a->create_transition(cur_format, dst_format); sub_a->add_conditions(t, sit->current_condition()); sub_a-> diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index 16df587c1..96c4acb7d 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -57,7 +57,7 @@ namespace spot std::ostringstream out_name; out_name << "(#" << out << ") " << this->aut_->format_state(out_s); - tgba_explicit::transition* t = + state_explicit_string::transition* t = out_->create_transition(in_name.str(), out_name.str()); out_->add_conditions(t, si->current_condition()); out_->add_acceptance_conditions(t, si->current_acceptance_conditions()); @@ -69,7 +69,7 @@ namespace spot } // anonymous - tgba_explicit* + tgba_explicit_string* tgba_dupexp_bfs(const tgba* aut) { dupexp_iter di(aut); @@ -77,7 +77,7 @@ namespace spot return di.result(); } - tgba_explicit* + tgba_explicit_string* tgba_dupexp_dfs(const tgba* aut) { dupexp_iter di(aut); diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index 5dabe35fd..c5680d004 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -29,11 +29,11 @@ namespace spot /// \brief Build an explicit automata from all states of \a aut, /// numbering states in bread first order as they are processed. /// \ingroup tgba_misc - tgba_explicit* tgba_dupexp_bfs(const tgba* aut); + tgba_explicit_string* tgba_dupexp_bfs(const tgba* aut); /// \brief Build an explicit automata from all states of \a aut, /// numbering states in depth first order as they are processed. /// \ingroup tgba_misc - tgba_explicit* tgba_dupexp_dfs(const tgba* aut); + tgba_explicit_string* tgba_dupexp_dfs(const tgba* aut); } #endif // SPOT_TGBAALGOS_DUPEXP_HH diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 008526d4c..0f0017831 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -302,12 +302,12 @@ namespace spot const state* s = a->get_init_state(); int number = 1; - tgba_explicit::state* source; - tgba_explicit::state* dest; + state_explicit_string* source; + state_explicit_string* dest; const tgba_run::steps* l; bdd seen_acc = bddfalse; - typedef Sgi::hash_map state_map; state_map seen; @@ -380,7 +380,8 @@ namespace spot else dest = its->second; - tgba_explicit::transition* t = res->create_transition(source, dest); + state_explicit_string::transition* t = + res->create_transition(source, dest); res->add_conditions(t, label); res->add_acceptance_conditions(t, acc); source = dest; diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 8ac292405..56e66a1b2 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -198,7 +198,7 @@ namespace spot void conj_bdd_to_acc(tgba_explicit_formula* a, bdd b, - tgba_explicit::transition* t) + state_explicit_formula::transition* t) { assert(b != bddfalse); while (b != bddtrue) @@ -692,7 +692,7 @@ namespace spot } - tgba_explicit* + tgba_explicit_formula* ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, @@ -945,7 +945,7 @@ namespace spot } if (!a->has_state(constant::true_instance())) formulae_to_translate.insert(constant::true_instance()); - tgba_explicit::transition* t = + state_explicit_formula::transition* t = a->create_transition(now, constant::true_instance()); a->add_condition(t, d.bdd_to_formula(cond_for_true)); } @@ -969,7 +969,7 @@ namespace spot bdd cond = j->second - cond_for_true; if (cond == bddfalse) // Skip false transitions. continue; - tgba_explicit::transition* t = + state_explicit_formula::transition* t = a->create_transition(now, dest); a->add_condition(t, d.bdd_to_formula(cond)); d.conj_bdd_to_acc(a, j->first, t); diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 61d657816..4c32a70a7 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -122,12 +122,13 @@ namespace spot /// \endverbatim /// /// \return A spot::tgba_explicit that recognizes the language of \a f. - tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, - bool exprop = false, bool symb_merge = true, - bool branching_postponement = false, - bool fair_loop_approx = false, - const ltl::atomic_prop_set* unobs = 0, - int reduce_ltl = ltl::Reduce_None); + tgba_explicit_formula* + ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, + bool exprop = false, bool symb_merge = true, + bool branching_postponement = false, + bool fair_loop_approx = false, + const ltl::atomic_prop_set* unobs = 0, + int reduce_ltl = ltl::Reduce_None); } #endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index a6a1b3f41..e74a944c9 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -131,7 +131,7 @@ namespace spot state_num[*hit] = num; ++num; } - typedef tgba_explicit_number::transition trs; + typedef state_explicit_number::transition trs; tgba_explicit_number* res = new tgba_explicit_number(a->get_dict()); // For each transition in the initial automaton, add the corresponding // transition in res. diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 84124bb28..a93bb487f 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -89,7 +89,7 @@ namespace spot // Add that transition. power_set::const_iterator i = seen.find(dest); int dest_num; - tgba_explicit::transition* t; + state_explicit_number::transition* t; if (i != seen.end()) { dest_num = i->second; diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 5c258a98e..08e86afd4 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -53,8 +53,9 @@ namespace spot } void - random_labels(tgba_explicit* aut, - tgba_explicit::state* src, const tgba_explicit::state* dest, + random_labels(tgba_explicit_string* aut, + state_explicit_string* src, + const state_explicit_string* dest, int* props, int props_n, float t, const std::list& accs, float a) { @@ -84,7 +85,7 @@ namespace spot if (drand() < a) ac |= *i; - tgba_explicit::transition* u = aut->create_transition(src, dest); + state_explicit_string::transition* u = aut->create_transition(src, dest); aut->add_conditions(u, p); aut->add_acceptance_conditions(u, ac); } @@ -107,7 +108,7 @@ namespace spot i != ap->end(); ++i) props[pi++] = dict->register_proposition(*i, res); - std::vector states(n); + std::vector states(n); // Indirect access to state[] to help random selection of successors. std::vector state_randomizer(n); @@ -153,7 +154,7 @@ namespace spot while (!nodes_to_process.empty()) { - tgba_explicit::state* src = states[*nodes_to_process.begin()]; + state_explicit_string* src = states[*nodes_to_process.begin()]; nodes_to_process.erase(nodes_to_process.begin()); // Choose a random number of successors (at least one), using @@ -195,7 +196,7 @@ namespace spot state_randomizer[index] = state_randomizer[possibilities]; state_randomizer[possibilities] = x; - tgba_explicit::state* dest = states[x]; + state_explicit_string* dest = states[x]; random_labels(res, src, dest, props, props_n, t, accs, a); diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 55f43ae2f..8b64aab99 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -30,7 +30,7 @@ namespace spot namespace { static - tgba_explicit::transition* + state_explicit_string::transition* create_transition(const tgba* aut, tgba_explicit_string* out_aut, const state* in_s, int in, const state* out_s, int out) @@ -43,7 +43,7 @@ namespace spot } static - tgba_explicit::transition* + state_explicit_formula::transition* create_transition(const tgba* aut, tgba_explicit_formula* out_aut, const state* in_s, int, const state* out_s, int) { @@ -62,6 +62,8 @@ namespace spot class filter_iter: public tgba_reachable_iterator_depth_first { public: + typedef T output_t; + filter_iter(const tgba* a, const scc_map& sm, const std::vector& useless, @@ -94,7 +96,7 @@ namespace spot const state* out_s, int out, const tgba_succ_iterator* si) { - tgba_explicit::transition* t = + typename output_t::state::transition* t = create_transition(this->aut_, out_, in_s, in, out_s, out); out_->add_conditions(t, si->current_condition()); diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 93a3bca23..2956bbb48 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -105,7 +105,7 @@ lines: line line: strident ',' strident ',' condition ',' acc_list ';' { - spot::tgba_explicit::transition* t + spot::state_explicit_string::transition* t = result->create_transition(*$1, *$3); if ($5) { diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 2594fb75a..2c68e7ea9 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -35,6 +35,7 @@ check_PROGRAMS = \ bddprod \ complement \ explicit \ + explicit2 \ expldot \ explprod \ intvcomp \ @@ -53,6 +54,7 @@ bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT complement_SOURCES = complementation.cc explicit_SOURCES = explicit.cc +explicit2_SOURCES = explicit2.cc expldot_SOURCES = powerset.cc expldot_CXXFLAGS = -DDOTTY explprod_SOURCES = explprod.cc diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 05dfaa24d..3217af462 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -131,7 +131,7 @@ int main(int argc, char* argv[]) { spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; - spot::tgba_explicit* a = spot::tgba_parse(file, pel, dict, env); + spot::tgba_explicit_string* a = spot::tgba_parse(file, pel, dict, env); if (spot::format_tgba_parse_errors(std::cerr, file, pel)) return 2; diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc index 4013b4301..b30256303 100644 --- a/src/tgbatest/explicit.cc +++ b/src/tgbatest/explicit.cc @@ -37,7 +37,7 @@ main() spot::ltl::default_environment::instance(); spot::tgba_explicit_string* a = new spot::tgba_explicit_string(dict); - typedef spot::tgba_explicit::transition trans; + typedef spot::state_explicit_string::transition trans; trans* t1 = a->create_transition("state 0", "state 1"); trans* t2 = a->create_transition("state 1", "state 2"); diff --git a/src/tgbatest/explicit2.cc b/src/tgbatest/explicit2.cc new file mode 100644 index 000000000..cfc344ef2 --- /dev/null +++ b/src/tgbatest/explicit2.cc @@ -0,0 +1,126 @@ +// Copyright (C) 2012 Laboratoire de Recherche et Développement +// 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 +#include + +#include "ltlenv/defaultenv.hh" +#include "ltlast/allnodes.hh" + +#include "tgba/tgbaexplicit.hh" + +using namespace spot; + +void +create_tgba_explicit_string(bdd_dict* d) +{ + tgba_explicit* tgba = + new tgba_explicit(d); + state_explicit_string* s1 = tgba->add_state("toto"); + state_explicit_string* s2 = tgba->add_state("tata"); + state_explicit_string::transition* t = + tgba->create_transition(s1, s2); + (void) t; + + tgba_explicit_succ_iterator* it + = tgba->succ_iter(tgba->get_init_state()); + for (it->first(); !it->done(); it->next()) + { + state_explicit_string* se = it->current_state(); + std::cout << se->label() << std::endl; + se->destroy(); + } + delete it; + + delete tgba; +} + +void +create_tgba_explicit_number(bdd_dict* d) +{ + tgba_explicit* tgba = + new tgba_explicit(d); + + state_explicit_number* s1 = tgba->add_state(51); + state_explicit_number* s2 = tgba->add_state(69); + + state_explicit_number::transition* t = + tgba->create_transition(s1, s2); + (void) t; + + tgba_explicit_succ_iterator* it = + tgba->succ_iter(tgba->get_init_state()); + for (it->first(); !it->done(); it->next()) + { + state_explicit_number* s = it->current_state(); + std::cout << s->label() << std::endl; + s->destroy(); + } + + delete it; + delete tgba; +} + +void +create_tgba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e) +{ + tgba_explicit* tgba = + new tgba_explicit(d); + + state_explicit_formula* s1 = tgba->add_state(e.require("a")); + state_explicit_formula* s2 = tgba->add_state(e.require("b")); + + state_explicit_formula::transition* t = + tgba->create_transition(s1, s2); + (void) t; + + tgba_explicit_succ_iterator* it = + tgba->succ_iter(tgba->get_init_state()); + for (it->first(); !it->done(); it->next()) + { + state_explicit_formula* s = it->current_state(); + std::cout << s->label() << std::endl; + s->destroy(); + } + + delete it; + delete tgba; +} + +int +main(int argc, char** argv) +{ + (void) argc; + (void) argv; + + bdd_dict* d = new spot::bdd_dict(); + spot::ltl::default_environment& e = + spot::ltl::default_environment::instance(); + + create_tgba_explicit_string(d); + create_tgba_explicit_number(d); + create_tgba_explicit_formula(d, e); + + delete d; + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); +} diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc index 5b4b8d77c..abcd7acf8 100644 --- a/src/tgbatest/explprod.cc +++ b/src/tgbatest/explprod.cc @@ -49,11 +49,11 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel1; - spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env); + spot::tgba_explicit_string* a1 = spot::tgba_parse(argv[1], pel1, dict, env); if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1)) return 2; spot::tgba_parse_error_list pel2; - spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); + spot::tgba_explicit_string* a2 = spot::tgba_parse(argv[2], pel2, dict, env); if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2)) return 2; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 6fc076151..4e46c492f 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1058,7 +1058,7 @@ main(int argc, char** argv) } } - const spot::tgba_explicit* expl = 0; + const spot::tgba_explicit_string* expl = 0; switch (dupexp) { case NoneDup: diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc index 259f3a0e6..3b00174f1 100644 --- a/src/tgbatest/mixprod.cc +++ b/src/tgbatest/mixprod.cc @@ -57,7 +57,7 @@ main(int argc, char** argv) return 2; spot::tgba_parse_error_list pel2; - spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); + spot::tgba_explicit_string* a2 = spot::tgba_parse(argv[2], pel2, dict, env); if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2)) return 2; diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc index 46177b0eb..1b3d6536c 100644 --- a/src/tgbatest/powerset.cc +++ b/src/tgbatest/powerset.cc @@ -50,13 +50,13 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; - spot::tgba_explicit* a = spot::tgba_parse(argv[1], pel, dict, env); + spot::tgba_explicit_string* a = spot::tgba_parse(argv[1], pel, dict, env); if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel)) return 2; #ifndef DOTTY - spot::tgba_explicit* e = spot::tgba_powerset(a); + spot::tgba_explicit_number* e = spot::tgba_powerset(a); spot::tgba_save_reachable(std::cout, e); delete e; #else diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc index 27ed5b564..1935310b8 100644 --- a/src/tgbatest/tgbaread.cc +++ b/src/tgbatest/tgbaread.cc @@ -58,8 +58,8 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel; - spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], - pel, dict, env, env, debug); + spot::tgba_explicit_string* a = spot::tgba_parse(argv[filename_index], + pel, dict, env, env, debug); if (spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel)) return 2; diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc index f8a5ff599..b0d566d60 100644 --- a/src/tgbatest/tripprod.cc +++ b/src/tgbatest/tripprod.cc @@ -49,15 +49,15 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::tgba_parse_error_list pel1; - spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, dict, env); + spot::tgba_explicit_string* a1 = spot::tgba_parse(argv[1], pel1, dict, env); if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1)) return 2; spot::tgba_parse_error_list pel2; - spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, dict, env); + spot::tgba_explicit_string* a2 = spot::tgba_parse(argv[2], pel2, dict, env); if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2)) return 2; spot::tgba_parse_error_list pel3; - spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, dict, env); + spot::tgba_explicit_string* a3 = spot::tgba_parse(argv[3], pel3, dict, env); if (spot::format_tgba_parse_errors(std::cerr, argv[3], pel3)) return 2;