Ease atomic proposition manipulation for twa.

* doc/org/tut22.org, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/parseaut/parseaut.yy,
src/tests/ikwiad.cc, src/tests/tgbagraph.test,
src/tests/twagraph.cc, src/twa/twa.cc,
src/twa/twa.hh, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/randomgraph.cc, src/twaalgos/relabel.cc,
src/twaalgos/stutter.cc, src/twaalgos/stutter.hh: here.

doc/org/tut22.org

@@ -20,19 +20,11 @@ The interface
     // This creates an empty automaton that we have yet to fill.
     spot::twa_graph_ptr aut = make_twa_graph(dict);
 
-    // The current way to associate a BDD to an atomic proposition is
+    // Since a BDD is associated to every atomic proposition, the
-    // not really nice, and should be improved in the future.  Currently
+    // register_ap() function returns a BDD variable number
-    // the string first have to be converted into (LTL) formulas...
-    spot::ltl::environment& e = spot::ltl::default_environment::instance();
-    const spot::ltl::formula* f1 = e.require("p1");
-    const spot::ltl::formula* f2 = e.require("p2");
-    // ...and then those formula can be registered to the BDD dict.  The
-    // BDD dict wants to keep track of which automaton uses which BDD
-    // variable, so we supply that pointer to aut.  The
-    // register_proposition() function returns a BDD variable number
     // that can be converted into a BDD using bdd_ithvar().
-    bdd p1 = bdd_ithvar(dict->register_proposition(f1, aut));
+    bdd p1 = bdd_ithvar(aut->register_ap("p1"));
-    bdd p2 = bdd_ithvar(dict->register_proposition(f2, aut));
+    bdd p2 = bdd_ithvar(aut->register_ap("p2"));
 
     // Set the acceptance condition of the automaton to Inf(0)&Inf(1)
     aut->set_generalized_buchi(2);

src/ltlvisit/apcollect.cc

@@ -85,18 +85,15 @@ namespace spot
     }
 
     bdd
-    atomic_prop_collect_as_bdd(const formula* f, const const_twa_ptr& a)
+    atomic_prop_collect_as_bdd(const formula* f, const twa_ptr& a)
     {
       spot::ltl::atomic_prop_set aps;
       atomic_prop_collect(f, &aps);
-      auto d = a->get_dict();
       bdd res = bddtrue;
       for (atomic_prop_set::const_iterator i = aps.begin();
 	   i != aps.end(); ++i)
-	res &= bdd_ithvar(d->register_proposition(*i, a));
+	res &= bdd_ithvar(a->register_ap(*i));
       return res;
     }
-
   }
-
 }

src/ltlvisit/apcollect.hh

@@ -68,7 +68,7 @@ namespace spot
     /// \return A conjunction the atomic propositions.
     SPOT_API bdd
     atomic_prop_collect_as_bdd(const formula* f,
-			       const const_twa_ptr& a);
+			       const twa_ptr& a);
 
     /// @}
   }

src/parseaut/parseaut.yy

