From ff8fe6802b7933761642d719edc88dcbeef0877b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 18 Feb 2005 14:13:26 +0000
Subject: [PATCH] * src/tgbaalgos/tau03opt.cc (tau03_opt_search): Implement the
 "condition heuristic".  Suggested by Heikki Tauriainen. *
 src/tgbatest/randtgba.cc: Test it.

---
 ChangeLog                 |  4 ++
 src/tgbaalgos/tau03opt.cc | 84 +++++++++++++++++++++++++++------------
 src/tgbatest/randtgba.cc  |  1 +
 3 files changed, 63 insertions(+), 26 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 02cdd6a1c..ff5be947c 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,9 @@
 2005-02-18  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/tau03opt.cc (tau03_opt_search): Implement the
+	"condition heuristic".  Suggested by Heikki Tauriainen.
+	* src/tgbatest/randtgba.cc: Test it.
+
 	* src/tgbatest/randtgba.cc: Remplace the -O option by -A, reading
 	all algorithms from a file.  Use the emptiness_check_instantiator
 	syntax as name in the output.
diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc
index 1e4d21bda..9bc63a66b 100644
--- a/src/tgbaalgos/tau03opt.cc
+++ b/src/tgbaalgos/tau03opt.cc
@@ -41,6 +41,7 @@
 #endif
 
 #include <cassert>
+#include <stack>
 #include "misc/hash.hh"
 #include "tgba/tgba.hh"
 #include "emptiness.hh"
@@ -66,7 +67,8 @@ namespace spot
         : emptiness_check(a, o),
           current_weight(a->neg_acceptance_conditions()),
           h(size),
-          all_acc(a->all_acceptance_conditions())
+          all_acc(a->all_acceptance_conditions()),
+	  use_condition_stack(o.get("condstack"))
       {
       }
 
@@ -161,6 +163,9 @@ namespace spot
       /// The unique accepting condition of the automaton \a a.
       bdd all_acc;
 
+      /// Whether to use the "condition stack".
+      bool use_condition_stack;
+
       bool dfs_blue()
       {
         while (!st_blue.empty())
@@ -266,10 +271,16 @@ namespace spot
         return false;
       }
 
-      bool dfs_red(const bdd& acu)
+      bool
+      dfs_red(bdd acu)
       {
         assert(!st_red.empty());
 
+	// These are useful only when USE_CONDITION_STACK is set.
+	typedef std::pair<bdd, unsigned> cond_level;
+	std::stack<cond_level> condition_stack;
+	unsigned depth = 1;
+
         while (!st_red.empty())
           {
             stack_item& f = st_red.front();
@@ -290,30 +301,38 @@ namespace spot
                     trace << "  It is white, pop it" << std::endl;
                     delete s_prime;
                   }
-                 else if (c_prime.get_color() == CYAN &&
-                     ((current_weight - c_prime.get_weight()) |
-                                c_prime.get_acc() | acu) == all_acc)
-                  {
-                    trace << "  It is cyan and acceptance condition "
-                          << "is reached, report cycle" << std::endl;
-                    c_prime.cumulate_acc(acu);
-                    push(st_red, s_prime, label, acc);
-                    return true;
-                  }
-                else if ((c_prime.get_acc() & acu) != acu)
-                  {
-                    trace << "  It is cyan or blue and propagation "
-                          << "is needed, go down"
-                          << std::endl;
-                    c_prime.cumulate_acc(acu);
-                    push(st_red, s_prime, label, acc);
-                  }
-                else
-                  {
-                    trace << "  It is cyan or blue and no propagation "
-                          << "is needed , pop it" << std::endl;
-                    h.pop_notify(s_prime);
-                  }
+		else if (c_prime.get_color() == CYAN &&
+			 ((current_weight - c_prime.get_weight()) |
+			  c_prime.get_acc() | acu) == all_acc)
+		  {
+		    trace << "  It is cyan and acceptance condition "
+			  << "is reached, report cycle" << std::endl;
+		    c_prime.cumulate_acc(acu);
+		    push(st_red, s_prime, label, acc);
+		    return true;
+		  }
+		else if ((c_prime.get_acc() & acu) != acu)
+		  {
+		    trace << "  It is cyan or blue and propagation "
+			  << "is needed, go down"
+			  << std::endl;
+		    c_prime.cumulate_acc(acu);
+		    push(st_red, s_prime, label, acc);
+		    if (use_condition_stack)
+		      {
+			bdd old = acu;
+			acu = c_prime.get_acc();
+			condition_stack.push(cond_level(acu - old, depth));
+			inc_depth();
+		      }
+		    ++depth;
+		  }
+		else
+		  {
+		    trace << "  It is cyan or blue and no propagation "
+			  << "is needed , pop it" << std::endl;
+		    h.pop_notify(s_prime);
+		  }
               }
             else // Backtrack
               {
@@ -321,8 +340,21 @@ namespace spot
                       << std::endl;
                 h.pop_notify(f.s);
                 pop(st_red);
+		--depth;
+		if (use_condition_stack)
+		  {
+		    while (!condition_stack.empty()
+			   && condition_stack.top().second == depth)
+		      {
+			acu -= condition_stack.top().first;
+			condition_stack.pop();
+			dec_depth();
+		      }
+		  }
               }
           }
+	assert(depth == 0);
+	assert(condition_stack.empty());
         return false;
       }
 
diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc
index 481f8ab0b..35d45d3b5 100644
--- a/src/tgbatest/randtgba.cc
+++ b/src/tgbatest/randtgba.cc
@@ -76,6 +76,7 @@ const char* default_algos[] = {
   "SE05(bsh=4K)",
   "Tau03",
   "Tau03_opt",
+  "Tau03_opt(condstack)",
   0
 };