merge_states: include sorting and detection of identical self-loops

* spot/twa/twagraph.cc: Implement it.
* spot/twa/twagraph.hh, NEWS: Document it.
* tests/python/mergedge.py: Test it.
* tests/core/ltlsynt.test, tests/python/games.ipynb: Adjust expectations.
This commit is contained in:
Alexandre Duret-Lutz 2021-05-17 18:30:16 +02:00
parent e12f22f82a
commit 634dd28379
6 changed files with 89 additions and 27 deletions

View file

@ -295,6 +295,27 @@ namespace spot
throw std::runtime_error(
"twa_graph::merge_states() does not work on alternating automata");
typedef graph_t::edge_storage_t tr_t;
g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
{
if (lhs.src < rhs.src)
return true;
if (lhs.src > rhs.src)
return false;
if (lhs.acc < rhs.acc)
return true;
if (lhs.acc > rhs.acc)
return false;
if (bdd_less_than_stable lt; lt(lhs.cond, rhs.cond))
return true;
if (rhs.cond != lhs.cond)
return false;
// The destination must be sorted last
// for our self-loop optimization to work.
return lhs.dst < rhs.dst;
});
g_.chain_edges_();
const unsigned nb_states = num_states();
std::vector<unsigned> remap(nb_states, -1U);
for (unsigned i = 0; i != nb_states; ++i)
@ -306,7 +327,9 @@ namespace spot
if (std::equal(out1.begin(), out1.end(), out2.begin(), out2.end(),
[](const edge_storage_t& a,
const edge_storage_t& b)
{ return a.dst == b.dst && a.data() == b.data(); }))
{ return ((a.dst == b.dst
|| (a.dst == a.src && b.dst == b.src))
&& a.data() == b.data()); }))
{
remap[i] = j;
break;

View file

@ -572,10 +572,14 @@ namespace spot
/// \brief Merge states that can be merged.
///
/// This merges states that have the exact same outgoing edges. This method
/// compares the successors of states in the order in which they are stored.
/// Therefore, it is better to call it when you know that the edges are
/// stored, e.g. after a call to merge_edges().
/// Two states can be merged if the set of outgoing transitions
/// is identical, i.e., same condition, same colors, same destination.
/// Two self-loops with the same condition and colors are considered
/// identical even if they do not actually have the same destination.
///
/// The implementation will sort the edges of the automaton to
/// ease the comparison between two states. This may miss some
/// self-loop based in non-deterministic automata.
void merge_states();
/// \brief Remove all dead states