* src/tgba/tgbabddconcretefactory.cc

(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the
formulae used as keys in prom_.
(tgba_bdd_concrete_factory::create_promise): Delete.
(tgba_bdd_concrete_factory::declare_promise,
tgba_bdd_concrete_factory::finish): New functions.
* src/tgba/tgbabddconcretefactory.hh
(tgba_bdd_concrete_factory::create_promise): Delete.
(tgba_bdd_concrete_factory::declare_promise,
tgba_bdd_concrete_factory::finish): New functions.
(tgba_bdd_concrete_factory::prom_): New map.
* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust
the Fx and aUb cases to register promises with
tgba_bdd_concrete_factory::declare_promise().
(ltl2tgba): Call tgba_bdd_concrete_factory::finish().

ChangeLog

@@ -1,5 +1,21 @@
 2003-06-19  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/tgbabddconcretefactory.cc 
+	(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the 
+	formulae used as keys in prom_.
+	(tgba_bdd_concrete_factory::create_promise): Delete.
+	(tgba_bdd_concrete_factory::declare_promise, 
+	tgba_bdd_concrete_factory::finish): New functions.
+	* src/tgba/tgbabddconcretefactory.hh 
+	(tgba_bdd_concrete_factory::create_promise): Delete.
+	(tgba_bdd_concrete_factory::declare_promise, 
+	tgba_bdd_concrete_factory::finish): New functions.
+	(tgba_bdd_concrete_factory::prom_): New map.
+	* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust
+	the Fx and aUb cases to register promises with
+	tgba_bdd_concrete_factory::declare_promise().
+	(ltl2tgba): Call tgba_bdd_concrete_factory::finish().
+
 	* src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter):
 	Revert the change from 2003-06-12, it needs more work (the
 	automaton generated on Xa&(b U !a) was bogus, with that

src/tgba/ltl2tgba.cc

@@ -65,18 +65,20 @@ namespace spot
 		   Fx  <=> x | XFx
 	       In other words:
 		   now <=> x | next
-
-		`x | next', doesn't actually encode the fact that x
-		should be fulfilled at some point.  We use the
-		`promise' variable for this purpose.
 	    */
 	    int v = fact_.create_state(node);
 	    bdd now = fact_.ithvar(v);
 	    bdd next = fact_.ithvar(v + 1);
-	    bdd promise = fact_.ithvar(fact_.create_promise(node->child()));
+	    bdd x = recurse(node->child());
-	    fact_.add_relation(bdd_apply(now, (recurse(node->child())
+	    fact_.add_relation(bdd_apply(now, x | next, bddop_biimp));
-					       | (promise & next)),
+	    /*
-					 bddop_biimp));
+	      `x | next', doesn't actually encode the fact that x
+	      should be fulfilled at eventually.  So we declare any
+	      transition going to NEXT without checking X as
+	      "promising x".  This promises will be checked by during
+	      the emptiness check.
+	    */
+	    fact_.declare_promise(next & !x, node->child());
 	    res_ = now;
 	    return;
 	  }
@@ -135,19 +137,18 @@ namespace spot
 	       f1 U f2 <=> f2 | (f1 & X(f1 U f2))
 	       In other words:
 		   now <=> f2 | (f1 & next)
-
-		The rightmost conjunction, f1 & next, doesn't actually
-		encode the fact that f2 should be fulfilled at some
-		point.  We use the `promise_f2' variable for this purpose.
 	    */
 	    int v = fact_.create_state(node);
 	    bdd now = fact_.ithvar(v);
 	    bdd next = fact_.ithvar(v + 1);
-	    bdd promise_f2 =
+	    fact_.add_relation(bdd_apply(now, f2 | (f1 & next), bddop_biimp));
-	      fact_.ithvar(fact_.create_promise(node->second()));
+	    /*
-	    fact_.add_relation(bdd_apply(now,
+	      The rightmost conjunction, f1 & next, doesn't actually
-					 f2 | (promise_f2 & f1 & next),
+	      encode the fact that f2 should be fulfilled eventually.
-					 bddop_biimp));
+	      We declare a promise for this purpose (see the comment
+	      in the unop::F case).
+	    */
+	    fact_.declare_promise(next & !f2, node->second());
 	    res_ = now;
 	    return;
 	  }
@@ -212,6 +213,7 @@ namespace spot
     tgba_bdd_concrete_factory fact;
     ltl_trad_visitor v(fact);
     f->accept(v);
+    fact.finish();
     tgba_bdd_concrete g(fact);
     g.set_init_state(v.result());
     return g;

src/tgba/tgbabddconcretefactory.cc

@@ -1,10 +1,14 @@
 #include "ltlvisit/clone.hh"
+#include "ltlvisit/destroy.hh"
 #include "tgbabddconcretefactory.hh"
 
 namespace spot
 {
   tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory()
   {
+    promise_map_::iterator pi;
+    for (pi = prom_.begin(); pi != prom_.end(); ++pi)
+      destroy(pi->first);
   }
 
   int
@@ -51,23 +55,45 @@ namespace spot
     return num;
   }
 
-  int
+  void
-  tgba_bdd_concrete_factory::create_promise(const ltl::formula* f)
+  tgba_bdd_concrete_factory::declare_promise(bdd b,
+					     const ltl::formula* p)
   {
-    // Do not build a promise that already exists.
+    // Maintain a disjunction of BDDs associated to P.
-    tgba_bdd_dict::fv_map::iterator sii = dict_.prom_map.find(f);
+    // We will latter (in tgba_bdd_concrete_factory::finish())
-    if (sii != dict_.prom_map.end())
+    // record this disjunction as equivalant to P.
-      return sii->second;
+    promise_map_::iterator pi = prom_.find(p);
+    if (pi == prom_.end())
+      {
+	p = clone(p);
+	prom_[p] = b;
+      }
+    else
+      {
+	pi->second |= b;
+      }
+  }
 
-    f = clone(f);
+  void
+  tgba_bdd_concrete_factory::finish()
+  {
+    promise_map_::iterator pi;
+    for (pi = prom_.begin(); pi != prom_.end(); ++pi)
+      {
+	// Register a BDD variable for this promise.
+	int p = create_node();
+	const ltl::formula* f = clone(pi->first); // The promised formula.
+	dict_.prom_map[f] = p;
+	dict_.prom_formula_map[p] = f;
 
-    int num = create_node();
+	bdd prom = ithvar(p);
-    dict_.prom_map[f] = num;
+	// Keep track of all promises for easy existential quantification.
-    dict_.prom_formula_map[num] = f;
+	data_.declare_promise(prom);
 
-    // Keep track of all promises for easy existential quantification.
+	// The promise P must hold if we have to verify any of the
-    data_.declare_promise(ithvar(num));
+	// (BDD) formulae registered.
-    return num;
+	add_relation(bdd_apply(prom, pi->second, bddop_biimp));
+      }
   }
 
   const tgba_bdd_core_data&

src/tgba/tgbabddconcretefactory.hh

@@ -4,6 +4,7 @@
 #include "ltlast/formula.hh"
 #include "bddfactory.hh"
 #include "tgbabddfactory.hh"
+#include <map>
 
 namespace spot
 {
@@ -33,15 +34,17 @@ namespace spot
     /// can be turned into BDD using ithvar().
     int create_atomic_prop(const ltl::formula* f);
 
-    /// Create a promise variable for formula \a f.
+    /// Declare a promise.
     ///
-    /// \param f The formula to create a promise for.
+    /// \param b that BDD of the expression that makes a promise
-    /// \return The variable number for this state.
+    /// \param p the formula promised
     ///
-    /// The promise is not created if it already exists.  Instead its
+    /// Formula such as 'f U g' or 'F g' make the promise
-    /// existing variable number is returned.  Variable numbers
+    /// that 'g' will be fulfilled eventually.  So once
-    /// can be turned into BDD using ithvar().
+    /// one of this formula has been translated into a BDD,
-    int create_promise(const ltl::formula* f);
+    /// we use declare_promise() to associate the promise 'g'
+    /// to this BDD.
+    void declare_promise(bdd b, const ltl::formula* p);
 
     const tgba_bdd_core_data& get_core_data() const;
     const tgba_bdd_dict& get_dict() const;
@@ -49,9 +52,19 @@ namespace spot
     /// Add a new constraint to the relation.
     void add_relation(bdd new_rel);
 
+    /// \Perfom final computations before the relation can be used.
+    ///
+    /// This function should be called after all propositions, state,
+    /// promise, and constraints have been declared, and before calling
+    /// get_code_data() or get_dict().
+    void finish();
+
   private:
     tgba_bdd_core_data data_;	///< Core data for the new automata.
     tgba_bdd_dict dict_;	///< Dictionary for the new automata.
+
+    typedef std::map<const ltl::formula*, bdd> promise_map_;
+    promise_map_ prom_;		///< BDD associated to each promises
   };
 
 }