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

propagate_marks_here can break state-acc prop

Browse source 
* spot/twaalgos/degen.cc: Fix
* tests/python/pdegen.py: Test
This commit is contained in:
Philipp Schlehuber-Caissier 2022-06-29 14:02:25 +02:00
parent ddbdcd39cb
commit 99bf152673
2 changed files with 45 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/degen.cc
View file

@ -1168,5 +1168,9 @@ namespace spot
unsigned idx = aut->edge_number(e);
e.acc = marks[idx];
}
// If aut was state-based acc before, this might no longer
// this might no longer be the case
if (aut->prop_state_acc() == 1)
aut->prop_state_acc(0);
}
}