* src/ltlvisit/tostring.cc: Fix output of F0, F1, G0, G1, X0, and X1.

* src/ltltest/tostring.test: Test these.

ChangeLog

+2004-01-30  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/ltlvisit/tostring.cc: Fix output of F0, F1, G0, G1, X0, and X1.
+	* src/ltltest/tostring.test: Test these.
+
 2004-01-29  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition):

src/ltltest/tostring.test

@@ -43,3 +43,5 @@ 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"'
+run 0 ./tostring 'GFfalse'
+run 0 ./tostring 'GFtrue'

src/ltlvisit/tostring.cc

@@ -96,10 +96,14 @@ namespace spot
       void
       visit(const unop* uo)
       {
+	// 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());
 	switch(uo->op())
 	  {
 	  case unop::Not:
 	    os_ << "!";
+	    need_parent = false;
 	    break;
 	  case unop::X:
 	    os_ << "X";
@@ -112,7 +116,11 @@ namespace spot
 	    break;
 	  }
 
+	if (need_parent)
+	  os_ << "(";
 	uo->child()->accept(*this);
+	if (need_parent)
+	  os_ << ")";
       }
 
       void