diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index d35d5be6b..c7d8a051d 100644 --- a/src/hoaparse/hoaparse.yy +++ b/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* state_names = nullptr; unsigned cur_state; int states = -1; int ap_count = -1; @@ -176,6 +177,7 @@ %type checked-state-num state-num acc-set %type label-expr %type acc-sig acc-sets trans-acc_opt state-acc_opt +%type 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(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 || diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 458805c3d..eb57bf5e8 100644 --- a/src/tgbaalgos/dotty.cc +++ b/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* 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>("state-names"); mark_states_ = !opt_force_acc_trans_ && aut_->is_sba(); auto si = std::unique_ptr(opt_scc_ ? new scc_info(aut) : nullptr); diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index 4c68ac006..e4b7c427c 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -283,6 +283,7 @@ namespace spot os << " deterministic"; os << nl; os << "--BODY--" << nl; + auto sn = aut->get_named_prop>("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; diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 6f63e11f7..0e448fc2e 100755 --- a/src/tgbatest/hoaparse.test +++ b/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} diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 0baa2e398..4b6505ebb 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -286,7 +286,7 @@ EOF diff output expected -$autfilt --dot=vcsn >output <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"]