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

ltlcross: fix swapped automata in error diagnostic

Browse source 
Failures could be reported against "Comp(Ni)*Comp(Pj)" when
it was really "Comp(Nj)*Comp(Pi)" that failed.

* bin/ltlcross.cc: Here.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2016-07-13 14:33:18 +02:00
parent 556db2a203
commit a2f0b22810
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -80,6 +80,12 @@ New in spot 2.0.3a (not yet released)
* A new example page shows how to test the equivalence of * A new example page shows how to test the equivalence of
two LTL/PSL formulas. https://spot.lrde.epita.fr/tut04.html two LTL/PSL formulas. https://spot.lrde.epita.fr/tut04.html
Bug fixes:
* When ltlcross found a bug using a product of complemented
automata, the error message would report "Comp(Ni)*Comp(Pj)" as
non-empty while the actual culprit was "Comp(Nj)*Comp(Pi)".
New in spot 2.0.3 (2016-07-11) New in spot 2.0.3 (2016-07-11)
Bug fixes: Bug fixes:

4
bin/ltlcross.cc
View file

@ -1184,8 +1184,8 @@ namespace
if (comp_pos[i] && comp_neg[j] && if (comp_pos[i] && comp_neg[j] &&
(i == j || (!comp_neg[i] && !comp_pos[j]))) (i == j || (!comp_neg[i] && !comp_pos[j])))
problems += problems +=
check_empty_prod(comp_pos[i], comp_neg[j], check_empty_prod(comp_neg[j], comp_pos[i],
i, j, true, true); j, i, true, true);
} }
} }
else else