hoaparse: validate use of explicit-labels and implicit-labels

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.

src/hoaparse/hoaparse.yy

@@ -54,7 +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 };
+  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
+		       Implicit_Labels };
 
   struct result_
   {
@@ -261,12 +262,31 @@ header: format-version header-items
 	    }
 	  // Process properties.
 	  {
+	    auto explicit_labels = res.props.find("explicit-labels");
+	    auto implicit_labels = res.props.find("implicit-labels");
+	    if (implicit_labels != res.props.end())
+	      {
+		if (explicit_labels == res.props.end())
+		  {
+		    res.label_style = Implicit_Labels;
+		  }
+		else
+		  {
+		    error(implicit_labels->second,
+			  "'property: implicit-labels' is incompatible "
+			  "with...");
+		    error(explicit_labels->second,
+			  "... 'property: explicit-labels'.");
+		  }
+	      }
+
 	    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())
 		  {
+		    if (res.label_style != Implicit_Labels)
 		      res.label_style = Trans_Labels;
 		  }
 		else
@@ -278,9 +298,19 @@ header: format-version header-items
 		  }
 	      }
 	    else if (state_labels != res.props.end())
+	      {
+		if (res.label_style != Implicit_Labels)
 		  {
 		    res.label_style = State_Labels;
 		  }
+		else
+		  {
+		    error(state_labels->second,
+			  "'property: state-labels' is incompatible with...");
+		    error(implicit_labels->second,
+			  "... 'property: implicit-labels'.");
+		  }
+	      }
 	  }
 	}
 
@@ -612,10 +642,21 @@ states: | states state
 state: state-name labeled-edges
      | state-name unlabeled-edges
        {
-	 if (!res.has_state_label)
+	 if (!res.has_state_label) // Implicit labels
 	   {
 	     if (res.cur_guard != res.guards.end())
 	       error(@$, "not enough transitions for this state");
+
+	     if (res.label_style == State_Labels)
+	       {
+		 error(@2, "these transitions have implicit labels but the"
+		       " automaton is...");
+		 error(res.props["state-labels"], "... declared with "
+		       "'property: state-labels'");
+		 // Do not repeat this message.
+		 res.label_style = Mixed_Labels;
+	       }
+
 	     res.cur_guard = res.guards.begin();
 	   }
        }
@@ -649,12 +690,18 @@ state-label_opt:       { res.has_state_label = false; }
 		 res.has_state_label = true;
 		 res.state_label_loc = @1;
 		 res.state_label = res.cur_label;
-		 if (res.label_style == Trans_Labels)
+		 if (res.label_style == Trans_Labels
+		     || res.label_style == Implicit_Labels)
 		   {
 		     error(@$,
 			   "state label used although the automaton was...");
+		     if (res.label_style == Trans_Labels)
 		       error(res.props["trans-labels"],
 			     "... declared with 'property: trans-labels' here");
+		     else
+		       error(res.props["implicit-labels"],
+			     "... declared with 'property: implicit-labels' "
+			     "here");
 		     // Do not show this error anymore.
 		     res.label_style = Mixed_Labels;
 		   }
@@ -668,12 +715,19 @@ trans-label: label
 			     "... the state is already labeled.");
 		       res.cur_label = res.state_label;
 		     }
-		   if (res.label_style == State_Labels)
+		   if (res.label_style == State_Labels
+		       || res.label_style == Implicit_Labels)
 		     {
 		       error(@$, "transition label used although the "
 			     "automaton was...");
+		       if (res.label_style == State_Labels)
 			 error(res.props["state-labels"],
-			     "... declared with 'property: state-labels' here");
+			       "... declared with 'property: state-labels' "
+			       "here");
+		       else
+			 error(res.props["implicit-labels"],
+			       "... declared with 'property: implicit-labels' "
+			       "here");
 		       // Do not show this error anymore.
 		       res.label_style = Mixed_Labels;
 		     }

src/tgbatest/hoaparse.test

@@ -295,6 +295,7 @@ cat >input<<EOF
     acc-name: generalized-Buchi 2
     Acceptance: 2 (Inf(0) & Inf(1))
     AP: 2 "a" "b"
+    properties: state-labels
     --BODY--
     State: 0 "foo" { 0 }
       2  /* !a  & !b */
@@ -309,7 +310,9 @@ cat >input<<EOF
 EOF
 
 expecterr input <<EOF
-input:8.5-11.7: not enough transitions for this state
+input:9.5-12.7: not enough transitions for this state
+input:10.7-12.7: these transitions have implicit labels but the automaton is...
+input:7.17-28: ... declared with 'property: state-labels'
 EOF
 
 cat >input<<EOF
@@ -319,6 +322,7 @@ cat >input<<EOF
     Start: 0
     acc-name: generalized-Buchi 2
     Acceptance: 2 (Inf(0) & Inf(1))
+    properties: implicit-labels explicit-labels /* ? */
     AP: 2 "a" "b"
     --BODY--
     State: 0 "foo" { 0 }
@@ -332,10 +336,54 @@ cat >input<<EOF
     State: 2 "sink state" { 0 }
       2 2 2 2
     --END--
+    HOA: v1
+    tool: "test"
+    States: 3
+    Start: 0
+    acc-name: generalized-Buchi 2
+    Acceptance: 2 (Inf(0) & Inf(1))
+    properties: implicit-labels state-labels /* ? */
+    AP: 2 "a" "b"
+    --BODY--
+    State: 0 "foo" { 0 }
+      2  /* !a  & !b */
+      0  /*  a  & !b */
+      1  /* !a  &  b */
+      1  /*  a  &  b */
+    State: 1 { 1 }
+      1 1 1 1       /* four transitions on one line */
+    State: 2 "sink state" { 0 }
+      2 2 2 2
+    --END--
+    HOA: v1
+    tool: "test"
+    States: 3
+    Start: 0
+    acc-name: generalized-Buchi 2
+    Acceptance: 2 (Inf(0) & Inf(1))
+    properties: implicit-labels
+    AP: 2 "a" "b"
+    --BODY--
+    State: 0 "foo" { 0 }
+      2  /* !a  & !b */
+      0  /*  a  & !b */
+      1  /* !a  &  b */
+      1  /*  a  &  b */
+    State: 1 { 1 }
+      1 1 1 1       /* four transitions on one line */
+    State: 2 "sink state" { 0 }
+      [t] 2
+    --END--
 EOF
 
 expecterr input <<EOF
-input:14.7: too many transition for this state, ignoring this one
+input:7.17-31: 'property: implicit-labels' is incompatible with...
+input:7.33-47: ... 'property: explicit-labels'.
+input:15.7: too many transition for this state, ignoring this one
+input:27.33-44: 'property: state-labels' is incompatible with...
+input:27.17-31: ... 'property: implicit-labels'.
+input:57.7-9: transition label used although the automaton was...
+input:46.17-31: ... declared with 'property: implicit-labels' here
 EOF