From 2ef0ea00f44cfb3901d43591dcb49a9cb59532dd Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Thu, 3 Nov 2022 06:58:21 +0100 Subject: [PATCH] sere_to_tgba: produce state-names --- spot/twaalgos/ltl2tgba_fm.cc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 97008b0df..97a2eceb3 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -2259,9 +2259,11 @@ namespace spot const auto acc_mark = res->set_buchi(); size_t sn = namer->state_to_name.size(); + auto names = new std::vector(sn); for (size_t i = 0; i < sn; ++i) { formula g = namer->state_to_name[i]; + (*names)[i] = str_psl(g); if (g.accepts_eword()) { if (res->get_graph().state_storage(i).succ == 0) @@ -2274,6 +2276,8 @@ namespace spot } } + res->set_named_prop("state-names", names); + return res; } }