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 d2bc100656
commit f0e4efa238
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

@ -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