Commit 778d8fe9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltl2tgba_fm: make it easier to preserve state names

* src/twa/twagraph.cc, src/twa/twagraph.hh (create_formula_namer,
release_formula_namer): New functions.
* src/twaalgos/ltl2tgba_fm.cc: Use it.
parent 487a86d0
......@@ -19,9 +19,39 @@
#include "twagraph.hh"
#include "ltlast/constant.hh"
#include "ltlvisit/tostring.hh"
namespace spot
{
void
twa_graph::release_formula_namer(typename namer<const ltl::formula*>::type*
namer, bool keep_names)
{
if (keep_names)
{
auto v = new std::vector<std::string>(num_states());
auto& n = namer->names();
unsigned ns = n.size();
assert(n.size() <= v->size());
for (unsigned i = 0; i < ns; ++i)
{
auto f = n[i];
if (f)
{
(*v)[i] = to_string(f);
f->destroy();
}
}
set_named_prop("state-names", v);
}
else
{
for (auto n: namer->names())
if (n)
n->destroy();
}
delete namer;
}
void twa_graph::merge_transitions()
{
......
......@@ -25,6 +25,7 @@
#include "twa/bdddict.hh"
#include "twa/twa.hh"
#include "twaalgos/dupexp.hh"
#include "ltlast/formula.hh"
#include <sstream>
namespace spot
......@@ -222,6 +223,16 @@ namespace spot
return new named_graph<graph_t, State_Name, Name_Hash, Name_Equal>(g_);
}
typename namer<const ltl::formula*>::type*
create_formula_namer()
{
return create_namer<const ltl::formula*>();
}
void
release_formula_namer(typename namer<const ltl::formula*>::type* namer,
bool keep_names);
graph_t& get_graph()
{
return g_;
......
......@@ -2537,9 +2537,8 @@ namespace spot
}
}
for (auto n: namer->names())
n->destroy();
delete namer;
// Set the following to true to preserve state names.
a->release_formula_namer(namer, false);
dict->register_propositions(fc.used_vars(), a);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment