alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltl2tgba: fix translation of !{xxx} when xxx reduces to false

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc: Typo.
* src/tgbatest/ltl2tgba.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2013-04-03 17:44:17 +02:00
parent a9fc213a44
commit c083c0df33
2 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // 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); const formula* dest2 = unop::instance(op, dest);
if (dest == constant::false_instance()) if (dest2 == constant::false_instance())
continue; continue;
int x = dict_.register_next_variable(dest2); int x = dict_.register_next_variable(dest2);

7
src/tgbatest/ltl2tgba.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- 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). # Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # 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 run 0 ../ltl2tgba -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout
grep 'transitions: 7$' stdout grep 'transitions: 7$' stdout
grep 'states: 4$' 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'