diff --git a/ChangeLog b/ChangeLog
index 7882812f0..0ab844fb9 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,14 @@
 2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlvisit/tostring.cc (to_spin_string_visitor,
+	to_string_visitor): Do not parenthesize the top-level formula.
+	* tgbatest/explicit.test, tgbatest/explpro2.test,
+	tgbatest/explpro3.test, tgbatest/explprod.test,
+	tgbatest/readsave.test, tgbatest/tgbaread.test,
+	tgbatest/tripprod.test: Adjust expected output.
+	* sanity/style.test: Fix regexes to catch an error seen in
+	tostring.cc.
+
 	* src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component):
 	Do not try to erase state that are not found in H.
 	Report from Soheib Baarir.
diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc
index 097733e97..9f6d6e3db 100644
--- a/src/ltlvisit/tostring.cc
+++ b/src/ltlvisit/tostring.cc
@@ -35,7 +35,7 @@ namespace spot
     {
     public:
       to_string_visitor(std::ostream& os = std::cout)
-      : os_(os)
+	: os_(os), top_level_(true)
       {
       }
 
@@ -69,10 +69,14 @@ namespace spot
       void
       visit(const binop* bo)
       {
-	os_ << "(";
+	bool top_level = top_level_;
+	top_level_ = false;
+	if (!top_level)
+	  os_ << "(";
+
 	bo->first()->accept(*this);
 
-	switch(bo->op())
+	switch (bo->op())
 	  {
 	  case binop::Xor:
 	    os_ << " ^ ";
@@ -92,7 +96,8 @@ namespace spot
 	  }
 
 	bo->second()->accept(*this);
-	os_ << ")";
+	if (!top_level)
+	  os_ << ")";
       }
 
       void
@@ -101,7 +106,7 @@ 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());
-	switch(uo->op())
+	switch (uo->op())
 	  {
 	  case unop::Not:
 	    os_ << "!";
@@ -118,6 +123,7 @@ namespace spot
 	    break;
 	  }
 
+	top_level_ = false;
 	if (need_parent)
 	  os_ << "(";
 	uo->child()->accept(*this);
@@ -128,7 +134,10 @@ namespace spot
       void
       visit(const multop* mo)
       {
-	os_ << "(";
+	bool top_level = top_level_;
+	top_level_ = false;
+	if (!top_level)
+	  os_ << "(";
 	unsigned max = mo->size();
 	mo->nth(0)->accept(*this);
 	const char* ch = " ";
@@ -147,10 +156,12 @@ namespace spot
 	    os_ << ch;
 	    mo->nth(n)->accept(*this);
 	  }
-	os_ << ")";
+	if (!top_level)
+	  os_ << ")";
       }
     protected:
       std::ostream& os_;
+      bool top_level_;
     };
 
     std::ostream&
@@ -185,9 +196,12 @@ namespace spot
       void
       visit(const binop* bo)
       {
-	os_ << "(";
+	bool top_level = top_level_;
+	top_level_ = false;
+	if (!top_level)
+	  os_ << "(";
 
-	switch(bo->op())
+	switch (bo->op())
 	  {
 	  case binop::Xor:
 	    os_ << "(!";
@@ -228,7 +242,8 @@ namespace spot
 	    break;
 	  }
 
-	os_ << ")";
+	if (!top_level)
+	  os_ << ")";
       }
 
       void
@@ -237,7 +252,7 @@ namespace spot
 	// The parser treats X0, and X1 as atomic propositions.	 So
 	// make sure we output X(0) and X(1).
 	bool need_parent = false;
-	switch(uo->op())
+	switch (uo->op())
 	  {
 	  case unop::Not:
 	    os_ << "!";
@@ -254,6 +269,7 @@ namespace spot
 	    break;
 	  }
 
+	top_level_ = false;
 	if (need_parent)
 	  os_ << "(";
 	uo->child()->accept(*this);
@@ -264,7 +280,10 @@ namespace spot
       void
       visit(const multop* mo)
       {
-	os_ << "(";
+	bool top_level = top_level_;
+	top_level_ = false;
+	if (!top_level)
+	  os_ << "(";
 	unsigned max = mo->size();
 	mo->nth(0)->accept(*this);
 	const char* ch = " ";
@@ -283,7 +302,8 @@ namespace spot
 	    os_ << ch;
 	    mo->nth(n)->accept(*this);
 	  }
