Initial code for TGBA (Transition Generalized B�chi Automata).

Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
a LTL-to-TGBA translator using Couvreur's algorithm.

* src/Makefile.am (SUBDIRS): Add tgba.
(libspot_la_LIBADD): Add tgba/libtgba.la.
* src/tgba/Makefile.am, src/tgba/bddfactory.cc,
src/tgba/bddfactory.hh, src/tgba/dictunion.cc,
src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
src/tgba/succiterconcrete.hh, src/tgba/succlist.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbabddtranslatefactory.cc,
src/tgba/tgbabddtranslatefactory.hh: New files.

ChangeLog

@@ -1,3 +1,27 @@
+2003-05-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	Initial code for TGBA (Transition Generalized Büchi Automata).
+	Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba,
+	a LTL-to-TGBA translator using Couvreur's algorithm.
+
+	* src/Makefile.am (SUBDIRS): Add tgba.
+	(libspot_la_LIBADD): Add tgba/libtgba.la.
+	* src/tgba/Makefile.am, src/tgba/bddfactory.cc,
+	src/tgba/bddfactory.hh, src/tgba/dictunion.cc,
+	src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
+	src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
+	src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
+	src/tgba/succiterconcrete.hh, src/tgba/succlist.hh,
+	src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
+	src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
+	src/tgba/tgbabddconcretefactory.hh,
+	src/tgba/tgbabddconcreteproduct.cc,
+	src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
+	src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.cc,
+	src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh,
+	src/tgba/tgbabddtranslatefactory.cc,
+	src/tgba/tgbabddtranslatefactory.hh: New files.
+
 2003-05-23  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* m4/gccwarn.m4: Do not use -Winline, this is inappropriate

configure.ac

@@ -31,6 +31,7 @@ AC_CONFIG_FILES([
   src/ltltest/Makefile
   src/ltltest/defs
   src/ltlvisit/Makefile
+  src/tgba/Makefile
   src/misc/Makefile
   wrap/Makefile
 ])

src/Makefile.am

@@ -1,7 +1,7 @@
 AUTOMAKE_OPTIONS = subdir-objects
 
 # List directories in the order they must be built.
-SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse ltltest 
+SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse ltltest tgba
 
 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =
@@ -9,4 +9,5 @@ libspot_la_LIBADD =  \
   ltlenv/libltlenv.la \
   ltlparse/libltlparse.la \
   ltlvisit/libltlvisit.la \
-  ltlast/libltlast.la
+  ltlast/libltlast.la \
+  tgba/libtgba.la

src/tgba/.cvsignore

@@ -0,0 +1,6 @@
+.deps
+.libs
+*.lo
+*.la
+Makefile
+Makefile.in

src/tgba/Makefile.am

@@ -0,0 +1,31 @@
+AM_CPPFLAGS = -I$(srcdir)/..
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+noinst_LTLIBRARIES = libtgba.la
+libtgba_la_SOURCES = \
+  bddfactory.cc \
+  bddfactory.hh \
+  dictunion.cc \
+  dictunion.hh \
+  ltl2tgba.cc \
+  ltl2tgba.hh \
+  state.hh \
+  statebdd.cc \
+  statebdd.hh \
+  succiter.hh \
+  succiterconcrete.cc \
+  succiterconcrete.hh \
+  tgba.hh \
+  tgbabddconcrete.cc \
+  tgbabddconcrete.hh \
+  tgbabddconcretefactory.cc \
+  tgbabddconcretefactory.hh \
+  tgbabddconcreteproduct.cc \
+  tgbabddconcreteproduct.hh \
+  tgbabddcoredata.cc \
+  tgbabddcoredata.hh \
+  tgbabdddict.cc \
+  tgbabdddict.hh \
+  tgbabddfactory.hh \
+  tgbabddtranslatefactory.cc \
+  tgbabddtranslatefactory.hh

src/tgba/bddfactory.cc

@@ -0,0 +1,48 @@
+#include "bddfactory.hh"
+
+namespace spot
+{
+  bdd_factory::bdd_factory()
+    : varused(0)
+  {
+    initialize();
+  }
+  
+  int
+  bdd_factory::create_node()
+  {
+    return create_nodes(1);
+  }
+  
+  int
+  bdd_factory::create_pair()
+  {
+    return create_nodes(2);
+  }
+  
+  int
+  bdd_factory::create_nodes(int i)
+  {
+    int res = varused;
+    varused += i;
+    if (varnum < varused)
+      {
+        bdd_extvarnum(varused - varnum);
+        varnum = varused;
+      }
+    return res;
+  }
+
+  void
+  bdd_factory::initialize()
+  {
+    if (initialized)
+      return;
+    initialized = true;
+    bdd_init(50000, 5000);
+    bdd_setvarnum(varnum);
+  }  
+  
+  bool bdd_factory::initialized = false;
+  int bdd_factory::varnum = 2;
+}

src/tgba/bddfactory.hh

