sccfilter: ignore more acceptance conditions

* src/tgbaalgos/sccfilter.cc: Compute useless variable SCC-wise, then
renumber the useful variables so that they can be shared between SCCs.
* src/tgbatest/sccsimpl.test, src/tgbatest/ltl2ta.test: Adjust test
cases.

src/tgbaalgos/sccfilter.cc

@@ -1,5 +1,6 @@
-// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+// -*- coding: utf-8 -*-
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,13 +21,15 @@
 #include "tgba/tgbaexplicit.hh"
 #include "reachiter.hh"
 #include "tgbaalgos/scc.hh"
-#include "misc/bddop.hh"
-#include <sstream>
 
 namespace spot
 {
   namespace
   {
+    // BDD.id -> Acc number
+    typedef std::map<int, unsigned> accremap_t;
+    typedef std::vector<accremap_t> remap_table_t;
+
     static
     state_explicit_number::transition*
     create_transition(const tgba*, tgba_explicit_number* out_aut,
@@ -67,20 +70,90 @@ namespace spot
     {
     public:
       typedef T output_t;
+      typedef std::map<int, bdd> map_t;
+      typedef std::vector<map_t> remap_t;
 
       filter_iter(const tgba* a,
 		  const scc_map& sm,
 		  const std::vector<bool>& useless,
-		  bdd useful, bdd strip, bool remove_all_useless)
+		  remap_table_t& remap_table,
+		  unsigned max_num,
+		  const std::vector<unsigned>& max_table,
+		  bool remove_all_useless)
 	: tgba_reachable_iterator_depth_first(a),
 	  out_(new T(a->get_dict())),
 	  sm_(sm),
 	  useless_(useless),
-	  useful_(useful),
+	  max_num_(max_num),
-	  strip_(strip),
+	  all_(remove_all_useless),
-	  all_(remove_all_useless)
+	  acc_(max_num)
       {
-	out_->set_acceptance_conditions(useful);
+	acc_[0] = bddfalse;
+	bdd tmp = a->all_acceptance_conditions();
+	bdd_dict* d = a->get_dict();
+	assert(a->number_of_acceptance_conditions() >= max_num_ - 1);
+	if (tmp != bddfalse)
+	  {
+	    for (unsigned n = max_num_ - 1; n > 0; --n)
+	      {
+		assert(tmp != bddfalse);
+		const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp));
+		out_->declare_acceptance_condition(a->clone());
+		tmp = bdd_low(tmp);
+	      }
+	    tmp = a->all_acceptance_conditions();
+	    for (unsigned n = max_num_ - 1; n > 0; --n)
+	      {
+		const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp));
+		acc_[n] = out_->get_acceptance_condition(a->clone());
+		tmp = bdd_low(tmp);
+	      }
+	  }
+	else
+	  {
+	    assert(max_num_ == 1);
+	  }
+
+	unsigned c = sm.scc_count();
+	remap_.resize(c);
+	bdd all_orig_neg = aut_->neg_acceptance_conditions();
+	bdd all_sup = bdd_support(all_orig_neg);
+
+	for (unsigned n = 0; n < c; ++n)
+	  {
+	    if (!sm.accepting(n))
+	      continue;
+
+	    bdd missingacc = bddfalse;
+	    for (unsigned a = max_table[n]; a < max_num_; ++a)
+	      missingacc |= acc_[a];
+
+	    bdd all = sm.useful_acc_of(n);
+	    while (all != bddfalse)
+	      {
+		bdd one = bdd_satoneset(all, all_sup, bddtrue);
+		all -= one;
+		bdd res = bddfalse;
+		bdd resacc = bddfalse;
+		while (one != bddtrue)
+		  {
+		    if (bdd_high(one) == bddfalse)
+		      {
+			one = bdd_low(one);
+			continue;
+		      }
+		    int vn = bdd_var(one);
+		    bdd v = bdd_ithvar(vn);
+		    resacc |= bdd_exist(all_orig_neg, v) & v;
+		    res |= acc_[remap_table[n][vn]];
+		    one = bdd_high(one);
+		  }
+		if (res != bddfalse)
+		  res |= missingacc;
+		int id = resacc.id();
+		remap_[n][id] = res;
+	      }
+	  }
       }
 
       T*