-	os_ << ")";
+	if (!top_level)
+	  os_ << ")";
       }
     };
 
diff --git a/src/sanity/style.test b/src/sanity/style.test
index 2389477c2..d0450e416 100755
--- a/src/sanity/style.test
+++ b/src/sanity/style.test
@@ -33,28 +33,28 @@ while read file; do
 
    sed 's,//.*,,' < $file > $tmp
 
-   grep ' if(' $tmp &&
+   grep '[	 ]if(' $tmp &&
      diag 'Missing space after "if"'
 
-   grep ' if (.*).*{' $tmp &&
+   grep '[	 ]if (.*).*{' $tmp &&
      diag 'Opening { should be on its own line.'
 
-   grep ' while(' $tmp &&
+   grep '[	 ]while(' $tmp &&
      diag 'Missing space after "while"'
 
-   grep ' while (.*).*{' $tmp &&
+   grep '[	 ]while (.*).*{' $tmp &&
      diag 'Opening { should be on its own line.'
 
-   grep ' for(' $tmp &&
+   grep '[	 ]for(' $tmp &&
      diag 'Missing space after "for"'
 
-   grep ' for (.*).*{' $tmp &&
+   grep '[	 ]for (.*).*{' $tmp &&
      diag 'Opening { should be on its own line.'
 
-   grep ' switch(' $tmp &&
-     diag 'Missing space after "for"'
+   grep '[	 ]switch(' $tmp &&
+     diag 'Missing space after "switch"'
 
-   grep ' switch (.*).*{' $tmp &&
+   grep '[	 ]switch (.*).*{' $tmp &&
      diag 'Opening { should be on its own line.'
 
    grep '( ' $tmp &&
@@ -69,10 +69,10 @@ while read file; do
    grep ',[(a-zA-Z+=_!]' $tmp &&
      diag 'Space after coma.'
 
-   grep '[^ \t\n]&&[^ \t\n]' $tmp &&
+   grep '[^	 ]&&[^	 ]' $tmp &&
      diag 'Space arround binary operators.'
 
-   grep '[^ \t\n]||[^ \t\n]' $tmp &&
+   grep '[^	 ]||[^	 ]' $tmp &&
      diag 'Space arround binary operators.'
 
    $fail && echo "$file" >>failures
diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test
index ef92279ab..38a050bbb 100755
--- a/src/tgbatest/explicit.test
+++ b/src/tgbatest/explicit.test
@@ -38,7 +38,7 @@ digraph G {
   2 [label="state 1"]
   2 -> 3 [label="a\n{Acc[r]}"]
   3 [label="state 2"]
-  3 -> 1 [label="(b & c)\n"]
+  3 -> 1 [label="b & c\n"]
 }
 EOF
 
diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test
index a80ddba75..43da4aac0 100755
--- a/src/tgbatest/explpro2.test
+++ b/src/tgbatest/explpro2.test
@@ -39,8 +39,8 @@ EOF
 
 cat >expected <<EOF
 acc = "p1" "p2" "p3";
-"s1 * s1", "s2 * s2", "(!a & b)",  "p1" "p2";
-"s1 * s1", "s3 * s3", "(a & !b)",  "p2" "p3";
+"s1 * s1", "s2 * s2", "!a & b",  "p1" "p2";
+"s1 * s1", "s3 * s3", "a & !b",  "p2" "p3";
 EOF
 
 run 0 ./explprod input1 input2 > stdout
@@ -48,7 +48,7 @@ run 0 ./explprod input1 input2 > stdout
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
 perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;
-          s/\(!b & a\)/(a & !b)/g;s/\(b & !a\)/(!a & b)/g' \
+          s/!b & a/a & !b/g;s/b & !a/!a & b/g' \
   stdout > tmp_ && mv tmp_ stdout
 
 cat stdout
diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test
index 2a1ed284b..de490ce45 100755
--- a/src/tgbatest/explpro3.test
+++ b/src/tgbatest/explpro3.test
@@ -39,16 +39,16 @@ EOF
 
 cat >expected <<EOF
 acc = "p2" "p3";
