diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 3746223b3..09c14f2e2 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -359,7 +359,9 @@ header-item: "States:" INT } | "name:" STRING { - delete $2; + res.h->aut->set_named_prop("automaton-name", $2, [](void* name) { + delete static_cast(name); + }); } | "properties:" properties | HEADERNAME header-spec diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index 9af87195b..b8a9e6772 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -250,7 +250,10 @@ namespace spot const char nl = newline ? '\n' : ' '; os << "HOA: v1" << nl; - if (f) + auto* n = aut->get_named_prop("automaton-name"); + if (n) + escape_str(os << "name: \"", *static_cast(n)) << '"' << nl; + else if (f) escape_str(os << "name: \"", to_string(f)) << '"' << nl; os << "States: " << num_states << nl << "Start: 0" << nl diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 958227236..9ba078ab0 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -384,6 +384,7 @@ EOF expectok input <expected <