* src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens.

(subformula): Recognize `ATOMIC_PROP OP_POST_POS' and
`ATOMIC_PROP OP_POST_NEG'.
* src/ltlparse/ltlscan.ll: Introduce the not_prop start condition,
to restrict the set of atomic propositions allowed in places
where they are not expected.  Make `true' and `false' case insensitive.
* src/ltltest/parse.test, src/ltltest/tostring.test: More cases.
* src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic
propositions equal to "true" or "false".

ChangeLog

@@ -1,3 +1,15 @@
+2004-05-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens.
+	(subformula): Recognize `ATOMIC_PROP OP_POST_POS' and
+	`ATOMIC_PROP OP_POST_NEG'.
+	* src/ltlparse/ltlscan.ll: Introduce the not_prop start condition,
+	to restrict the set of atomic propositions allowed in places
+	where they are not expected.  Make `true' and `false' case insensitive.
+	* src/ltltest/parse.test, src/ltltest/tostring.test: More cases.
+	* src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic
+	propositions equal to "true" or "false".
+
 2004-05-11  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltltest/Makefile.am (TESTS): Run inf.test and reduc.test last.

src/ltlparse/ltlparse.yy

@@ -82,7 +82,7 @@ using namespace spot::ltl;
 %token <str> ATOMIC_PROP "atomic proposition" OP_NOT "not operator"
 %token CONST_TRUE "constant true" CONST_FALSE "constant false"
 %token END_OF_INPUT "end of formula"
-
+%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
 
 /* Priorities.  */
 
@@ -97,9 +97,11 @@ using namespace spot::ltl;
 %nonassoc OP_F OP_G
 %nonassoc OP_X
 
-/* Not has the most important priority.  */
+/* Not has the most important priority after Wring's `=0' and `=1'.  */
 %nonassoc OP_NOT
 
+%nonassoc OP_POST_NEG OP_POST_POS
+
 %type <ltl> result subformula
 
 /* At the time of writing (2004-01-05) there is a bug in CVS Bison: if
@@ -152,6 +154,41 @@ subformula: ATOMIC_PROP
 		else
 		  delete $1;
 	      }
+	    | ATOMIC_PROP OP_POST_POS
+	      {
+		$$ = parse_environment.require(*$1);
+		if (! $$)
+		  {
+		    std::string s = "unknown atomic proposition `";
+		    s += *$1;
+		    s += "' in environment `";
+		    s += parse_environment.name();
+		    s += "'";
+		    error_list.push_back(parse_error(@1, s));
+		    delete $1;
+		    YYERROR;
+		  }
+		else
+		  delete $1;
+	      }
+	    | ATOMIC_PROP OP_POST_NEG
+	      {
+		$$ = parse_environment.require(*$1);
+		if (! $$)
+		  {
+		    std::string s = "unknown atomic proposition `";
+		    s += *$1;
+		    s += "' in environment `";
+		    s += parse_environment.name();
+		    s += "'";
+		    error_list.push_back(parse_error(@1, s));
+		    delete $1;
+		    YYERROR;
+		  }
+		else
+		  delete $1;
+		$$ = unop::instance(unop::Not, $$);
+	      }
 	    | CONST_TRUE
 	      { $$ = constant::true_instance(); }
 	    | CONST_FALSE

src/ltlparse/ltlscan.ll

@@ -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.
 **
@@ -51,57 +51,87 @@ flex_set_buffer(const char* buf)
 
 %}
 
+%s not_prop
+
 %%
 
 %{
   yylloc->step();
 %}
 
-"("			return PAR_OPEN;
+"("				BEGIN(0); return PAR_OPEN;
-")"			return PAR_CLOSE;
+")"				BEGIN(not_prop); return PAR_CLOSE;
+
+  /* Must go before the other operators, because the F of FALSE
+     should not be mistaken with a unary F. */
+"1"|[tT][rR][uU][eE]		BEGIN(0); return CONST_TRUE;
+"0"|[fF][aA][lL][sS][eE]	BEGIN(0); return CONST_FALSE;
+
+
+
+"!"				BEGIN(0); return OP_NOT;
 
-"!"			return OP_NOT;
   /* & and | come from Spin.  && and || from LTL2BA.
      /\, \/, and xor are from LBTT.
   */
-"||"|"|"|"+"|"\\/"	return OP_OR;
+"||"|"|"|"+"|"\\/"		BEGIN(0); return OP_OR;
-"&&"|"&"|"."|"*"|"/\\"	return OP_AND;
+"&&"|"&"|"."|"*"|"/\\"		BEGIN(0); return OP_AND;
-"^"|"xor"		return OP_XOR;
+"^"|"xor"			BEGIN(0); return OP_XOR;
-"=>"|"->"		return OP_IMPLIES;
+"=>"|"->"			BEGIN(0); return OP_IMPLIES;
-"<=>"|"<->"		return OP_EQUIV;
+"<=>"|"<->"			BEGIN(0); return OP_EQUIV;
 
   /* <>, [], and () are used in Spin.  */