@@ -0,0 +1,33 @@
+#ifndef SPOT_TGBA_BDDFACTORY_HH
+# define SPOT_TGBA_BDDFACTORY_HH
+
+#include <bdd.h>
+
+namespace spot
+{
+
+  class bdd_factory
+  {
+  public:
+    bdd_factory();
+
+    int create_node();
+    int create_pair();
+  
+    static bdd
+    ithvar(int i)
+    {
+      return bdd_ithvar(i);
+    }
+  
+  protected:
+    static void initialize();
+    int create_nodes(int i);
+  
+    static bool initialized;
+    static int varnum;
+    int varused;
+  };
+}
+
+#endif // SPOT_TGBA_BDDFACTORY_HH

src/tgba/dictunion.cc

@@ -0,0 +1,75 @@
+#include <set>
+#include "dictunion.hh"
+#include <bdd.h>
+
+namespace spot
+{
+
+  tgba_bdd_dict
+  tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r)
+  {
+    tgba_bdd_dict res;
+  
+    std::set<const ltl::formula*> now;
+    std::set<const ltl::formula*> var;
+    std::set<const ltl::formula*> prom;
+  
+    tgba_bdd_dict::fv_map::const_iterator i;
+  
+    // Merge Now variables.
+    for (i = l.now_map.begin(); i != l.now_map.end(); ++i)
+      now.insert(i->first);
+    for (i = r.now_map.begin(); i != r.now_map.end(); ++i)
+      now.insert(i->first);
+  
+    // Merge atomic propositions.
+    for (i = l.var_map.begin(); i != l.var_map.end(); ++i)
+      var.insert(i->first);
+    for (i = r.var_map.begin(); i != r.var_map.end(); ++i)
+      var.insert(i->first);
+  
+    // Merge promises.
+    for (i = l.prom_map.begin(); i != l.prom_map.end(); ++i)
+      prom.insert(i->first);
+    for (i = r.prom_map.begin(); i != r.prom_map.end(); ++i)
+      prom.insert(i->first);
+  
+    // Ensure we have enough BDD variables.
+    int have = bdd_extvarnum(0);
+    int want = now.size() * 2 + var.size() + prom.size();
+    if (have < want)
+      bdd_setvarnum(want);
+  
+    // Fill in the "defragmented" union dictionary.
+  
+    // FIXME: Make some experiments with ordering of prom/var/now variables.
+    // Maybe there is one order that usually produces smaller BDDs?
+  
+    // Next BDD variable to use.
+    int v = 0;
+  
+    std::set<const ltl::formula*>::const_iterator f;
+    for (f = prom.begin(); f != prom.end(); ++f)
+      {
+        res.prom_map[*f] = v;
+        res.prom_formula_map[v] = *f;
+        ++v;
+      }
+    for (f = var.begin(); f != var.end(); ++f)
+      {
+        res.var_map[*f] = v;
+        res.var_formula_map[v] = *f;
+        ++v;
+      }
+    for (f = now.begin(); f != now.end(); ++f)
+      {
+        res.now_map[*f] = v;
+        res.now_formula_map[v] = *f;
+        v += 2;
+      }
+  
+    assert (v == want);
+    return res;
+  }
+
+}

src/tgba/dictunion.hh

@@ -0,0 +1,12 @@
+#ifndef SPOT_TGBA_DICTUNION_HH
+# define SPOT_TGBA_DICTUNION_HH
+
+#include "tgbabdddict.hh"
+
+namespace spot
+{
+  tgba_bdd_dict
+  tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r);
+}
+
+#endif // SPOT_TGBA_DICTUNION_HH

src/tgba/ltl2tgba.cc

