Halaman utama Jelajahi Bantuan
Masuk
fnordomat
/
dPDA
Liatin 1
Bintangi 0
Fork 0
Berkas Masalah 0 Tarik Permintaan 0 Wiki

Automaton inference from examples using z3py

Cabang: master
Ranting Tag
dPDA
ZIP TAR.GZ
Your Name e2a2ff55f5 1) make it more stable 2) show 14 words and ask user about first word not in trie 4 tahun lalu
examples b0a0030dee Initial commit 4 tahun lalu
.gitignore a882b53c7e Initial commit 4 tahun lalu
LICENSE a882b53c7e Initial commit 4 tahun lalu
README.md e2a2ff55f5 1) make it more stable 2) show 14 words and ask user about first word not in trie 4 tahun lalu
dpda.py e2a2ff55f5 1) make it more stable 2) show 14 words and ask user about first word not in trie 4 tahun lalu

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?

Related work

z3gi