From 47b2bea865069d6d06ce1f0f4502aa6b1c6a2972 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 13 Mar 2010 00:32:06 +0100
Subject: [PATCH] Print '{!a}*' rather than '!a*'.

* src/ltlvisit/tostring.cc: Use braces for unary operators in
Star.
* src/ltltest/tostring.test: Add some PSL formulae, it cannot
hurt.
---
 src/ltltest/tostring.test | 7 ++++++-
 src/ltlvisit/tostring.cc  | 9 +++++++--
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test
index f0ba885d2..bca0c66fb 100755
--- a/src/ltltest/tostring.test
+++ b/src/ltltest/tostring.test
@@ -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}'
diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc
index 7c15b6928..5b8032342 100644
--- a/src/ltlvisit/tostring.cc
+++ b/src/ltlvisit/tostring.cc
@@ -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;
 	    }