During the complementation, transform the auxiliary Streett automaton

into a TGBA instead of a TBA.

    * src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc:
    Adjust the transformation from Streett to Büchi to support
    generalized acceptance conditions.
    * src/tgbatest/complementation.cc: Improve output messages.
    * src/tgbatest/complementation.test: New tests.

ChangeLog

@@ -1,6 +1,18 @@
+2009-06-10  Guillaume Sadegh  <sadegh@lrde.epita.fr>
+
+	During the complementation, transform the auxiliary Streett
+	automaton into a TGBA instead of a TBA.
+
+	* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc:
+	Adjust the transformation from Streett to Büchi to support
+	generalized acceptance conditions.
+	* src/tgbatest/complementation.cc: Improve output messages.
+	* src/tgbatest/complementation.test: New tests.
+
 2009-06-09  Guillaume Sadegh  <sadegh@lrde.epita.fr>
 
-	* src/tgba/tgbacomplement.cc, src/tgbatest/complementation.cc: Fix style.
+	* src/tgba/tgbacomplement.cc, src/tgbatest/complementation.cc:
+	Fix style.
 
 2009-06-07  Guillaume Sadegh  <sadegh@lrde.epita.fr>
 

src/tgba/tgbacomplement.cc

@@ -901,7 +901,7 @@ namespace spot
     state_complement::state_complement(bitset_t L, bitset_t U,
                                        const safra_tree* tree,
                                        bool use_bitset)
-      : U(U), L(L), tree(tree), use_bitset(use_bitset)
+      : state(), U(U), L(L), tree(tree), use_bitset(use_bitset)
     {
     }
 
@@ -921,8 +921,11 @@ namespace spot
       const state_complement* s = dynamic_cast<const state_complement*>(other);
       if (s == 0)
         return 1;
+#if TRANSFORM_TO_TBA
+      // When we transform to TBA instead of TGBA, states depend on the U set.
       if (U != s->U)
         return (U < s->U) ? -1 : 1;
+#endif
       if (L != s->L)
         return (L < s->L) ? -1 : 1;
       if (use_bitset != s->use_bitset)
@@ -940,7 +943,9 @@ namespace spot
       for (unsigned i = 0; i < size_bitset; ++i)
       {
         hash ^= wang32_hash(L[i]);
-        hash ^= wang32_hash(U[i]); // \todo To not apply for TGBAs
+#if TRANSFORM_TO_TBA
+        hash ^= wang32_hash(U[i]);
+#endif
       }
 
       return hash;
@@ -964,7 +969,13 @@ namespace spot
       std::stringstream ss;
       ss << tree;
       if (use_bitset)
-        ss << " - I:" << U << " J:" << L;
+      {
+        ss << " - I:" << U;
+#if TRANSFORM_TO_TBA
+        ss << " J:" << L;
+#endif
+      }
+
       return ss.str();
     }
 
@@ -1102,7 +1113,25 @@ namespace spot
     // Let's call it Acc[True].
     int v = get_dict()
       ->register_acceptance_variable(ltl::constant::true_instance(), safra_);
+
+#if TRANSFORM_TO_TBA
     the_acceptance_cond_ = bdd_ithvar(v);
+#endif
+
+#if TRANSFORM_TO_TGBA
+    unsigned nb_acc = safra_->get_nb_acceptance_pairs();
+    all_acceptance_cond_ = bddfalse;
+    neg_acceptance_cond_ = bddtrue;
+    acceptance_cond_vec_.reserve(nb_acc);
+    for (unsigned i = 0; i < nb_acc; ++i)
+    {
+      int r = get_dict()->register_clone_acc(v, safra_);
+      all_acceptance_cond_ |= bdd_ithvar(r);
+      acceptance_cond_vec_[i] = r;
+      neg_acceptance_cond_ &= bdd_nithvar(r);
+    }
+#endif
+
   }
 
   tgba_complement::~tgba_complement()
