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

Print '{!a}*' rather than '!a*'.

Browse source 
* src/ltlvisit/tostring.cc: Use braces for unary operators in
Star.
* src/ltltest/tostring.test: Add some PSL formulae, it cannot
hurt.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-13 00:32:06 +01:00
parent aef6c1a06b
commit 47b2bea865
2 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ltltest/tostring.test
View file

@ -1,5 +1,5 @@
#! /bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement
# Copyright (C) 2009, 2010 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
@ -56,3 +56,8 @@ run 0 ../tostring 'p=0UFXp=1'
run 0 ../tostring 'GF"\GF"'
run 0 ../tostring 'GF"foo bar"'
run 0 ../tostring 'FFG__GFF'
run 0 ../tostring '{a;b;{c && d*};**}|=>G{a*:b*}'
run 0 ../tostring 'GF!{{a || c} && b}'
run 0 ../tostring 'GF!{{a || c*} && b}<>->{{!a}*}'
run 0 ../tostring 'GF{{a || c*} & b[*]}[]->{d}'

9
src/ltlvisit/tostring.cc
View file

@ -233,7 +233,9 @@ namespace spot
return;
}
// 1* is OK, no need to print {1}*.
need_parent = false;
// However want braces for {!a}*, the only unary
// operator that can be nested with *.
need_parent = !!dynamic_cast<const unop*>(uo->child());
// Do not output anything yet, star is a postfix operator.
break;
}
@ -481,8 +483,11 @@ namespace spot
os_ << "*";
return;
}
// 1* is OK, no need to print {1}*.
// However want braces for {!a}*, the only unary
// operator that can be nested with *.
need_parent = !!dynamic_cast<const unop*>(uo->child());
// Do not output anything yet, star is a postfix operator.
need_parent = false;
break;
}