ltlcross: show cross-comparison checks counterexamples

Part of #38.

* bin/ltlcross.cc: Implement it.
* NEWS: Mention it.
* doc/org/ltlcross.org: Adjust example.
* tests/core/ltlcrossce2.test: New test case.

NEWS

@@ -75,6 +75,9 @@ New in spot 2.0.3a (not yet released)
     'b U (a & b)' instead.  The operators that can be listed between
     brackets are the same as those of ltlfilt --unabbreviate option.
 
+  * ltlcross learned to show some counterexamples when diagnosing
+    failures of cross-comparison checks against random state spaces.
+
   * genltl learned three new families: --dac-patterns=1..45,
     --eh-patterns=1..12, and --sb-patterns=1..27.  Unlike other options
     these do not output scalable patterns, but simply a list of formulas

bin/ltlcross.cc

@@ -761,6 +761,7 @@ namespace
               err << l << i;
             }
         err << "} disagree with {";
+        std::ostringstream os;
         first = true;
         for (size_t i = 0; i < m; ++i)
           if (maps[i] && !res[i])
@@ -768,14 +769,22 @@ namespace
               if (first)
                 first = false;
               else
-                err << ',';
+                os << ',';
-              err << l << i;
+              os << l << i;
             }
-        err << "} when evaluating ";
+        err << os.str() << "} when evaluating ";
         if (products > 1)
           err << "state-space #" << p << '/' << products << '\n';
         else
           err << "the state-space\n";
+        err << "       the following word(s) are not accepted by {"
+            << os.str() << "}:\n";
+        for (size_t i = 0; i < m; ++i)
+          if (maps[i] && res[i])
+            {
+              global_error() << "  " << l << i << " accepts: ";
+              example() << *maps[i]->get_aut()->accepting_word() << '\n';
+            }
         end_error();
         return true;
       }

doc/org/ltlcross.org

@@ -656,7 +656,10 @@ positive and negative formulas by the ith translator).
 
     A cross-comparison failure could be displayed as:
 
-    : error: {P0,P2,P3,P4,P5,P6,P7,P8,P9} disagree with {P1} when evaluating the state-space
+    : error: {P0,P2} disagree with {P1} when evaluating the state-space
+    :        the following word(s) are not accepted by {P1}:
+    :  P0 accepts: p0 & !p1 & !p2 & p3; p0 & p1 & !p2 & p3; p0 & p1 & p2 & p3; cycle{p0 & p1 & p2 & p3; p0 & p1 & !p2 & !p3; p0 & p1 & p2 & !p3; p0 & p1 & !p2 & !p3}
+    :  P2 accepts: p0 & !p1 & !p2 & p3; cycle{p0 & p1 & !p2 & !p3; p0 & p1 & p2 & p3; p0 & p1 & !p2 & p3}
 
     If =--products=N= is used with =N= greater than one, the number of
     the state-space is also printed.  This number is of no use by

tests/core/ltlcrossce2.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et
+# Copyright (C) 2015, 2016 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -70,3 +70,39 @@ grep 'error: P1\*N1 is nonempty' errors
 grep 'error: Comp..1.\*Comp..1. is nonempty' errors
 test `grep cycle errors | wc -l` = 3
 test `grep '^error:' errors | wc -l` = 4
+
+
+cat >fake <<\EOF
+#!/bin/sh
+case $1 in
+"G((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))")
+
+# genltl --eh=9 | ltldo modella  -Hl | fmt
+cat <<\END
+HOA: v1 States: 1 Start: 0 AP: 0 acc-name: Buchi Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic --BODY--
+State: 0 --END--
+END
+;;
+"!(G((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))")
+# genltl --neg --eh=9 | ltldo modella  -Hl | fmt
+cat <<\END
+HOA: v1 States: 10 Start: 0 AP: 4 "p0" "p1" "p2" "p3" acc-name: Buchi
+Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc
+--BODY-- State: 0 [!0] 1 [0] 2 [0] 3 State: 1 [t] 4 State: 2 [!0] 1 [0]
+2 [0] 3 State: 3 [!1] 5 [1] 6 State: 4 {0} [t] 4 State: 5 {0} [!1] 5 [1]
+6 State: 6 [!2] 7 [2] 8 State: 7 {0} [!2] 7 [2] 8 State: 8 [!3] 9 State:
+9 {0} [!3] 9 --END--
+END
+;;
+esac
+EOF
+chmod +x fake
+
+genltl --eh=9 | ltlcross 'ltl2tgba' './fake %f >%O' 2>errors && exit 1
+cat errors
+grep 'error: P0\*Comp(P1) is nonempty' errors
+grep 'error: {P0} disagree with {P1}' errors
+grep 'P0 accepts' errors
+test `grep cycle errors | wc -l` = 2
+test `grep '^error:' errors | wc -l` = 3