Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Rick Smetsers
z3gi
Commits
718eefd6
Commit
718eefd6
authored
Oct 04, 2017
by
Paul Fiterau Brostean
Browse files
Yannakakis tester
parent
6eb9fc23
Changes
10
Hide whitespace changes
Inline
Side-by-side
example_runs.py
View file @
718eefd6
import
itertools
import
os.path
from
encode.fa
import
MealyEncoder
,
DFAEncoder
from
encode.ra
import
RAEncoder
...
...
@@ -17,6 +17,7 @@ from test.yanna import YannakakisTestGenerator
from
tests.iora_testscenario
import
*
from
encode.iora
import
IORAEncoder
# some example runs
def
scalable_learn_iora
():
...
...
@@ -69,7 +70,6 @@ def scalable_learn_mbt_ra():
def
sim_learn_mbt_mealy
():
learner
=
FALearner
(
MealyEncoder
())
learner
.
set_timeout
(
10000
)
import
os.path
maestro_aut
=
build_automaton_from_dot
(
"MealyMachine"
,
os
.
path
.
join
(
"resources"
,
"models"
,
"bankcards"
,
"MAESTRO.dot"
))
maestro_sut
=
MealyMachineSimulation
(
maestro_aut
)
mbt
=
MealyRWalkFromState
(
maestro_sut
,
3
,
0.2
)
...
...
@@ -77,18 +77,30 @@ def sim_learn_mbt_mealy():
print
(
model
)
print
(
statistics
)
def
sim_learn_mbt_yan_mealy
():
def
sim_learn_mbt_yan_mealy
(
dot_path
):
learner
=
FALearner
(
MealyEncoder
())
learner
.
set_timeout
(
10000
)
import
os.path
maestro_aut
=
build_automaton_from_dot
(
"MealyMachine"
,
os
.
path
.
join
(
"resources"
,
"models"
,
"bankcards"
,
"MAESTRO.dot"
))
maestro_sut
=
MealyMachineSimulation
(
maestro_aut
)
dot_aut
=
build_automaton_from_dot
(
"MealyMachine"
,
dot_path
)
dot_sut
=
MealyMachineSimulation
(
dot_aut
)
yan_cmd
=
os
.
path
.
join
(
"resources"
,
"binaries"
,
"yannakakis.exe"
)
mbt
=
YannakakisTestGenerator
(
maestro
_sut
,
yan_cmd
)
mbt
=
YannakakisTestGenerator
(
dot
_sut
,
yan_cmd
)
(
model
,
statistics
)
=
learn_mbt
(
learner
,
mbt
,
10000
)
print
(
model
)
print
(
statistics
)
sim_learn_mbt_yan_mealy
()
models_loc
=
os
.
path
.
join
(
"resources"
,
"models"
)
def
maestro_learn_mbt_yan_mealy
():
sim_learn_mbt_yan_mealy
(
os
.
path
.
join
(
models_loc
,
"bankcards"
,
"MAESTRO.dot"
))
def
visa_learn_mbt_yan_mealy
():
sim_learn_mbt_yan_mealy
(
os
.
path
.
join
(
models_loc
,
"bankcards"
,
"VISA.dot"
))
def
biometric_learn_mbt_yan_mealy
():
sim_learn_mbt_yan_mealy
(
os
.
path
.
join
(
"models_loc"
,
"biometric.dot"
))
visa_learn_mbt_yan_mealy
()
#scalable_learn_mbt_mealy()
#scalable_learn_mbt_iora()
resources/binaries/yannakakis.exe
0 → 100644
View file @
718eefd6
File added
resources/models/biometric.dot
View file @
718eefd6
digraph
g
{
node
[
shape
=
oval
]
;
11
;
10
;
26
;
18
;
31
;
0
[
peripheries
=
2
,
color
=
"red"
]
;
0
->
10
[
label
=
"ITA/ONOK"
]
;
0
->
10
[
label
=
"IFAILEAC/ONOK"
]
;
0
->
10
[
label
=
"ICA/ONOK"
]
;
0
->
10
[
label
=
"IAA/ONOK"
]
;
0
->
10
[
label
=
"IREADFILE_0/ONOK"
]
;
0
->
10
[
label
=
"IFAILBAC/ONOK"
]
;
0
->
10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
0
->
11
[
label
=
"IGETCHALLENGE/OOK"
]
;
0
->
10
[
label
=
"IRESET/OOK"
]
;
10
->
10
[
label
=
"ITA/ONOK"
]
;
10
->
10
[
label
=
"IFAILEAC/ONOK"
]
;
10
->
10
[
label
=
"ICA/ONOK"
]
;
10
->
10
[
label
=
"IAA/ONOK"
]
;
10
->
10
[
label
=
"IREADFILE_0/ONOK"
]
;
10
->
10
[
label
=
"IFAILBAC/ONOK"
]
;
10
->
10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
10
->
11
[
label
=
"IGETCHALLENGE/OOK"
]
;
10
->
10
[
label
=
"IRESET/OOK"
]
;
11
->
10
[
label
=
"IFAILBAC/ONOK"
]
;
11
->
10
[
label
=
"IRESET/OOK"
]
;
11
->
11
[
label
=
"IGETCHALLENGE/OOK"
]
;
11
->
11
[
label
=
"IFAILEAC/ONOK"
]
;
11
->
11
[
label
=
"ITA/ONOK"
]
;
11
->
11
[
label
=
"ICA/ONOK"
]
;
11
->
11
[
label
=
"IREADFILE_0/ONOK"
]
;
11
->
11
[
label
=
"IAA/ONOK"
]
;
11
->
18
[
label
=
"ICOMPLETEBAC/OOK"
]
;
18
->
10
[
label
=
"IFAILBAC/ONOK"
]
;
18
->
10
[
label
=
"IRESET/OOK"
]
;
18
->
18
[
label
=
"IREADFILE_0/ONOK"
]
;
18
->
26
[
label
=
"IFAILEAC/ONOK"
]
;
18
->
26
[
label
=
"ICA/OOK"
]
;
18
->
18
[
label
=
"ITA/ONOK"
]
;
18
->
18
[
label
=
"IAA/OOK"
]
;
18
->
10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
18
->
10
[
label
=
"IGETCHALLENGE/ONOK"
]
;
26
->
10
[
label
=
"IFAILBAC/ONOK"
]
;
26
->
10
[
label
=
"IRESET/OOK"
]
;
26
->
26
[
label
=
"IFAILEAC/ONOK"
]
;
26
->
26
[
label
=
"IREADFILE_0/ONOK"
]
;
26
->
31
[
label
=
"ITA/OOK"
]
;
26
->
26
[
label
=
"ICA/OOK"
]
;
26
->
26
[
label
=
"IAA/OOK"
]
;
26
->
10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
26
->
10
[
label
=
"IGETCHALLENGE/ONOK"
]
;
31
->
31
[
label
=
"IREADFILE_0/ONOK"
]
;
31
->
31
[
label
=
"ITA/OOK"
]
;
31
->
31
[
label
=
"ICA/OOK"
]
;
31
->
31
[
label
=
"IAA/OOK"
]
;
31
->
26
[
label
=
"IFAILEAC/ONOK"
]
;
31
->
10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
31
->
10
[
label
=
"IGETCHALLENGE/ONOK"
]
;
31
->
10
[
label
=
"IFAILBAC/ONOK"
]
;
31
->
10
[
label
=
"IRESET/OOK"
]
;
s0
[
color
=
"red"
]
;
s11
;
s10
;
s26
;
s18
;
s31
;
s0
->
s10
[
label
=
"ITA/ONOK"
]
;
s0
->
s10
[
label
=
"IFAILEAC/ONOK"
]
;
s0
->
s10
[
label
=
"ICA/ONOK"
]
;
s0
->
s10
[
label
=
"IAA/ONOK"
]
;
s0
->
s10
[
label
=
"IREADFILE_0/ONOK"
]
;
s0
->
s10
[
label
=
"IFAILBAC/ONOK"
]
;
s0
->
s10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
s0
->
s11
[
label
=
"IGETCHALLENGE/OOK"
]
;
s0
->
s10
[
label
=
"IRESET/OOK"
]
;
s10
->
s10
[
label
=
"ITA/ONOK"
]
;
s10
->
s10
[
label
=
"IFAILEAC/ONOK"
]
;
s10
->
s10
[
label
=
"ICA/ONOK"
]
;
s10
->
s10
[
label
=
"IAA/ONOK"
]
;
s10
->
s10
[
label
=
"IREADFILE_0/ONOK"
]
;
s10
->
s10
[
label
=
"IFAILBAC/ONOK"
]
;
s10
->
s10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
s10
->
s11
[
label
=
"IGETCHALLENGE/OOK"
]
;
s10
->
s10
[
label
=
"IRESET/OOK"
]
;
s11
->
s10
[
label
=
"IFAILBAC/ONOK"
]
;
s11
->
s10
[
label
=
"IRESET/OOK"
]
;
s11
->
s11
[
label
=
"IGETCHALLENGE/OOK"
]
;
s11
->
s11
[
label
=
"IFAILEAC/ONOK"
]
;
s11
->
s11
[
label
=
"ITA/ONOK"
]
;
s11
->
s11
[
label
=
"ICA/ONOK"
]
;
s11
->
s11
[
label
=
"IREADFILE_0/ONOK"
]
;
s11
->
s11
[
label
=
"IAA/ONOK"
]
;
s11
->
s18
[
label
=
"ICOMPLETEBAC/OOK"
]
;
s18
->
s10
[
label
=
"IFAILBAC/ONOK"
]
;
s18
->
s10
[
label
=
"IRESET/OOK"
]
;
s18
->
s18
[
label
=
"IREADFILE_0/ONOK"
]
;
s18
->
s26
[
label
=
"IFAILEAC/ONOK"
]
;
s18
->
s26
[
label
=
"ICA/OOK"
]
;
s18
->
s18
[
label
=
"ITA/ONOK"
]
;
s18
->
s18
[
label
=
"IAA/OOK"
]
;
s18
->
s10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
s18
->
s10
[
label
=
"IGETCHALLENGE/ONOK"
]
;
s26
->
s10
[
label
=
"IFAILBAC/ONOK"
]
;
s26
->
s10
[
label
=
"IRESET/OOK"
]
;
s26
->
s26
[
label
=
"IFAILEAC/ONOK"
]
;
s26
->
s26
[
label
=
"IREADFILE_0/ONOK"
]
;
s26
->
s31
[
label
=
"ITA/OOK"
]
;
s26
->
s26
[
label
=
"ICA/OOK"
]
;
s26
->
s26
[
label
=
"IAA/OOK"
]
;
s26
->
s10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
s26
->
s10
[
label
=
"IGETCHALLENGE/ONOK"
]
;
s31
->
s31
[
label
=
"IREADFILE_0/ONOK"
]
;
s31
->
s31
[
label
=
"ITA/OOK"
]
;
s31
->
s31
[
label
=
"ICA/OOK"
]
;
s31
->
s31
[
label
=
"IAA/OOK"
]
;
s31
->
s26
[
label
=
"IFAILEAC/ONOK"
]
;
s31
->
s10
[
label
=
"ICOMPLETEBAC/ONOK"
]
;
s31
->
s10
[
label
=
"IGETCHALLENGE/ONOK"
]
;
s31
->
s10
[
label
=
"IFAILBAC/ONOK"
]
;
s31
->
s10
[
label
=
"IRESET/OOK"
]
;
}
z3gi/benchmark.py
View file @
718eefd6
...
...
@@ -11,7 +11,8 @@ from learn.fa import FALearner
from
learn.ra
import
RALearner
from
model
import
Automaton
from
model.ra
import
RegisterMachine
from
sut
import
SUTType
,
ScalableSUTClass
from
sut
import
SUTType
from
sut.scalable
import
ScalableSUTClass
from
sut.fifoset
import
FIFOSetClass
from
sut.login
import
LoginClass
from
sut.stack
import
StackClass
...
...
z3gi/learn/algorithm.py
View file @
718eefd6
...
...
@@ -32,13 +32,15 @@ class Statistics():
def
add_learning_time
(
self
,
time
):
self
.
learning_times
.
append
(
time
)
def
__str__
(
self
):
return
"Total number tests used in learning: {0}
\n
"
\
"Total number inputs used in learning: {1}
\n
"
\
"Test suite size: {2}
\n
"
\
"Average learner test size: {3}
\n
"
\
"Learning time for each model: {4}
\n
"
\
"Total learning time: {5} "
.
format
(
self
.
num_learner_tests
,
def
__str__
(
self
):
return
"Total number of tests used in learning/testing: {0}
\n
"
\
"Total number of inputs used in learning/testing: {1}
\n
"
\
"Total number of hypotheses used in learning/testing: {2}
\n
"
\
"Test suite size: {3}
\n
"
\
"Average learner test size: {4}
\n
"
\
"Learning time for each model: {5}
\n
"
\
"Total learning time: {6} "
.
format
(
self
.
num_learner_tests
,
self
.
num_learner_inputs
,
len
(
self
.
learning_times
),
self
.
suite_size
,
self
.
num_learner_inputs
/
self
.
num_learner_tests
,
self
.
learning_times
,
...
...
@@ -121,12 +123,12 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
break
if
not
done
:
continue
test_generator
.
initialize
(
model
)
# we then generate and check new tests, until either we find a CE,
# or the suite is exhausted or we have run the intended number of tests
for
i
in
range
(
0
,
max_tests
):
next_test
=
test_generator
.
gen_test
(
model
)
if
next_test
is
None
:
raise
Exception
(
"Should never be none"
)
break
generated_tests
.
append
(
next_test
)
ce
=
next_test
.
check
(
model
)
...
...
@@ -136,6 +138,7 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
statistics
.
add_learner_test
(
next_test
)
done
=
False
break
test_generator
.
terminate
()
#print([str(test.trace() for test in learner_tests)])
statistics
.
set_suite_size
(
len
(
generated_tests
))
...
...
z3gi/learn/fa.py
View file @
718eefd6
...
...
@@ -20,7 +20,6 @@ class FALearner(Learner):
def
model
(
self
,
min_states
=
1
,
max_states
=
20
,
old_definition
:
define
.
fa
.
FSM
=
None
)
->
Tuple
[
Automaton
,
define
.
fa
.
FSM
]:
if
old_definition
is
not
None
:
min_states
=
len
(
old_definition
.
states
)
print
(
"initial def "
,
min_states
)
(
succ
,
fa
,
m
)
=
self
.
_learn_model
(
min_states
=
min_states
,
max_states
=
max_states
)
self
.
solver
.
reset
()
...
...
z3gi/parse/importer.py
View file @
718eefd6
...
...
@@ -95,7 +95,6 @@ def build_automaton_from_dot (aut_type:str, file_name:str) -> Automaton:
print
(
"Available DotImporters: "
,
[
a
.
replace
(
"DotImporter"
,
""
)
for
a
in
crt
.
__dict__
.
keys
()
if
a
.
endswith
(
"DotImporter"
)
and
isinstance
(
crt
.
__dict__
[
a
],
type
)
and
not
inspect
.
isabstract
(
crt
.
__dict__
[
a
])])
exit
(
1
)
"""From .dot representation produces an automata"""
dot_stream
=
file_stream
(
file_name
)
...
...
@@ -145,7 +144,6 @@ class DotImporter(metaclass=ABCMeta):
matches
=
[]
for
line
in
stream
:
line
=
line
.
strip
()
print
(
line
)
# if the line only contained spaces continue
if
len
(
line
)
==
0
:
continue
...
...
z3gi/test/__init__.py
View file @
718eefd6
...
...
@@ -48,6 +48,7 @@ class EqualTestsMixin(metaclass=ABCMeta):
class
TestGenerator
(
metaclass
=
ABCMeta
):
#TODO gen_test should take the sut as param (relieving the testgens of having to store it in a field)
@
abstractmethod
def
gen_test
(
self
,
model
:
Automaton
)
->
Test
:
"""generates a Test. Returns None if the test suite is exhausted"""
...
...
@@ -61,7 +62,7 @@ class TestGenerator(metaclass=ABCMeta):
test
=
self
.
gen_test
(
model
)
self
.
terminate
()
def
gen_blind_
test
(
self
,
sut
:
SUT
):
def
gen_blind_
inp_seq
(
self
,
sut
:
SUT
):
"""generates a sequence covering all input elements in the sut interface"""
seq
=
[]
for
abs_inp
in
self
.
sut
.
input_interface
():
...
...
z3gi/test/rwalk.py
View file @
718eefd6
...
...
@@ -34,7 +34,7 @@ class RWalkFromState(TestGenerator, metaclass=ABCMeta):
if
model
is
None
:
# if the model is None, generate a test which includes all inputs (so at least we know the next generated
# model will be input enabled)
seq
=
self
.
gen_blind_
test
(
self
.
sut
)
seq
=
self
.
gen_blind_
inp_seq
(
self
.
sut
)
else
:
# select a random state
if
self
.
rand_start_state
:
...
...
z3gi/test/yanna.py
0 → 100644
View file @
718eefd6
from
abc
import
ABCMeta
,
abstractmethod
from
model
import
Automaton
from
sut.simulation
import
MealyMachineSimulation
from
test
import
TestGenerator
,
MealyTest
import
parse.exporter
import
subprocess
import
os.path
class
YannakakisTestGenerator
(
TestGenerator
):
def
__init__
(
self
,
sut
,
yan_path
=
os
.
path
.
join
(
os
.
path
.
dirname
(
__file__
),
".."
,
".."
,
"resources"
,
"binaries"
,
"yannakakis.exe"
),
mode
=
"random"
,
max_k
=
3
,
rand_length
=
3
):
self
.
yan_path
=
yan_path
self
.
mode
=
mode
self
.
max_k
=
max_k
self
.
sut
=
sut
self
.
r_length
=
rand_length
self
.
yan_proc
=
None
def
initialize
(
self
,
model
:
Automaton
):
hyp_file
=
"hyp.dot"
parse
.
exporter
.
to_dot
(
model
,
hyp_file
)
self
.
yan_proc
=
subprocess
.
Popen
([
self
.
yan_path
,
hyp_file
,
self
.
mode
,
str
(
self
.
max_k
),
str
(
self
.
r_length
)],
stdout
=
subprocess
.
PIPE
,
bufsize
=
10
,
universal_newlines
=
True
)
def
gen_test
(
self
,
model
:
Automaton
):
if
model
is
None
:
seq
=
self
.
gen_blind_inp_seq
(
self
.
sut
)
obs
=
self
.
sut
.
run
(
seq
)
else
:
test_string
=
self
.
yan_proc
.
stdout
.
readline
()
if
test_string
is
None
:
return
None
inputs
=
test_string
.
split
()
obs
=
self
.
sut
.
run
(
inputs
)
test
=
MealyTest
(
obs
.
trace
())
return
test
def
terminate
(
self
):
os
.
remove
(
"hyp.dot"
)
self
.
yan_proc
.
terminate
()
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment