hoa,dot: propagate state names

* src/hoaparse/hoaparse.yy: Store state names.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/hoa.cc: Output them.
* src/tgbatest/readsave.test: Test this.
* src/tgbatest/hoaparse.test: Update.

src/hoaparse/hoaparse.yy

@@ -81,6 +81,7 @@
       spot::acc_cond::mark_t acc_state;
       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;
       unsigned cur_state;
       int states = -1;
       int ap_count = -1;
@@ -176,6 +177,7 @@
 %type <num> checked-state-num state-num acc-set
 %type <b> label-expr
 %type <mark> acc-sig acc-sets trans-acc_opt state-acc_opt
+%type <str> string_opt
 
 /**** NEVERCLAIM tokens ****/
 
@@ -245,7 +247,8 @@ aut-1: hoa
 hoa: header "--BODY--" body "--END--"
 hoa: error "--END--"
 
-string_opt: | STRING
+string_opt: { $$ = nullptr; }
+          | STRING { $$ = $1; }
 BOOLEAN: 't' | 'f'
 
 header: format-version header-items
@@ -495,6 +498,7 @@ header-item: "States:" INT
            | "tool:" STRING string_opt
              {
 	       delete $2;
+	       delete $3;
 	     }
            | "name:" STRING
              {
@@ -772,6 +776,7 @@ state: state-name labeled-edges
 	 res.complete = false;
        }
 
+
 state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt
 	  {
 	    res.cur_state = $3;
@@ -783,6 +788,17 @@ state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt
 	      }
 	    res.declared_states[$3] = true;
 	    res.acc_state = $5;
