tgba_digraph: add a set_single_acceptance_set() method.

* src/tgba/tgbagraph.cc: New file.
* src/tgba/Makefile.am: Adjust.
* src/tgba/tgbagraph.hh (set_single_acceptance_set,
new_acc_transition): New methods.
(set_acceptance_conditions, merge_transitions): Move body
to tgbagraph.cc.
* src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbacomp.cc,
src/neverparse/neverclaimparse.yy, src/dstarparse/dra2ba.cc,
src/dstarparse/nra2nba.cc: Simplify using these new methods.

src/dstarparse/dra2ba.cc

@@ -23,7 +23,6 @@
 #include "tgbaalgos/reachiter.hh"
 #include "tgbaalgos/gtec/gtec.hh"
 #include "tgbaalgos/sccfilter.hh"
-#include "ltlast/constant.hh"
 
 namespace spot
 {
@@ -239,13 +238,7 @@ namespace spot
 	bdd_dict* bd = a->aut->get_dict();
 	bd->register_all_variables_of(a->aut, out_);
 	out_->set_bprop(tgba_digraph::StateBasedAcc);
-
+	acc_ = out_->set_single_acceptance_set();
-	// Invent a new acceptance set for the degeneralized automaton.
-	int accvar =
-	  bd->register_acceptance_variable(ltl::constant::true_instance(),
-					   out_);
-	acc_ = bdd_ithvar(accvar);
-	out_->set_acceptance_conditions(acc_);
 	out_->new_states(num_states_ * (a->accpair_count + 1));
 	out_->set_init_state(a->aut->get_init_state_number());
       }
@@ -299,10 +292,9 @@ namespace spot
 		    // accepting cycle.
 		    out_->new_transition(in, out + shift, cond);
 
-		    bdd acc = bddfalse;
+		    // Acceptance transitions are those in the Li set. (Löding's Fi set.)
-		    if (l.get(i))	// In the Li set. (Löding's Fi set.)
+		    out_->new_acc_transition(in + shift, out + shift, cond,
-		      acc = acc_;
+					     l.get(i));
-		    out_->new_transition(in + shift, out + shift, cond, acc);
 		  }
 	      }
 	  }

src/dstarparse/nra2nba.cc

@@ -20,7 +20,6 @@
 #include "public.hh"
 #include "tgbaalgos/reachiter.hh"
 #include "tgbaalgos/sccfilter.hh"
-#include "ltlast/constant.hh"
 
 namespace spot
 {
@@ -49,13 +48,8 @@ namespace spot
 	bd->register_all_variables_of(aut, out_);
 
 	// Invent a new acceptance set for the degeneralized automaton.
-	int accvar =
+	out_->set_single_acceptance_set();
-	  bd->register_acceptance_variable(ltl::constant::true_instance(),
-					   out_);
 	out_->set_bprop(tgba_digraph::StateBasedAcc);
-
-	acc_ = bdd_ithvar(accvar);
-	out_->set_acceptance_conditions(acc_);
 	out_->new_states(num_states_ * (d_->accpair_count + 1));
 
 	auto i = aut->get_init_state();
@@ -104,10 +98,10 @@ namespace spot
 		// accepting cycle.
 		out_->new_transition(in, out + shift, cond);
 
-		bdd acc = bddfalse;
+		// A transition is accepting if it is in the Li
-		if (l.get(i))	// In the Li set. (Löding's Fi set.)
+		// set. (Löding's Fi set.)
-		  acc = acc_;
+		out_->new_acc_transition(in + shift, out + shift, cond,
-		out_->new_transition(in + shift, out + shift, cond, acc);
+					 l.get(i));
 	      }
 	  }
       }
@@ -116,7 +110,6 @@ namespace spot
       tgba_digraph* out_;
       const dstar_aut* d_;
       size_t num_states_;
-      bdd acc_;
     };
 
   }

src/neverparse/neverclaimparse.yy

@@ -31,7 +31,6 @@
 {
 #include <string>
 #include <cstring>
-#include "ltlast/constant.hh"
 #include "public.hh"
 #include "tgba/formula2bdd.hh"
 
@@ -168,7 +167,6 @@ state:
   | ident_list "false" { delete $1; }
   | ident_list transition_block
     {
-      std::list<pair>::iterator it;
       bdd acc = !strncmp("accept", $1->c_str(), 6) ?
 	result->all_acceptance_conditions() :
 	static_cast<const bdd>(bddfalse);
@@ -304,11 +302,7 @@ namespace spot
     formula_cache fcache;
     tgba_digraph* result = new tgba_digraph(dict);
     auto namer = result->create_namer<std::string>();
-
+    result->set_single_acceptance_set();
-    const ltl::formula* t = ltl::constant::true_instance();
-    bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result));
-    result->set_acceptance_conditions(acc);
-
     result->set_bprop(tgba_digraph::SBA);
 
     neverclaimyy::parser parser(error_list, env, result, namer, fcache);
