From 6c76ba408ec78b01cadde6ae8fcd83b3af29d71f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 29 May 2014 15:48:31 +0200
Subject: [PATCH] neverparse: Fix parsing of Modella's neverclaims.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reported by František Blahoudek.

* src/neverparse/neverclaimparse.yy: Fix.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention the fix.
---
 NEWS                              |  1 +
 src/neverparse/neverclaimparse.yy |  4 ++--
 src/tgbatest/neverclaimread.test  | 38 +++++++++++++++++++++++++++++--
 3 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index e2f767453..289c3ef2f 100644
--- a/NEWS
+++ b/NEWS
@@ -3,6 +3,7 @@ New in spot 1.2.4a (not yet released)
   * Bug fixes:
 
     - Fix simplification of bounded repetition in SERE formulas.
+    - Fix parsing of neverclaims produced by Modella.
 
 New in spot 1.2.4 (2014-05-15)
 
diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy
index 8d32440b8..6e915b600 100644
--- a/src/neverparse/neverclaimparse.yy
+++ b/src/neverparse/neverclaimparse.yy
@@ -1,5 +1,5 @@
 /* -*- coding: utf-8 -*-
-** Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
+** Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 ** Développement de l'Epita (LRDE).
 **
 ** This file is part of Spot, a model checking library.
@@ -191,7 +191,7 @@ transitions:
     }
 
 
-formula: FORMULA | "false" { $$ = new std::string("0"); }
+formula: FORMULA | IDENT | "false" { $$ = new std::string("0"); }
 
 opt_dest:
   /* empty */
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 3e75a715e..06d0b3c7c 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
+# et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -172,6 +172,40 @@ EOF
 grep input: stderr >> stderrfilt
 diff stderrfilt expected
 
+
+# This output from MoDeLLa was not property parsed by Spot because of
+# the missing parentheses around p0.  Report from František Blahoudek.
+cat >input <<EOF
+never{
+T0_init:
+	if
+	:: true -> goto T1
+	:: p0 -> goto T2
+	fi;
+T1:
+	if
+	:: true -> goto T1
+	:: p0 -> goto accept_T3
+	fi;
+T2:
+	if
+	:: p0 -> goto accept_T3
+	fi;
+accept_T3:
+	if
+	:: p0 -> goto T2
+	fi;
+}
+EOF
+cat >expected<<EOF
+transitions: 6
+states: 4
+EOF
+
+run 0 ../ltl2tgba -ks -XN input > output
+diff output expected
+
+
 cat >formulae<<EOF
 a
 FG a