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
|
4 lat temu | |
|---|---|---|
| examples | 4 lat temu | |
| .gitignore | 4 lat temu | |
| LICENSE | 4 lat temu | |
| README.md | 4 lat temu | |
| dpda.py | 4 lat temu |
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?