diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc index 0e81ad9d8..fe61419fc 100644 --- a/src/tgba/wdbacomp.cc +++ b/src/tgba/wdbacomp.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita. +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -248,18 +249,12 @@ namespace spot return !the_acceptance_cond_; } - protected: - virtual bdd - compute_support_conditions(const state* ostate) const + protected: + virtual bdd + compute_support_conditions(const state*) const { - const state_wdba_comp_proxy* s = - down_cast(ostate); - assert(s); - const state* rs = s->real_state(); - if (rs) - return a_->support_conditions(rs); - else - return bddtrue; + // The automaton is complete, so we always support all variables. + return bddtrue; } virtual bdd compute_support_variables(const state* ostate) const diff --git a/src/tgbatest/wdba2.test b/src/tgbatest/wdba2.test index c2224a6c7..5ac11644f 100755 --- a/src/tgbatest/wdba2.test +++ b/src/tgbatest/wdba2.test @@ -1,4 +1,5 @@ #!/bin/sh +# -*- coding: utf-8 -*- # Copyright (C) 2012 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # @@ -36,3 +37,12 @@ run 0 ../ltl2tgba -Rm -kt 'Fa | XGd' > out2 cmp out expected cmp out2 expected + + +# This non-obligation formula used to be minimized by mistake when +# translated with lacim. +x=`../ltl2tgba -l -Rm 'F(Fa R (Gb & !a))' | + grep -v -- '->' | + sed -n 's/.*label="\(..*\)".*/\1/p' | + tr -d '0-9\n'` +test -n "$x"