@@ -0,0 +1,183 @@
+#include "ltlast/visitor.hh"
+#include "ltlast/allnodes.hh"
+#include "tgbabddconcretefactory.hh"
+
+#include "ltl2tgba.hh"
+// FIXME: Add ref to Couvreur's paper.
+
+namespace spot
+{
+  using namespace ltl;
+  class ltl_trad_visitor: public const_visitor
+  {
+  public:
+    ltl_trad_visitor(tgba_bdd_concrete_factory& fact)
+      : fact_(fact)
+    {
+    }
+
+    virtual
+    ~ltl_trad_visitor()
+    {
+    }
+
+    bdd
+    result()
+    {
+      return res_;
+    }
+
+    void
+    visit(const atomic_prop* node)
+    {
+      res_ = fact_.ithvar(fact_.create_atomic_prop(node));
+    }
+
+    void
+    visit(const constant* node)
+    {
+      switch (node->val())
+	{
+	case constant::True:
+	  res_ = bddtrue;
+	  return;
+	case constant::False:
+	  res_ = bddfalse;
+	  return;
+	}
+      /* Unreachable code.  */
+      assert(0);
+    }
+
+    void
+    visit(const unop* node)
+    {
+      switch (node->op())
+	{
+	case unop::F:
+	case unop::G:
+	  // FIXME: We can normalize on the fly, here.
+	  assert(!"unexpected operator, normalize first");
+	case unop::Not:
+	  res_ = bdd_not(recurse(node->child()));
+	  return;
+	case unop::X:
+	  // FIXME: Can be smarter on X(a U b) and X(a R b).
+	  int v = fact_.create_state(node->child());
+	  bdd now = fact_.ithvar(v);
+	  bdd next = fact_.ithvar(v + 1);
+	  fact_.add_relation(bdd_apply(now, recurse(node->child()),
+				       bddop_biimp));
+	  res_ = next;
+	  return;
+	}
+      /* Unreachable code.  */
+      assert(0);
+    }
+
+    void
+    visit(const binop* node)
+    {
+      bdd f1 = recurse(node->first());
+      bdd f2 = recurse(node->second());
+
+      switch (node->op())
+	{
+	case binop::Xor:
+	  res_ = bdd_apply(f1, f2, bddop_xor);
+	  return;
+	case binop::Implies:
+	  res_ = bdd_apply(f1, f2, bddop_imp);
+	  return;
+	case binop::Equiv:
+	  res_ = bdd_apply(f1, f2, bddop_biimp);
+	  return;
+	case binop::U:
+	  {
+	    int v = fact_.create_state(node);
+	    bdd now = fact_.ithvar(v);
+	    bdd next = fact_.ithvar(v + 1);
+
+	    bdd promise_f2 =
+	      fact_.ithvar(fact_.create_promise(node->second()));
+	    /*
+	       f1 U f2 <=> f2 | (f1 & X(f1 U f2))
+	       In other words:
+		   now <=> f2 | (f1 & next)
+
+		The rightmost conjunction, f1 & next, doesn't actually
+		encodes the fact that f2 should be fulfilled at some
+		point.  We use the `promise_f2' variable for this purpose.
+	    */
+	    fact_.add_relation(bdd_apply(now,
+					 f2 | (promise_f2 & f1 & next),
+					 bddop_biimp));
+	    res_ = now;
+	    return;
+	  }
+	case binop::R:
+	  {
+	    int v = fact_.create_state(node);
+	    bdd now = fact_.ithvar(v);
+	    bdd next = fact_.ithvar(v + 1);
+	    /*
+	       f1 R f2 <=> f2 & (f1 | X(f1 U f2))
+	       In other words:
+		   now <=> f2 & (f1 | next)
+	    */
+	    fact_.add_relation(bdd_apply(now, f2 & (f1 | next), bddop_biimp));
+	    res_ = now;
+	    return;
+	  }
+	}
+      /* Unreachable code.  */
+      assert(0);
+    }
+
+    void
+    visit(const multop* node)
+    {
+      int op = -1;
+      switch (node->op())
+	{
+	case multop::And:
+	  op = bddop_and;
+	  res_ = bddtrue;
+	  break;
+	case multop::Or:
+	  op = bddop_or;
+	  res_ = bddfalse;
+	  break;
+	}
+      assert(op != -1);
+      unsigned s = node->size();
+      for (unsigned n = 0; n < s; ++n)
+	{
+	  res_ = bdd_apply(res_, recurse(node->nth(n)), op);
+	}
+    }
+
+    bdd
+    recurse(const formula* f)
+    {
+      ltl_trad_visitor v(*this);
+      f->accept(v);
+      return v.result();
+    }
+
+  private:
+    bdd res_;
+    tgba_bdd_concrete_factory& fact_;
+  };
+
+  tgba_bdd_concrete
+  ltl_to_tgba(const formula* f)
+  {
+    tgba_bdd_concrete_factory fact;
+    ltl_trad_visitor v(fact);
+    f->accept(v);
+    tgba_bdd_concrete g(fact);
+    g.set_init_state(v.result());
+    return g;
+  }
+}

src/tgba/ltl2tgba.hh

@@ -0,0 +1,13 @@
+#ifndef SPOT_TGBA_LTL2TGBA_HH
+# define SPOT_TGBA_LTL2TGBA_HH
+
+#include "ltlast/formula.hh"
+#include "tgbabddconcrete.hh"
+
+namespace spot
+{
+  tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f);
+}
+
+#endif // SPOT_TGBA_LTL2TGBA_HH
+

src/tgba/state.hh

@@ -0,0 +1,25 @@
+#ifndef SPOT_TGBA_STATE_HH
+# define SPOT_TGBA_STATE_HH
+
+namespace spot
+{
+  class state
+  {
+  public:
+    // Compares two states (that come from the same automaton).
+    //
+    // This method returns an integer less than, equal to, or greater
+    // than zero if THIS is found, respectively, to be less than, equal
+    // to, or greater than OTHER according to some implicit total order.
+    //
+    // This method should not be called to compare state from
+    // different automata.
+    virtual int compare(const state& other) const = 0;
+
+    virtual ~state()
+    {
+    }
+  };
+}
+
+#endif // SPOT_TGBA_STATE_HH

src/tgba/statebdd.cc

@@ -0,0 +1,16 @@
+#include "statebdd.hh"
+#include <cassert>
+
+namespace spot
+{
+  int
+  state_bdd::compare(const state& other) const
+  {
+    // This method should not be called to compare states from different
+    // automata, and all states from the same automaton will use the same
+    // state class.
+    const state_bdd* o = dynamic_cast<const state_bdd*>(&other);
+    assert(o);
+    return o->as_bdd().id() - state_.id();
+  }
+}

