Skip to content

Commit

Permalink
Merge pull request #334 from VeriFIT/binding-parser #patch
Browse files Browse the repository at this point in the history 
Extend binding with parsing
  • Loading branch information
@tfiedor
tfiedor authored Sep 15, 2023
2 parents 6bfac4a + 91fee94 commit fde78f4
Show file tree
Hide file tree
Showing 8 changed files with 1,250 additions and 1 deletion.
37 changes: 37 additions & 0 deletions bindings/python/libmata/parser.pxd
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,45 @@
from libcpp cimport bool
from libcpp.string cimport string
from libcpp.vector cimport vector

from libmata.nfa.nfa cimport CNfa
from libmata.alphabets cimport CAlphabet

cdef extern from "<iostream>" namespace "std":
cdef cppclass istream:
istream& write(const char*, int) except +

cdef extern from "<fstream>" namespace "std":
cdef cppclass ifstream(istream):
ifstream() except+
ifstream(const char*) except +

cdef extern from "mata/parser/re2parser.hh" namespace "mata::parser":
cdef void create_nfa(CNfa*, string) except +
cdef void create_nfa(CNfa*, string, bool) except +

cdef extern from "mata/parser/inter-aut.hh" namespace "mata":
cdef struct CInterAut "mata::IntermediateAut":
CInterAut() except +
bool is_bitvector()


cdef extern from "mata/nfa/builder.hh" namespace "mata::nfa::builder":
cdef void construct(CNfa*, CInterAut&, CAlphabet*);

cdef extern from "mata/parser/parser.hh" namespace "mata::parser":
cdef struct CParsedSection "mata::parser::ParsedSection":
CParsedSection() except +

ctypedef vector[CParsedSection] Parsed

cdef Parsed parse_mf(istream, bool) except +

cdef extern from "mata/parser/inter-aut.hh" namespace "mata::IntermediateAut":
vector[CInterAut] parse_from_mf(Parsed&)

cdef extern from "mata/parser/mintermization.hh" namespace "mata":
cdef cppclass CMintermization "mata::Mintermization":
CMintermization()
CInterAut c_mintermize "mata::Mintermization::mintermize" (CInterAut&);
vector[CInterAut] c_mintermize_vec "mata::Mintermization::mintermize" (vector[CInterAut]&);
64 changes: 63 additions & 1 deletion bindings/python/libmata/parser.pyx
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
from libcpp.memory cimport shared_ptr, make_shared
from libcpp.string cimport string

from libmata.nfa.nfa cimport CNfa

cimport libmata.parser as parser
cimport libmata.nfa.nfa as mata_nfa
cimport libmata.alphabets as alph