@@ -112,20 +185,24 @@ namespace spot
 	//
 	// (See the documentation of scc_filter() for a rational.)
 	unsigned u = sm_.scc_of_state(out_s);
-	if (sm_.accepting(u)
+	unsigned v = sm_.scc_of_state(in_s);
-	    && (!all_ || u == sm_.scc_of_state(in_s)))
+	if (sm_.accepting(u) && (!all_ || u == v))
-	  out_->add_acceptance_conditions
+	  {
-	    (t, (bdd_exist(si->current_acceptance_conditions(), strip_)
+	    bdd acc = si->current_acceptance_conditions();
-		 & useful_));
+	    if (acc == bddfalse)
+	      return;
+	    t->acceptance_conditions = remap_[u][acc.id()];
+	  }
       }
 
     private:
       T* out_;
       const scc_map& sm_;
       const std::vector<bool>& useless_;
-      bdd useful_;
+      unsigned max_num_;
-      bdd strip_;
       bool all_;
+      std::vector<bdd> acc_;
+      remap_t remap_;
     };
 
   } // anonymous
@@ -137,48 +214,96 @@ namespace spot
     sm.build_map();
     scc_stats ss = build_scc_stats(sm);
 
-    bdd useful = ss.useful_acc;
+    remap_table_t remap_table(ss.scc_total);
-    bdd negall = aut->neg_acceptance_conditions();
+    std::vector<unsigned> max_table(ss.scc_total);
-    // Compute a set of useless acceptance conditions.
+    unsigned max_num = 1;
-    // If the acceptance combinations occurring in
-    // the automata are  { a, ab, abc, bd }, then
-    // USEFUL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d)
-    // and we want to find that 'a' and 'b' are useless because
-    // they always occur with 'c'.
-    // The way we check if 'a' is useless that is to look whether
-    // USEFUL implies (x -> a) for some other acceptance condition x.
-    bdd allconds = bdd_support(negall);
-    bdd allcondscopy = allconds;
-    bdd useless = bddtrue;
-    while (allconds != bddtrue)
-      {
-	bdd a = bdd_ithvar(bdd_var(allconds));
-	bdd others = allcondscopy;
 
-	while (others != bddtrue)
+    for (unsigned n = 0; n < ss.scc_total; ++n)
+      {
+	if (!sm.accepting(n))
+	  continue;
+	bdd all = sm.useful_acc_of(n);
+	bdd negall = aut->neg_acceptance_conditions();
+
+	// Compute a set of useless acceptance conditions.
+	// If the acceptance combinations occurring in
+	// the automata are  { a, ab, abc, bd }, then
+	// ALL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d)
+	// and we want to find that 'a' and 'b' are useless because
+	// they always occur with 'c'.
+	// The way we check if 'a' is useless is to look whether ALL
+	// implies (x -> a) for some other acceptance condition x.
+	bdd allconds = bdd_support(negall);
+	bdd allcondscopy = allconds;
+	bdd useless = bddtrue;
+	while (allconds != bddtrue)
 	  {
-	    bdd x = bdd_ithvar(bdd_var(others));
+	    // Speed-up the computation of implied acceptance by
-	    if (x != a)
+	    // removing those that are always present.  We detect
+	    // those that appear as conjunction of positive variables
+	    // at the start of ALL.
+	    bdd prefix = bdd_satprefix(all);
+	    if (prefix != bddtrue)
 	      {
-		if (bdd_implies(useful, x >> a))
+		assert(prefix == bdd_support(prefix));
+		allcondscopy = bdd_exist(allcondscopy, prefix);
+		if (allcondscopy != bddtrue)
 		  {
-		    // a is useless
+		    useless &= prefix;
-		    useful = bdd_exist(useful, a);
+		  }
+		else
+		  {
+		    // Never erase all conditions: at least keep one.
+		    useless &= bdd_high(prefix);
+		    break;
+		  }
+		allconds = bdd_exist(allconds, prefix);
+	      }
+
+	    // Pick a non-useless acceptance condition a.
+	    bdd a = bdd_ithvar(bdd_var(allconds));
+	    // For all acceptance condition x that is not already useless...
+	    bdd others = allcondscopy;
+	    while (others != bddtrue)
+	      {
+		bdd x = bdd_ithvar(bdd_var(others));
+		// ... check whether it always implies a.
+		if (x != a && bdd_implies(all, x >> a))
+		  {
+		    // If so, a is useless.
+		    all = bdd_exist(all, a);
 		    useless &= a;
 		    allcondscopy = bdd_exist(allcondscopy, a);
 		    break;
 		  }
+		others = bdd_high(others);
 	      }
-	    others = bdd_high(others);
+	    allconds = bdd_high(allconds);
 	  }
-	allconds = bdd_high(allconds);
+
+	// We never remove ALL acceptance marks.
+	assert(negall == bddtrue || useless != bdd_support(negall));
+
+	bdd useful = bdd_exist(negall, useless);
+
+	// Go over all useful sets of acceptance marks, and give them
+	// a number.
+	unsigned num = 1;
+	// First compute the number of acceptance conditions used.
+	for (BDD c = useful.id(); c != 1; c = bdd_low(c))
+	  ++num;
+	max_table[n] = num;
+	if (num > max_num)
+	  max_num = num;
+	// Then number all of these acceptance conditions in the
+	// reverse order.  This makes sure that the associated number
+	// varies in the same direction as the bdd variables, which in
+	// turn makes sure we preserve the acceptance condition
+	// ordering (which matters for degeneralization).
+	for (BDD c = useful.id(); c != 1; c = bdd_low(c))
+	  remap_table[n].insert(std::make_pair(bdd_var(c), --num));
       }
 
-    // We never remove ALL acceptance conditions.
-    assert(negall == bddtrue || useless != bdd_support(negall));
-
-    useful = compute_all_acceptance_conditions(bdd_exist(negall, useless));
-
     // In most cases we will create a tgba_explicit_string copy of the
     // initial tgba, but this is not very space efficient as the
     // labels are built using the "format_state()" string output of
@@ -190,8 +315,8 @@ namespace spot
     if (af)
       {
 	filter_iter<tgba_explicit_formula> fi(af, sm, ss.useless_scc_map,
-					      useful, useless,
+					      remap_table, max_num,
-					      remove_all_useless);
+					      max_table, remove_all_useless);
 	fi.run();
 	tgba_explicit_formula* res = fi.result();
 	res->merge_transitions();
@@ -202,8 +327,8 @@ namespace spot
     if (as)
       {
 	filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map,
-					     useful, useless,
+					     remap_table, max_num,
-					     remove_all_useless);
+					     max_table, remove_all_useless);
 	fi.run();
 	tgba_explicit_string* res = fi.result();
 	res->merge_transitions();
