diff --git a/ChangeLog b/ChangeLog index 139ad8e7c..6abb10caf 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2004-01-30 Alexandre Duret-Lutz + + * 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 * src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition): diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test index c3b64bd7f..614c21bac 100755 --- a/src/ltltest/tostring.test +++ b/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' diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 3d2f110d2..c3b2a7529 100644 --- a/src/ltlvisit/tostring.cc +++ b/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(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