ltl: allow \" and \\ in double-quoted atomic propositions

* src/ltlparse/ltlscan.ll: Adjust parser.
* src/ltlvisit/print.cc: Adjust printer.
* src/tests/ltlfilt.test: Add some tests.
* NEWS: Mention it.

NEWS

@@ -16,6 +16,10 @@ New in spot 1.99.2a (not yet released)
     the list of rewritting rules to enable.  This function is also
     available via ltlfilt --unabbreviate.
 
+  * In LTL formulas, atomic propositions specified using double-quotes
+    can now include \" and \\.  (This is more consistent with the HOA
+    format, which already allows that.)
+
   * Bugs fixed
     - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
       were not detected as generalized-Rabin.

src/ltlparse/ltlscan.ll

@@ -52,7 +52,7 @@ typedef ltlyy::parser::token token;
 %x in_bra
 %x sqbracket
 %x lbt
-%x in_COMMENT
+%x in_COMMENT in_STRING
 
 BOX       "[]"|"□"|"⬜"|"◻"
 DIAMOND   "<>"|"◇"|"⋄"|"♢"
@@ -77,6 +77,7 @@ eol2        (\n\r)+|(\r\n)+
       return t;
     }
   yylloc->step();
+  std::string s;
 %}
 
 <*>"/""*"+		{
@@ -315,13 +316,44 @@ eol2        (\n\r)+|(\r\n)+
 			  return token::ATOMIC_PROP;
 			}
 
-  /* Atomic propositions can also be enclosed in double quotes.  */
+  /* Atomic propositions can also be enclosed in double quotes.
-\"[^\"]*\"		{
+
-			  yylval->str = new std::string(yytext + 1,
+     orig_cond stores the parsing condition to use after the
-							yyleng - 2);
+     string has been parsed. */
-			  BEGIN(not_prop);
+"\""                    {
-			  return token::ATOMIC_PROP;
+                          orig_cond = not_prop;
+			  BEGIN(in_STRING);
 			}
+<lbt>"\""		{
+			  orig_cond = lbt;
+			  BEGIN(in_STRING);
+			}
+
+<in_STRING>{
+  \"	                {
+                           BEGIN(orig_cond);
+			   yylval->str = new std::string(s);
+			   return token::ATOMIC_PROP;
+ 			}
+  {eol}			{
+  			  s.append(yytext, yyleng);
+                          yylloc->lines(yyleng); yylloc->end.column = 1;
+			}
+  {eol2}		{
+  			  s.append(yytext, yyleng);
+                          yylloc->lines(yyleng / 2); yylloc->end.column = 1;
+			}
+  \\.			s += yytext[1];
+  [^\\\"\n\r]+		s.append(yytext, yyleng);
+  <<EOF>>		{
+                           error_list.push_back(
+			     spot::ltl::one_parse_error(*yylloc,
+			       "unclosed string"));
+                           BEGIN(orig_cond);
+			   yylval->str = new std::string(s);
+			   return token::ATOMIC_PROP;
+                        }
+}
 
   /* these are operators */
 <lbt>[eitfXFGUVRWM]	return *yytext;
@@ -333,12 +365,6 @@ eol2        (\n\r)+|(\r\n)+
 			  return token::ATOMIC_PROP;
 			}
 
-  /* Atomic propositions can also be enclosed in double quotes.  */
-<lbt>\"[^\"]*\"		{
-			  yylval->str = new std::string(yytext + 1,
-							yyleng - 2);
-			  return token::ATOMIC_PROP;
-			}
 
 <*>.			return *yytext;
 

src/ltlvisit/print.cc

@@ -418,7 +418,7 @@ namespace spot
 	      if (kw_ == sclatex_kw  || kw_ == latex_kw)
 		escape_latex(os_ << "``\\mathit{", str) << "}\\textrm{''}";
 	      else if (kw_ != spin_kw)
-		os_ << '"' << str << '"';
+		escape_str(os_ << '"', str) << '"';
 	      else if (!full_parent_)
 		os_ << '(' << str << ')';
 	      else
@@ -1111,7 +1111,7 @@ namespace spot
 	  blank();
 	  std::string str = ap->name();
 	  if (!is_pnum(str.c_str()))
-	    os_ << '"' << str << '"';
+	    escape_str(os_ << '"', str) << '"';
 	  else
 	    os_ << str;
 	}

src/tests/ltlfilt.test

@@ -312,4 +312,10 @@ out=`$ltlfilt -f 'G(a xor b) -> F(c <-> Xd)' --unabbreviate='^iF'`
 exp='(1 U (c <-> Xd)) | !G!(a <-> b)'
 test "$out" = "$exp"
 
+$ltlfilt -f 'GF"a\"\\b"' > out
+test "`cat out`" = 'GF"a\"\\b"'
+
+$ltlfilt --lbt-input -f 'G F "a\"\\b"' -l > out
+test "`cat out`" = 'G F "a\"\\b"'
+
 true