improve failure reporting of ltlcross
Improve failure reporting of
ltlcross. Currently it only reports
counterexample for errors in cross products. We should improve
diagnostics in the other checks.
Also we could have heuristics to highlight the most pertinent error to look at (e.g., the smallest automaton causing a problem), and to hint at probable erroneous translators (e.g., if the $P_i\otimes N_i$ is non-empty, or if $P_i\otimes N_j$ is non-empty for one $i$ and multiple $j$).