src/tgba/statebdd.hh

@@ -0,0 +1,30 @@
+#ifndef SPOT_TGBA_STATEBDD_HH
+# define SPOT_TGBA_STATEBDD_HH
+
+#include <bdd.h>
+#include "state.hh"
+
+namespace spot
+{
+  class state_bdd: public state
+  {
+  public:
+    state_bdd(bdd s)
+      : state_(s)
+    {
+    }
+
+    bdd
+    as_bdd() const
+    {
+      return state_;
+    }
+
+    virtual int compare(const state& other) const;
+
+  protected:
+    bdd state_;
+  };
+}
+
+#endif // SPOT_TGBA_STATEBDD_HH

src/tgba/succiter.hh

@@ -0,0 +1,31 @@
+#ifndef SPOT_TGBA_SUCCITER_H
+# define SPOT_TGBA_SUCCITER_H
+
+#include "statebdd.hh"
+
+namespace spot
+{
+
+  class tgba_succ_iterator
+  {
+  public:
+    virtual 
+    ~tgba_succ_iterator() 
+    {
+    }
+    
+    // iteration
+    virtual void first() = 0;
+    virtual void next() = 0;
+    virtual bool done() = 0;
+    
+    // inspection
+    virtual state_bdd current_state() = 0;
+    virtual bdd current_condition() = 0;
+    virtual bdd current_promise() = 0;
+  };
+
+}
+
+
+#endif // SPOT_TGBA_SUCCITER_H

src/tgba/succiterconcrete.cc

@@ -0,0 +1,64 @@
+#include "succiterconcrete.hh"
+
+namespace spot
+{
+  tgba_succ_iterator_concrete::tgba_succ_iterator_concrete
+  (const tgba_bdd_core_data& d, bdd successors)
+    : data_(d), succ_set_(successors), next_succ_set_(successors),
+      current_(bddfalse)
+  {
+  }
+  
+  tgba_succ_iterator_concrete::~tgba_succ_iterator_concrete()
+  {
+  }
+  
+  void
+  tgba_succ_iterator_concrete::first()
+  {
+    next_succ_set_ = succ_set_;
+    if (!done())
+      next();
+  }
+  
+  void
+  tgba_succ_iterator_concrete::next()
+  {
+    assert(!done());
+  
+    // FIXME: Iterating on the successors this way (calling bdd_satone
+    // and NANDing out the result from the set) requires several descent
+    // of the BDD.  Maybe it would be faster to compute all satisfying
+    // formula in one operation.
+    next_succ_set_ &= !current_;
+    current_ = bdd_satone(next_succ_set_);
+  }
+  
+  bool
+  tgba_succ_iterator_concrete::done()
+  {
+    return next_succ_set_ == bddfalse;
+  }
+  
+  state_bdd
+  tgba_succ_iterator_concrete::current_state()
+  {
+    assert(!done());
+    return bdd_exist(current_, data_.notnow_set);
+  }
+  
+  bdd
+  tgba_succ_iterator_concrete::current_condition()
+  {
+    assert(!done());
+    return bdd_exist(current_, data_.notvar_set);
+  }
+  
+  bdd
+  tgba_succ_iterator_concrete::current_promise()
+  {
+    assert(!done());
+    return bdd_exist(current_, data_.notprom_set);
+  }
+
+}

src/tgba/succiterconcrete.hh

@@ -0,0 +1,33 @@
+#ifndef SPOT_TGBA_SUCCITERCONCRETE_HH
+# define SPOT_TGBA_SUCCITERCONCRETE_HH
+
+#include "succiter.hh"
+#include "tgbabddcoredata.hh"
+
+namespace spot
+{
+  class tgba_succ_iterator_concrete: public tgba_succ_iterator
+  {
+  public:
+    tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors);
+    virtual ~tgba_succ_iterator_concrete();
+  
+    // iteration
+    void first();
+    void next();
+    bool done();
+  
+    // inspection
+    state_bdd current_state();
+    bdd current_condition();
+    bdd current_promise();
+  
+  private:
+    const tgba_bdd_core_data& data_;
+    bdd succ_set_;		// The set of successors.
+    bdd next_succ_set_;		// Unexplored successors (including current_).
+    bdd current_;		// Current successor.
+  };
+}
+
+#endif // SPOT_TGBA_SUCCITERCONCRETE_HH

src/tgba/succlist.hh

@@ -0,0 +1,15 @@
+#ifndef SPOT_WAUTO_SUCCLIST_HH
+# define SPOT_WAUTO_SUCCLIST_HH
+
+namespace spot
+{
+
+  struct successor_list 
+  {
+    virtual 
+
+  };
+
+}
+
+#endif SPOT_WAUTO_SUCCLIST_HH

src/tgba/tgba.hh

@@ -0,0 +1,8 @@
+#ifndef SPOT_TGBA_TGBA_HH
+# define SPOT_TGBA_TGBA_HH
+
+# include "tgbabddconcrete.hh"
+# include "tgbabddconcreteproduct.hh"
+# include "ltl2tgba.hh"
+
+#endif // SPOT_TGBA_TGBA_HH