@@ -319,7 +313,7 @@ namespace spot
     if (accept_all_needed && !accept_all_seen)
       {
 	unsigned n = namer->new_state("accept_all");
-	result->new_transition(n, n, bddtrue, acc);
+	result->new_acc_transition(n, n, bddtrue);
       }
     accept_all_needed = false;
     accept_all_seen = false;

src/tgba/Makefile.am

@@ -53,6 +53,7 @@ libtgba_la_SOURCES = \
   futurecondcol.cc \
   taatgba.cc \
   tgba.cc \
+  tgbagraph.cc \
   tgbakvcomplement.cc \
   tgbaproduct.cc \
   tgbamask.cc \

src/tgba/tgbagraph.cc

@@ -0,0 +1,102 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche et Développement de
+// l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "tgbagraph.hh"
+#include "ltlast/constant.hh"
+
+namespace spot
+{
+
+  void tgba_digraph::set_acceptance_conditions(bdd all)
+  {
+    if (all_acceptance_conditions_ != bddfalse)
+      dict_->unregister_all_typed_variables(bdd_dict::acc, this);
+
+    bdd sup = bdd_support(all);
+    dict_->register_acceptance_variables(sup, this);
+    neg_acceptance_conditions_ = bddtrue;
+    while (sup != bddtrue)
+      {
+	neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup));
+	sup = bdd_high(sup);
+      }
+    all_acceptance_conditions_ =
+      compute_all_acceptance_conditions(neg_acceptance_conditions_);
+
+    if (number_of_acceptance_conditions() == 1)
+      set_bprop(tgba_digraph::SingleAccSet);
+    else
+      clear_bprop(tgba_digraph::SingleAccSet);
+  }
+
+  bdd tgba_digraph::set_single_acceptance_set()
+  {
+    if (all_acceptance_conditions_ != bddfalse)
+      dict_->unregister_all_typed_variables(bdd_dict::acc, this);
+
+    set_bprop(tgba_digraph::SingleAccSet);
+    int accvar =
+      dict_->register_acceptance_variable(ltl::constant::true_instance(),
+					  this);
+    bdd degen_acc = bdd_ithvar(accvar);
+    all_acceptance_conditions_ = degen_acc;
+    neg_acceptance_conditions_ = bdd_nithvar(accvar);
+    return degen_acc;
+  }
+
+  void tgba_digraph::merge_transitions()
+  {
+    for (auto& s: g_.states())
+      {
+	// Map a pair (dest state, acc) to the first transition seen
+	// with such characteristic.
+
+	typedef std::pair<graph_t::state, int> key_t;
+	std::unordered_map<key_t, graph_t::transition, pair_hash> trmap;
+
+	auto t = g_.out_iteraser(s);
+	while (t)
+	  {
+	    // Simply skip false transitions.
+	    if (t->cond == bddfalse)
+	      {
+		t.erase();
+		continue;
+	      }
+
+	    key_t k(t->dst, t->acc.id());
+	    auto p = trmap.emplace(k, t.trans());
+	    if (!p.second)
+	      {
+		// A previous transitions exist for k, merge the
+		// condition, and schedule the transition for
+		// removal.
+		g_.trans_data(p.first->second).cond |= t->cond;
+		t.erase();
+	      }
+	    else
+	      {
+		++t;
+	      }
+	  }
+      }
+    g_.defrag();
+  }
+
+}

src/tgba/tgbagraph.hh

@@ -90,7 +90,7 @@ namespace spot
 
 
   template<class Graph>
-  class tgba_digraph_succ_iterator: public tgba_succ_iterator
+  class SPOT_API tgba_digraph_succ_iterator: public tgba_succ_iterator
   {
   private:
     typedef typename Graph::transition transition;
@@ -153,7 +153,7 @@ namespace spot
 
   };
 
-  class tgba_digraph: public tgba
+  class SPOT_API tgba_digraph: public tgba
   {
   public:
     typedef digraph<tgba_graph_state, tgba_graph_trans_data> graph_t;
@@ -302,24 +302,8 @@ namespace spot
       return g_.trans_data(t);
     }
 