-"s1 * s1", "s2 * s2", "(!a & b)", "p2";
-"s1 * s1", "s3 * s3", "(a & !b)", "p3";
+"s1 * s1", "s2 * s2", "!a & b", "p2";
+"s1 * s1", "s3 * s3", "a & !b", "p3";
 EOF
 
 run 0 ./explprod input1 input2 > stdout
 
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
-sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g;
-     s/(b & !a)/(!a \& b)/g' stdout > tmp_ && mv tmp_ stdout
+sed 's/"p3" "p2"/"p2" "p3"/g;s/!b & a/a \& !b/g;
+     s/b & !a/!a \& b/g' stdout > tmp_ && mv tmp_ stdout
 
 cat stdout
 diff stdout expected
diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test
index 3f01d5a8c..5496e6021 100755
--- a/src/tgbatest/explprod.test
+++ b/src/tgbatest/explprod.test
@@ -41,16 +41,16 @@ EOF
 
 cat >expected <<EOF
 acc = "p1" "p2" "p3";
-"s1 * s1", "s3 * s2", "(a & b)",  "p1" "p2";
+"s1 * s1", "s3 * s2", "a & b",  "p1" "p2";
 "s1 * s1", "s2 * s2", "b",  "p1" "p2";
-"s2 * s2", "s3 * s1", "(a & c)",  "p1" "p3";
+"s2 * s2", "s3 * s1", "a & c",  "p1" "p3";
 EOF
 
 run 0 ./explprod input1 input2 > stdout
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
 perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;
-          s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \
+          s/c & a/a & c/g;s/b & a/a & b/g' \
   stdout > tmp_ && mv tmp_ stdout
 
 cat stdout
diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test
index 964f4b6c7..83a9ad8c6 100755
--- a/src/tgbatest/readsave.test
+++ b/src/tgbatest/readsave.test
@@ -36,7 +36,7 @@ EOF
 
 cat >expected <<\EOF
 acc = "c" "d";
-"s1", "s2", "(a & !b)", "c" "d";
+"s1", "s2", "a & !b", "c" "d";
 "s2", "state 3", "\"F\\G\"", "c";
 "state 3", "s1", "1",;
 EOF
diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test
index f3014ac9f..509ad29d0 100755
--- a/src/tgbatest/tgbaread.test
+++ b/src/tgbatest/tgbaread.test
@@ -39,7 +39,7 @@ digraph G {
   0 [label="", style=invis, height=0]
   0 -> 1
   1 [label="s1"]
-  1 -> 2 [label="(a & !b)\n{Acc[d], Acc[c]}"]
+  1 -> 2 [label="a & !b\n{Acc[d], Acc[c]}"]
   2 [label="s2"]
   2 -> 3 [label="a\n{Acc[c]}"]
   3 [label="state 3"]
diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test
index 66a6ee1eb..472ec731e 100755
--- a/src/tgbatest/tripprod.test
+++ b/src/tgbatest/tripprod.test
@@ -49,12 +49,12 @@ EOF
 
 cat >expected <<EOF
 acc = "p1" "p2" "p3" "p4";
-"s1 * s1 * s1", "s3 * s2 * s2", "(a & b)",   "p1" "p2";
-"s1 * s1 * s1", "s2 * s2 * s2", "(a & b)",   "p1" "p2";
-"s1 * s1 * s1", "s3 * s2 * s3", "(a & b)",   "p1" "p2";
+"s1 * s1 * s1", "s3 * s2 * s2", "a & b",   "p1" "p2";
+"s1 * s1 * s1", "s2 * s2 * s2", "a & b",   "p1" "p2";
+"s1 * s1 * s1", "s3 * s2 * s3", "a & b",   "p1" "p2";
 "s1 * s1 * s1", "s2 * s2 * s3", "b",   "p1" "p2";
-"s2 * s2 * s2", "s3 * s1 * s3", "(a & c)",   "p3" "p4";
-"s2 * s2 * s3", "s3 * s1 * s2", "(a & c)",   "p3" "p4";
+"s2 * s2 * s2", "s3 * s1 * s3", "a & c",   "p3" "p4";
+"s2 * s2 * s3", "s3 * s1 * s2", "a & c",   "p3" "p4";
 EOF
 
 run 0 ./tripprod input1 input2 input3 > stdout
@@ -62,7 +62,7 @@ run 0 ./tripprod input1 input2 input3 > stdout
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
 perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1,$2,$3,$4]}/g;
-          s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \
+          s/c & a/a & c/g;s/b & a/a & b/g' \
   stdout > tmp_ &&
   mv tmp_ stdout