src/tgba/tgbabddconcrete.cc

@@ -0,0 +1,58 @@
+#include "tgbabddconcrete.hh"
+
+namespace spot
+{
+  tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact)
+    : data_(fact.get_core_data()), dict_(fact.get_dict())
+  {
+  }
+
+  tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init)
+    : data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init)
+  {
+  }
+
+  tgba_bdd_concrete::~tgba_bdd_concrete()
+  {
+  }
+
+  void
+  tgba_bdd_concrete::set_init_state(bdd s)
+  {
+    init_ = s;
+  }
+
+  state_bdd
+  tgba_bdd_concrete::get_init_state() const
+  {
+    return init_;
+  }
+
+  tgba_succ_iterator_concrete*
+  tgba_bdd_concrete::succ_iter(bdd state) const
+  {
+    bdd succ_set = bdd_replace(bdd_exist(data_.relation & state,
+					 data_.now_set),
+			       data_.next_to_now);
+    return new tgba_succ_iterator_concrete(data_, succ_set);
+  }
+
+  tgba_succ_iterator_concrete*
+  tgba_bdd_concrete::init_iter() const
+  {
+    return new tgba_succ_iterator_concrete(data_, init_);
+  }
+
+  const tgba_bdd_dict&
+  tgba_bdd_concrete::get_dict() const
+  {
+    return dict_;
+  }
+
+  const tgba_bdd_core_data&
+  tgba_bdd_concrete::get_core_data() const
+  {
+    return data_;
+  }
+
+}

src/tgba/tgbabddconcrete.hh

@@ -0,0 +1,34 @@
+#ifndef SPOT_TGBA_TGBABDDCONCRETE_HH
+# define SPOT_TGBA_TGBABDDCONCRETE_HH
+
+#include "statebdd.hh"
+#include "tgbabddfactory.hh"
+#include "succiterconcrete.hh"
+
+namespace spot
+{
+  class tgba_bdd_concrete
+  {
+  public:
+    tgba_bdd_concrete(const tgba_bdd_factory& fact);
+    tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init);
+    ~tgba_bdd_concrete();
+  
+    void set_init_state(bdd s);
+    state_bdd get_init_state() const;
+  
+    tgba_succ_iterator_concrete* succ_iter(bdd state) const;
+    tgba_succ_iterator_concrete* init_iter() const;
+  
+    const tgba_bdd_dict& get_dict() const;
+    const tgba_bdd_core_data& get_core_data() const;
+  
+  protected:
+    tgba_bdd_core_data data_;
+    tgba_bdd_dict dict_;
+    bdd init_;
+    friend class tgba_tgba_succ_iterator;
+  };
+}
+
+#endif // SPOT_TGBA_TGBABDDCONCRETE_HH

src/tgba/tgbabddconcretefactory.cc

@@ -0,0 +1,84 @@
+#include "tgbabddconcretefactory.hh"
+
+namespace spot 
+{
+  tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory()
+  {
+  }
+
+  int
+  tgba_bdd_concrete_factory::create_state(const ltl::formula* f)
+  {
+    // Do not build a state that already exists.
+    tgba_bdd_dict::fv_map::iterator sii = dict_.now_map.find(f);
+    if (sii != dict_.now_map.end())
+      return sii->second;
+
+    int num = create_pair();
+
+    dict_.now_map[f] = num;
+    dict_.now_formula_map[num] = f;
+
+    // Record that num+1 should be renamed as num when
+    // the next state becomes current.
+    bdd_setpair(data_.next_to_now, num + 1, num);
+
+    // Keep track of all "Now" variables for easy
+    // existential quantification.
+    data_.declare_now_next (ithvar(num), ithvar(num + 1));
+    return num;
+  }
+
+  int
+  tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f)
+  {
+    // Do not build a variable that already exists.
+    tgba_bdd_dict::fv_map::iterator sii = dict_.var_map.find(f);
+    if (sii != dict_.var_map.end())
+      return sii->second;
+
+    int num = create_node();
+    dict_.var_map[f] = num;
+    dict_.var_formula_map[num] = f;
+
+    // Keep track of all atomic proposition for easy
+    // existential quantification.
+    data_.declare_atomic_prop(ithvar(num));
+    return num;
+  }
+
+  int
+  tgba_bdd_concrete_factory::create_promise(const ltl::formula* f)
+  {
+    // Do not build a promise that already exists.
+    tgba_bdd_dict::fv_map::iterator sii = dict_.prom_map.find(f);
+    if (sii != dict_.prom_map.end())
+      return sii->second;
+
+    int num = create_node();
+    dict_.prom_map[f] = num;
+    dict_.prom_formula_map[num] = f;
+
+    // Keep track of all promises for easy existential quantification.
+    data_.declare_promise(ithvar(num));
+    return num;
+  }
+
+  const tgba_bdd_core_data&
+  tgba_bdd_concrete_factory::get_core_data() const
+  {
+    return data_;
+  }
+
+  const tgba_bdd_dict&
+  tgba_bdd_concrete_factory::get_dict() const
+  {
+    return dict_;
+  }
+
+  void
+  tgba_bdd_concrete_factory::add_relation(bdd new_rel)
+  {
+    data_.relation &= new_rel;
+  }
+}

