search

VeriFIT / mata

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

Incorrect counterexample in `is_included_antichains` #440

Closed jurajsic closed 3 weeks ago

jurajsic commented 1 month ago

When I call https://github.com/VeriFIT/mata/blob/17ffaf6e2a90a506c21abe5075893b505947322b/include/mata/nfa/algorithms.hh#L77 with the following two automata:

@NFA-explicit
%Alphabet-auto
%Initial q0
%Final q10
q0 65 q1
q0 66 q1
q0 67 q1
q0 196608 q1
q1 65 q2
q1 66 q2
q1 67 q2
q1 196608 q2
q2 65 q2
q2 65 q3
q2 66 q2
q2 66 q4
q2 67 q2
q2 196608 q2
q3 67 q11
q4 66 q5
q5 66 q6
q6 65 q6
q6 65 q7
q6 66 q6
q6 67 q6
q6 196608 q6
q7 67 q8
q8 67 q9
q9 67 q10
q10 65 q10
q10 66 q10
q10 67 q10
q10 196608 q10
q11 67 q12
q12 67 q13
q13 65 q13
q13 66 q13
q13 66 q14
q13 67 q13
q13 196608 q13
q14 66 q15
q15 66 q16
q16 65 q10
q16 66 q10
q16 67 q10
q16 196608 q10

and

@NFA-explicit
%Alphabet-auto
%Initial q0 q7
%Final q6
q0 65 q1
q0 66 q1
q0 67 q1
q0 196608 q1
q1 65 q2
q1 66 q2
q1 67 q2
q1 196608 q2
q2 65 q2
q2 66 q2
q2 66 q3
q2 67 q2
q2 196608 q2
q3 66 q4
q4 66 q5
q5 66 q6
q6 65 q6
q6 66 q6
q6 67 q6
q6 196608 q6
q7 65 q8
q7 66 q8
q7 67 q8
q7 196608 q8
q8 65 q8
q8 66 q9
q8 67 q8
q8 196608 q8
q9 65 q9
q9 65 q10
q9 66 q9
q9 67 q9
q9 196608 q9
q10 67 q5

I get incorrect counterexample, a word 65, 66, 66, 66, 66, 65, 67, 67. It seems that it missed the last symbol 67.

jurajsic commented 1 month ago

@kilohsakul says that when he was updating the code for antichain he did not touch counterexample generation, so it probably computes bullshit.

jurajsic commented 1 month ago

It seems the problem is in this test https://github.com/VeriFIT/mata/blob/15282c5eeaa7d786da27d0d73171679237f5c1f0/src/nfa/inclusion.cc#L163

lengths_incompatible is some heuristic to find that the inclusion does not hold sooner and counterexample will then be a prefix of some word from the first automaton.