Add full_parent support to to_spin_string().

* src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent
optional parameter, like for the to_string() function.
* src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the
handling of full_parent.
(to_spin_string_visitor): Handle full_parent.

ChangeLog

@@ -1,9 +1,19 @@
-2010-12-01  Alexandre Duret-Lutz  <adl@gnu.org>
+2010-12-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Add full_parent support to to_spin_string().
+
+	* src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent
+	optional parameter, like for the to_string() function.
+	* src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the
+	handling of full_parent.
+	(to_spin_string_visitor): Handle full_parent.
+
+2010-12-01  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Halve the number of application of eventual_universal_visitor in
 	reduce_visitor::visit(binop).
 
-	* src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_): 
+	* src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_):
 	Move this method...
 	(recurse_eu): ... outside as a separate function.  Likewise for
 	the universal/eventual result struct.

src/ltlvisit/tostring.cc

@@ -75,6 +75,8 @@ namespace spot
 	visit(const atomic_prop* ap)
 	{
 	  std::string str = ap->name();
+	  if (full_parent_)
+	    os_ << "(";
 	  if (!is_bare_word(str.c_str()))
 	    {
 	      os_ << '"' << str << '"';
@@ -83,12 +85,18 @@ namespace spot
 	    {
 	      os_ << str;
 	    }
+	  if (full_parent_)
+	    os_ << ")";
 	}
 
 	void
 	visit(const constant* c)
 	{
+	  if (full_parent_)
+	    os_ << "(";
 	  os_ << c->val_name();
+	  if (full_parent_)
+	    os_ << ")";
 	}
 
 	void
@@ -137,6 +145,16 @@ namespace spot
 	  // The parser treats F0, F1, G0, G1, X0, and X1 as atomic
 	  // propositions.  So make sure we output F(0), G(1), etc.
 	  bool need_parent = !!dynamic_cast<const constant*>(uo->child());
+	  bool top_level = top_level_;
+
+	  if (full_parent_)
+	    {
+	      need_parent = false; // These will be printed by each subformula
+
+	      if (!top_level)
+		os_ << "(";
+	    }
+
 	  switch (uo->op())
 	    {
 	    case unop::Not:
@@ -159,10 +177,13 @@ namespace spot
 	    }
 
 	  top_level_ = false;
-	  if (need_parent || full_parent_)
+	  if (need_parent)
 	    os_ << "(";
 	  uo->child()->accept(*this);
-	  if (need_parent || full_parent_)
+	  if (need_parent)
+	    os_ << ")";
+
+	  if (full_parent_ && !top_level)
 	    os_ << ")";
 	}
 
@@ -225,8 +246,8 @@ namespace spot
       class to_spin_string_visitor : public to_string_visitor
       {
       public:
-      to_spin_string_visitor(std::ostream& os)
-	: to_string_visitor(os)
+	to_spin_string_visitor(std::ostream& os, bool full_parent = false)
+	  : to_string_visitor(os, full_parent)
 	{
 	}
 
@@ -302,8 +323,9 @@ namespace spot
 	void
 	visit(const unop* uo)
 	{
-	  // The parser treats X0, and X1 as atomic propositions.	 So
-	  // make sure we output X(0) and X(1).
+	  bool top_level = top_level_;
+	  if (full_parent_ && !top_level)
+	    os_ << "(";
 	  bool need_parent = false;
 	  switch (uo->op())
 	    {
@@ -311,7 +333,11 @@ namespace spot
 	      os_ << "!";
 	      break;
 	    case unop::X:
+	      // The parser treats X0, and X1 as atomic propositions.	 So
+	      // make sure we output X(0) and X(1).
 	      need_parent = !!dynamic_cast<const constant*>(uo->child());
+	      if (full_parent_)
+		need_parent = false;
 	      os_ << "X";
 	      break;
 	    case unop::F:
@@ -332,6 +358,8 @@ namespace spot
 	  uo->child()->accept(*this);
 	  if (need_parent)
 	    os_ << ")";
+	  if (full_parent_ && !top_level)
+	    os_ << ")";
 	}
 
 	void
@@ -405,18 +433,18 @@ namespace spot
     }
 
     std::ostream&
-    to_spin_string(const formula* f, std::ostream& os)
+    to_spin_string(const formula* f, std::ostream& os, bool full_parent)
     {
-      to_spin_string_visitor v(os);
+      to_spin_string_visitor v(os, full_parent);
       f->accept(v);
       return os;
     }
 
     std::string
-    to_spin_string(const formula* f)
+    to_spin_string(const formula* f, bool full_parent)
     {
       std::ostringstream os;
-      to_spin_string(f, os);
+      to_spin_string(f, os, full_parent);
       return os.str();
     }
   }

src/ltlvisit/tostring.hh

@@ -1,3 +1,5 @@
+// Copyright (C) 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
 // et Marie Curie.
@@ -52,11 +54,16 @@ namespace spot
     /// \brief Output a formula as a (parsable by Spin) string.
     /// \param f The formula to translate.
     /// \param os The stream where it should be output.
-    std::ostream& to_spin_string(const formula* f, std::ostream& os);
+    /// \param full_parent Whether or not the string should by fully
+    ///	                   parenthesized.
+    std::ostream& to_spin_string(const formula* f, std::ostream& os,
+				 bool full_parent = false);
 
     /// \brief Convert a formula into a (parsable by Spin) string.
     /// \param f The formula to translate.
-    std::string to_spin_string(const formula* f);
+    /// \param full_parent Whether or not the string should by fully
+    ///	                   parenthesized.
+    std::string to_spin_string(const formula* f, bool full_parent = false);
 
     /// @}
   }