From 8008deeddd25f53a2631ed3e4b6e3a4152c17c78 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 6 Jan 2004 15:45:00 +0000
Subject: [PATCH] * src/ltlvisit/tostring.cc (to_string_visitor::visit(const
 atomic_prop*)): Quote propositions that start with F, G, or X. *
 src/ltltest/tostring.test: Test quoted propositions. * src/tgbaalgos/save.cc
 (save_bfs::process_state): Escape " and +	characters in formulae. *
 src/tgbatest/readsave.test: Test for this.

---
 ChangeLog                  |  8 ++++++++
 src/ltltest/tostring.test  |  5 +++--
 src/ltlvisit/tostring.cc   | 12 ++++++++++--
 src/tgbaalgos/save.cc      | 18 +++++++++++++++++-
 src/tgbatest/readsave.test | 10 +++++-----
 5 files changed, 43 insertions(+), 10 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index e7a08dd9e..f1939b992 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,13 @@
 2004-01-06  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlvisit/tostring.cc
+	(to_string_visitor::visit(const atomic_prop*)): Quote propositions
+	that start with F, G, or X.
+	* src/ltltest/tostring.test: Test quoted propositions.
+	* src/tgbaalgos/save.cc (save_bfs::process_state): Escape " and \
+	characters in formulae.
+	* src/tgbatest/readsave.test: Test for this.
+
 	* src/tgbaalgos/reachiter.hh: Typos in comments.
 
 	* iface/gspn/eesrg.cc (tgba_gspn_eesrg::all_acceptance_conditions,
diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test
index 001e26d4f..c3b64bd7f 100755
--- a/src/ltltest/tostring.test
+++ b/src/ltltest/tostring.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003  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
 # et Marie Curie.
 #
@@ -25,7 +25,7 @@
 
 . ./defs || exit 1
 
-set -e 
+set -e
 
 run 0 ./tostring 'a'
 run 0 ./tostring '1'
@@ -42,3 +42,4 @@ run 0 ./tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
 run 0 ./tostring 'a <=> b'
 run 0 ./tostring 'a & b & (c |(f U g)| e)'
 run 0 ./tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
+run 0 ./tostring 'F"F1"&G"G"&X"X"'
diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc
index a5a4ae380..3d2f110d2 100644
--- a/src/ltlvisit/tostring.cc
+++ b/src/ltlvisit/tostring.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2003  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
 // et Marie Curie.
 //
@@ -47,7 +47,15 @@ namespace spot
       void
       visit(const atomic_prop* ap)
       {
-	os_ << ap->name();
+	std::string str = ap->name();
+	if (str[0] == 'F' || str[0] == 'G' || str[0] == 'X' )
+	  {
+	    os_ << '"' << str << '"';
+	  }
+	else
+	  {
+	    os_ << str;
+	  }
       }
 
       void
diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc
index a83402779..6f5128e58 100644
--- a/src/tgbaalgos/save.cc
+++ b/src/tgbaalgos/save.cc
@@ -78,7 +78,23 @@ namespace spot
 	  state* dest = si->current_state();
 	  os_ << "\"" << cur << "\", \""
 	      << automata_->format_state(dest) << "\", \"";
-	  bdd_print_formula(os_, d, si->current_condition()) << "\",";
+	  std::string s = bdd_format_formula(d, si->current_condition());
+	  // Escape " and \ characters in s.
+	  for (std::string::const_iterator i = s.begin();
+	       i != s.end(); ++i)
+	    switch (*i)
+	      {
+	      case '\\':
+		os_ << "\\\\";
+		break;
+	      case '"':
+		os_ << "\\\"";
+		break;
+	      default:
+		os_ << *i;
+		break;
+	      }
+	  os_ << "\",";
 	  bdd_print_acc(os_, d, si->current_acceptance_conditions());
 	  os_ << ";" << std::endl;
 	  delete dest;
diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test
index f306437e7..cd0c03bfb 100755
--- a/src/tgbatest/readsave.test
+++ b/src/tgbatest/readsave.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003  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
 # et Marie Curie.
 #
@@ -25,19 +25,19 @@
 
 set -e
 
-cat >input <<EOF
+cat >input <<\EOF
 acc = c d;
 s1, "s2", "a&!b", c d;
-"s2", "state 3", "a", c;
+"s2", "state 3", "\"F\\G\"", c;
 "state 3", s1,,;
 EOF
 
 ./readsave input > stdout
 
-cat >expected <<EOF
+cat >expected <<\EOF
 acc = "c" "d";
 "s1", "s2", "(a & !b)", "c" "d";
-"s2", "state 3", "a", "c";
+"s2", "state 3", "\"F\\G\"", "c";
 "state 3", "s1", "1",;
 EOF