diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 972e72418..0988e461f 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis @@ -1449,7 +1449,7 @@ namespace spot const formula* dest2 = unop::instance(op, dest); - if (dest == constant::false_instance()) + if (dest2 == constant::false_instance()) continue; int x = dict_.register_next_variable(dest2); diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 5a3950b3b..a3098dd5a 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -204,3 +204,8 @@ cmp count.never count.spot run 0 ../ltl2tgba -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout grep 'transitions: 7$' stdout grep 'states: 4$' stdout + +# A bug in the translation of !{xxx} when xxx reduces to false caused +# the following formula to be considered equivalent to anything... +../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'false' && exit 1 +../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'true'