Skip to content

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).