# External Constructors
def from_regex(regex, encoding='utf-8'):
Expand All @@ -17,4 +19,64 @@ def from_regex(regex, encoding='utf-8'):
"""
result = mata_nfa.Nfa()
parser.create_nfa((<mata_nfa.Nfa>result).thisptr.get(), regex.encode(encoding))
return result
return result

def from_mata(src, alph.Alphabet alphabet):
"""Loads automata from either single file or list or other stream of files.
All automata passed in sources are mintermized together. If you wish to load
multiple automata and mintermize them, then you have to pass them as a list.
:param src: list of paths to automata or single path
:param alphabet: target alphabet
:return: single automaton or list of automata
"""
cdef CAlphabet * c_alphabet = NULL
cdef parser.Parsed parsed
cdef parser.ifstream fs
cdef vector[parser.CInterAut] inter_aut
cdef vector[parser.CInterAut] res_inter_aut
cdef vector[parser.CInterAut] mintermized_inter_aut
cdef parser.CMintermization mintermization

if alphabet:
c_alphabet = alphabet.as_base()

# either load single automata
if isinstance(src, str):
fs = parser.ifstream(src.encode('utf-8'))
res_inter_aut = parser.parse_from_mf(parser.parse_mf(fs, True))
result = mata_nfa.Nfa()
if res_inter_aut[0].is_bitvector():
parser.construct(
(<mata_nfa.Nfa>result).thisptr.get(),
mintermization.c_mintermize(res_inter_aut[0]),
c_alphabet
)
else:
parser.construct(
(<mata_nfa.Nfa>result).thisptr.get(),
res_inter_aut[0],
c_alphabet
)
return result
# load multiple automata
else:
automata = []
for file in src:
fs = parser.ifstream(file.encode('utf-8'))
res_inter_aut = parser.parse_from_mf(parser.parse_mf(fs, True))
inter_aut.emplace_back(res_inter_aut[0])
if inter_aut[0].is_bitvector():
mintermized_inter_aut = mintermization.c_mintermize_vec(inter_aut)
else:
mintermized_inter_aut = inter_aut
for ia in mintermized_inter_aut:
result = mata_nfa.Nfa()
parser.construct(
(<mata_nfa.Nfa>result).thisptr.get(),
ia,
c_alphabet
)
automata.append(result)
return automata
39 changes: 39 additions & 0 deletions bindings/python/tests/automata/aut0.mata
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
@NFA-bits
%Initial q0
%Final !q0 & !q1 & !q2 & !q3 & !q4 & !q5 & !q6 & !q7 & !q8 & !q9 & !q10 & !q11 & !q13 & !q14 & !q16
q10 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q12
q17 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q18
q6 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & ((!a1 & a0) | (a1 & !a0))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & a4 & a3 & a2 & a1 & a0) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q7
q6 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q8
q21 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q22
q8 (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & a1 & !a0) q9
q15 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q17
q4 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & ((!a1 & a0) | (a1 & !a0))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & a4 & a3 & a2 & a1 & a0) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q3
q4 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q4
q4 (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & !a4 & !a3 & !a2 & !a1 & !a0) q5
q3 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & ((!a1 & a0) | (a1 & !a0))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & a4 & a3 & a2 & a1 & a0) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q3
q3 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q4
q19 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q20
q13 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q14
q13 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & ((!a1 & a0) | (a1 & !a0))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & a4 & a3 & a2 & a1 & a0) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q13
q16 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q10
q16 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q11
q1 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q2
q1 (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) q1
q11 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & ((!a1 & a0) | (a1 & !a0))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & a4 & a3 & a2 & a1 & a0) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q13
q11 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q14
q14 (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & a1 & !a0) q16
q7 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & ((!a1 & a0) | (a1 & !a0))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & a4 & a3 & a2 & a1 & a0) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q7
q7 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q8
q20 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q21
q2 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & !a4 & a3 & a2 & ((!a1 & a0) | (a1 & !a0))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & a4 & a3 & a2 & a1 & a0) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q3
q2 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q4
q2 (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & !a4 & !a3 & !a2 & !a1 & !a0) q5
q9 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q10
q9 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q11
q18 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q19
q12 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q15
q22 false true
q5 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q6
q0 ((!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & !a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0)))))) | (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & a6 & a5 & ((!a4 & (a3 | a2 | a1 | a0)) | (a4 & (!a3 | (!a2 & (!a1 | !a0))))))) q2
q0 (!a15 & !a14 & !a13 & !a12 & !a11 & !a10 & !a9 & !a8 & !a7 & !a6 & a5 & a4 & (!a3 | (a3 & !a2 & !a1))) q1
16 changes: 16 additions & 0 deletions bindings/python/tests/automata/aut1.mata
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
@NFA-bits
%Initial q0
%Final !q0 & !q2 & !q3
q0 (!a1 & a2 & a3 & a4 & !a5) q3
q0 (a1 & !a2 & a3 & a4 & !a5) q3
q1 (a1 & a2 & a3 & a4 & a5) q1
q1 (!a1 & a2 & a3 & a4 & a5) q1
q1 (a1 & !a2 & a3 & a4 & a5) q1
q1 (a1 & a2 & !a3 & a4 & a5) q1
q1 (a1 & a2 & a3 & !a4 & a5) q1
q1 (!a1 & a2 & a3 & a4 & !a5) q1
q1 (a1 & !a2 & a3 & a4 & !a5) q1
q2 (!a1 & a2 & a3 & a4 & !a5) q1
q2 (a1 & !a2 & a3 & a4 & !a5) q1
q3 (!a1 & a2 & a3 & a4 & !a5) q2
q3 (a1 & !a2 & a3 & a4 & !a5) q2
Loading

0 comments on commit fde78f4

Please sign in to comment.