@@ -1184,7 +1213,21 @@ 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)
         {
@@ -1220,13 +1263,21 @@ namespace spot
   bdd
   tgba_complement::all_acceptance_conditions() const
   {
+#if TRANSFORM_TO_TBA
     return the_acceptance_cond_;
+#else
+    return all_acceptance_cond_;
+#endif
   }
 
   bdd
   tgba_complement::neg_acceptance_conditions() const
   {
+#if TRANSFORM_TO_TBA
     return !the_acceptance_cond_;
+#else
+    return neg_acceptance_cond_;
+#endif
   }
 
   bdd

src/tgba/tgbacomplement.hh

@@ -1,8 +1,14 @@
 #ifndef SPOT_TGBA_TGBACOMPLEMENT_HH
 # define SPOT_TGBA_TGBACOMPLEMENT_HH
 
+# include <vector>
 # include "tgba/tgba.hh"
 
+#ifndef TRANSFORM_TO_TBA
+# define TRANSFORM_TO_TBA 0
+#endif
+#define TRANSFORM_TO_TGBA (!TRANSFORM_TO_TBA)
+
 namespace spot
 {
   struct safra_tree_automaton;
@@ -53,7 +59,16 @@ namespace spot
   private:
     const tgba* automaton_;
     safra_tree_automaton* safra_;
+#if TRANSFORM_TO_TBA
     bdd the_acceptance_cond_;
+#endif
+#if TRANSFORM_TO_TGBA
+    bdd all_acceptance_cond_;
+    bdd neg_acceptance_cond_;
+    // Map to i the i-th acceptance condition of the final automaton.
+    std::vector<int> acceptance_cond_vec_;
+#endif
+
   };
 
   /// \brief Produce a dot output of the Safra automaton associated

src/tgbatest/complementation.cc

@@ -137,19 +137,25 @@ int main(int argc, char* argv[])
     spot::tgba_statistics a_size =  spot::stats_reachable(a);
     std::cout << "Original: "
               << a_size.states << ", "
-              << a_size.transitions << std::endl;
+              << a_size.transitions << ", "
+              << a->number_of_acceptance_conditions()
+              << std::endl;
 
     spot::tgba *buchi = new spot::tgba_sba_proxy(a);
     a_size =  spot::stats_reachable(buchi);
     std::cout << "Buchi: "
               << a_size.states << ", "
-              << a_size.transitions << std::endl;
+              << a_size.transitions << ", "
+              << buchi->number_of_acceptance_conditions()
+              << std::endl;
     delete buchi;
 
     spot::tgba_statistics b_size =  spot::stats_reachable(complement);
     std::cout << "Complement: "
               << b_size.states << ", "
-              << b_size.transitions << std::endl;
+              << b_size.transitions << ", "
+              << complement->number_of_acceptance_conditions()
+              << std::endl;
 
     delete complement;
     delete a;
@@ -162,7 +168,9 @@ int main(int argc, char* argv[])
       spot::tgba_statistics a_size =  spot::stats_reachable(a2);
       std::cout << "Not Formula: "
                 << a_size.states << ", "
-                << a_size.transitions << std::endl;
+                << a_size.transitions << ", "
+                << a2->number_of_acceptance_conditions()
+                << std::endl;
 
       delete a2;
       spot::ltl::destroy(f1);
@@ -187,18 +195,20 @@ int main(int argc, char* argv[])
     spot::emptiness_check* ec = spot::couvreur99(prod);
     spot::emptiness_check_result* res = ec->check();
     spot::tgba_statistics a_size =  spot::stats_reachable(ec->automaton());
-    std::cout << std::right << std::setw(10)
+    std::cout << "States: "
-              << a_size.states << ", "
+              << a_size.states << std::endl
-              << std::right << std::setw(10)
+              << "Transitions: "
-              << a_size.transitions << ", "
+              << a_size.transitions << std::endl
-              << ec->automaton()->number_of_acceptance_conditions();
+              << "Acc Cond: "
+              << ec->automaton()->number_of_acceptance_conditions()
+              << std::endl;
     if (res)
     {
-      std::cout << ", FAIL";
+      std::cout << "FAIL";
       return_value = 1;
     }
     else
-      std::cout << ", OK";
+      std::cout << "OK";
     std::cout << std::endl;
 
     delete res;

src/tgbatest/complementation.test

@@ -24,8 +24,17 @@
 
 set -e
 
-FORMULAE='GFa FGa <>p1->(p0Up1) [](p0-><>p3) GFa&&FGa'
+while read f; do
-
-for f in $FORMULAE; do
     run 0 ./complement -f "$f"
-done
+done <<EOF
+GFa
+FGa
+<>p1->(p0Up1)
+[](p0-><>p3)
+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