diff --git a/ChangeLog b/ChangeLog index 178c0b7ad..2f292c65b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2011-01-05 Alexandre Duret-Lutz + + 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 * wrap/python/cgi-bin/ltl2tgba.in: Remove all "new" markers. diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index df3bb08fc..3e45cc202 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/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 diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc index 685fe5a96..ccd69c3ae 100644 --- a/src/tgba/tgbabddconcretefactory.cc +++ b/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" diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index a24a63ee4..63b3d5eec 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/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), diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 0db119bff..5c9c165b5 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/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