From a160b3504bc580ef5874b01bbeaae0e28f079352 Mon Sep 17 00:00:00 2001
From: Guillaume Sadegh <sadegh@lrde.epita.fr>
Date: Tue, 7 Jul 2009 14:07:52 +0200
Subject: [PATCH] * src/tgba/tgbacomplement.cc: Fix the transformation from
 Streett to TGBA. * src/tgbatest/complementation.test: Modify tests.

---
 ChangeLog                         |  6 +++
 src/tgba/tgbacomplement.cc        | 62 ++++++++++++++++++++++---------
 src/tgbatest/complementation.test |  2 -
 3 files changed, 50 insertions(+), 20 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index a7e15c273..4ae76de91 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2009-07-07  Guillaume Sadegh  <sadegh@lrde.epita.fr>
+
+	* src/tgba/tgbacomplement.cc: Fix the transformation from
+	Streett to TGBA.
+	* src/tgbatest/complementation.test: Modify tests.
+
 2009-06-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.0.
diff --git a/src/tgba/tgbacomplement.cc b/src/tgba/tgbacomplement.cc
index f7d8486ba..2aa048d6a 100644
--- a/src/tgba/tgbacomplement.cc
+++ b/src/tgba/tgbacomplement.cc
@@ -976,7 +976,6 @@ namespace spot
         ss << " J:" << L;
 #endif
       }
-
       return ss.str();
     }
 
@@ -1153,7 +1152,7 @@ namespace spot
   /// @brief Compute successors of the state @a local_state, and returns an
   /// iterator on the successors collection.
   ///
-  /// This algorithm is a Deterministic Streett to nondeterministic Büchi
+  /// The old algorithm is a Deterministic Streett to nondeterministic Büchi
   /// transformation, presented by Christof Löding in his Diploma thesis.
   ///
   /// @MastersThesis{	  loding.98,
@@ -1164,6 +1163,24 @@ namespace spot
   ///   year		= {1998}
   /// }
   ///
+  ///
+  /// The new algorithm produce a TGBA instead of a TBA. This algorithm
+  /// comes from:
+  ///
+  /// @InProceedings{   duret.09.atva,
+  ///   author        = {Alexandre Duret-Lutz and Denis Poitrenaud and Jean-Michel
+  ///                   Couvreur},
+  ///   title         = {On-the-fly Emptiness Check of Transition-based {S}treett
+  ///                   Automata},
+  ///   booktitle     = {Proceedings of the 7th International Symposium on
+  ///                   Automated Technology for Verification and Analysis
+  ///                   (ATVA'09)},
+  ///   year          = {2009},
+  ///   editor        = {Zhiming Liu and Anders P. Ravn},
+  ///   series        = {Lecture Notes in Computer Science},
+  ///   publisher     = {Springer-Verlag}
+  /// }
+  ///
   /// @param local_state
   ///
   tgba_succ_iterator*
@@ -1203,9 +1220,11 @@ namespace spot
         u.flip();
         s->get_safra()->getL(l); // {i : q \in L_i}
         s->get_safra()->getU(u); // {j : q \in U_i}
+        state_complement* st;
+
+#if TRANSFORM_TO_TBA
         bitset_t newI = s->get_L() | l; // {I' = I \cup {i : q \in L_i}}
         bitset_t newJ = s->get_U() | u; // {J' = J \cup {j : q \in U_i}}
-        state_complement* st;
 
         if (newI.is_subset_of(newJ)) // \delta'((q, I, J), a) if I'\subseteq J'
         {
@@ -1214,21 +1233,7 @@ namespace spot
             st = new state_complement(e, e, i->second, true);
             succ_list.insert(std::make_pair(i->first, st));
           }
-
-#if TRANSFORM_TO_TBA
           condition = the_acceptance_cond_;
-#else
-          for (unsigned i = 0; i < l.size(); ++i)
-          {
-            if (u[i])
-            {
-              if (condition == bddfalse)
-                condition = bdd_ithvar(acceptance_cond_vec_[i]);
-              else
-                condition &= bdd_ithvar(acceptance_cond_vec_[i]);
-            }
-          }
-#endif
         }
         else  // \delta'((q, I, J), a)
         {
@@ -1238,11 +1243,32 @@ namespace spot
             succ_list.insert(std::make_pair(i->first, st));
           }
         }
+#else
+        bitset_t S = s->get_L();
+        bitset_t pending = (S | l) - u;  // {pending = S \cup {i : q \in L_i}
+                                          // \setminus {j : q \in U_j})}
+        for (trans_iter i = tr->second.begin(); i != tr->second.end(); ++i)
+        {
+          st = new state_complement(pending, e, i->second, true);
+          succ_list.insert(std::make_pair(i->first, st));
+        }
+
+        for (unsigned i = 0; i < l.size(); ++i)
+        {
+          if (!S[i])
+          {
+            if (condition == bddfalse)
+              condition = bdd_ithvar(acceptance_cond_vec_[i]);
+            else
+              condition &= bdd_ithvar(acceptance_cond_vec_[i]);
+          }
+        }
+#endif
       }
 
       return new tgba_complement_succ_iterator(succ_list, condition);
     }
-    assert("Safra automaton do not find this node");
+    assert("Safra automaton does not find this node");
     return 0;
   }
 
diff --git a/src/tgbatest/complementation.test b/src/tgbatest/complementation.test
index 934e4df67..5b5c31444 100755
--- a/src/tgbatest/complementation.test
+++ b/src/tgbatest/complementation.test
@@ -35,6 +35,4 @@ GFa&&FGa
 [] ((p2 && ! p1) -> (p0 U (p1 || [] p0)))
 [] (p2 -> ((! p0 && ! p1) U (p1 || ((p0 && ! p1) U (p1 || ((! p0 && ! p1) \
  U (p1 || ((p0 && ! p1) U ((p1 || (! p0 U (p1 || [] ! p0))) || [] p0)))))))))
-(p0 U (p1 && X (p2 && (true U (p3 && X (true U (p4 && X \
-(true U (p5 && X (true U p6))))))))))
 EOF