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

witness looks buggy #177

Open
cshardin opened this issue Jul 29, 2020 · 2 comments
Open

witness looks buggy #177

cshardin opened this issue Jul 29, 2020 · 2 comments

Comments

@cshardin
Copy link

The witness function in core.ml can generate strings that don't match the expression, because it ignores the semantics of things like eow. Minimal example:

let t = Re.seq [ Re.eow; Re.str "foo" ] in
let witness = Re.witness t in
assert (not (Re.execp (Re.compile t) witness)) (* assertion succeeds but shouldn't *)

(For me personally this is low priority since I don't need that function. I just happened to notice it looked buggy.)

@Drup
Copy link
Collaborator

Drup commented Aug 18, 2020

It does ignore things like eow. I'm not quite sure how we would handle that ...

@cshardin
Copy link
Author

I think fixing it is nontrivial. If nothing else, you could represent as a nondeterministic finite automaton (NFA) and then do a traversal that marks every accessible state with a witness for how to get into that state, and if that traversal hits an accepting state you have your witness.

The right "fix" might just be to change the doc comment for witness to make weaker claims about the semantics.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants