* src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant.

* src/tgba/tgbabddtranslateproxy.cc,
src/tgba/tgbabddtranslateproxy.hh: New files.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.

ChangeLog

+2003-05-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant.
+	* src/tgba/tgbabddtranslateproxy.cc,
+	src/tgba/tgbabddtranslateproxy.hh: New files.
+	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
+
 2003-05-27  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/tgba/bddprint.cc, src/tgba/bddprint.hh,
@@ -8,8 +15,8 @@
 	src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc:
 	Add Doxygen comments.
 
-	* src/tgba/bddfactory.hh, src/tgba/statebdd.hh, 
-	src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, 
+	* src/tgba/bddfactory.hh, src/tgba/statebdd.hh,
+	src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh,
 	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add
 	Doxygen comments.
 
@@ -18,7 +25,7 @@
 	* src/tgba/state.hh: Add Doxygen comments.
 	(state::compare): Take a state*, not a state&.
 	(state_ptr_less_than): New functor.
-	* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a 
+	* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
 	state&.
 	* src/tgba/statebdd.cc (state_bdd::compare): Likewise.
 	* src/tgba/succiter.hh: Add Doxygen comments.

src/tgba/Makefile.am

@@ -31,4 +31,6 @@ libtgba_la_SOURCES = \
   tgbabdddict.hh \
   tgbabddfactory.hh \
   tgbabddtranslatefactory.cc \
-  tgbabddtranslatefactory.hh
+  tgbabddtranslatefactory.hh \
+  tgbabddtranslateproxy.cc \
+  tgbabddtranslateproxy.hh

src/tgba/statebdd.hh

@@ -16,12 +16,19 @@ namespace spot
     }
 
     /// Return the BDD part of the state.
-    bdd 
+    bdd
     as_bdd() const
     {
       return state_;
     }
-    
+
+    /// Return the BDD part of the state.
+    bdd&
+    as_bdd()
+    {
+      return state_;
+    }
+
     virtual int compare(const state* other) const;
 
   protected:

src/tgba/succiterconcrete.hh

@@ -12,7 +12,7 @@ namespace spot
   {
   public:
     /// \brief Build a spot::tgba_succ_iterator_concrete.
-    /// 
+    ///
     /// \param successors The set of successors with ingoing conditions
     /// and promises, represented as a BDD.  The job of this iterator
     /// will be to enumerate the satisfactions of that BDD and split

src/tgba/tgba.hh

@@ -77,7 +77,7 @@ namespace spot
     /// This formating is the responsability of the automata
     /// who owns the state.
     virtual std::string format_state(const state* state) const = 0;
-  }; 
+  };
 
 }
 

src/tgba/tgbabddcoredata.hh

@@ -15,7 +15,7 @@ namespace spot
     /// \li "Next" variables, that encode the destination state
     /// \li atomic propositions, which are things to verify before going on
     ///     to the next state
-    /// \li promises: \c a \c U \c b, or \c F \cb, both imply that \c b
+    /// \li promises: \c a \c U \c b, or \c F \c b, both imply that \c b
     ///     should be verified eventually.  We encode this with \c Prom[b],
     ///     and check that promises are fullfilled in the emptyness check.
     bdd relation;

src/tgba/tgbabddtranslateproxy.cc

