diff --git a/NEWS b/NEWS index 91b3a8918..af80b72c3 100644 --- a/NEWS +++ b/NEWS @@ -80,6 +80,12 @@ New in spot 2.0.3a (not yet released) * A new example page shows how to test the equivalence of 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) Bug fixes: diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 04f908dd3..e44fbef89 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1184,8 +1184,8 @@ namespace if (comp_pos[i] && comp_neg[j] && (i == j || (!comp_neg[i] && !comp_pos[j]))) problems += - check_empty_prod(comp_pos[i], comp_neg[j], - i, j, true, true); + check_empty_prod(comp_neg[j], comp_pos[i], + j, i, true, true); } } else