Fix computation of support_conditions for bdd-based TGBA.

This fixes a bug in the powerset of such TGBA on the minimize branch.

* src/tgba/tgbabddconcrete.cc (compute_support_conditions): Also
account for the conditions from the acceptance relations.
* rc/tgba/tgbabddconcretefactory.hh, rc/tgba/tgbabddconcretefactory.cc
(acceptance_conditions_support): New variable to hold the value
of bdd_support(acceptance_conditions_support).
* src/tgba/tgbabddconcretefactory.cc (finish): Update
data_.acceptance_conditions_support.

ChangeLog

@@ -1,3 +1,16 @@
+2011-01-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Fix computation of support_conditions for bdd-based TGBA.
+	This fixes a bug in the powerset of such TGBA on the minimize branch.
+
+	* src/tgba/tgbabddconcrete.cc (compute_support_conditions): Also
+	account for the conditions from the acceptance relations.
+	* rc/tgba/tgbabddconcretefactory.hh, rc/tgba/tgbabddconcretefactory.cc
+	(acceptance_conditions_support): New variable to hold the value
+	of bdd_support(acceptance_conditions_support).
+	* src/tgba/tgbabddconcretefactory.cc (finish): Update
+	data_.acceptance_conditions_support.
+
 2010-12-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* wrap/python/cgi-bin/ltl2tgba.in: Remove all "new" markers.

src/tgba/tgbabddconcrete.cc

@@ -1,4 +1,6 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2011 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -127,9 +129,16 @@ namespace spot
     // bdd_support must be called BEFORE bdd_exist
     // because bdd_exist(bdd_support((a&Next[f])|(!a&Next[g])),Next[*])
     // is obviously not the same as bdd_support(a|!a).
-    // In other words: we can reuse compute_support_conditions() for
+    // In other words: we cannot reuse compute_support_conditions() for
     // this computation.
-    return bdd_exist(bdd_support(succ_set), data_.notvar_set);
+    //
+    // Also we need to inject the support of acceptance conditions, because a
+    // "Next[f]" that looks like one transition might in fact be two
+    // transitions if the acceptance condition distinguish between
+    // letters, e.g. "Next[f] & ((a & Acc[1]) | (!a))"
+    return bdd_exist(bdd_support(succ_set)
+		     & data_.acceptance_conditions_support,
+		     data_.notvar_set);
   }
 
   std::string

src/tgba/tgbabddconcretefactory.cc

@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -118,6 +118,9 @@ namespace spot
 	data_.all_acceptance_conditions |= acc;
       }
 
+    data_.acceptance_conditions_support =
+      bdd_support(data_.acceptance_conditions);
+
     // Any constraint between Now variables also exist between Next
     // variables.  Doing this limits the quantity of useless
     // successors we will have to explore.  (By "useless successors"

src/tgba/tgbabddcoredata.cc

@@ -1,3 +1,5 @@
+// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 // Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -27,6 +29,7 @@ namespace spot
   tgba_bdd_core_data::tgba_bdd_core_data(bdd_dict* dict)
     : relation(bddtrue),
       acceptance_conditions(bddfalse),
+      acceptance_conditions_support(bddtrue),
       all_acceptance_conditions(bddfalse),
       now_set(bddtrue),
       next_set(bddtrue),
@@ -46,6 +49,7 @@ namespace spot
   tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy)
     : relation(copy.relation),
       acceptance_conditions(copy.acceptance_conditions),
+      acceptance_conditions_support(copy.acceptance_conditions_support),
       all_acceptance_conditions(copy.all_acceptance_conditions),
       now_set(copy.now_set),
       next_set(copy.next_set),
@@ -68,6 +72,8 @@ namespace spot
     : relation(left.relation & right.relation),
       acceptance_conditions(left.acceptance_conditions
 			   | right.acceptance_conditions),
+      acceptance_conditions_support(left.acceptance_conditions_support
+				    & right.acceptance_conditions_support),
       all_acceptance_conditions(left.all_acceptance_conditions
 			       | right.all_acceptance_conditions),
       now_set(left.now_set & right.now_set),

src/tgba/tgbabddcoredata.hh

@@ -1,3 +1,5 @@
+// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
 // Copyright (C) 2003, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -74,6 +76,9 @@ namespace spot
     /// \li "Acc" variables.
     bdd acceptance_conditions;
 
+    /// The value of \c bdd_support(acceptance_conditions)
+    bdd acceptance_conditions_support;
+
     /// \brief The set of all acceptance conditions used by the Automaton.
     ///
     /// The goal of the emptiness check is to ensure that