Add counterexample to the output of NFA language equivalence and inclusion tests

[ondrik]

mata/include/mata/nfa/nfa.hh

Line 683 in 17ffaf6

bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet* alphabet,

It is often necessary to obtain a counterexample to equivalence/inclusion. If the equivalence does not hold, we would like to know what is a word in the symmetric difference of the two automata and in the language of which automaton it is.

[jurajsic]

For inclusion you can call

mata/include/mata/nfa/algorithms.hh

Line 77 in 17ffaf6

bool is_included_antichains(const Nfa& smaller, const Nfa& bigger, const Alphabet* alphabet = nullptr, Run* cex = nullptr);

or

mata/include/mata/nfa/algorithms.hh

Line 66 in 17ffaf6

bool is_included_naive(const Nfa& smaller, const Nfa& bigger, const Alphabet* alphabet = nullptr, Run* cex = nullptr);

directly to get counterexample.
We should add it to dispatcher functions too.

However, it seems that at least for is_included_antichains, the counterexample is incorrect right now (#440).

[jurajsic]

Also, related #113