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

relabel: do not unregister old AP that are also new

Browse source 
Reported by Ayrat Khalimov against the trans.html page when using
ltl3ba.

* spot/twaalgos/relabel.cc: Here.
* tests/core/ltl3dra.test: Test it.
* NEWS: Mention it.
* THANKS: Add Ayrat.
This commit is contained in:
Alexandre Duret-Lutz 2016-07-07 15:57:14 +02:00
parent 70064d0b75
commit 2665b5780a
4 changed files with 19 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -13,6 +13,10 @@ New in spot 2.0.2a (Not yet released)
* The generalized testing automata displayed by the on-line
translator were incorrect (those output by ltl2tgta were OK).
* ltl2tgta should not offer options --ba, --monitor, --tgba and such.
* the relabel() function could incorrectly unregister old atomic
propositions even if they are still used in the output (e.g., if
a&p0 is relabeled to p0&p1). This could cause ltldo and on-line
translator to report errors.
New in spot 2.0.2 (2016-06-17)