Strip useless acceptance conditions in scc_filter().

A useless acceptance conditions is one that is always implied by
another.

* src/misc/bddop.hh, src/misc/bddop.cc
(compute_neg_acceptance_conditions): New function.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(set_acceptance_conditions): New function.
* src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot):
Keep track of useful acceptance conditions.
(useful_acc_of): New function.
* src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New
attributes.
* src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter
useless acceptance conditions.
(scc_filter): Compute useful acceptance conditions and pass them
to filter_iter.

ChangeLog

@@ -1,3 +1,24 @@
+2009-11-20  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Strip useless acceptance conditions in scc_filter().
+
+	A useless acceptance conditions is one that is always implied by
+	another.
+
+	* src/misc/bddop.hh, src/misc/bddop.cc
+	(compute_neg_acceptance_conditions): New function.
+	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
+	(set_acceptance_conditions): New function.
+	* src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot):
+	Keep track of useful acceptance conditions.
+	(useful_acc_of): New function.
+	* src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New
+	attributes.
+	* src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter
+	useless acceptance conditions.
+	(scc_filter): Compute useful acceptance conditions and pass them
+	to filter_iter.
+
 2009-11-20  Alexandre Duret-Lutz  <adl@va-et-vient.net>
 
 	* src/tgbaalgos/sccfilter.cc (scc_filter): Merge transitions

src/misc/bddop.cc

@@ -48,4 +48,19 @@ namespace spot
 
     return all;
   }
+
+  bdd
+  compute_neg_acceptance_conditions(bdd all_acceptance_conditions)
+  {
+    bdd cur = bdd_support(all_acceptance_conditions);
+    bdd neg = bddtrue;
+    while (cur != bddtrue)
+      {
+	neg &= bdd_nithvar(bdd_var(cur));
+	assert(bdd_low(cur) != bddtrue);
+	cur = bdd_high(cur);
+      }
+    return neg;
+  }
+
 }

src/misc/bddop.hh

@@ -29,6 +29,10 @@ namespace spot
   /// \brief Compute all acceptance conditions from all neg acceptance
   /// conditions.
   bdd compute_all_acceptance_conditions(bdd neg_acceptance_conditions);
+
+  /// \brief Compute neg acceptance conditions from all acceptance
+  /// conditions.
+  bdd compute_neg_acceptance_conditions(bdd all_acceptance_conditions);
 }
 
 #endif // SPOT_MISC_BDDOP_HH

src/tgba/tgbaexplicit.cc

@@ -159,6 +159,17 @@ namespace spot
     neg_acceptance_conditions_ = f;
   }
 
+  void
+  tgba_explicit::set_acceptance_conditions(bdd acc)
+  {
+    assert(neg_acceptance_conditions_ == bddtrue);
+    assert(all_acceptance_conditions_computed_ == false);
+    dict_->register_acceptance_variables(bdd_support(acc), this);
+    neg_acceptance_conditions_ = compute_neg_acceptance_conditions(acc);
+    all_acceptance_conditions_computed_ = true;
+    all_acceptance_conditions_ = acc;
+  }
+
   bool
   tgba_explicit::has_acceptance_condition(const ltl::formula* f) const
   {

src/tgba/tgbaexplicit.hh

@@ -69,6 +69,9 @@ namespace spot
     /// transition.
     void copy_acceptance_conditions_of(const tgba *a);
 
+    /// The the acceptance conditions.
+    void set_acceptance_conditions(bdd acc);
+
     bool has_acceptance_condition(const ltl::formula* f) const;
     void add_acceptance_condition(transition* t, const ltl::formula* f);
     /// This assumes that all acceptance conditions in \a f are known from dict.

src/tgbaalgos/scc.cc

@@ -259,13 +259,17 @@ namespace spot
 	cond_set conds;
 	conds.insert(cond);
 	bdd supp = bdd_support(cond);
+	bdd all = aut_->all_acceptance_conditions();
+	bdd useful = all - acc;
 	while (threshold > root_.front().index)
 	  {
 	    assert(!root_.empty());
 	    assert(!arc_acc_.empty());
 	    assert(arc_acc_.size() == arc_cond_.size());
 	    acc |= root_.front().acc;
-	    acc |= arc_acc_.top();
+	    bdd lacc = arc_acc_.top();
+	    acc |= lacc;
+	    useful |= (all - lacc) | root_.front().useful_acc;
 	    states.splice(states.end(), root_.front().states);
 	    succs.insert(root_.front().succ.begin(),
 			 root_.front().succ.end());
@@ -292,6 +296,7 @@ namespace spot
 	root_.front().supp &= supp;
 	// This SCC is no longer trivial.
 	root_.front().trivial = false;
+	root_.front().useful_acc |= useful;
       }
 
     // recursively update supp_rec
@@ -347,6 +352,13 @@ namespace spot
     return scc_map_.size();
   }
 