-"F"|"<>"		return OP_F;
+"F"|"<>"			BEGIN(0); return OP_F;
-"G"|"[]"		return OP_G;
+"G"|"[]"			BEGIN(0); return OP_G;
-"U"			return OP_U;
+"U"				BEGIN(0); return OP_U;
-"R"|"V"			return OP_R;
+"R"|"V"				BEGIN(0); return OP_R;
-"X"|"()"		return OP_X;
+"X"|"()"			BEGIN(0); return OP_X;
 
-"1"|"true"		return CONST_TRUE;
+"=0"				return OP_POST_NEG;
-"0"|"false"		return CONST_FALSE;
+"=1"				return OP_POST_POS;
 
-[ \t\n]+		/* discard whitespace */ yylloc->step ();
+[ \t\n]+			/* discard whitespace */ yylloc->step ();
 
   /* An Atomic proposition cannot start with the letter
      used by a unary operator (F,G,X), unless this
      letter is followed by a digit in which case we assume
      it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we
-     don't).  */
+     don't).
-[a-zA-EH-WYZ_][a-zA-Z0-9_]* |
+  */
-[FGX][0-9_][a-zA-Z0-9_]* {
+<INITIAL>[a-zA-EH-WYZ_][a-zA-Z0-9_]* |
-		  yylval->str = new std::string(yytext);
+<INITIAL>[FGX][0-9_][a-zA-Z0-9_]* |
-	          return ATOMIC_PROP;
+  /*
-		}
+     However if we have just parsed an atomic proposition, then we
+     are not expecting another atomic proposition, so we can be stricter
+     and disallow propositions that start with U, R and V.  If you wonder
+     why we do this, consider the Wring formula `p=0Uq=1'.  When p is
+     parsed, we enter the not_prop start condition, we remain into this
+     condition when `=0' is processed, and then because we are in this
+     condition we will not consider `Uq' as an atomic proposition but as
+     a `U' operator followed by a `q' atomic proposition.
+
+     We also disable atomic proposition that may look  a combination
+     of a binary operator followed by several unary operators.
+     E.g. UFXp.   This way, `p=0UFXp=1' will be parsed as `(p=0)U(F(X(p=1)))'.
+  */
+<not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_]* |
+<not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_][a-zA-Z0-9_]* {
+			  yylval->str = new std::string(yytext);
+			  BEGIN(not_prop);
+			  return ATOMIC_PROP;
+			}
 
   /* Atomic propositions can also be enclosed in double quotes.  */
-\"[^\"]*\"	{
+\"[^\"]*\"		{
-		  yylval->str = new std::string(yytext + 1, yyleng - 2);
+			  yylval->str = new std::string(yytext + 1,
-	          return ATOMIC_PROP;
+			                                yyleng - 2);
-		}
+			  BEGIN(not_prop);
+			  return ATOMIC_PROP;
+			}
 
-.		return *yytext;
+.			return *yytext;
 
-<<EOF>>		return END_OF_INPUT;
+<<EOF>>			return END_OF_INPUT;
 
 %{
   /* Dummy use of yyunput to shut up a gcc warning.  */

src/ltltest/parse.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.
 #
@@ -70,7 +70,11 @@ for f in \
   'a U b U c U d U e U f U g U h U i U j U k U l U m' \
   '(ab * !Xad + ad U ab) & FG p12 /\ GF p13' \
   '((([]<>()p12))   )' \
-  'a R ome V anille'
+  'a R ome V anille' \
+  'p=0Uq=1' \
+  '((p=1Rq=1)+p=0)UXq=0' \
+  '((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)'
+
 do
   if ./ltl2text "$f"; then
     :

src/ltltest/tostring.test

@@ -45,3 +45,9 @@ 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'
+run 0 ./tostring 'p=0Uq=1Ut=1'
+run 0 ./tostring 'F"FALSE"'
+run 0 ./tostring 'G"TruE"'
+run 0 ./tostring 'FFALSE'
+run 0 ./tostring 'GTruE'
+run 0 ./tostring 'p=0UFXp=1'

src/ltlvisit/tostring.cc

@@ -48,7 +48,9 @@ namespace spot
       visit(const atomic_prop* ap)
       {
 	std::string str = ap->name();
-	if (str[0] == 'F' || str[0] == 'G' || str[0] == 'X')
+	if (str[0] == 'F' || str[0] == 'G' || str[0] == 'X'
+	    || !strcasecmp(str.c_str(), "true")
+	    || !strcasecmp(str.c_str(), "false"))
 	  {
 	    os_ << '"' << str << '"';
 	  }