src/tgba/tgbabddconcretefactory.hh

@@ -0,0 +1,31 @@
+#ifndef SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH
+# define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH
+
+#include "ltlast/formula.hh"
+#include "bddfactory.hh"
+#include "tgbabddfactory.hh"
+
+namespace spot 
+{
+
+  class tgba_bdd_concrete_factory: public bdd_factory, public tgba_bdd_factory
+  {
+  public:
+    virtual ~tgba_bdd_concrete_factory();
+  
+    int create_state(const ltl::formula* f);  
+    int create_atomic_prop(const ltl::formula* f);
+    int create_promise(const ltl::formula* f);
+  
+    const tgba_bdd_core_data& get_core_data() const;
+    const tgba_bdd_dict& get_dict() const;
+  
+    void add_relation(bdd new_rel);
+  
+  private:
+    tgba_bdd_core_data data_;
+    tgba_bdd_dict dict_;
+  };
+
+}
+#endif // SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH

src/tgba/tgbabddconcreteproduct.cc

@@ -0,0 +1,59 @@
+#include "tgbabddconcreteproduct.hh"
+#include "tgbabddtranslatefactory.hh"
+#include "dictunion.hh"
+
+namespace spot
+{
+  class tgba_bdd_product_factory: public tgba_bdd_factory
+  {
+  public:
+    tgba_bdd_product_factory(const tgba_bdd_concrete& left,
+			     const tgba_bdd_concrete& right)
+      : dict_(tgba_bdd_dict_union(left.get_dict(),
+				  right.get_dict())),
+        fact_left_(left, dict_),
+        fact_right_(right, dict_),
+        data_(fact_left_.get_core_data(), fact_right_.get_core_data()),
+        init_(fact_left_.get_init_state() & fact_right_.get_init_state())
+    {
+    }
+  
+    virtual
+    ~tgba_bdd_product_factory()
+    {
+    }
+  
+    const tgba_bdd_core_data&
+    get_core_data() const
+    {
+      return data_;
+    }
+  
+    const tgba_bdd_dict&
+    get_dict() const
+    {
+      return dict_;
+    }
+  
+    bdd
+    get_init_state() const
+    {
+      return init_;
+    }
+  
+  private:
+    tgba_bdd_dict dict_;
+    tgba_bdd_translate_factory fact_left_;
+    tgba_bdd_translate_factory fact_right_;
+    tgba_bdd_core_data data_;
+    bdd init_;
+  };
+  
+  tgba_bdd_concrete
+  product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right)
+  {
+  
+    tgba_bdd_product_factory p(left, right);
+    return tgba_bdd_concrete(p, p.get_init_state());
+  }
+}

src/tgba/tgbabddconcreteproduct.hh

@@ -0,0 +1,12 @@
+#ifndef SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH
+# define SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH
+
+#include "tgbabddconcrete.hh"
+
+namespace spot
+{
+  tgba_bdd_concrete
+  product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right);
+}
+
+#endif // SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH

src/tgba/tgbabddcoredata.cc

@@ -0,0 +1,74 @@
+#include "tgbabddcoredata.hh"
+
+namespace spot
+{
+  tgba_bdd_core_data::tgba_bdd_core_data()
+    : relation(bddtrue),
+      now_set(bddtrue), negnow_set(bddtrue), notnow_set(bddtrue),
+      notvar_set(bddtrue), notprom_set(bddtrue), next_to_now(bdd_newpair())
+  {
+  }
+
+  tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy)
+    : relation(copy.relation),
+      now_set(copy.now_set), negnow_set(copy.negnow_set),
+      notnow_set(copy.notnow_set), notvar_set(copy.notvar_set),
+      notprom_set(copy.notprom_set),
+      next_to_now(bdd_copypair(copy.next_to_now))
+  {
+  }
+
+  // Merge two core_data.
+  tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& left,
+					   const tgba_bdd_core_data& right)
+    : relation(left.relation & right.relation),
+      now_set(left.now_set & right.now_set),
+      negnow_set(left.negnow_set & right.negnow_set),
+      notnow_set(left.notnow_set & right.notnow_set),
+      notvar_set(left.notvar_set & right.notvar_set),
+      notprom_set(left.notprom_set & right.notprom_set),
+      next_to_now(bdd_mergepairs(left.next_to_now, right.next_to_now))
+  {
+  }
+
+  const tgba_bdd_core_data&
+  tgba_bdd_core_data::operator= (const tgba_bdd_core_data& copy)
+  {
+    if (this != &copy)
+      {
+	this->~tgba_bdd_core_data();
+	new (this) tgba_bdd_core_data(copy);
+      }
+    return *this;
+  }
+
+  tgba_bdd_core_data::~tgba_bdd_core_data()
+  {
+    bdd_freepair(next_to_now);
+  }
+  
+  void
+  tgba_bdd_core_data::declare_now_next(bdd now, bdd next)
+  {
+    now_set &= now;
+    negnow_set &= !now;
+    notnow_set &= next;
+    bdd both = now & next;
+    notvar_set &= both;
+    notprom_set &= both;
+  }
+  
+  void
+  tgba_bdd_core_data::declare_atomic_prop(bdd var)
+  {
+    notnow_set &= var;
+    notprom_set &= var;
+  }
+  
+  void
+  tgba_bdd_core_data::declare_promise(bdd prom)
+  {
+    notnow_set &= prom;
+    notvar_set &= prom;
+  }
+}

