hoaparse: fix parsing of LBTT with non 0-based states

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/lbttparse.test: Add test cases.
* src/tgbatest/hoaparse.test: Adjust.

src/hoaparse/hoaparse.yy

@@ -82,6 +82,7 @@
       spot::acc_cond::mark_t neg_acc_sets = 0U;
       spot::acc_cond::mark_t pos_acc_sets = 0U;
       std::vector<std::string>* state_names = nullptr;
+      std::map<unsigned, unsigned> states_map;
       unsigned cur_state;
       int states = -1;
       int ap_count = -1;
@@ -1202,6 +1203,36 @@ nc-transition:
 lbtt: lbtt-header lbtt-body ENDAUT
       {
 	res.pos_acc_sets = res.h->aut->acc().all_sets();
+	assert(!res.states_map.empty());
+	auto n = res.states_map.size();
+	if (n != (unsigned) res.states)
+	  {
+	    std::ostringstream err;
+	    err << res.states << " states have been declared, but "
+		<< n << " different state numbers have been used";
+	    error(@$, err.str());
+	  }
+	if (res.states_map.rbegin()->first > (unsigned) res.states)
+	  {
+	    // We have seen number larger that the total number of
+	    // state in the automaton.  Usually this happens when the
+	    // states are numbered from 1 instead of 0, but the LBTT
+	    // documentation actually allow any number to be used.
+	    // What we have done is to map all input state numbers 0
+	    // <= .. < n to the digraph states with the same number,
+	    // and any time we saw a number larger than n, we mapped
+	    // it to a new state.  The correspondence is given by
+	    // res.states_map.  Now we just need to remove the useless
+	    // states we allocated.
+	    std::vector<unsigned> rename(res.h->aut->num_states(), -1U);
+	    unsigned s = 0;
+	    for (auto& i: res.states_map)
+	      rename[i.second] = s++;
+	    assert(s == (unsigned) res.states);
+	    for (auto& i: res.start)
+	      i.second = rename[i.second];
+	    res.h->aut->get_graph().defrag_states(std::move(rename), s);
+	  }
       }
     | lbtt-header-states LBTT_EMPTY
       {
@@ -1232,16 +1263,20 @@ lbtt-states:
 
 lbtt-state: STATE_NUM INT lbtt-acc
           {
-	    res.cur_state = $1;
+	    if ($1 >= (unsigned) res.states)
-	    if ((int) res.cur_state >= res.states)
 	      {
-		error(@1, "state number is larger than state "
+		auto p = res.states_map.emplace($1, 0);
-		      "count...");
+		if (p.second)
-		error(res.states_loc, "... declared here.");
+		  p.first->second = res.h->aut->new_state();
-		res.cur_state = 0;
+		res.cur_state = p.first->second;
 	      }
-	    else if ($2)
+	    else
-	      res.start.emplace_back(@1 + @2, $1);
+	      {
+		res.states_map.emplace($1, $1);
+		res.cur_state = $1;
+	      }
+	    if ($2)
+	      res.start.emplace_back(@1 + @2, res.cur_state);
 	    res.acc_state = $3;
 	  }
 lbtt-acc:               { $$ = 0U; }
@@ -1290,16 +1325,21 @@ lbtt-guard: STRING
 lbtt-transitions:
                 | lbtt-transitions DEST_NUM lbtt-acc lbtt-guard
                 {
-		  if ((int) $2 >= res.states)
+		  unsigned dst = $2;
+		  if (dst >= (unsigned) res.states)
 		    {
-		      error(@2, "state number is larger than state "
+		      auto p = res.states_map.emplace(dst, 0);
-			    "count...");
+		      if (p.second)
-		      error(res.states_loc, "... declared here.");
+			p.first->second = res.h->aut->new_state();
+		      dst = p.first->second;
 		    }
 		  else
-		    res.h->aut->new_transition(res.cur_state, $2,
+		    {
-					       res.cur_label,
+		      res.states_map.emplace(dst, dst);
-					       res.acc_state | $3);
+	            }
+		  res.h->aut->new_transition(res.cur_state, dst,
+		                             res.cur_label,
+					     res.acc_state | $3);
 		}
 
 %%

src/tgbatest/hoaparse.test

@@ -84,6 +84,7 @@ State: 1 {0}
 -1
 EOF
 
+diff='different state numbers have been used'
 expecterr input <<EOF
 input:8.5: state number is larger than state count...
 input:2.1-9: ... declared here.
@@ -91,10 +92,7 @@ input:9.8: state number is larger than state count...
 input:2.1-9: ... declared here.
 input:10.5: state number is larger than state count...
 input:2.1-9: ... declared here.
-input:13.1: state number is larger than state count...
+input:12.1-19.2: 2 states have been declared, but 3 $diff
-input:12.1: ... declared here.
-input:18.1: state number is larger than state count...
-input:12.1: ... declared here.
 EOF
 
 cat >input <<EOF

src/tgbatest/lbttparse.test

@@ -100,6 +100,48 @@ cat >input <<EOF
 -1 4 0 1 -1 4 ! p1
 -1 5 0 1 -1 5 t
 -1
+/* this one show that state numbers do not always start from 0 */
+1 1t
+1 1
+1 -1 !p0
+1 0 -1 p0
+-1
+/* This is the output of 'lbt' on the formula 'U p0 p1', but with
+   states 1 and 2 changed to 100 and 200 */
+4 1
+0 1 -1
+100 p0
+200 p1
+-1
+100 0 -1
+100 p0
+200 p1
+-1
+200 0 0 -1
+3 t
+-1
+3 0 0 -1
+3 t
+-1
+/* This is the output of 'lbt' on the formula 'U p0 p1', but with
+   states 0 and 2 changed to 100 and 200.  This make sure the renaming
+   also applies to the initial state.
+ */
+4 1
+100 1 -1
+1 p0
+200 p1
+-1
+1 0 -1
+1 p0
+200 p1
+-1
+200 0 0 -1
+3 t
+-1
+3 0 0 -1
+3 t
+-1
 EOF
 
 run 0 ../../bin/autfilt --stats '%s %t %e %a' input > output
@@ -108,6 +150,9 @@ cat >expected<<EOF
 4 16 6 1
 1 0 0 3
 6 20 9 1
+1 2 2 1
+4 16 6 1
+4 16 6 1
 EOF
 
 diff output expected