hoaparse: validate use of deterministic and complete

* src/hoaparse/hoaparse.yy: validate deterministic and
complete when parsing HOA.  Also set the deterministic
property on the TGBA.
* src/tgbatest/hoaparse.test: Test errors.

src/hoaparse/hoaparse.yy

@@ -98,6 +98,10 @@
     bool accept_all_needed = false;
     bool accept_all_seen = false;
     bool aliased_states = false;
+
+    bool deterministic = false;
+    bool complete = false;
+
     std::map<std::string, spot::location> labels;
 
     ~result_()
@@ -312,6 +316,43 @@ header: format-version header-items
 		  }
 	      }
 	  }
+	  {
+	    unsigned ss = res.start.size();
+	    if (ss > 1)
+	      {
+		auto det = res.props.find("deterministic");
+		if (det != res.props.end())
+		  {
+		    error(det->second,
+			  "deterministic automata should have at most "
+			  "one initial state");
+		  }
+		res.deterministic = false;
+	      }
+	    else
+	      {
+		// Assume the automaton is deterministic until proven
+		// wrong.
+		res.deterministic = true;
+	      }
+	    if (ss < 1)
+	      {
+		auto complete = res.props.find("complete");
+		if (complete != res.props.end())
+		  {
+		    error(complete->second,
+			  "complete automata should have at least "
+			  "one initial state");
+		  }
+		res.complete = false;
+	      }
+	    else
+	      {
+		// Assume the automaton is complete until proven
+		// wrong.
+		res.complete = true;
+	      }
+	  }
 	}
 
 version: IDENTIFIER
@@ -639,6 +680,39 @@ checked-state-num: state-num
 		   }
 
 states: | states state
+        {
+	  if (res.deterministic || res.complete)
+	    {
+	      bdd available = bddtrue;
+	      bool det = true;
+	      for (auto& t: res.h->aut->out(res.cur_state))
+		{
+		  if (det && !bdd_implies(t.cond, available))
+		    det = false;
+		  available -= t.cond;
+		}
+	      if (res.deterministic && !det)
+		{
+		  res.deterministic = false;
+		  auto p = res.props.find("deterministic");
+		  if (p != res.props.end())
+		    {
+		      error(@2, "automaton is not deterministic...");
+		      error(p->second, "... despite 'property: deterministic'");
+		    }
+		}
+	      if (res.complete && available != bddfalse)
+		{
+		  res.complete = false;
+		  auto p = res.props.find("complete");
+		  if (p != res.props.end())
+		    {
+		      error(@2, "automaton is not complete...");
+		      error(p->second, "... despite 'property: complete'");
+		    }
+		}
+	    }
+	}
 state: state-name labeled-edges
      | state-name unlabeled-edges
        {
@@ -661,6 +735,11 @@ state: state-name labeled-edges
 	   }
        }
      | error
+       {
+	 // Assume the worse.
+	 res.deterministic = false;
+	 res.complete = false;
+       }
 
 state-name: "State:" state-label_opt checked-state-num string_opt acc-sig_opt
 	  {
@@ -1066,6 +1145,7 @@ lbtt-header: lbtt-header-states INT_S
 lbtt-body: lbtt-states
 lbtt-states:
            | lbtt-states lbtt-state lbtt-transitions
+
 lbtt-state: STATE_NUM INT lbtt-acc
           {
 	    res.cur_state = $1;
@@ -1225,6 +1305,12 @@ static void fix_initial_state(result_& r)
     }
 }
 
+static void fix_properties(result_& r)
+{
+  r.h->aut->prop_deterministic(r.deterministic);
+  //r.h->aut->prop_complete(r.complete);
+}
+
 namespace spot
 {
   hoa_stream_parser::hoa_stream_parser(const std::string& name)
@@ -1272,6 +1358,7 @@ namespace spot
     if (r.neg_acc_sets)
       fix_acceptance(r);
     fix_initial_state(r);
+    fix_properties(r);
     return r.h;
   };
 }

src/tgbatest/hoaparse.test

@@ -295,7 +295,7 @@ cat >input<<EOF
     acc-name: generalized-Buchi 2
     Acceptance: 2 (Inf(0) & Inf(1))
     AP: 2 "a" "b"
-    properties: state-labels
+    properties: state-labels complete
     --BODY--
     State: 0 "foo" { 0 }
       2  /* !a  & !b */
@@ -307,12 +307,34 @@ cat >input<<EOF
     State: 2 "sink state" { 0 }
       2 2 2 2
     --END--
+HOA: v1
+States: 3
+Start: 0
+acc-name: generalized-Buchi 2
+Acceptance: 2 (Inf(0) & Inf(1))
+AP: 2 "a" "b"
+properties: implicit-labels complete
+--BODY--
+State: [t] 0 "foo" { 0 }
+  2  /* !a  & !b */
+  0  /*  a  & !b */
+  1  /* !a  &  b */
+  0  /*  a  &  b */
+State: 1 { 1 }
+  1 1 1 1       /* four transitions on one line */
+State: 2 "sink state" { 0 }
+  2 2 2 2
+--END--
 EOF
 
 expecterr input <<EOF
 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'
+input:9.5-12.7: automaton is not complete...
+input:7.30-37: ... despite 'property: complete'
+input:27.8-10: state label used although the automaton was...
+input:25.13-27: ... declared with 'property: implicit-labels' here
 EOF
 
 cat >input<<EOF
@@ -322,7 +344,7 @@ cat >input<<EOF
     Start: 0
     acc-name: generalized-Buchi 2
     Acceptance: 2 (Inf(0) & Inf(1))
-    properties: implicit-labels explicit-labels /* ? */
+    properties: implicit-labels explicit-labels /* ? */ complete
     AP: 2 "a" "b"
     --BODY--
     State: 0 "foo" { 0 }
@@ -550,6 +572,50 @@ EOF
 
 diff expected input.out
 
+cat >input <<EOF
+HOA: v1
+States: 2
+Start: 0
+Start: 1
+AP: 2 "a" "\"b\""
+Acceptance: 1 Inf(0)
+properties: deterministic
+--BODY--
+State: 0 {0}
+[1] 1
+[!1] 0
+State: 1
+[!0] 1
+[0] 0
+--END--
+HOA: v1
+States: 0
+AP: 0
+Acceptance: 1 Inf(0)
+properties: complete
+--BODY--
+--END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "\"b\""
+Acceptance: 1 Inf(0)
+properties: deterministic
+--BODY--
+State: 0 {0}
+[1] 1
+[!1] 0
+State: 1
+[!0] 1
+[!0] 0
+--END--
+EOF
+expecterr input <<EOF
+input:7.13-25: deterministic automata should have at most one initial state
+input:20.13-20: complete automata should have at least one initial state
+input:33.1-35.6: automaton is not deterministic...
+input:28.13-25: ... despite 'property: deterministic'
+EOF
 
 # Mix HOA with neverclaims and LBTT automata
 cat >input <<EOF