src/tgba/tgbabddcoredata.hh

@@ -0,0 +1,54 @@
+#ifndef SPOT_TGBA_TGBABDDCOREDATA_HH
+# define SPOT_TGBA_TGBABDDCOREDATA_HH
+
+#include <bdd.h>
+
+namespace spot
+{
+  struct tgba_bdd_core_data
+  {
+    // RELATION encodes the transition relation of the TGBA.
+    // It uses four kinds of variables:
+    //   - "Now" variables, that encode the current state
+    //   - "Next" variables, that encode the destination state
+    //   - atomic propositions, which are things to verify before going on
+    //                          to the next state
+    //   - promises: a U b, or F b, both implie that b should be verified
+    //                eventually.  We encode this with Prom[b], and check
+    //                that promises are fullfilled in the emptyness check.
+    bdd relation;
+  
+    // The conjunction of all Now variables, in their positive form.
+    bdd now_set;
+    // The conjunction of all Now variables, in their negated form.
+    bdd negnow_set;
+    // The (positive) conjunction of all variables which are not Now variables.
+    bdd notnow_set;
+    // The (positive) conjunction of all variables which are not atomic
+    // propositions.
+    bdd notvar_set;
+    // The (positive) conjunction of all variables which are not promises.
+    bdd notprom_set;
+  
+    // Record pairings between Next and Now variables.
+    bddPair* next_to_now;
+
+  
+    tgba_bdd_core_data();
+    tgba_bdd_core_data(const tgba_bdd_core_data& copy);
+  
+    // Merge two core_data.
+    tgba_bdd_core_data(const tgba_bdd_core_data& left,
+		       const tgba_bdd_core_data& right);
+  
+    const tgba_bdd_core_data& operator= (const tgba_bdd_core_data& copy);
+  
+    ~tgba_bdd_core_data();
+  
+    void declare_now_next(bdd now, bdd next);
+    void declare_atomic_prop(bdd var);
+    void declare_promise(bdd prom);
+  };
+}
+
+#endif // SPOT_TGBA_TGBABDDCOREDATA_HH

src/tgba/tgbabdddict.cc

@@ -0,0 +1,32 @@
+#include "tgbabdddict.hh"
+#include "ltlvisit/tostring.hh"
+
+namespace spot
+{
+  std::ostream&
+  tgba_bdd_dict::dump(std::ostream& os) const
+  {
+    fv_map::const_iterator sii;
+    os << "Atomic Propositions:" << std::endl;
+    for (sii = var_map.begin(); sii != var_map.end(); ++sii)
+      {
+	os << "  " << sii->second << ": ";
+	to_string(sii->first, os) << std::endl;
+      }
+    os << "States:" << std::endl;
+    for (sii = now_map.begin(); sii != now_map.end(); ++sii)
+      {
+	os << "  " << sii->second << ": Now[";
+	to_string(sii->first, os) << "]" << std::endl;
+	os << "  " << sii->second + 1 << ": Next[";
+	to_string(sii->first, os) << "]" << std::endl;
+      }
+    os << "Promises:" << std::endl;
+    for (sii = prom_map.begin(); sii != prom_map.end(); ++sii)
+      {
+	os << "  " << sii->second << ": ";
+	to_string(sii->first, os) << std::endl;
+      }
+    return os;
+  }
+}

src/tgba/tgbabdddict.hh

@@ -0,0 +1,30 @@
+#ifndef SPOT_TGBA_TGBABDDDICT_H
+# define SPOT_TGBA_TGBABDDDICT_H
+
+#include <map>
+#include <iostream>
+#include "ltlast/formula.hh"
+
+namespace spot
+{
+  struct tgba_bdd_dict
+  {
+    // Dictionaries for BDD variables.
+
+    // formula-to-BDD-variable maps
+    typedef std::map<const ltl::formula*, int> fv_map;
+    // BDD-variable-to-formula maps
+    typedef std::map<int, const ltl::formula*> vf_map;
+
+    fv_map now_map;
+    vf_map now_formula_map;
+    fv_map var_map;
+    vf_map var_formula_map;
+    fv_map prom_map;
+    vf_map prom_formula_map;
+
+    std::ostream& dump(std::ostream& os) const;
+  };
+}
+
+#endif // SPOT_TGBA_TGBABDDDICT_H

src/tgba/tgbabddfactory.hh