+#include "tgbabddtranslateproxy.hh"
+#include "bddprint.hh"
+
+namespace spot
+{
+
+  // tgba_bdd_translate_proxy_succ_iterator
+  // --------------------------------------
+  
+  tgba_bdd_translate_proxy_succ_iterator::
+  tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator_concrete* it,
+					 bddPair* rewrite)
+    : iter_(it), rewrite_(rewrite)
+  {
+  }
+  
+  void 
+  tgba_bdd_translate_proxy_succ_iterator::first()
+  {
+    iter_->first();
+  }
+  
+  void 
+  tgba_bdd_translate_proxy_succ_iterator::next()
+  {
+    iter_->next();
+  }
+  
+  bool 
+  tgba_bdd_translate_proxy_succ_iterator::done()
+  {
+    return iter_->done();
+  }
+
+  state_bdd* 
+  tgba_bdd_translate_proxy_succ_iterator::current_state()
+  {
+    state_bdd* s = iter_->current_state();
+    s->as_bdd() = bdd_replace(s->as_bdd(), rewrite_);
+    return s;
+  }
+
+  bdd 
+  tgba_bdd_translate_proxy_succ_iterator::current_condition()
+  {
+    return bdd_replace(iter_->current_condition(), rewrite_);
+  }
+
+  bdd 
+  tgba_bdd_translate_proxy_succ_iterator::current_promise()
+  {
+    return bdd_replace(iter_->current_promise(), rewrite_);
+  }
+
+
+  // tgba_bdd_translate_proxy
+  // ------------------------
+
+  tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from, 
+						     const tgba_bdd_dict& to)
+    : from_(from), to_(to)
+  {
+    const tgba_bdd_dict& f = from.get_dict();
+    rewrite_to_ = bdd_newpair();
+    rewrite_from_ = bdd_newpair();
+
+    tgba_bdd_dict::fv_map::const_iterator i_from;
+    tgba_bdd_dict::fv_map::const_iterator i_to;
+
+    for (i_from = f.now_map.begin(); i_from != f.now_map.end(); ++i_from)
+      {
+	i_to = to_.now_map.find(i_from->first);
+	assert(i_to != to_.now_map.end());
+	bdd_setpair(rewrite_to_, i_from->second, i_to->second);
+	bdd_setpair(rewrite_to_, i_from->second + 1, i_to->second + 1);
+	bdd_setpair(rewrite_from_, i_to->second, i_from->second);
+	bdd_setpair(rewrite_from_, i_to->second + 1, i_from->second + 1);
+      }
+    for (i_from = f.var_map.begin(); i_from != f.var_map.end(); ++i_from)
+      {
+	i_to = to_.var_map.find(i_from->first);
+	assert(i_to != to_.var_map.end());
+	bdd_setpair(rewrite_to_, i_from->second, i_to->second);
+	bdd_setpair(rewrite_from_, i_to->second, i_from->second);
+      }
+    for (i_from = f.prom_map.begin(); i_from != f.prom_map.end(); ++i_from)
+      {
+	i_to = to_.prom_map.find(i_from->first);
+	assert(i_to != to_.prom_map.end());
+	bdd_setpair(rewrite_to_, i_from->second, i_to->second);
+	bdd_setpair(rewrite_from_, i_to->second, i_from->second);
+      }
+  }
+
+  tgba_bdd_translate_proxy::~tgba_bdd_translate_proxy()
+  {
+    bdd_freepair(rewrite_from_);
+    bdd_freepair(rewrite_to_);
+  }
+  
+  state_bdd* 
+  tgba_bdd_translate_proxy::get_init_state() const
+  {
+    state_bdd* s = dynamic_cast<state_bdd*>(from_.get_init_state());
+    assert(s);
+    s->as_bdd() = bdd_replace(s->as_bdd(), rewrite_to_);
+    return s;
+  }
+
+  tgba_bdd_translate_proxy_succ_iterator* 
+  tgba_bdd_translate_proxy::succ_iter(const state* state) const
+  {
+    const state_bdd* s = dynamic_cast<const state_bdd*>(state);
+    assert(s);
+    state_bdd s2(bdd_replace(s->as_bdd(), rewrite_from_));    
+    tgba_succ_iterator_concrete* it = 
+      dynamic_cast<tgba_succ_iterator_concrete*>(from_.succ_iter(&s2));
+    assert(it);
+    return new tgba_bdd_translate_proxy_succ_iterator(it, rewrite_to_);
+  }
+
+  const tgba_bdd_dict& 
+  tgba_bdd_translate_proxy::get_dict() const
+  {
+    return to_;
+  }
+  
+  std::string
+  tgba_bdd_translate_proxy::format_state(const state* state) const
+  {
+    const state_bdd* s = dynamic_cast<const state_bdd*>(state);
+    assert(s);
+    return bdd_format_set(to_, s->as_bdd());
+  }
+
+
+}

src/tgba/tgbabddtranslateproxy.hh

+#ifndef SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH
+# define SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH
+
+#include "tgba.hh"
+#include "succiterconcrete.hh"
+
+namespace spot
+{
+  /// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber 
+  /// BDD variables on the fly.
+  class tgba_bdd_translate_proxy_succ_iterator: public tgba_succ_iterator
+  {
+  public:
+    tgba_bdd_translate_proxy_succ_iterator
+    (tgba_succ_iterator_concrete* it, bddPair* rewrite);
+
+    // iteration
+    void first();
+    void next();
+    bool done();
+
+    // inspection
+    state_bdd* current_state();
+    bdd current_condition();
+    bdd current_promise();
+  protected:
+    tgba_succ_iterator_concrete* iter_;
+    bddPair* rewrite_;
+  };
+
+
+  /// \brief Proxy for a spot::tgba_bdd_concrete that renumber BDD variables
+  /// on the fly.
+  class tgba_bdd_translate_proxy: public tgba
+  {
+  public:
+    /// \brief Construcor.
+    /// \param from The spot::tgba to masquerade.
+    /// \param to The new dictionary to use.
+    tgba_bdd_translate_proxy(const tgba& from, 
+			     const tgba_bdd_dict& to);
+
+    virtual ~tgba_bdd_translate_proxy();
+
+    virtual state_bdd* get_init_state() const;
+
+    virtual tgba_bdd_translate_proxy_succ_iterator* 
+    succ_iter(const state* state) const;
+
+    virtual const tgba_bdd_dict& get_dict() const;
+
+    virtual std::string
+    tgba_bdd_translate_proxy::format_state(const state* state) const;
+    
+  private:
+    const tgba& from_;		///< The spot::tgba to masquerade.
+    tgba_bdd_dict to_;		///< The new dictionar to use.
+    bddPair* rewrite_to_;	///< The rewriting pair for from->to.
+    bddPair* rewrite_from_;	///< The rewriting pair for to->from.
+  };
+  
+}
+
+#endif // SPOT_TGBA_TGBABDDTRANSLATEPROXY_HH