Safra: Fix usage of multiple acceptance conditions and fix text output.

* src/tgba/tgbasafracomplement.cc
(tgba_safra_complement::tgba_safra_complement)
(tgba_safra_complement::succ_iter): Correct the declaration and
use of multiple acceptance conditions.
(state_complement::to_string): Output the L set, not U.  The previous
code caused different states to share the same names, causing issues
with the text-based output (state with identical names get merged).
* src/tgba/tgbasafracomplement.hh
(tgba_safra_complement::acceptance_cond_vec_): Adjust type to
store BDDs.
* src/tgbatest/complementation.cc: Implement a new "-b" option
to output automata in Spot's syntax.
* src/tgbatest/complementation.test: Add a test-case supplied
by Martin Dieguez Lodeiro.
* THANKS: Add Martin.

ChangeLog

@@ -1,3 +1,23 @@
+2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Safra: Fix usage of multiple acceptance conditions and fix text output.
+
+	* src/tgba/tgbasafracomplement.cc
+	(tgba_safra_complement::tgba_safra_complement)
+	(tgba_safra_complement::succ_iter): Correct the declaration and
+	use of multiple acceptance conditions.
+	(state_complement::to_string): Output the L set, not U.  The previous
+	code caused different states to share the same names, causing issues
+	with the text-based output (state with identical names get merged).
+	* src/tgba/tgbasafracomplement.hh
+	(tgba_safra_complement::acceptance_cond_vec_): Adjust type to
+	store BDDs.
+	* src/tgbatest/complementation.cc: Implement a new "-b" option
+	to output automata in Spot's syntax.
+	* src/tgbatest/complementation.test: Add a test-case supplied
+	by Martin Dieguez Lodeiro.
+	* THANKS: Add Martin.
+
 2011-10-23  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/tgba/tgbasafracomplement.cc: Fix two asserts.

THANKS

@@ -5,6 +5,7 @@ Heikki Tauriainen
 Jean-Michel Couvreur
 Jean-Michel Ilié
 Kristin Y. Rozier
+Martin Dieguez Lodeiro
 Michael Weber
 Rüdiger Ehlers
 Silien Hong

src/tgba/tgbasafracomplement.cc

@@ -942,8 +942,7 @@ namespace spot
       if (other == this)
         return 0;
       const state_complement* s = down_cast<const state_complement*>(other);
-      if (s == 0)
+      assert(s);
-        return 1;
 #if TRANSFORM_TO_TBA
       // When we transform to TBA instead of TGBA, states depend on the U set.
       if (U != s->U)
@@ -993,9 +992,9 @@ namespace spot
       ss << tree;
       if (use_bitset)
       {
-        ss << " - I:" << U;
+        ss << " - I:" << L;
 #if TRANSFORM_TO_TBA
-        ss << " J:" << L;
+        ss << " J:" << U;
 #endif
       }
       return ss.str();
@@ -1147,14 +1146,19 @@ namespace spot
     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_);
+	int r = get_dict()->register_clone_acc(v, safra_);
-      all_acceptance_cond_ |= bdd_ithvar(r);
+	all_acceptance_cond_ &= bdd_nithvar(r);
-      acceptance_cond_vec_[i] = r;
+	all_acceptance_cond_ |= bdd_ithvar(r) & neg_acceptance_cond_;
-      neg_acceptance_cond_ &= bdd_nithvar(r);
+	neg_acceptance_cond_ &= bdd_nithvar(r);
-    }
+	acceptance_cond_vec_.push_back(bdd_ithvar(r));
+      }
+    for (unsigned i = 0; i < nb_acc; ++i)
+      {
+	bdd c = acceptance_cond_vec_[i];
+	acceptance_cond_vec_[i] = bdd_exist(neg_acceptance_cond_, c) & c;
+      }
 #endif
-
   }
 
   tgba_safra_complement::~tgba_safra_complement()
@@ -1278,15 +1282,8 @@ namespace spot
         }
 
         for (unsigned i = 0; i < l.size(); ++i)
-        {
           if (!S[i])
-          {
+	    condition |= acceptance_cond_vec_[i];
-            if (condition == bddfalse)
-              condition = bdd_ithvar(acceptance_cond_vec_[i]);
-            else
-              condition &= bdd_ithvar(acceptance_cond_vec_[i]);
-          }
-        }
 #endif
       }
 

src/tgba/tgbasafracomplement.hh

@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -84,7 +84,7 @@ namespace spot
     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_;
+    std::vector<bdd> acceptance_cond_vec_;
 #endif
   };
 

src/tgbatest/complementation.cc

@@ -21,6 +21,7 @@
 #include <iomanip>
 #include <iostream>
 #include "tgbaalgos/dotty.hh"
+#include "tgbaalgos/save.hh"
 #include "tgbaparse/public.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/gtec/gtec.hh"
@@ -40,6 +41,7 @@ void usage(const char* prog)
 {
   std::cout << "usage: " << prog << " [options]" << std::endl;
   std::cout << "with options" << std::endl
+            << "-b                      Output in spot's format" << std::endl
             << "-S                      Use Safra's complementation "
 	    << "instead of Kupferman&Vardi's" << std::endl
             << "-s     buchi_automaton  display the safra automaton"
@@ -63,6 +65,7 @@ int main(int argc, char* argv[])
   bool formula = false;
   bool safra = false;
   bool print_formula = false;
+  bool save_spot = false;
 
   if (argc < 3)
   {
@@ -74,6 +77,12 @@ int main(int argc, char* argv[])
   {
     if (argv[i][0] == '-')
     {
+      if (strcmp(argv[i] + 1, "b") == 0)
+      {
+	save_spot = true;
+	continue;
+      }
+
       if (strcmp(argv[i] + 1, "astat") == 0)
       {
         stats = true;
@@ -134,7 +143,12 @@ int main(int argc, char* argv[])
       complement = new spot::tgba_kv_complement(a);
 
     if (print_automaton)
-      spot::dotty_reachable(std::cout, complement);
+      {
+	if (save_spot)
+	  spot::tgba_save_reachable(std::cout, complement);
+	else
+	  spot::dotty_reachable(std::cout, complement);
+      }
 
     if (print_safra)
     {

src/tgbatest/complementation.test

@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -42,3 +42,25 @@ GFa&&FGa
 [] (p2 -> ((! p0 && ! p1) U (p1 || ((p0 && ! p1) U (p1 || ((! p0 && ! p1) \
  U (p1 || ((p0 && ! p1) U ((p1 || (! p0 U (p1 || [] ! p0))) || [] p0)))))))))
 EOF
+
+
+
+# The following test-case was supplied by Martin Dieguez Lodeiro to
+# demonstrate a bug in our Safra implementation.
+cat >x.tgba <<EOF
+acc = "1";
+"1", "1", "1",;
+"1", "2", "p",;
+"2", "3", "p", "1";
+"2", "2", "1",;
+"3", "3", "p", "1";
+"3", "2", "1",;
+EOF
+# x.tgba accepts some run
+run 0 ../ltl2tgba -X -e x.tgba
+# so does its complement
+run 0 ../complement -b -S -a x.tgba > nx.tgba
+run 0 ../ltl2tgba -X -e nx.tgba
+# however the intersection of both should not
+# accept any run.
+run 0 ../ltl2tgba -X -E -Pnx.tgba x.tgba