From f0e4efa238f57d72bf90952bbafe3a10edb5c6c7 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Thu, 10 Mar 2022 12:16:18 +0100 Subject: [PATCH] twagraph: merge_edges supports finite automata * spot/twa/twagraph.cc: don't remove false-labeled edges if the automaton uses state-based acceptance and the edge is a self loop --- spot/twa/twagraph.cc | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 2a72702f3..197ea190c 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -241,11 +241,15 @@ namespace spot // them. }); + bool is_state_acc = this->prop_state_acc().is_true(); + unsigned out = 0; unsigned in = 1; // Skip any leading false edge. - while (in < tend && trans[in].cond == bddfalse) + while (in < tend + && trans[in].cond == bddfalse + && (!is_state_acc || trans[in].src != trans[in].dst)) ++in; if (in < tend) { @@ -254,7 +258,9 @@ namespace spot trans[out] = trans[in]; for (++in; in < tend; ++in) { - if (trans[in].cond == bddfalse) // Unusable edge + if (trans[in].cond == bddfalse + && (!is_state_acc + || trans[in].src != trans[in].dst)) // Unusable edge continue; // Merge edges with the same source, destination, and // colors. (We test the source last, because this is the