From d401fadc65163f6cbb40908d790d72c695b35ab4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 31 Aug 2014 19:07:53 +0200
Subject: [PATCH] neverparse: diagnose redefinition of state labels

Reported by Joachim Klein.

* src/neverparse/neverclaimparse.yy: Store labels and the
location of their first definition in a global map to catch
redefinitions.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention it.
---
 NEWS                              |  2 +
 src/neverparse/neverclaimparse.yy | 19 +++++--
 src/tgbatest/neverclaimread.test  | 83 ++++++++++++++++++++++++++++++-
 3 files changed, 99 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 12456d143..d824666c4 100644
--- a/NEWS
+++ b/NEWS
@@ -12,6 +12,8 @@ New in spot 1.2.5a (not yet released)
       positive formula.  The same procedure should be performed with
       automata obtained from negated formulas, but because of a typo
       this was not the case.
+    - the neverclaim parser will now diagnose redefinitions of
+      state labels.
 
 New in spot 1.2.5 (2014-08-21)
 
diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy
index 6e915b600..db601a853 100644
--- a/src/neverparse/neverclaimparse.yy
+++ b/src/neverparse/neverclaimparse.yy
@@ -59,6 +59,7 @@
 using namespace spot::ltl;
 static bool accept_all_needed = false;
 static bool accept_all_seen = false;
+static std::map<std::string, spot::location> labels;
 }
 
 %token NEVER "never"
@@ -77,7 +78,7 @@ static bool accept_all_seen = false;
 %type <str> formula opt_dest
 %type <p> transition src_dest
 %type <list> transitions transition_block
-%type <str> ident_list
+%type <str> one_ident ident_list
 
 
 %destructor { delete $$; } <str>
@@ -108,12 +109,21 @@ states:
   | states ';' state
   | states ';'
 
-ident_list:
-    IDENT ':'
+one_ident: IDENT ':'
     {
+      std::pair<std::map<std::string, spot::location>::const_iterator, bool>
+	res = labels.insert(std::make_pair(*$1, @1));
+      if (!res.second)
+	{
+	  error(@1, std::string("redefinition of ") + *$1 + "...");
+	  error(res.first->second, std::string("... ")  + *$1 + " previously defined here");
+	}
       $$ = $1;
     }
-  | ident_list IDENT ':'
+
+
+ident_list: one_ident
+  | ident_list one_ident
     {
       result->add_state_alias(*$2, *$1);
       // Keep any identifier that starts with accept.
@@ -294,6 +304,7 @@ namespace spot
       }
     accept_all_needed = false;
     accept_all_seen = false;
+    labels.clear();
 
     return result;
   }
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 06d0b3c7c..ab8db0332 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -169,7 +169,7 @@ run 2 ../ltl2tgba -XN input > stdout 2>stderr
 cat >expected <<\EOF
 input:9.16: syntax error, unexpected $undefined, expecting fi or ':'
 EOF
-grep input: stderr >> stderrfilt
+grep input: stderr > stderrfilt
 diff stderrfilt expected
 
 
@@ -206,6 +206,87 @@ run 0 ../ltl2tgba -ks -XN input > output
 diff output expected
 
 
+# Test duplicated labels.  The following neverclaim was produced by
+# ltl2ba 1.1 for '[](<>[]p1 U X[]<>Xp0)', but is rejected by Spin
+# because of a duplicate label (accept_S10).  We should
+# complain as well.  This was reported by Joachim Klein.
+
+cat >input <<\EOF
+never { /* [](<>[]p1 U X[]<>Xp0) */
+T0_init:
+	if
+	:: (1) -> goto accept_S2
+	:: (1) -> goto T1_S3
+	:: (p1) -> goto T2_S4
+	fi;
+accept_S2:
+	if
+	:: (1) -> goto accept_S39
+	:: (1) -> goto T1_S24
+	:: (p1) -> goto accept_S10
+	fi;
+accept_S39:
+	if
+	:: (p0) -> goto accept_S39
+	:: (1) -> goto T0_S39
+	:: (1) -> goto T0_S24
+	:: (p1) -> goto T0_S10
+	fi;
+T0_S39:
+	if
+	:: (p0) -> goto accept_S39
+	:: (1) -> goto T0_S39
+	:: (1) -> goto T0_S24
+	:: (p1) -> goto T0_S10
+	fi;
+T0_S24:
+	if
+	:: (1) -> goto T0_S24
+	:: (p1) -> goto T0_S10
+	fi;
+T0_S10:
+	if
+	:: (p0 && p1) -> goto accept_S10
+	:: (p1) -> goto T0_S10
+	fi;
+accept_S10:
+	if
+	:: (p0 && p1) -> goto accept_S10
+	:: (p1) -> goto T0_S10
+	fi;
+T1_S24:
+	if
+	:: (1) -> goto T1_S24
+	:: (p1) -> goto accept_S10
+	fi;
+accept_S10:
+	if
+	:: (p1) -> goto accept_S10
+	fi;
+T1_S3:
+	if
+	:: (1) -> goto T1_S3
+	:: (1) -> goto T1_S24
+	:: (p1) -> goto T2_S4
+	:: (p1) -> goto accept_S10
+	fi;
+T2_S4:
+	if
+	:: (p1) -> goto T2_S4
+	:: (p1) -> goto accept_S10
+	fi;
+}
+EOF
+
+run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr
+cat stderr
+cat >expected-err <<\EOF
+input:48.1-10: redefinition of accept_S10...
+input:38.1-10: ... accept_S10 previously defined here
+EOF
+grep input: stderr > stderrfilt
+diff stderrfilt expected-err
+
 cat >formulae<<EOF
 a
 FG a