-    void set_acceptance_conditions(bdd all)
+    void set_acceptance_conditions(bdd all);
-    {
+    bdd set_single_acceptance_set();
-      bdd sup = bdd_support(all);
-      this->dict_->register_acceptance_variables(sup, this);
-      neg_acceptance_conditions_ = bddtrue;
-      while (sup != bddtrue)
-	{
-	  neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup));
-	  sup = bdd_high(sup);
-	}
-      all_acceptance_conditions_ =
-	compute_all_acceptance_conditions(neg_acceptance_conditions_);
-
-      if (number_of_acceptance_conditions() == 1)
-	set_bprop(tgba_digraph::SingleAccSet);
-      else
-	clear_bprop(tgba_digraph::SingleAccSet);
-    }
 
     unsigned new_state()
     {
@@ -337,6 +321,15 @@ namespace spot
       return g_.new_transition(src, dst, cond, acc);
     }
 
+    unsigned new_acc_transition(unsigned src, unsigned dst,
+				bdd cond, bool acc = true)
+    {
+      if (acc)
+	return g_.new_transition(src, dst, cond, all_acceptance_conditions_);
+      else
+	return g_.new_transition(src, dst, cond);
+    }
+
     auto out(unsigned src) const
       SPOT_RETURN(g_.out(src));
     auto out(unsigned src)
@@ -378,45 +371,7 @@ namespace spot
 
     /// Iterate over all transitions, and merge those with compatible
     /// extremities and acceptance.
-    void merge_transitions()
+    void merge_transitions();
-    {
-      for (auto& s: g_.states())
-	{
-	  // Map a pair (dest state, acc) to the first transition seen
-	  // with such characteristic.
-
-	  typedef std::pair<graph_t::state, int> key_t;
-	  std::unordered_map<key_t, graph_t::transition, pair_hash> trmap;
-
-	  auto t = g_.out_iteraser(s);
-	  while (t)
-	    {
-	      // Simply skip false transitions.
-	      if (t->cond == bddfalse)
-		{
-		  t.erase();
-		  continue;
-		}
-
-	      key_t k(t->dst, t->acc.id());
-	      auto p = trmap.emplace(k, t.trans());
-	      if (!p.second)
-		{
-		  // A previous transitions exist for k, merge the
-		  // condition, and schedule the transition for
-		  // removal.
-		  g_.trans_data(p.first->second).cond |= t->cond;
-		  t.erase();
-		}
-	      else
-		{
-		  ++t;
-		}
-	    }
-	}
-      g_.defrag();
-    }
-
 
   protected:
     unsigned bprops_ = 0;

src/tgbaalgos/complete.cc

@@ -18,7 +18,6 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include "complete.hh"
-#include "ltlast/constant.hh"
 #include "dupexp.hh"
 
 namespace spot
@@ -33,10 +32,7 @@ namespace spot
 	// We cannot safely complete an automaton if it has no
 	// acceptance set as the added sink would become accepting.
 	// In this case, add an acceptance set to all transitions.
-	const ltl::formula* t = ltl::constant::true_instance();
+	allacc = aut->set_single_acceptance_set();
-	int v = aut->get_dict()->register_acceptance_variable(t, aut);
-	allacc = bdd_ithvar(v);
-	aut->set_acceptance_conditions(allacc);
 	for (auto& t: aut->transitions())
 	  t.acc = allacc;
       }

src/tgbaalgos/degen.cc

@@ -22,7 +22,6 @@
 #include "tgba/tgbagraph.hh"
 #include "misc/hash.hh"
 #include "misc/hashfunc.hh"
-#include "ltlast/constant.hh"
 #include <deque>
 #include <vector>
 #include <algorithm>
@@ -261,19 +260,13 @@ namespace spot
 
       // The result automaton is an SBA.
       auto res = new tgba_digraph(dict);
+      res->set_single_acceptance_set();
       if (want_sba)
 	res->set_bprop(tgba_digraph::StateBasedAcc);
 
       // We use the same BDD variables as the input, except for the
       // acceptance.
       dict->register_all_variables_of(a, res);
-      dict->unregister_all_typed_variables(bdd_dict::acc, res);
-
-      // Invent a new acceptance set for the degeneralized automaton.
-      int accvar =
-	dict->register_acceptance_variable(ltl::constant::true_instance(), res);
-      bdd degen_acc = bdd_ithvar(accvar);
-      res->set_acceptance_conditions(degen_acc);
 
       // Create an order of acceptance conditions.  Each entry in this
       // vector correspond to an acceptance set.  Each index can
