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

twagraph: merge_edges supports finite automata

Browse source 
* spot/twa/twagraph.cc: don't remove false-labeled edges if the
  automaton uses state-based acceptance and the edge is a self loop
This commit is contained in:
Antoine Martin 2022-03-10 12:16:18 +01:00
parent 05c40cfdf7
commit 50bb4eca6f
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/twa/twagraph.cc
View file

@ -164,11 +164,15 @@ namespace spot
// them. // them.
}); });
bool is_state_acc = this->prop_state_acc().is_true();
unsigned out = 0; unsigned out = 0;
unsigned in = 1; unsigned in = 1;
// Skip any leading false edge. // 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; ++in;
if (in < tend) if (in < tend)
{ {
@ -177,7 +181,9 @@ namespace spot
trans[out] = trans[in]; trans[out] = trans[in];
for (++in; in < tend; ++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; continue;
// Merge edges with the same source, destination, and // Merge edges with the same source, destination, and
// colors. (We test the source last, because this is the // colors. (We test the source last, because this is the