From 34b798e1155821ac55e4c58c6c5d91ee91a5b941 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 5 Jan 2015 12:10:49 +0100
Subject: [PATCH] hoaparse: validate use of state-labels and trans-labels

* src/hoaparse/hoaparse.yy: Fix a map with properties, and use it to
report error when state-label or trans-label are misused.
* src/tgbatest/hoaparse.test: Test that.
---
 src/hoaparse/hoaparse.yy   | 58 +++++++++++++++++++++++++++++++++++---
 src/tgbatest/hoaparse.test | 40 ++++++++++++++++++++++++--
 2 files changed, 91 insertions(+), 7 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index 859cccba1..05fc8d896 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -1,5 +1,5 @@
 /* -*- coding: utf-8 -*-
-** Copyright (C) 2014 Laboratoire de Recherche et Développement
+** Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
 ** de l'Epita (LRDE).
 **
 ** This file is part of Spot, a model checking library.
@@ -54,6 +54,8 @@
   // chance to reach the end of the current automaton in order to
   // process the next one.  Several variables below are used to keep
   // track of various error conditions.
+  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels };
+
   struct result_
   {
     spot::hoa_aut_ptr h;
@@ -67,6 +69,7 @@
     std::vector<bool> declared_states; // States that have been declared.
     std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
     std::unordered_map<std::string, bdd> alias;
+    std::unordered_map<std::string, spot::location> props;
     spot::location states_loc;
     spot::location ap_loc;
     spot::location state_label_loc;
@@ -89,6 +92,8 @@
     bool ignore_more_acc = false; // Set to true after the first
 				  // "Acceptance:" line has been read.
 
+    label_style_t label_style = Mixed_Labels;
+
     bool accept_all_needed = false;
     bool accept_all_seen = false;
     bool aliased_states = false;
@@ -254,6 +259,29 @@ header: format-version header-items
 	      error(@$, "missing 'Acceptance:' header");
 	      res.ignore_acc = true;
 	    }
+	  // Process properties.
+	  {
+	    auto trans_labels = res.props.find("trans-labels");
+	    auto state_labels = res.props.find("state-labels");
+	    if (trans_labels != res.props.end())
+	      {
+		if (state_labels == res.props.end())
+		  {
+		    res.label_style = Trans_Labels;
+		  }
+		else
+		  {
+		    error(trans_labels->second,
+			  "'property: trans-labels' is incompatible with...");
+		    error(state_labels->second,
+			  "... 'property: state-labels'.");
+		  }
+	      }
+	    else if (state_labels != res.props.end())
+	      {
+		res.label_style = State_Labels;
+	      }
+	  }
 	}
 
 version: IDENTIFIER
@@ -417,6 +445,7 @@ acc-spec: | acc-spec BOOLEAN
 	    }
 properties: | properties IDENTIFIER
 	      {
+		res.props.emplace(*$2, @2);
 		delete $2;
 	      }
 header-spec: | header-spec BOOLEAN
@@ -615,9 +644,21 @@ label: '[' label-expr ']'
 	     res.cur_label = bddtrue;
 	   }
 state-label_opt:       { res.has_state_label = false; }
-               | label { res.has_state_label = true;
-                         res.state_label_loc = @1;
-		         res.state_label = res.cur_label; }
+               | label
+	       {
+		 res.has_state_label = true;
+		 res.state_label_loc = @1;
+		 res.state_label = res.cur_label;
+		 if (res.label_style == Trans_Labels)
+		   {
+		     error(@$,
+			   "state label used although the automaton was...");
+		     error(res.props["trans-labels"],
+			   "... declared with 'property: trans-labels' here");
+		     // Do not show this error anymore.
+		     res.label_style = Mixed_Labels;
+		   }
+	       }
 trans-label: label
 	         {
 		   if (res.has_state_label)
@@ -627,6 +668,15 @@ trans-label: label
 			     "... the state is already labeled.");
 		       res.cur_label = res.state_label;
 		     }
+		   if (res.label_style == State_Labels)
+		     {
+		       error(@$, "transition label used although the "
+			     "automaton was...");
+		       error(res.props["state-labels"],
+			     "... declared with 'property: state-labels' here");
+		       // Do not show this error anymore.
+		       res.label_style = Mixed_Labels;
+		     }
 		 }
 
 acc-sig_opt:
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 886f0ccc9..4ac18c620 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -349,6 +349,7 @@ cat >input <<EOF
     AP: 3 "a" "b" "c"
     Alias: @a 0
     Alias: @a 1 & 2 /* should be @bc */
+    properties: state-labels /* this is bogus */
     --BODY--
     State: 0
     [!@a & !@bc] 0
@@ -360,10 +361,12 @@ EOF
 
 expecterr input <<EOF
 input:9.5-19: ignoring redefinition of alias @a
-input:12.13-15: unknown alias @bc
-input:13.12-14: unknown alias @bc
+input:13.13-15: unknown alias @bc
+input:13.5-16: transition label used although the automaton was...
+input:10.17-28: ... declared with 'property: state-labels' here
 input:14.12-14: unknown alias @bc
-input:15.11-13: unknown alias @bc
+input:15.12-14: unknown alias @bc
+input:16.11-13: unknown alias @bc
 EOF
 
 cat >input <<EOF
@@ -685,6 +688,33 @@ State: 2
 [t] 2
    1 2
 --END--
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Inf(0)
+properties: trans-labels /* this is bogus */
+--BODY--
+State: [1] 0 {0} 0
+--END--
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Inf(0)
+properties: state-labels trans-labels /* this is bogus */
+--BODY--
+State: [1] 0 {0} 0
+--END--
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 1 Inf(0)
+properties: state-labels /* OK */
+--BODY--
+State: [1] 0 {0} 0
+--END--
 EOF
 
 expecterr input <<EOF
@@ -692,6 +722,10 @@ input:10.1-4: cannot label this edge because...
 input:9.8-10: ... the state is already labeled.
 input:14.6: missing label for this edge (previous edge is labeled)
 input:17.1-3: ignoring this label, because previous edge has no label
+input:27.8-10: state label used although the automaton was...
+input:25.13-24: ... declared with 'property: trans-labels' here
+input:34.26-37: 'property: trans-labels' is incompatible with...
+input:34.13-24: ... 'property: state-labels'.
 EOF