@@ -600,24 +593,12 @@ namespace spot
 
 	      unsigned& t = tr_cache[dest * 2 + is_acc];
 
-	      if (t == 0)
+	      if (t == 0)	// Create transition.
-		{
+		t = res->new_acc_transition(src, dest,
-		  // Actually create the transition.  If the source
+					    i->current_condition(), is_acc);
-		  // state is accepting, we have to put degen_acc on all
+	      else		// Update existing transition.
-		  // outgoing transitions.  (We are still building a
-		  // TGBA; we only assure that it can be used as an
-		  // SBA.)
-		  bdd acc = bddfalse;
-		  if (is_acc)
-		    acc = degen_acc;
-		  t = res->new_transition(src, dest,
-					  i->current_condition(), acc);
-		}
-	      else
-		{
 		res->trans_data(t).cond |= i->current_condition();
 	    }
-	    }
 	  tr_cache.clear();
 	}
 

src/tgbaalgos/dtbasat.cc

@@ -26,7 +26,6 @@
 #include <utility>
 #include "scc.hh"
 #include "tgba/bddprint.hh"
-#include "ltlast/constant.hh"
 #include "stats.hh"
 #include "misc/satsolver.hh"
 #include "misc/timer.hh"
@@ -673,11 +672,7 @@ namespace spot
       auto autdict = aut->get_dict();
       auto a = new tgba_digraph(autdict);
       autdict->register_all_variables_of(aut, a);
-
+      bdd acc = a->set_single_acceptance_set();
-      const ltl::formula* t = ltl::constant::true_instance();
-      bdd acc = bdd_ithvar(autdict->register_acceptance_variable(t, a));
-      a->set_acceptance_conditions(acc);
-
       a->new_states(satdict.cand_size);
 
       unsigned last_aut_trans = -1U;
@@ -710,16 +705,13 @@ namespace spot
 	      if (seen_trans.insert(src_cond(t->second.src,
 					     t->second.cond)).second)
 		{
-		  bdd accept = bddfalse;
 		  // Mark the transition as accepting if the source is.
-		  if (state_based
+		  bool accept = state_based
-		      && acc_states.find(t->second.src) != acc_states.end())
+		    && acc_states.find(t->second.src) != acc_states.end();
-		    accept = acc;
 
-		  last_aut_trans = a->new_transition(t->second.src - 1,
+		  last_aut_trans =
-						     t->second.dst - 1,
+		    a->new_acc_transition(t->second.src - 1, t->second.dst - 1,
-						     t->second.cond,
+					  t->second.cond, accept);
-						     accept);
 		  last_sat_trans = &t->second;
 
 		  dout << v << '\t' << t->second << "δ\n";

src/tgbaalgos/dtgbacomp.cc

@@ -18,7 +18,6 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include "dtgbacomp.hh"
-#include "ltlast/constant.hh"
 #include "dupexp.hh"
 
 namespace spot
@@ -28,18 +27,12 @@ namespace spot
     // Clone the original automaton.
     tgba_digraph* res = tgba_dupexp_dfs(aut);
 
-    auto dict = res->get_dict();
-
     bdd oldaccs = aut->all_acceptance_conditions();
     bdd oldnegs = aut->neg_acceptance_conditions();
 
     // We will modify res in place, and the resulting
     // automaton will only have one acceptance set.
-    dict->unregister_all_typed_variables(bdd_dict::acc, res);
+    res->set_single_acceptance_set();
-    bdd theacc =
-      bdd_ithvar(dict->register_acceptance_variable
-		 (ltl::constant::true_instance(), res));
-    res->set_acceptance_conditions(theacc);
 
     unsigned num_acc =  aut->number_of_acceptance_conditions();
     unsigned n = res->num_states();
@@ -48,7 +41,7 @@ namespace spot
     res->new_states(num_acc * n + 1);
     unsigned sink = res->num_states() - 1;
     // The sink state has an accepting self-loop.
-    res->new_transition(sink, sink, bddtrue, theacc);
+    res->new_acc_transition(sink, sink, bddtrue);
 
     for (unsigned src = 0; src < n; ++src)
       {
@@ -85,7 +78,7 @@ namespace spot
 		if (h == bddfalse)
 		  {
 		    // Clone the transition
-		    res->new_transition(src + add, dst + add, cond, theacc);
+		    res->new_acc_transition(src + add, dst + add, cond);
 		    assert(dst + add < sink);
 		    // Using `t' is disallowed from now on as it is a
 		    // reference to a transition that may have been