alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sere_to_tgba: produce state-names

Browse source
This commit is contained in:
Antoine Martin 2022-11-03 06:58:21 +01:00
parent 7b936819cc
commit e80c98751d
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -2218,9 +2218,11 @@ namespace spot
const auto acc_mark = res->set_buchi(); const auto acc_mark = res->set_buchi();
size_t sn = namer->state_to_name.size(); size_t sn = namer->state_to_name.size();
auto names = new std::vector<std::string>(sn);
for (size_t i = 0; i < sn; ++i) for (size_t i = 0; i < sn; ++i)
{ {
formula g = namer->state_to_name[i]; formula g = namer->state_to_name[i];
(*names)[i] = str_psl(g);
if (g.accepts_eword()) if (g.accepts_eword())
{ {
if (res->get_graph().state_storage(i).succ == 0) if (res->get_graph().state_storage(i).succ == 0)
@ -2233,6 +2235,8 @@ namespace spot
} }
} }
res->set_named_prop("state-names", names);
return res; return res;
} }
} }