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

twa_graph: introduce copy_state_names_from()

Browse source 
* spot/twa/twagraph.cc, spot/twa/twagraph.hh: Here.  Also
make sure "original-states" survives defrag_states().
* NEWS: Mention it.
* tests/python/origstate.py: New file.
* tests/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz 2017-04-10 19:26:52 +02:00
parent 865171230f
commit 46d8aaaae1
5 changed files with 160 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

39
spot/twa/twagraph.cc
View file

@ -542,6 +542,7 @@ namespace spot
unsigned dst = newst[s];
if (dst == s || dst == -1U)
continue;
assert(dst < s);
(*names)[dst] = std::move((*names)[s]);
}
names->resize(used_states);
@ -558,6 +559,19 @@ namespace spot
}
std::swap(*hs, hs2);
}
if (auto os = get_named_prop<std::vector<unsigned>>("original-states"))
{
unsigned size = os->size();
for (unsigned s = 0; s < size; ++s)
{
unsigned dst = newst[s];
if (dst == s || dst == -1U)
continue;
assert(dst < s);
(*os)[dst] = (*os)[s];
}
os->resize(used_states);
}
init_number_ = newst[init_number_];
g_.defrag_states(std::move(newst), used_states);
}
@ -582,5 +596,30 @@ namespace spot
}
}
void twa_graph::copy_state_names_from(const const_twa_graph_ptr& other)
{
if (other == shared_from_this())
return;
auto orig = get_named_prop<std::vector<unsigned>>("original-states");
if (orig && orig->size() != num_states())
throw std::runtime_error("copy_state_names_from(): unexpected size "
"for original-states");
auto names = std::unique_ptr<std::vector<std::string>>
(new std::vector<std::string>);
unsigned ns = num_states();
unsigned ons = other->num_states();
for (unsigned s = 0; s < ns; ++s)
{
unsigned other_s = orig ? (*orig)[s] : s;
if (other_s >= ons)
throw std::runtime_error("copy_state_names_from(): state does not"
" exist in source automaton");
names->emplace_back(other->format_state(other_s));
}
set_named_prop("state-names", names.release());
}
}

8
spot/twa/twagraph.hh
View file

@ -566,6 +566,14 @@ namespace spot
/// automaton, those that are not actually used by its labels.
void remove_unused_ap();
/// \brief Define the state names of this automaton using
/// the names from \a other.
///
/// If the "original-states" named property is set, it is used to
/// map the state numbers, otherwise an identity mapping is
/// assumed.
void copy_state_names_from(const const_twa_graph_ptr& other);
acc_cond::mark_t state_acc_sets(unsigned s) const
{
if (SPOT_UNLIKELY(!(bool)prop_state_acc()))