+	    if ($4)
+	      {
+		if (!res.state_names)
+		  res.state_names =
+		    new std::vector<std::string>(res.states > 0 ?
+						 res.states : 0);
+		if (res.state_names->size() < $3 + 1)
+		  res.state_names->resize($3 + 1);
+		(*res.state_names)[$3] = std::move(*$4);
+		delete $4;
+	      }
 	  }
 label: '[' label-expr ']'
 	   {
@@ -1434,6 +1450,8 @@ namespace spot
       return r.h;
     if (!r.h->aut)
       return nullptr;
+    if (r.state_names)
+      r.h->aut->set_named_prop("state-names", r.state_names);
     if (r.neg_acc_sets)
       fix_acceptance(r);
     if (r.acc_style == State_Acc ||

src/tgbaalgos/dotty.cc

@@ -46,6 +46,7 @@ namespace spot
       bool mark_states_ = false;
       bool opt_scc_ = false;
       const_tgba_digraph_ptr aut_;
+      std::vector<std::string>* sn_;
 
     public:
       dotty_output(std::ostream& os, const char* options)
@@ -107,8 +108,12 @@ namespace spot
       void
       process_state(unsigned s)
       {
-	os_ << "  " << s << " [label=\"" << escape_str(aut_->format_state(s))
-	    << '"';
+	os_ << "  " << s << " [label=\"";
+	if (sn_ && s < sn_->size() && !(*sn_)[s].empty())
+	  os_ << escape_str((*sn_)[s]);
+	else
+	  os_ << s;
+	os_ << '"';
 	if (mark_states_ && aut_->state_is_accepting(s))
 	  os_ << ", peripheries=2";
 	os_ << "]\n";
@@ -132,6 +137,7 @@ namespace spot
       void print(const const_tgba_digraph_ptr& aut)
       {
 	aut_ = aut;
+	sn_ = aut->get_named_prop<std::vector<std::string>>("state-names");
 	mark_states_ = !opt_force_acc_trans_ && aut_->is_sba();
 	auto si =
 	  std::unique_ptr<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr);

src/tgbaalgos/hoa.cc

@@ -283,6 +283,7 @@ namespace spot
       os << " deterministic";
     os << nl;
     os << "--BODY--" << nl;
+    auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
     for (unsigned i = 0; i < num_states; ++i)
       {
 	hoa_acceptance this_acc = acceptance;
@@ -291,6 +292,8 @@ namespace spot
 		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
 
 	os << "State: " << i;
+	if (sn && i < sn->size() && !(*sn)[i].empty())
+	  os << " \"" << (*sn)[i] << '"';
 	if (this_acc == Hoa_Acceptance_States)
 	  {
 	    acc_cond::mark_t acc = 0U;

src/tgbatest/hoaparse.test

@@ -270,7 +270,7 @@ acc-name: generalized-Buchi 2
 Acceptance: 2 Inf(0)&Inf(1)
 properties: trans-labels explicit-labels state-acc complete deterministic
 --BODY--
-State: 0 {0}
+State: 0 "foo" {0}
 [!0&!1] 2
 [0&!1] 0
 [!0&1] 1
@@ -280,7 +280,7 @@ State: 1 {1}
 [0&!1] 1
 [!0&1] 1
 [0&1] 1
-State: 2 {0}
+State: 2 "sink state" {0}
 [!0&!1] 2
 [0&!1] 2
 [!0&1] 2
@@ -1191,30 +1191,30 @@ acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete
 --BODY--
-State: 0
+State: 0 "T0_init"
 [5] 5
 [t] 4
 [0] 3
 [0&1&2] 2
 [0&1&2&3 | 0&1&2&4] 1
-State: 1 {0}
+State: 1 "accept_S1" {0}
 [t] 4
 [0] 3
 [0&1&2] 2
 [0&1&2&3 | 0&1&2&4] 1
-State: 2
+State: 2 "T2_S1"
 [t] 2
 [3 | 4] 1
-State: 3
+State: 3 "T1_S1"
 [t] 3
 [1&2] 2
 [1&2&3 | 1&2&4] 1
-State: 4
+State: 4 "T0_S1"
 [t] 4
 [0] 3
 [0&1&2] 2
 [0&1&2&3 | 0&1&2&4] 1
-State: 5 {0}
+State: 5 "accept_all" {0}
 [t] 5
 --END--
 EOF
@@ -1260,7 +1260,7 @@ acc-name: generalized-Buchi 3
 Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
 properties: trans-labels explicit-labels trans-acc complete
 --BODY--
-State: 0
+State: 0 "(x)"
 [5] 1 {0 1 2}
 [t] 2
 [0] 2
@@ -1270,9 +1270,9 @@ State: 0
 [0&3 | 0&4] 2
 [1&2&3 | 1&2&4] 2
 [0&1&2&3 | 0&1&2&4] 2
-State: 1
+State: 1 "t"
 [t] 1 {0 1 2}
-State: 2
+State: 2 "G((F(a) && F((b) && (c))) && F((d) || (e)))"
 [t] 2
 [0] 2 {0}
 [1&2] 2 {1}

src/tgbatest/readsave.test

@@ -286,7 +286,7 @@ EOF
 diff output expected
 
 
-$autfilt --dot=vcsn >output <<EOF
+$autfilt -H <<EOF | $autfilt --dot=vcsn >output
 HOA: v1
 States: 4
 Start: 2
@@ -296,13 +296,13 @@ acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc
 --BODY--
-State: 0 {0}
+State: 0 "s0" {0}
 [1] 0
-State: 1 {0}
+State: 1 "s1" {0}
 [0] 1
-State: 2
+State: 2 "s2"
 [1] 0
-State: 3
+State: 3 "s3"
 [0] 1
 --END--
 EOF
@@ -314,19 +314,19 @@ digraph G {
   I -> 3
   subgraph cluster_0 {
   label=""
-  1 [label="1"]
+  1 [label="s1"]
   }
   subgraph cluster_1 {
   label=""
-  0 [label="0"]
+  0 [label="s0"]
   }
   subgraph cluster_2 {
   label=""
-  3 [label="3"]
+  3 [label="s3"]
   }
   0 -> 0 [label="b\n{0}"]
   1 -> 1 [label="a\n{0}"]
-  2 [label="2"]
+  2 [label="s2"]
   2 -> 0 [label="b"]
   3 -> 1 [label="a"]
   3 -> 0 [label="b"]