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.

ChangeLog

@@ -1,10 +1,14 @@
 2003-07-07  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	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.
 

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

iface/gspn/gspn.cc

@@ -0,0 +1,334 @@
+#include <sstream>
+#include <map>
+#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<AtomicPropKind, bdd> ab_pair;
+    typedef std::map<AtomicProp, ab_pair> 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<const state_gspn*>(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<const state_gspn*>(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<const state_gspn*>(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;
+  }
+
+
+
+}

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 <string>
+# 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<const std::string, ltl::atomic_prop*> 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

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);