From 84c9f03767d2953b0839721ceacd044cfff31448 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 20 Jul 2013 19:38:14 +0200
Subject: [PATCH] neverpase: fix parsing of neverclaim produced by ltl2ba and
 ltl3ba

These translator may output guards such as (a) || (b), but with the
changes in Spot 1.1.3 it would only work with ((a) || (b)).

Furthermore when ltlcross would fail to parse a neverclaim containing
such a guard, it would fail to parse all later neverclaims, because
the lexer was not properly reset.

* src/neverparse/neverclaimscan.ll: Scan (a) || (b) as a single
token.
(neverclaimyyopen): Reset the lexer.
* src/tgbatest/neverclaimread.test: Add a test for (a) || (b).
* NEWS: Update.
---
 NEWS                             |  7 ++++++-
 src/neverparse/neverclaimscan.ll |  8 ++++++++
 src/tgbatest/neverclaimread.test | 31 +++++++++++++++++++++++++++++++
 3 files changed, 45 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index b6e826959..feddc4544 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,11 @@
 New in spot 1.1.3a (not released)
 
-  * Nothing yet.
+  * Bug fixes:
+    - The parser for neverclaim, updated in 1.1.3, would fail to
+      parse guards of the form (a) || (b) output by ltl2ba or
+      ltl3ba, and would only understand ((a) || (b)).
+    - When used from ltlcross, the same parser would fail to
+      parser further neverclaims after the first failure.
 
 New in spot 1.1.3 (2013-07-09)
 
diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll
index 77656137d..79609034e 100644
--- a/src/neverparse/neverclaimscan.ll
+++ b/src/neverparse/neverclaimscan.ll
@@ -74,6 +74,10 @@ eol      \n|\r|\n\r|\r\n
 			  ++parent_level;
 			  yylval->str->append(yytext, yyleng);
 			}
+         /* if we match ")&&(" or ")||(", stay in <in_par> mode */
+         ")"[ \t]*("&&"|"||")[ \t]*"(" {
+	                  yylval->str->append(yytext, yyleng);
+			}
 	 ")"		{
 	                  yylval->str->append(yytext, yyleng);
 			  if (!--parent_level)
@@ -128,6 +132,10 @@ namespace spot
         if (!yyin)
 	  return 1;
       }
+    // Reset the lexer in case a previous parse
+    // ended badly.
+    BEGIN(0);
+    YY_NEW_FILE;
     return 0;
   }
 
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 5407fce59..3d3b033d6 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -112,6 +112,37 @@ diff stdout expected
 rm input stdout expected
 
 
+# Unparenthesed disjunction
+cat >input <<EOF
+never { /* p0 || p1  */
+accept_init:
+        if
+        :: (p1) || (p0) -> goto accept_all
+        fi;
+accept_all:
+        skip
+}
+EOF
+run 0 ../ltl2tgba -XN input > stdout
+
+cat >expected <<EOF
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="accept_init", peripheries=2]
+  1 -> 2 [label="p1 | p0\n{Acc[1]}"]
+  2 [label="accept_all", peripheries=2]
+  2 -> 2 [label="1\n{Acc[1]}"]
+}
+EOF
+
+# Sort out some possible inversions in the output.
+# (The order is not guaranteed by SPOT.)
+sed -e 's/p0 | p1/p1 | p0/g' stdout > tmp_ && mv tmp_ stdout
+diff stdout expected
+
+rm input stdout expected
+
 
 # Test broken guards in input
 cat >input <<EOF