@@ -555,7 +555,6 @@ ap-name: STRING
 	   if (!res.ignore_more_ap)
 	     {
 	       auto f = res.env->require(*$1);
-	       auto d = res.h->aut->get_dict();
 	       int b = 0;
 	       if (f == nullptr)
 		 {
@@ -564,11 +563,11 @@ ap-name: STRING
 		   error(@1, out.str());
 		   f = spot::ltl::default_environment::instance()
 		     .require("$unknown$");
-		   b = d->register_proposition(f, res.h->aut);
+		   b = res.h->aut->register_ap(f);
 		 }
 	       else
 		 {
-		   b = d->register_proposition(f, res.h->aut);
+		   b = res.h->aut->register_ap(f);
 		   if (!res.ap_set.emplace(b).second)
 		     {
 		       std::ostringstream out;

src/tests/ikwiad.cc

@@ -1255,7 +1255,7 @@ checked_main(int argc, char** argv)
 
       if (opt_stutterize)
 	{
-	  a = sl(ensure_digraph(a), f);
+	  a = sl(ensure_digraph(a));
 	}
 
       if (opt_monitor)

src/tests/tgbagraph.test

@@ -33,6 +33,8 @@ set -e
 run 0 ../tgbagraph | tee stdout
 
 cat >expected <<EOF
+p1
+p2
 digraph G {
   rankdir=LR
   node [shape="circle"]

src/tests/twagraph.cc

@@ -26,18 +26,13 @@
 void f1()
 {
   auto d = spot::make_bdd_dict();
-
-  auto& e = spot::ltl::default_environment::instance();
-
   auto tg = make_twa_graph(d);
-
+  bdd p1 = bdd_ithvar(tg->register_ap("p1"));
-  auto* f1 = e.require("p1");
+  bdd p2 = bdd_ithvar(tg->register_ap("p2"));
-  auto* f2 = e.require("p2");
-  bdd p1 = bdd_ithvar(d->register_proposition(f1, tg));
-  bdd p2 = bdd_ithvar(d->register_proposition(f2, tg));
   tg->acc().add_sets(2);
-  f1->destroy();
+
-  f2->destroy();
+  for (auto *f: tg->ap())
+    std::cout << f->name() << '\n';
 
   auto s1 = tg->new_state();
   auto s2 = tg->new_state();

src/twa/twa.cc

@@ -34,10 +34,13 @@ namespace spot
       last_support_conditions_input_(0)
   {
     props = 0U;
+    bddaps_ = bddtrue;
   }
 
   twa::~twa()
   {
+    for (auto* ap: aps_)
+      ap->destroy();
     if (last_support_conditions_input_)
       last_support_conditions_input_->destroy();
     delete iter_cache_;

src/twa/twa.hh

@@ -30,8 +30,10 @@
 #include <unordered_map>
 #include <functional>
 #include <array>
+#include <vector>
 #include "misc/casts.hh"
 #include "misc/hash.hh"
+#include "ltlast/atomic_prop.hh"
 
 namespace spot
 {
@@ -590,6 +592,46 @@ namespace spot
       return dict_;
     }
 
+    /// \brief Register an atomic proposition designated by formula \a ap.
+    ///
+    /// \return The variable number inside of the BDD.
+    int register_ap(const ltl::formula* ap)
+    {
+      aps_.push_back(dynamic_cast<const ltl::atomic_prop*>(ap));
+      ap->clone();
+      int res = dict_->register_proposition(ap, this);
+      bddaps_ &= bdd_ithvar(res);
+      return res;
+    }
+
+    /// \brief Register an atomic proposition designated by string \a ap.
+    ///
+    /// This string is converted into a formula and registered
+    /// inside of the BDD manager.
+    ///
+    /// \return The variable number inside of the BDD.
+    int register_ap(std::string name,
+		    ltl::environment& e = ltl::default_environment::instance())
+    {
+      auto* ap = e.require(name);
+      aps_.push_back(dynamic_cast<const ltl::atomic_prop*>(ap));
+      int res = dict_->register_proposition(ap, this);
+      bddaps_ &= bdd_ithvar(res);
+      return res;
+    }
+
+    /// \brief Get the vector of atomic propositions used by this
+    /// automaton.
+    const std::vector<const ltl::atomic_prop*>&  ap() const
+    {
+      return aps_;
+    }
+
+    bdd ap_var() const
+    {
+      return bddaps_;
+    }
+
     /// \brief Format the state as a string for printing.
     ///
     /// This formating is the responsability of the automata
@@ -688,6 +730,8 @@ namespace spot
     void copy_ap_of(const const_twa_ptr& a)
     {
       get_dict()->register_all_propositions_of(a, this);
+      for (auto *f: a->ap())
+	this->register_ap(f);
     }
 
     void set_generalized_buchi(unsigned num)
@@ -710,6 +754,8 @@ namespace spot
     mutable const state* last_support_conditions_input_;
   private:
     mutable bdd last_support_conditions_output_;
+    std::vector<const ltl::atomic_prop*> aps_;
+    bdd bddaps_;
 
   protected:
 

src/twaalgos/ltl2tgba_fm.cc

@@ -139,11 +139,13 @@ namespace spot
     {
     public:
 
-      translate_dict(const bdd_dict_ptr& dict,
+      translate_dict(twa_graph_ptr& a,
+		     const bdd_dict_ptr& dict,
 		     acc_cond& acc,
 		     ltl_simplifier* ls, bool exprop,
 		     bool single_acc, bool unambiguous)
-	: dict(dict),
+	: a_(a),
+	  dict(dict),
 	  ls(ls),
 	  a_set(bddtrue),
 	  var_set(bddtrue),
@@ -168,6 +170,7 @@ namespace spot
 	  j++->first.f->destroy();
       }
 
+      twa_graph_ptr& a_;
       bdd_dict_ptr dict;
       ltl_simplifier* ls;
       mark_tools mt;
@@ -418,6 +421,26 @@ namespace spot
       {
 	bdd res = ls->as_bdd(f);
 	var_set &= bdd_support(res);
+
+	bdd all = var_set;
+	while (all != bddfalse)
+	  {
+	    bdd one = bdd_satone(all);
+	    all -= one;
+	    while (one != bddtrue)
+	      {
+		int v = bdd_var(one);
+		auto *f = var_to_formula(v);
+		a_->register_ap(f);
+		f->destroy();
+		if (bdd_high(one) == bddfalse)
+		  one = bdd_low(one);
+		else
+		  one = bdd_high(one);
+	      }
+	  }
+
+
 	return res;
       }
 
@@ -2301,7 +2324,8 @@ namespace spot
     twa_graph_ptr a = make_twa_graph(dict);
     auto namer = a->create_namer<const formula*>();
 
-    translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence(),
+    translate_dict d(a, dict, a->acc(), s, exprop,
+		     f->is_syntactic_persistence(),
 		     unambiguous);
 
     // Compute the set of all promises that can possibly occur
@@ -2568,10 +2592,7 @@ namespace spot
     // Set the following to true to preserve state names.
     a->release_formula_namer(namer, false);
 
-    dict->register_propositions(fc.used_vars(), a);
-
     auto& acc = a->acc();
-
     unsigned ns = a->num_states();
     for (unsigned s = 0; s < ns; ++s)
       for (auto& t: a->out(s))

src/twaalgos/randomgraph.cc

@@ -139,7 +139,7 @@ namespace spot
 
     int pi = 0;
     for (auto i: *ap)
-      props[pi++] = dict->register_proposition(i, res);
+      props[pi++] = res->register_ap(i);
 
     res->set_generalized_buchi(n_accs);
 

src/twaalgos/relabel.cc

@@ -30,8 +30,8 @@ namespace spot
     vars.reserve(relmap->size());
     for (auto& p: *relmap)
       {
-	int oldv = d->register_proposition(p.first, aut);
+	int oldv = aut->register_ap(p.first);
-	int newv = d->register_proposition(p.second, aut);
+	int newv = aut->register_ap(p.second);
 	bdd_setpair(pairs, oldv, newv);
 	vars.push_back(oldv);
       }

src/twaalgos/stutter.cc

@@ -281,34 +281,18 @@ namespace spot
 
     // Queue of state to be processed.
     typedef std::deque<stutter_state> queue_t;
-
-    static bdd
-    get_all_ap(const const_twa_graph_ptr& a)
-    {
-      bdd res = bddtrue;
-      for (auto& i: a->edges())
-	res &= bdd_support(i.cond);
-      return res;
-    }
-
   }
 
   twa_graph_ptr
-  sl(const const_twa_graph_ptr& a, const ltl::formula* f)
+  sl(const twa_graph_ptr& a)
   {
-    bdd aps = f
+    return sl(a, a->ap_var());
-      ? atomic_prop_collect_as_bdd(f, a)
-      : get_all_ap(a);
-    return sl(a, aps);
   }
 
   twa_graph_ptr
-  sl2(const const_twa_graph_ptr& a, const ltl::formula* f)
+  sl2(const twa_graph_ptr& a)
   {
-    bdd aps = f
+    return sl2(a, a->ap_var());
-      ? atomic_prop_collect_as_bdd(f, a)
-      : get_all_ap(a);
-    return sl2(a, aps);
   }
 
   twa_graph_ptr
@@ -379,7 +363,7 @@ namespace spot
   sl2(twa_graph_ptr&& a, bdd atomic_propositions)
   {
     if (atomic_propositions == bddfalse)
-      atomic_propositions = get_all_ap(a);
+      atomic_propositions = a->ap_var();
     unsigned num_states = a->num_states();
     unsigned num_edges = a->num_edges();
     std::vector<bdd> selfloops(num_states, bddfalse);
@@ -666,7 +650,7 @@ namespace spot
       }
 
     is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()),
-				   std::move(neg), get_all_ap(aut));
+				   std::move(neg), aut->ap_var());
     aut->prop_stutter_invariant(is_stut);
     aut->prop_stutter_sensitive(!is_stut);
     return is_stut;

src/twaalgos/stutter.hh

@@ -24,13 +24,13 @@
 namespace spot
 {
   SPOT_API twa_graph_ptr
-  sl(const const_twa_graph_ptr&, const ltl::formula* = nullptr);
+  sl(const twa_graph_ptr&);
 
   SPOT_API twa_graph_ptr
   sl(const const_twa_graph_ptr&, bdd);
 
   SPOT_API twa_graph_ptr
-  sl2(const const_twa_graph_ptr&, const ltl::formula* = nullptr);
+  sl2(const twa_graph_ptr&);
 
   SPOT_API twa_graph_ptr
   sl2(const const_twa_graph_ptr&, bdd);