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

simplify: improve the logic of some implication checks

Browse source 
Fixes #293.

* spot/tl/simplify.cc: Test implications that would yield tt or ff
first.  In rules of the form "if a => b, a op b = b" also check
if b => a, and in this case return smallest(a,b).
* tests/core/reduccmp.test: Add a test.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2017-10-11 21:47:31 +02:00
parent e6c4eb15c1
commit 42452ba4a3
3 changed files with 96 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -5,6 +5,9 @@ New in spot 2.4.1.dev (not yet released)
- Automata produced by "genaut --ks-nca=N" were incorrectly marked
as not complete.
- Fix some cases for which the highest setting of formulas
simplification would produce worse results than lower settings.
New in spot 2.4.1 (2017-10-05)
Bugs fixed: