parseaut: diagnose states that are unused and undefined

Reported by Pierre Ganty.

* spot/parseaut/parseaut.yy: Add diagnostics.
* tests/core/parseaut.test: Adjust expected output, and add a test
case.
* NEWS: Mention the bug.

NEWS

@@ -19,6 +19,10 @@ New in spot 2.11.2.dev  (not yet released)
     otherwise, libraries get installed in the wrong place on Debian.
     (Issue #512.)
 
+  - The HOA parser used to silently declare unused and undefined states
+    (e.g., when the State: header declare many more states than the body
+    of the file).  It now warns about those.
+
 New in spot 2.11.2  (2022-10-26)
 
   Command-line tools:

spot/parseaut/parseaut.yy

@@ -1231,6 +1231,7 @@ body: states
 	// diagnostic, so let not add another one.
 	if (res.states >= 0)
 	  n = res.states;
+        std::vector<unsigned> unused_undeclared;
 	for (unsigned i = 0; i < n; ++i)
 	  {
 	    auto& p = res.info_states[i];
@@ -1239,17 +1240,43 @@ body: states
                 if (p.used)
                   error(p.used_loc,
                         "state " + std::to_string(i) + " has no definition");
-                if (!p.used && res.complete)
+                if (!p.used)
-                  if (auto p = res.prop_is_true("complete"))
+                  unused_undeclared.push_back(i);
-                    {
-                      error(res.states_loc,
-                            "state " + std::to_string(i) +
-                            " has no definition...");
-                      error(p.loc, "... despite 'properties: complete'");
-                    }
                 res.complete = false;
               }
 	  }
+        if (!unused_undeclared.empty())
+          {
+            std::ostringstream out;
+            unsigned uus = unused_undeclared.size();
+            int rangestart = -2;
+            int rangecur = -2;
+            const char* sep = uus > 1 ? "states " : "state ";
+            auto print_range = [&]() {
+              if (rangecur < 0)
+                return;
+              out << sep << rangestart;
+              if (rangecur != rangestart)
+                out << '-' << rangecur;
+              sep = ",";
+            };
+            for (unsigned s: unused_undeclared)
+              {
+                if ((int)s != rangecur + 1)
+                  {
+                    print_range();
+                    rangestart = s;
+                  }
+                rangecur = s;
+              }
+            print_range();
+            out << (uus > 1 ? " are" : " is") << " unused and undefined";
+            error(res.states_loc, out.str());
+
+            if (auto p = res.prop_is_true("complete"))
+              error(p.loc, "automaton is incomplete because it has "
+                    "undefined states");
+          }
         if (res.complete)
           if (auto p = res.prop_is_false("complete"))
             {

tests/core/parseaut.test

@@ -230,6 +230,7 @@ input:3.1-8: initial state number is larger than state count...
 input:4.1-9: ... declared here.
 input:1.1-4.9: missing 'Acceptance:' header
 input:3.1-8: initial state 1 has no definition
+input:4.1-9: state 0 is unused and undefined
 EOF
 
 cat >input <<EOF
@@ -2096,8 +2097,8 @@ input:46.30-33: 'properties: weak' contradicts...
 input:46.13-28: ... 'properties: !inherently-weak' given here
 input:55.22-26: 'properties: !weak' contradicts...
 input:55.28-36: ... 'properties: very-weak' given here
-input:51.1-9: state 1 has no definition...
+input:51.1-9: state 1 is unused and undefined
-input:55.13-20: ... despite 'properties: complete'
+input:55.13-20: automaton is incomplete because it has undefined states
 EOF
 
 
@@ -2281,6 +2282,15 @@ State: 0
 [!0&1] 2
 [0&1] 0&1
 --END--
+HOA: v1
+Start: 2
+States: 10
+AP: 2 "a" "b"
+Acceptance: 1 Fin(0)
+--BODY--
+State: 2
+[!0&!1] 6
+--END--
 EOF
 
 expecterr input<<EOF
@@ -2299,6 +2309,8 @@ input:26.11: state 1 has no definition
 input:28.8: state 2 has no definition
 input:32.1-10: initial state 1 has no definition
 input:42.8: state 2 has no definition
+input:52.9: state 6 has no definition
+input:47.1-10: states 0-1,3-5,7-9 are unused and undefined
 EOF