From bf3c3aecde44ef8179c534e53eafb9c3247ba696 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 19 Jan 2013 14:15:17 +0100
Subject: [PATCH] tostring: quote U, W, M, R when used as atomic propositions

* src/ltltest/tostring.test, src/ltltest/parse.test: More tests.
* src/ltlvisit/tostring.cc (is_bare_word): Quote U, W, M, R.
* NEWS: Mention it.
---
 NEWS                      |  4 ++++
 src/ltltest/parse.test    | 14 +++++++++++---
 src/ltltest/tostring.test | 11 ++++++++---
 src/ltlvisit/tostring.cc  | 10 ++++++----
 4 files changed, 29 insertions(+), 10 deletions(-)

diff --git a/NEWS b/NEWS
index 374fad926..351d1d8bc 100644
--- a/NEWS
+++ b/NEWS
@@ -9,6 +9,10 @@ New in spot 1.0a (not released):
     - "P0.init" is parsed as an atomic even without the double quotes,
       but it was always output with double quotes.  This version will
       not quote this atomic proposition anymore.
+    - "U", "W", "M", "R" were correctly parsed as atomic propositions
+      (instead of binary operators) when placed in double quotes, but
+      on output they were output without quotes, making the result
+      unparsable.
     - tgba_product::transition_annotation() would segfault when
       called in a product against a Kripke structure.
   * Minor improvements:
diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test
index 0d71b1ea6..9310b01bb 100755
--- a/src/ltltest/parse.test
+++ b/src/ltltest/parse.test
@@ -1,6 +1,7 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Developpement
-# de l'Epita (LRDE).
+# -*- coding: utf-8 -*-
+# 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
 # et Marie Curie.
@@ -61,6 +62,13 @@ for f in \
   '<>b' \
   'X b' \
   '()b' \
+  'X"X"' \
+  'X"F"' \
+  'X"G"' \
+  'X"U"' \
+  'X"W"' \
+  'X"R"' \
+  'X"M"' \
   'long_atomic_proposition_1 U long_atomic_proposition_2' \
   '  ab & ac | ad ^ af' \
   '((b & a) + a) & d' \
@@ -81,7 +89,7 @@ do
   if ../ltl2text "$f"; then
     :
   else
-    echo "ltl2dot failed to parse '$f'"
+    echo "ltl2text failed to parse '$f'"
     exit 1
   fi
 
diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test
index 8b876186d..a3d76125f 100755
--- a/src/ltltest/tostring.test
+++ b/src/ltltest/tostring.test
@@ -1,8 +1,9 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2010, 2011, 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
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -54,6 +55,10 @@ 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 'X"U"'
+run 0 ../tostring 'X"W"'
+run 0 ../tostring 'X"M"'
+run 0 ../tostring 'X"R"'
 
 run 0 ../tostring '{a;b;{c && d*};**}|=>G{a*:b*}'
 run 0 ../tostring 'GF!{{a || c} && b}'
diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc
index ada53b33f..5992ae35e 100644
--- a/src/ltlvisit/tostring.cc
+++ b/src/ltlvisit/tostring.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2010, 2012 Laboratoire de Recherche et
+// Copyright (C) 2008, 2010, 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
@@ -191,14 +191,16 @@ namespace spot
       static bool
       is_bare_word(const char* str)
       {
-	// Bare words cannot be empty, start with the letter of a unary
-	// operator, or be the name of an existing constant.  Also they
-	// should start with an letter.
+	// Bare words cannot be empty, start with the letter of a
+	// unary operator, or be the name of an existing constant or
+	// operator.  Also they should start with an letter.
 	if (!*str
 	    || *str == 'F'
 	    || *str == 'G'
 	    || *str == 'X'
 	    || !(isalpha(*str) || *str == '_' || *str == '.')
+	    || ((*str == 'U' || *str == 'W' || *str == 'M' || *str == 'R')
+		&& str[1] == 0)
 	    || !strcasecmp(str, "true")
 	    || !strcasecmp(str, "false"))
 	  return false;