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 سال پیش | |
---|---|---|
examples | 4 سال پیش | |
.gitignore | 4 سال پیش | |
LICENSE | 4 سال پیش | |
README.md | 4 سال پیش | |
dpda.py | 4 سال پیش |
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).
Automatically determine good value for number of state/stack symbols.
Is it possible to speed up the procedure?