+  bdd
+  scc_map::useful_acc_of(unsigned n) const
+  {
+    assert(scc_map_.size() > n);
+    return scc_map_[n].useful_acc;
+  }
+
   namespace
   {
     struct scc_recurse_data
@@ -422,8 +434,14 @@ namespace spot
     res.dead_paths = d.dead_paths[init];
 
     res.useless_scc_map.reserve(res.scc_total);
+    bdd useful_acc = bddfalse;
     for (unsigned n = 0; n < res.scc_total; ++n)
-      res.useless_scc_map[n] = !d.acc_paths[n];
+      {
+	res.useless_scc_map[n] = !d.acc_paths[n];
+	if (m.accepting(n))
+	  useful_acc |= m.useful_acc_of(n);
+      }
+    res.useful_acc = useful_acc;
 
     return res;
   }
@@ -481,7 +499,10 @@ namespace spot
 				      m.ap_set_of(state)));
 	    ostr << "]\\n APrec=[";
 	    escape_str(ostr, bdd_format_sat(m.get_aut()->get_dict(),
-					    m.aprec_set_of(state))) << "]";
+					    m.aprec_set_of(state)));
+	    ostr << "]\\n useful=[";
+	    escape_str(ostr, bdd_format_accset(m.get_aut()->get_dict(),
+					       m.useful_acc_of(state))) << "]";
 	  }
 
 	std::cout << "  " << state << " [shape=box,"

src/tgbaalgos/scc.hh

@@ -59,6 +59,11 @@ namespace spot
     /// A map of the useless SCCs.
     std::vector<bool> useless_scc_map;
 
+    /// The set of useful acceptance conditions (i.e. acceptance
+    /// conditions that are not always implied by other acceptance
+    /// conditions).
+    bdd useful_acc;
+
     std::ostream& dump(std::ostream& out) const;
   };
 
@@ -129,6 +134,12 @@ namespace spot
     /// \pre This should only be called once build_map() has run.
     bdd acc_set_of(unsigned n) const;
 
+    /// \brief Return the set of useful acceptance conditions if SCC \a n.
+    ///
+    /// Useless acceptances conditions are always implied by other acceptances
+    /// conditions.  This returns all the other acceptance conditions.
+    bdd useful_acc_of(unsigned n) const;
+
     /// \brief Return the set of states of an SCC.
     ///
     /// The states in the returned list are still owned by the scc_map
@@ -154,7 +165,7 @@ namespace spot
     public:
       scc(int index) : index(index), acc(bddfalse),
 		       supp(bddtrue), supp_rec(bddfalse),
-		       trivial(true) {};
+		       trivial(true), useful_acc(bddfalse) {};
       /// Index of the SCC.
       int index;
       /// The union of all acceptance conditions of transitions which
@@ -172,6 +183,8 @@ namespace spot
       succ_type succ;
       /// Trivial SCC have one state and no self-loops.
       bool trivial;
+      /// Useful acceptance conditions.
+      bdd useful_acc;
     };
 
     const tgba* aut_;		// Automata to decompose.

src/tgbaalgos/sccfilter.cc

@@ -33,14 +33,16 @@ namespace spot
     public:
       filter_iter(const tgba* a,
 		  const scc_map& sm,
-		  const std::vector<bool>& useless)
+		  const std::vector<bool>& useless,
+		  bdd useful, bdd strip)
 	: tgba_reachable_iterator_depth_first(a),
 	  out_(new tgba_explicit_string(a->get_dict())),
 	  sm_(sm),
-	  useless_(useless)
+	  useless_(useless),
-
+	  useful_(useful),
+	  strip_(strip)
       {
-	out_->copy_acceptance_conditions_of(a);
+	out_->set_acceptance_conditions(useful);
       }
 
       tgba_explicit_string*
@@ -73,14 +75,17 @@ namespace spot
 	// the destination state do not belong to an accepting state.
 	if (sm_.accepting(sm_.scc_of_state(in_s))
 	    && sm_.accepting(sm_.scc_of_state(out_s)))
-	  out_->add_acceptance_conditions(t,
+	  out_->add_acceptance_conditions
-					  si->current_acceptance_conditions());
+	    (t, (bdd_exist(si->current_acceptance_conditions(), strip_)
+		 & useful_));
       }
 
     private:
       tgba_explicit_string* out_;
       const scc_map& sm_;
       const std::vector<bool>& useless_;
+      bdd useful_;
+      bdd strip_;
     };
   } // anonymous
 
@@ -91,7 +96,33 @@ namespace spot
     sm.build_map();
     scc_stats ss = build_scc_stats(sm);
 
-    filter_iter fi(aut, sm, ss.useless_scc_map);
+    bdd useful = ss.useful_acc;
+    if (useful == bddfalse)
+      // Even if no acceptance conditions are useful in a SCC,
+      // we need to keep at least one acceptance conditions
+      useful = bdd_satone(aut->all_acceptance_conditions());
+
+    bdd positive = bddtrue;
+    bdd cur = useful;
+    while (cur != bddfalse)
+      {
+	bdd a = bdd_satone(cur);
+	cur -= a;
+	for (;;)
+	  {
+	    if (bdd_low(a) == bddfalse)
+	      {
+		positive &= bdd_ithvar(bdd_var(a));
+		break;
+	      }
+	    a = bdd_low(a);
+	  }
+      }
+
+    bdd strip = bdd_exist(bdd_support(aut->all_acceptance_conditions()),
+			  positive);
+    useful = bdd_exist(useful, strip);
+    filter_iter fi(aut, sm, ss.useless_scc_map, useful, strip);
     fi.run();
     tgba_explicit_string* res = fi.result();
     res->merge_transitions();