search

VeriFIT / mata

A fast and simple automata library
MIT License
22 stars 13 forks source link

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

Open ondrik opened 3 weeks ago

ondrik commented 3 weeks ago

https://github.com/VeriFIT/mata/blob/17ffaf6e2a90a506c21abe5075893b505947322b/include/mata/nfa/nfa.hh#L683

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 commented 1 week ago

For inclusion you can call https://github.com/VeriFIT/mata/blob/17ffaf6e2a90a506c21abe5075893b505947322b/include/mata/nfa/algorithms.hh#L77 or https://github.com/VeriFIT/mata/blob/17ffaf6e2a90a506c21abe5075893b505947322b/include/mata/nfa/algorithms.hh#L66 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 commented 1 week ago

Also, related #113