diff --git a/ChangeLog b/ChangeLog index 93699a3c2..4317f65eb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,10 +1,14 @@ 2003-07-07 Alexandre Duret-Lutz + First sketch of the GSPN wrapper objects. + * iface/gspn/gspn.cc, iface/gspn/gspn.hh: New files. + * iface/gspn/Makefile.am (libspotgspn_la_SOURCES): Add them. + * src/tgba/succiter.hh (current_state, current_conditions current_accepting_conditions): Mark as const. - * src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, - src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, - src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, + * src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, + src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, + src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: Likewise. diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am index cc63b1307..6b2a6803b 100644 --- a/iface/gspn/Makefile.am +++ b/iface/gspn/Makefile.am @@ -1,6 +1,8 @@ -AM_CPPFLAGS = -I$(top_srcdir)/src +AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) lib_LTLIBRARIES = libspotgspn.la libspotgspn_la_SOURCES = \ + gspn.hh \ + gspn.cc \ gspnlib.h diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc new file mode 100644 index 000000000..15717a7ec --- /dev/null +++ b/iface/gspn/gspn.cc @@ -0,0 +1,334 @@ +#include +#include +#include "gspnlib.h" +#include "gspn.hh" +#include "ltlvisit/destroy.hh" +#include "tgba/bddfactory.hh" + +namespace spot +{ + + // tgba_gspn_private_ + ////////////////////////////////////////////////////////////////////// + + struct tgba_gspn_private_ : public bdd_factory + { + int refs; // reference count + + tgba_bdd_dict dict; + typedef std::pair ab_pair; + typedef std::map prop_map; + prop_map prop_dict; + AtomicProp *all_indexes; + size_t index_count; + + tgba_gspn_private_(const gspn_environment& env) + : refs(0) + { + const gspn_environment::prop_map& p = env.get_prop_map(); + + for (gspn_environment::prop_map::const_iterator i = p.begin(); + i != p.end(); ++i) + { + int var = create_node(); + i->second->ref(); + dict.var_map[i->second] = var; + dict.var_formula_map[var] = i->second; + + AtomicProp index; + int err = prop_index(i->first.c_str(), &index); + if (err) + throw gspn_exeption(err); + AtomicPropKind kind; + err = prop_kind(index, &kind); + if (err) + throw gspn_exeption(err); + + prop_dict[index] = ab_pair(kind, ithvar(var)); + } + // If an exception occurs during the loop, dict will + // be cleaned and that will dereferenciate the formula + // it contains. No need to handle anything explicitely. + + index_count = prop_dict.size(); + all_indexes = new AtomicProp[index_count]; + + unsigned idx = 0; + for (prop_map::const_iterator i = prop_dict.begin(); + i != prop_dict.end(); ++i) + all_indexes[idx++] = i->first; + } + + bdd index_to_bdd(AtomicProp index) const + { + if (index == EVENT_TRUE) + return bddtrue; + prop_map::const_iterator i = prop_dict.find(index); + assert(i != prop_dict.end()); + return i->second.second; + } + }; + + // state_gspn + ////////////////////////////////////////////////////////////////////// + + class state_gspn: public state + { + public: + state_gspn(State s) + : state_(s) + { + } + + virtual + ~state_gspn() + { + } + + virtual int + compare(const state* other) const + { + const state_gspn* o = dynamic_cast(other); + assert(o); + return o->get_state() - get_state(); + } + + virtual state_gspn* clone() const + { + return new state_gspn(get_state()); + } + + State + get_state() const + { + return state_; + } + + private: + State state_; + }; // state_gspn + + + // tgba_succ_iterator_gspn + ////////////////////////////////////////////////////////////////////// + + class tgba_succ_iterator_gspn: public tgba_succ_iterator + { + public: + tgba_succ_iterator_gspn(bdd state_conds, State state, + tgba_gspn_private_* data) + : state_conds_(state_conds), + successors_(0), + size_(0), + current_(0), + data_(data) + { + AtomicProp want[] = { EVENT_TRUE }; + int res = succ(state, want, sizeof(want) / sizeof(*want), + &successors_, &size_); + if (res) + throw res; + assert(successors_); + // GSPN is expected to return a looping "dead" transition where + // there is no successor, + assert(size_> 0); + } + + virtual + ~tgba_succ_iterator_gspn() + { + succ_free(successors_); + } + + virtual void + first() + { + current_ = 0; + } + + virtual void + next() + { + assert(!done()); + ++current_; + } + + virtual bool + done() const + { + return current_ >= size_; + } + + virtual state* + current_state() const + { + return new state_gspn(successors_[current_].s); + } + + virtual bdd + current_condition() const + { + bdd p = data_->index_to_bdd(successors_[current_].p); + return state_conds_ & p; + } + + virtual bdd + current_accepting_conditions() const + { + // There is no accepting conditions in GSPN systems. + return bddfalse; + } + private: + bdd state_conds_; /// All conditions known on STATE. + EventPropSucc* successors_; /// array of successors + size_t size_; /// size of successors_ + size_t current_; /// current position in successors_ + tgba_gspn_private_* data_; + }; // tgba_succ_iterator_gspn + + + // gspn_environment + ////////////////////////////////////////////////////////////////////// + + gspn_environment::gspn_environment() + { + } + + gspn_environment::~gspn_environment() + { + for (prop_map::iterator i = props_.begin(); i != props_.end(); ++i) + ltl::destroy(i->second); + } + + bool + gspn_environment::declare(const std::string& prop_str) + { + if (props_.find(prop_str) != props_.end()) + return false; + props_[prop_str] = ltl::atomic_prop::instance(prop_str, *this); + return true; + } + + ltl::formula* + gspn_environment::require(const std::string& prop_str) + { + prop_map::iterator i = props_.find(prop_str); + if (i == props_.end()) + return 0; + // It's an atomic_prop, so we do not have to use the clone() visitor. + return i->second->ref(); + } + + /// Get the name of the environment. + const std::string& + gspn_environment::name() + { + static std::string name("gspn environment"); + return name; + } + + const gspn_environment::prop_map& + gspn_environment::get_prop_map() const + { + return props_; + } + + + // tgba_gspn + ////////////////////////////////////////////////////////////////////// + + + tgba_gspn::tgba_gspn(const gspn_environment& env) + { + data_ = new tgba_gspn_private_(env); + } + + tgba_gspn::tgba_gspn(const tgba_gspn& other) + : tgba() + { + data_ = other.data_; + ++data_->refs; + } + + tgba_gspn::~tgba_gspn() + { + if (--data_->refs == 0) + delete data_; + } + + tgba_gspn& + tgba_gspn::operator=(const tgba_gspn& other) + { + if (&other == this) + return *this; + this->~tgba_gspn(); + new (this) tgba_gspn(other); + return *this; + } + + state* tgba_gspn::get_init_state() const + { + State s; + int err = initial_state(&s); + if (err) + throw gspn_exeption(err); + return new state_gspn(s); + } + + tgba_succ_iterator* + tgba_gspn::succ_iter(const state* state) const + { + const state_gspn* s = dynamic_cast(state); + assert(s); + + // Build the BDD of the conditions available on this state. + unsigned char* cube = 0; + int res = satisfy(s->get_state(), + data_->all_indexes, &cube, data_->index_count); + if (res) + throw res; + assert(cube); + bdd state_conds = bddtrue; + for (size_t i = 0; i < data_->index_count; ++i) + { + state_conds &= data_->index_to_bdd(cube[i]); + } + satisfy_free(cube); + + return new tgba_succ_iterator_gspn(state_conds, s->get_state(), data_); + } + + const tgba_bdd_dict& + tgba_gspn::get_dict() const + { + return data_->dict; + } + + std::string + tgba_gspn::format_state(const state* state) const + { + const state_gspn* s = dynamic_cast(state); + assert(s); + // FIXME: We ought to ask GSPN to format the state. + std::ostringstream os; + os << s->get_state(); + return os.str(); + } + + bdd + tgba_gspn::all_accepting_conditions() const + { + // There is no accepting conditions in GSPN systems. + return bddfalse; + } + + bdd + tgba_gspn::neg_accepting_conditions() const + { + // There is no accepting conditions in GSPN systems. + return bddtrue; + } + + + +} diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh new file mode 100644 index 000000000..c2e225079 --- /dev/null +++ b/iface/gspn/gspn.hh @@ -0,0 +1,81 @@ +#ifndef SPOT_IFACE_GSPN_HH +# define SPOT_IFACE_GSPN_HH + +// Try not to include gspnlib.h here, or it will polute the user's +// namespace with internal C symbols. + +# include +# include "tgba/tgba.hh" +# include "ltlast/atomic_prop.hh" +# include "ltlenv/environment.hh" + +namespace spot +{ + + /// An exeption used to forward GSPN errors. + class gspn_exeption + { + public: + gspn_exeption(int err) + : err(err) + { + } + + int + get_err() const + { + return err; + } + private: + int err; + }; + + + class gspn_environment : public ltl::environment + { + public: + gspn_environment(); + ~gspn_environment(); + + /// Declare an atomic proposition. Return false iff the + /// proposition was already declared. + bool declare(const std::string& prop_str); + + virtual ltl::formula* require(const std::string& prop_str); + + /// Get the name of the environment. + virtual const std::string& name(); + + typedef std::map prop_map; + + /// Get the map of atomic proposition known to this environment. + const prop_map& get_prop_map() const; + + private: + prop_map props_; + }; + + + /// Data private to tgba_gspn. + struct tgba_gspn_private_; + + class tgba_gspn: public tgba + { + public: + tgba_gspn(const gspn_environment& env); + tgba_gspn(const tgba_gspn& other); + tgba_gspn& operator=(const tgba_gspn& other); + virtual ~tgba_gspn(); + virtual state* get_init_state() const; + virtual tgba_succ_iterator* succ_iter(const state* state) const; + virtual const tgba_bdd_dict& get_dict() const; + virtual std::string format_state(const state* state) const; + virtual bdd all_accepting_conditions() const; + virtual bdd neg_accepting_conditions() const; + private: + tgba_gspn_private_* data_; + }; + +} + +#endif // SPOT_IFACE_GSPN_HH diff --git a/iface/gspn/gspnlib.h b/iface/gspn/gspnlib.h index 33e183ef1..62c7696ad 100644 --- a/iface/gspn/gspnlib.h +++ b/iface/gspn/gspnlib.h @@ -64,7 +64,7 @@ int initial_state (pState M0); NB : the vector "truth" is allocated in this function */ -int satisfy (const State s, const AtomicProp props [], +int satisfy (const State s, const AtomicProp props [], unsigned char ** truth, size_t props_size); /* free the "truth" vector allocated by satisfy @@ -89,7 +89,7 @@ int satisfy_free (unsigned char * truth); NB : "succ" vector is allocated in the function, use succ_free for memory release */ -int succ (const State s, +int succ (const State s, const AtomicProp enabled_events [], size_t enabled_events_size, EventPropSucc ** succ, size_t * succ_size);