@@ -0,0 +1,17 @@
+#ifndef SPOT_TGBA_TGBABDDFACTORY_H
+# define SPOT_TGBA_TGBABDDFACTORY_H
+
+#include "tgbabddcoredata.hh"
+#include "tgbabdddict.hh"
+
+namespace spot
+{
+  class tgba_bdd_factory
+  {
+  public:
+    virtual const tgba_bdd_core_data& get_core_data() const = 0;
+    virtual const tgba_bdd_dict& get_dict() const = 0;
+  };
+}
+
+#endif // SPOT_TGBA_TGBABDDFACTORY_H

src/tgba/tgbabddtranslatefactory.cc

@@ -0,0 +1,93 @@
+#include "tgbabddtranslatefactory.hh"
+#include "dictunion.hh"
+
+namespace spot
+{
+  tgba_bdd_translate_factory::tgba_bdd_translate_factory
+  (const tgba_bdd_concrete& from, const tgba_bdd_dict& to)
+    : dict_(to)
+  {
+    bddPair* rewrite = compute_pairs(from.get_dict());
+
+    const tgba_bdd_core_data& in = from.get_core_data();
+
+    data_.relation = bdd_replace(in.relation, rewrite);
+    data_.now_set = bdd_replace(in.now_set, rewrite);
+    data_.negnow_set = bdd_replace(in.negnow_set, rewrite);
+    data_.notnow_set = bdd_replace(in.notnow_set, rewrite);
+    data_.notvar_set = bdd_replace(in.notvar_set, rewrite);
+    data_.notprom_set = bdd_replace(in.notprom_set, rewrite);
+
+    init_ = bdd_replace(from.get_init_state().as_bdd(), rewrite);
+
+    bdd_freepair(rewrite);
+  }
+
+  tgba_bdd_translate_factory::~tgba_bdd_translate_factory()
+  {
+  }
+
+  bddPair*
+  tgba_bdd_translate_factory::compute_pairs(const tgba_bdd_dict& from)
+  {
+    bddPair* rewrite = bdd_newpair();
+
+    tgba_bdd_dict::fv_map::const_iterator i_from;
+    tgba_bdd_dict::fv_map::const_iterator i_to;
+
+    from.dump(std::cerr);
+
+    for (i_from = from.now_map.begin(); i_from != from.now_map.end(); ++i_from)
+      {
+	i_to = dict_.now_map.find(i_from->first);
+	assert(i_to != dict_.now_map.end());
+
+	bdd_setpair(rewrite, i_from->second, i_to->second);
+	bdd_setpair(rewrite, i_from->second + 1, i_to->second + 1);
+	bdd_setpair(data_.next_to_now, i_to->second + 1, i_to->second);
+      }
+    for (i_from = from.var_map.begin(); i_from != from.var_map.end(); ++i_from)
+      {
+	i_to = dict_.var_map.find(i_from->first);
+	assert(i_to != dict_.var_map.end());
+	bdd_setpair(rewrite, i_from->second, i_to->second);
+      }
+    for (i_from = from.prom_map.begin();
+	 i_from != from.prom_map.end();
+	 ++i_from)
+      {
+	i_to = dict_.prom_map.find(i_from->first);
+	assert(i_to != dict_.prom_map.end());
+	bdd_setpair(rewrite, i_from->second, i_to->second);
+      }
+    return rewrite;
+  }
+
+  const tgba_bdd_core_data&
+  tgba_bdd_translate_factory::get_core_data() const
+  {
+    return data_;
+  }
+
+  const tgba_bdd_dict&
+  tgba_bdd_translate_factory::get_dict() const
+  {
+    return dict_;
+  }
+
+  bdd
+  tgba_bdd_translate_factory::get_init_state() const
+  {
+    return init_;
+  }
+
+
+  tgba_bdd_concrete
+  defrag(const tgba_bdd_concrete& a)
+  {
+    const tgba_bdd_dict& ad = a.get_dict();
+    tgba_bdd_dict u = tgba_bdd_dict_union(ad, ad);
+    tgba_bdd_translate_factory f(a, u);
+    return tgba_bdd_concrete(f, f.get_init_state());
+  }
+}

src/tgba/tgbabddtranslatefactory.hh

@@ -0,0 +1,34 @@
+#ifndef SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH
+# define SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH
+
+#include "tgbabddfactory.hh"
+#include "tgbabddconcrete.hh"
+
+namespace spot
+{
+
+  class tgba_bdd_translate_factory: public tgba_bdd_factory
+  {
+  public:
+    tgba_bdd_translate_factory(const tgba_bdd_concrete& from,
+			       const tgba_bdd_dict& to);
+
+    virtual ~tgba_bdd_translate_factory();
+
+    bddPair* compute_pairs(const tgba_bdd_dict& from);
+  
+    const tgba_bdd_core_data& get_core_data() const;
+    const tgba_bdd_dict& get_dict() const;
+  
+    bdd get_init_state() const;
+  
+  private:
+    tgba_bdd_core_data data_;
+    tgba_bdd_dict dict_;
+    bdd init_;  
+  };
+  
+  tgba_bdd_concrete defrag(const tgba_bdd_concrete& a);
+}
+
+#endif // SPOT_TGBA_TGBABDDTRANSLATEFACTORY_HH