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

fix "requires separate Inf and Fin sets" error from ltl2tgba -G

Browse source 
Report from David Müller.

* spot/twaalgos/simulation.cc: Add wrapper to deal with automata
sharing Fin/Inf sets.
* tests/core/ltl2tgba2.test: New test cases.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2019-04-26 11:33:04 +02:00
parent 26e2f9cec8
commit b928d8c82a
3 changed files with 58 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -5,6 +5,11 @@ New in spot 2.7.3.dev (not yet released)
- separate_sets_here() (and therefore autfilt --separate-sets) could
loop infinitely on some inputs.
- In some situation, ltl2tgba -G could abort with
"direct_simulation() requires separate Inf and Fin sets". This
was fixed by teaching simulation-based reductions how to deal
with such cases.
New in spot 2.7.3 (2019-04-19)
Bugs fixed: