Automaton inference from examples using z3py
Your Name
e2a2ff55f5
1) make it more stable 2) show 14 words and ask user about first word not in trie
|
%!s(int64=4) %!d(string=hai) anos | |
|---|---|---|
| examples | %!s(int64=4) %!d(string=hai) anos | |
| .gitignore | %!s(int64=4) %!d(string=hai) anos | |
| LICENSE | %!s(int64=4) %!d(string=hai) anos | |
| README.md | %!s(int64=4) %!d(string=hai) anos | |
| dpda.py | %!s(int64=4) %!d(string=hai) anos |
README.md
dPDA
Automaton inference from examples using z3py:
-m simple: Positive examples only-m advanced: Both positive and negative examples accepted. Much more useful.
In -m advanced, examples can be provided and the solver can be queried in an interactive session:
p blah: "blah is a word of L"n quux: "quux is not a word of L"?: automaton?q: quit
(note that examples can be overridden, and p a ... n a does not lead to unsat but rather to an automaton that doesn't accept a).
Future work
Automatically determine good value for number of state/stack symbols.
Is it possible to speed up the procedure?