@@ -212,8 +337,8 @@ namespace spot
     else
       {
 	filter_iter<tgba_explicit_number> fi(aut, sm, ss.useless_scc_map,
-					     useful, useless,
+					     remap_table, max_num,
-					     remove_all_useless);
+					     max_table, remove_all_useless);
 	fi.run();
 	tgba_explicit_number* res = fi.result();
 	res->merge_transitions();

src/tgbatest/ltl2ta.test

@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -101,8 +101,8 @@ grep 'states: 21$' stdout
 # Note:  after minimization with -TA -RT.
 # has 20 states and 89 transitions, after minimization.
 ../ltl2tgba -ks -TA -RT  -DS "$f" > stdout
-grep 'transitions: 89$' stdout
+grep 'transitions: 85$' stdout
-grep 'states: 20$' stdout
+grep 'states: 19$' stdout
 
 
 f='GFa & GFb & GFc & GFd & GFe & GFg'
@@ -119,12 +119,12 @@ grep 'states: 290$' stdout
 
 #tests with artificial livelock state:
 run 0 ../ltl2tgba -ks -TA -lv  -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
-grep 'transitions: 882$' stdout
+grep 'transitions: 790$' stdout
-grep 'states: 78$' stdout
+grep 'states: 66$' stdout
 
 run 0 ../ltl2tgba -TA -RT -ks -lv -DS  "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
-grep 'transitions: 440$' stdout
+grep 'transitions: 390$' stdout
-grep 'states: 28$' stdout
+grep 'states: 26$' stdout
 
 run 0 ../ltl2tgba -TGTA -RT -ks  'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout
 grep 'transitions: 294$' stdout
@@ -153,16 +153,16 @@ grep 'states: 32$' stdout
 
 
 run 0 ../ltl2tgba -TA -RT -ks -in -R3 -x  -DS  "$f" >stdout
-grep 'transitions: 436$' stdout
+grep 'transitions: 450$' stdout
-grep 'states: 36$' stdout
+grep 'states: 38$' stdout
 
 run 0 ../ltl2tgba -TA -RT -ks -sp -lv -R3 -x   -DS "$f" >stdout
-grep 'transitions: 537$' stdout
+grep 'transitions: 551$' stdout
-grep 'states: 38$' stdout
+grep 'states: 40$' stdout
 
 
 run 0 ../ltl2tgba -TA -ks -sp -lv -DS "$f" >stdout
-grep 'transitions: 609$' stdout
+grep 'transitions: 597$' stdout
 grep 'states: 46$' stdout
 
 
@@ -177,7 +177,7 @@ grep 'states: 32$' stdout
 g="G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))"
 
 run 0 ../ltl2tgba -TA -RT -ks -DS "$g" >stdout
-grep 'transitions: 2147$' stdout
+grep 'transitions: 2133$' stdout
 grep 'states: 97$' stdout
 
 

src/tgbatest/sccsimpl.test

@@ -1,6 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+# Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement
-# l'Epita
+# de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -54,7 +54,7 @@ S4, S4, "!p1",;
 EOF
 
 run 0 ../ltl2tgba -X -R3 -b aut.txt > out.txt
-grep '^acc = "p1";$' out.txt
+grep '^acc = "[^"]*";$' out.txt
 
 
 # Here, acceptances A and C can both be removed.
@@ -66,7 +66,7 @@ S1, S1, "c", A B C;
 S1, S1, "d", C D;
 EOF
 run 0 ../ltl2tgba -X -R3 -b aut2.txt > out2.txt
-grep '^acc = "B" "D";$' out2.txt || grep '^acc = "D" "B";$' out2.txt || exit 1
+grep '^acc = "." ".";$' out2.txt || exit 1
 # only 4 lines output, because the "b" and "c" lines have been merged.
 test `wc -l < out2.txt` = 4
 
@@ -80,7 +80,7 @@ S1, S1, "c", A B C;
 S1, S1, "d", B D;
 EOF
 run 0 ../ltl2tgba -X -R3 -b aut3.txt > out3.txt
-grep '^acc = "C" "D";$' out3.txt || grep '^acc = "D" "C";$' out3.txt || exit 1
+grep '^acc = "." ".";$' out3.txt || exit 1
 # only 4 lines output, because the "a" and "b" lines have been merged.
 test `wc -l < out3.txt` = 4
 
@@ -158,6 +158,4 @@ S6, S6, "(p1 & !p2) | (p3 & !p2)", ZZ "!p2";
 S6, S6, "p1 | p2 | p3", ZZ;
 EOF
 run 0 ../ltl2tgba -X -R3 -b aut7.txt > out7.txt
-# ZZ should disappear
-grep ZZ out7.txt && exit 1
 test `grep '^acc' out7.txt | wc -w` = 4