Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Incorrect counterexample in is_included_antichains #440

Open
jurajsic opened this issue Oct 8, 2024 · 1 comment
Open

Incorrect counterexample in is_included_antichains #440

jurajsic opened this issue Oct 8, 2024 · 1 comment
Labels
For:library The issue is related to library (c++ implementation) Module:nfa The issue is related to Nondeterministic Finite Automata Type:bug A bug or an issue in implementation or performance

Comments

@jurajsic
Copy link
Member

jurajsic commented Oct 8, 2024

When I call

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

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 jurajsic added For:library The issue is related to library (c++ implementation) Module:nfa The issue is related to Nondeterministic Finite Automata Type:bug A bug or an issue in implementation or performance labels Oct 8, 2024
@jurajsic
Copy link
Member Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
For:library The issue is related to library (c++ implementation) Module:nfa The issue is related to Nondeterministic Finite Automata Type:bug A bug or an issue in implementation or performance
Projects
None yet
Development

No branches or pull requests

1 participant