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
28d7109a
Commit
28d7109a
authored
Oct 24, 2017
by
Paul Fiterau Brostean
Browse files
Will need to optimize test algorithm
parent
795797a0
Changes
18
Hide whitespace changes
Inline
Side-by-side
z3gi/benchmark.py
View file @
28d7109a
import
functools
from
abc
import
ABCMeta
from
typing
import
Tuple
,
List
,
Dict
import
collections
from
encode.fa
import
DFAEncoder
,
MealyEncoder
from
encode.iora
import
IORAEncoder
from
encode.ra
import
RAEncoder
from
encode.iora
import
IORAEncoder
,
IORAQREncoder
from
encode.ra
import
RAEncoder
,
RAQREncoder
from
learn
import
Learner
from
learn.fa
import
FALearner
from
learn.ra
import
RALearner
...
...
@@ -29,11 +30,11 @@ class SutDesc(collections.namedtuple("SutDesc", 'sut_class type size')):
return
str
(
self
.
type
).
replace
(
"SUTType."
,
""
)
+
"_"
+
str
(
self
.
sut_class
.
__class__
.
__name__
).
replace
(
"Class"
,
""
)
+
"("
+
str
(
self
.
size
)
+
")"
TestDesc
=
collections
.
namedtuple
(
"TestDesc"
,
'max_tests rand_length prop_reset'
)
class
ExperimentStats
(
collections
.
namedtuple
(
"CollectedStats"
,
"states registers tests "
class
ExperimentStats
(
collections
.
namedtuple
(
"CollectedStats"
,
"states
minimal
registers tests "
"inputs max_ltime learn_time"
)):
pass
class
CollatedStats
(
collections
.
namedtuple
(
"CollatedStats"
,
"exp_succ states registers consistent avg_tests std_tests avg_inputs std_inputs max_ltime avg_ltime std_ltime"
)):
class
CollatedStats
(
collections
.
namedtuple
(
"CollatedStats"
,
"exp_succ states registers
minimal
consistent avg_tests std_tests avg_inputs std_inputs max_ltime avg_ltime std_ltime"
)):
pass
def
get_learner_setup
(
sut
,
sut_type
:
SUTType
,
size
,
test_desc
:
TestDesc
):
...
...
@@ -43,9 +44,13 @@ def get_learner_setup(sut, sut_type:SUTType, size, test_desc:TestDesc):
elif
sut_type
is
SUTType
.
Mealy
:
return
(
FALearner
(
MealyEncoder
()),
MealyRWalkFromState
(
*
args
))
elif
sut_type
is
SUTType
.
RA
:
return
(
RALearner
(
RAEncoder
()),
RARWalkFromState
(
*
args
))
ra_learner
=
RALearner
(
RAEncoder
())
ra_learner
.
set_num_reg
(
size
)
return
(
ra_learner
,
RARWalkFromState
(
*
args
))
elif
sut_type
is
SUTType
.
IORA
:
return
(
RALearner
(
IORAEncoder
()),
IORARWalkFromState
(
*
args
))
ra_learner
=
RALearner
(
IORAEncoder
())
ra_learner
.
set_num_reg
(
size
)
return
(
ra_learner
,
IORARWalkFromState
(
*
args
))
raise
Exception
(
"Invalid setup"
)
class
Benchmark
:
...
...
@@ -68,10 +73,10 @@ class Benchmark:
self
.
learn_setup
[
sut_type
]
=
(
sut_learner
,
sut_tester
)
return
self
def
_run_benchmark
(
self
,
sut_class
:
ScalableSUTClass
,
sut_type
:
SUTType
,
test_desc
:
TestDesc
,
tout
:
int
,
max_size
:
int
,
use_coloring
:
bool
)
\
->
List
[
Tuple
[
SutDesc
,
ExperimentStats
]]:
def
_run_benchmark
(
self
,
sut_class
:
ScalableSUTClass
,
sut_type
:
SUTType
,
test_desc
:
TestDesc
,
tout
:
int
,
\
min_size
:
int
,
max_size
:
int
,
use_coloring
:
bool
)
->
List
[
Tuple
[
SutDesc
,
ExperimentStats
]]:
results
=
[]
size
=
1
size
=
min_size
while
True
:
if
max_size
is
not
None
and
size
>
max_size
:
break
...
...
@@ -101,25 +106,27 @@ class Benchmark:
if
model
is
None
:
break
else
:
imp_stats
=
self
.
_collect_stats
(
model
,
statistics
)
sut_desc
=
SutDesc
(
sut_class
,
sut_type
,
size
)
imp_stats
=
self
.
_collect_stats
(
sut_desc
,
model
,
statistics
)
results
.
append
(
(
sut_desc
,
imp_stats
))
size
+=
1
return
results
def
_collect_stats
(
self
,
model
:
Automaton
,
statistics
:
Statistics
)
->
ExperimentStats
:
def
_collect_stats
(
self
,
sut_desc
:
SutDesc
,
model
:
Automaton
,
statistics
:
Statistics
)
->
ExperimentStats
:
states
=
len
(
model
.
states
())
registers
=
len
(
model
.
registers
())
if
isinstance
(
model
,
RegisterMachine
)
else
None
exp_size
=
sut_desc
.
sut_class
.
num_states
(
sut_desc
.
type
,
sut_desc
.
size
)
minimal
=
None
if
exp_size
is
None
else
exp_size
==
len
(
model
.
states
())
learn_tests
=
statistics
.
resets
learn_inputs
=
statistics
.
inputs
learn_time
=
sum
(
statistics
.
learning_times
)
max_ltime
=
max
(
statistics
.
learning_times
)
return
ExperimentStats
(
states
=
states
,
registers
=
registers
,
tests
=
learn_tests
,
inputs
=
learn_inputs
,
max_ltime
=
max_ltime
,
learn_time
=
learn_time
)
return
ExperimentStats
(
states
=
states
,
minimal
=
minimal
,
registers
=
registers
,
tests
=
learn_tests
,
inputs
=
learn_inputs
,
max_ltime
=
max_ltime
,
learn_time
=
learn_time
)
def
run_benchmarks
(
self
,
test_desc
:
TestDesc
,
timeout
:
int
,
max_size
:
int
=
None
,
use_coloring
:
bool
=
False
)
->
List
[
Tuple
[
SutDesc
,
ExperimentStats
]]:
def
run_benchmarks
(
self
,
test_desc
:
TestDesc
,
timeout
:
int
,
min_size
:
int
=
1
,
max_size
:
int
=
1
,
use_coloring
:
bool
=
False
)
->
List
[
Tuple
[
SutDesc
,
ExperimentStats
]]:
results
=
[]
for
sut_class
,
sut_type
in
self
.
suts
:
res
=
self
.
_run_benchmark
(
sut_class
,
sut_type
,
test_desc
,
timeout
,
max_size
,
use_coloring
)
res
=
self
.
_run_benchmark
(
sut_class
,
sut_type
,
test_desc
,
timeout
,
min_size
,
max_size
,
use_coloring
)
results
.
extend
(
res
)
return
results
...
...
@@ -134,6 +141,10 @@ def collate_stats(sut_desc: SutDesc, exp_stats:List[ExperimentStats]):
avg_reg
=
median
(
regs
)
else
:
avg_reg
=
None
if
sut_desc
.
sut_class
.
num_states
(
sut_desc
.
type
,
sut_desc
.
size
)
is
None
:
minimal
=
None
else
:
minimal
=
functools
.
reduce
(
lambda
x
,
y
:
x
&
y
,
[
e
.
minimal
for
e
in
exp_stats
])
consistent
=
len
(
set
(
states
))
==
1
and
\
(
not
sut_desc
.
type
.
has_registers
()
or
len
(
set
(
regs
))
==
1
)
exp_succ
=
len
(
exp_stats
)
...
...
@@ -145,6 +156,7 @@ def collate_stats(sut_desc: SutDesc, exp_stats:List[ExperimentStats]):
exp_succ
=
exp_succ
,
states
=
avg_states
,
registers
=
avg_reg
,
minimal
=
minimal
,
consistent
=
consistent
,
avg_tests
=
median
(
ltests
),
std_tests
=
0
if
len
(
ltests
)
==
1
else
stdev
(
ltests
),
...
...
@@ -177,14 +189,16 @@ b = Benchmark()
#b.add_setup(SUTType.IORA, RALearner(IORAEncoder()), IORARWalkFromState)
# add the sut classes we want to benchmark
#
b.add_sut(FIFOSetClass())
b
.
add_sut
(
FIFOSetClass
()
,
SUTType
.
DFA
)
b
.
add_sut
(
LoginClass
(),
SUTType
.
DFA
)
#b.add_sut(StackClass())
b
.
add_sut
(
FIFOSetClass
(),
SUTType
.
Mealy
)
b
.
add_sut
(
LoginClass
(),
SUTType
.
Mealy
)
#b.add_sut(StackClass(), SUTType.DFA)
#b.add_sut(FIFOSetClass(), SUTType.DFA)
#b.add_sut(FIFOSetClass(), SUTType.
IO
RA)
#b.add_sut(LoginClass(), SUTType.
IORA
)
#b.add_sut(FIFOSetClass(), SUTType.RA)
#b.add_sut(LoginClass(), SUTType.
Mealy
)
#b.add_sut(StackClass(), SUTType.IORA)
# create a test description
...
...
@@ -194,7 +208,10 @@ t_desc = TestDesc(max_tests=10000, prop_reset=0.2, rand_length=3)
timeout
=
10000
# how many times each experiment should be run
num_exp
=
2
num_exp
=
5
# the start size
min_size
=
1
# up to what systems of what size do we want to run experiments (set to None if size is ignored as a stop condition)
max_size
=
None
...
...
@@ -205,7 +222,7 @@ use_coloring = False
# run the benchmark and collect results
results
=
[]
for
i
in
range
(
0
,
num_exp
):
results
+=
b
.
run_benchmarks
(
t_desc
,
timeout
,
max_size
,
use_coloring
)
results
+=
b
.
run_benchmarks
(
t_desc
,
timeout
,
min_size
,
max_size
,
use_coloring
)
print
(
"============================"
)
print_results
(
results
)
sut_dict
=
dict
()
...
...
z3gi/console.py
View file @
28d7109a
...
...
@@ -8,7 +8,7 @@ import model.fa
from
encode.fa
import
MealyEncoder
,
DFAEncoder
from
encode.iora
import
IORAEncoder
from
encode.ra
import
RAEncoder
from
encode.ra
import
RAEncoder
,
RAQREncoder
from
learn.fa
import
FALearner
from
learn.ra
import
RALearner
from
test
import
AcceptorTest
,
IORATest
,
MealyTest
...
...
@@ -20,7 +20,7 @@ from test.rwalk import DFARWalkFromState
"""some configuration mappings"""
aut2learner
=
{
model
.
ra
.
RegisterAutomaton
:
RALearner
(
RAEncoder
()),
model
.
ra
.
RegisterAutomaton
:
RALearner
(
RA
QR
Encoder
()),
model
.
ra
.
IORegisterAutomaton
:
RALearner
(
IORAEncoder
()),
model
.
fa
.
MealyMachine
:
FALearner
(
MealyEncoder
()),
model
.
fa
.
DFA
:
FALearner
(
DFAEncoder
())
...
...
@@ -73,7 +73,7 @@ if __name__ == '__main__':
parser
.
add_argument
(
'-y'
,
'--yannakakis'
,
action
=
'store_true'
,
help
=
'use yannakakis instead of rwalkfromstate '
'(only supports Mealy Machines)'
)
print
(
sut
.
scalable_sut_classes
())
args
=
parser
.
parse_args
()
formalism
=
args
.
aut
formalisms
=
model
.
defined_formalisms
()
...
...
z3gi/define/fa.py
View file @
28d7109a
...
...
@@ -50,9 +50,6 @@ class Mapper(object):
self
.
_elements
=
dict
()
def
element
(
self
,
name
):
#if name not in self._elements:
# self._elements[name] = z3.Const("n"+str(name), self.Element)
#return self._elements[name]
return
z3
.
Const
(
"n"
+
str
(
name
),
self
.
Element
)
...
...
z3gi/define/ra.py
View file @
28d7109a
import
z3
from
model.ra
import
*
from
define
import
dt_enum
,
Automaton
from
define
import
dt_enum
,
Automaton
,
declsort_enum
class
RegisterMachine
(
Automaton
):
...
...
@@ -10,6 +10,9 @@ class RegisterMachine(Automaton):
[
'register{0}'
.
format
(
i
)
for
i
in
range
(
num_registers
)]
+
[
'fresh'
])
self
.
param_size
=
param_size
def
real_reg
(
self
):
return
self
.
registers
[:
-
1
]
class
RegisterAutomaton
(
RegisterMachine
):
def
__init__
(
self
,
labels
,
param_size
,
num_locations
,
num_registers
):
...
...
@@ -24,6 +27,7 @@ class RegisterAutomaton(RegisterMachine):
self
.
update
=
z3
.
Function
(
'update'
,
self
.
Location
,
self
.
Label
,
self
.
Register
)
def
export
(
self
,
model
:
z3
.
ModelRef
)
->
RegisterAutomaton
:
print
(
model
)
builder
=
RegisterAutomatonBuilder
(
self
)
ra
=
builder
.
build_ra
(
model
)
return
ra
...
...
@@ -165,9 +169,9 @@ class IORegisterAutomatonBuilder(object):
self
.
ra
.
transition
(
self
.
ra
.
start
,
z3label
,
self
.
ra
.
fresh
)
!=
self
.
ra
.
sink
))
]
z3output_labels
=
[
z3label
for
z3label
in
self
.
ra
.
labels
.
values
()
if
z3label
not
in
z3input_labels
]
print
(
"Input labels "
,
z3input_labels
,
"; Output labels"
,
z3output_labels
,
"Input states "
,
z3input_states
,
"; Output and sink states"
,
[
z3state
for
z3state
in
self
.
ra
.
locations
if
z3state
not
in
z3input_states
])
#
print("Input labels ", z3input_labels, "; Output labels", z3output_labels,
#
"Input states ", z3input_states, "; Output and sink states",
#
[z3state for z3state in self.ra.locations if z3state not in z3input_states])
for
z3state
in
z3input_states
:
self
.
_add_state
(
translator
,
mut_ra
,
z3state
)
...
...
@@ -229,7 +233,7 @@ class IORegisterAutomatonBuilder(object):
z3end_state
=
model
.
eval
(
self
.
ra
.
transition
(
z3out_state
,
z3output_label
,
z3output_guard
))
z3output_update
=
model
.
eval
(
self
.
ra
.
update
(
z3out_state
,
z3output_label
))
output_mapping
=
None
if
self
.
ra
.
param_size
[
translator
.
z3_to_label
(
z3output_label
)]
==
0
\
else
translator
.
z3_to_mapping
(
z3output_guard
)
else
translator
.
z3_to_mapping
(
z3output_guard
)
transition
=
IORATransition
(
translator
.
z3_to_state
(
z3start_state
),
translator
.
z3_to_label
(
z3label
),
...
...
z3gi/encode/fa.py
View file @
28d7109a
...
...
@@ -2,6 +2,7 @@ import itertools
import
z3
from
define
import
dt_enum
from
define.fa
import
DFA
,
MealyMachine
,
Mapper
from
encode
import
Encoder
from
utils
import
Tree
...
...
@@ -35,7 +36,8 @@ class DFAEncoder(Encoder):
for
label
in
dfa
.
labels
.
values
()]),
z3
.
Distinct
(
list
(
dfa
.
labels
.
values
())),
z3
.
Distinct
(
list
(
dfa
.
states
)),
z3
.
Distinct
([
mapper
.
element
(
node
.
id
)
for
node
in
self
.
cache
])
z3
.
Distinct
([
mapper
.
element
(
node
.
id
)
for
node
in
self
.
cache
]),
# z3.And([z3.Or([mapper.map(mapper.element(node.id)) == q for node in self.cache]) for q in dfa.states])
]
def
node_constraints
(
self
,
dfa
,
mapper
):
...
...
@@ -89,9 +91,9 @@ class MealyEncoder(Encoder):
z3
.
Distinct
(
list
(
mm
.
inputs
.
values
())),
z3
.
Distinct
(
list
(
mm
.
outputs
.
values
())),
z3
.
Distinct
(
list
(
mm
.
states
)),
z3
.
Distinct
([
mapper
.
element
(
node
.
id
)
for
node
in
self
.
cache
])
z3
.
Distinct
([
mapper
.
element
(
node
.
id
)
for
node
in
self
.
cache
]),
# z3.And([z3.Or([mapper.map(mapper.element(node.id)) == q for node in self.cache]) for q in mm.states])
]
#return []
def
node_constraints
(
self
,
mm
,
mapper
):
constraints
=
[]
...
...
z3gi/encode/iora.py
View file @
28d7109a
...
...
@@ -249,7 +249,6 @@ class IORAEncoder(Encoder):
)
for
l
in
self
.
output_labels
:
if
self
.
param_size
[
l
]
==
0
:
print
(
"Added for "
,
l
)
axioms
.
append
(
z3
.
ForAll
(
[
q
,
r
],
...
...
@@ -385,3 +384,362 @@ class IORAEncoder(Encoder):
constraints
.
append
(
z3
.
Distinct
(
list
(
values
)))
return
constraints
class
IORAQREncoder
(
Encoder
):
def
__init__
(
self
):
self
.
tree
=
Tree
(
itertools
.
count
(
0
))
self
.
values
=
set
()
self
.
input_labels
=
set
()
self
.
output_labels
=
set
()
self
.
param_size
=
dict
()
def
add
(
self
,
trace
):
seq
=
list
(
itertools
.
chain
(
*
map
(
iter
,
trace
)))
_
=
self
.
tree
[
determinize
(
seq
)]
self
.
values
.
update
([
action
.
value
for
action
in
seq
])
self
.
input_labels
.
update
([
action
.
label
for
action
in
[
i
for
(
i
,
_
)
in
trace
]])
self
.
output_labels
.
update
([
action
.
label
for
action
in
[
o
for
(
_
,
o
)
in
trace
]])
for
action
in
seq
:
if
action
.
label
not
in
self
.
param_size
:
self
.
param_size
[
action
.
label
]
=
action
.
param_size
()
else
:
if
self
.
param_size
[
action
.
label
]
!=
action
.
param_size
():
raise
Exception
(
"It is not allowed to have actions with different param sizes."
"Problem action: "
+
str
(
action
))
def
build
(
self
,
num_locations
,
num_registers
):
ra
=
IORegisterAutomaton
(
list
(
self
.
input_labels
),
list
(
self
.
output_labels
),
self
.
param_size
,
num_locations
,
num_registers
)
mapper
=
Mapper
(
ra
)
constraints
=
[]
constraints
.
extend
(
self
.
axioms
(
ra
,
mapper
))
constraints
.
extend
(
self
.
node_constraints
(
ra
,
mapper
))
constraints
.
extend
(
self
.
transition_constraints
(
ra
,
mapper
))
return
ra
,
constraints
def
axioms
(
self
,
ra
:
IORegisterAutomaton
,
mapper
:
Mapper
):
#l, lp = z3.Consts('l lp', ra.Label)
#q, qp = z3.Consts('q qp', ra.Location)
#r, rp = z3.Consts('r rp', ra.Register)
norm_loc
=
set
(
ra
.
locations
).
difference
(
set
([
ra
.
sink
]))
axioms
=
[
# In the start state of the mapper,
# all registers contain an uninitialized value.
# axiom not needed
z3
.
And
([
mapper
.
valuation
(
mapper
.
start
,
r
)
==
mapper
.
init
for
r
in
ra
.
registers
]),
# The fresh register is never used
z3
.
And
([
ra
.
used
(
q
,
ra
.
fresh
)
==
False
for
q
in
norm_loc
]),
# If a variable is used after a transition, it means it was either used before, or it was assigned
z3
.
And
([
z3
.
Implies
(
z3
.
And
(
ra
.
used
(
ra
.
transition
(
q
,
l
,
rp
),
r
)
==
True
,
q
!=
ra
.
sink
,
r
!=
ra
.
fresh
),
z3
.
Or
(
ra
.
used
(
q
,
r
)
==
True
,
z3
.
And
(
ra
.
update
(
q
,
l
)
==
r
,
rp
==
ra
.
fresh
),
)
)
for
rp
in
ra
.
registers
for
r
in
ra
.
registers
for
l
in
ra
.
labels
.
values
()
for
q
in
ra
.
locations
]),
# If a variable is updated, then it should have been used.
z3
.
And
([
z3
.
Implies
(
z3
.
And
(
r
!=
ra
.
fresh
,
ra
.
update
(
q
,
l
)
==
r
,
q
!=
ra
.
sink
),
ra
.
used
(
ra
.
transition
(
q
,
l
,
ra
.
fresh
),
r
)
==
True
)
for
r
in
ra
.
registers
for
l
in
ra
.
labels
.
values
()
for
q
in
ra
.
locations
]
),
# Registers are not used in the start state
z3
.
And
([
ra
.
used
(
ra
.
start
,
r
)
==
False
for
r
in
ra
.
registers
])
]
l
,
lp
=
z3
.
Consts
(
'l lp'
,
ra
.
Label
)
q
,
qp
=
z3
.
Consts
(
'q qp'
,
ra
.
Location
)
r
,
rp
=
z3
.
Consts
(
'r rp'
,
ra
.
Register
)
# # IO axioms
axioms
.
extend
([
# The sink is labeled as an input location
ra
.
loctype
(
ra
.
sink
)
==
True
,
# Alternating input and output locations
z3
.
And
(
[
z3
.
If
(
ra
.
loctype
(
q
)
==
True
,
z3
.
And
([
z3
.
Or
(
ra
.
loctype
(
ra
.
transition
(
q
,
l
,
r
))
==
False
,
ra
.
transition
(
q
,
l
,
r
)
==
ra
.
sink
)
for
l
,
r
in
itertools
.
product
(
ra
.
labels
.
values
(),
ra
.
registers
)]),
z3
.
And
([
ra
.
loctype
(
ra
.
transition
(
q
,
l
,
r
))
==
True
for
l
,
r
in
itertools
.
product
(
ra
.
labels
.
values
(),
ra
.
registers
)])
)
for
q
in
ra
.
locations
]
),
# The sink is the only rejecting state
z3
.
And
([
z3
.
If
(
q
==
ra
.
sink
,
ra
.
output
(
q
)
==
False
,
ra
.
output
(
q
)
==
True
)
for
q
in
ra
.
locations
]
),
# The start location is an input location
ra
.
loctype
(
ra
.
start
)
==
True
,
# more readable version
z3
.
ForAll
(
[
q
],
z3
.
Implies
(
z3
.
And
(
q
!=
ra
.
sink
,
ra
.
loctype
(
q
)
==
False
,
),
z3
.
And
(
z3
.
Exists
(
[
r
,
l
],
ra
.
transition
(
q
,
l
,
r
)
!=
ra
.
sink
,
),
z3
.
ForAll
(
[
r
,
l
,
rp
,
lp
],
z3
.
Implies
(
z3
.
And
(
ra
.
transition
(
q
,
l
,
r
)
!=
ra
.
sink
,
z3
.
Or
(
rp
!=
r
,
lp
!=
l
,
)
),
ra
.
transition
(
q
,
lp
,
rp
)
==
ra
.
sink
)
)
)
)
),
# The sink is a sink
z3
.
And
([
ra
.
transition
(
ra
.
sink
,
l
,
r
)
==
ra
.
sink
for
l
,
r
in
itertools
.
product
(
ra
.
labels
.
values
(),
ra
.
registers
)]
),
# The sink doesn't update registers
z3
.
And
([
ra
.
update
(
ra
.
sink
,
l
)
==
ra
.
fresh
for
l
in
ra
.
labels
.
values
()]
)
])
# From input locations, all output transitions go to sink.
axioms
.
extend
([
z3
.
And
([
z3
.
Implies
(
ra
.
loctype
(
q
)
==
True
,
ra
.
transition
(
q
,
ra
.
labels
[
l
],
r
)
==
ra
.
sink
)
for
q
,
r
in
itertools
.
product
(
ra
.
locations
,
ra
.
registers
)]
)
for
l
in
self
.
output_labels
])
# From output locations, all input transitions go to sink.
axioms
.
extend
([
z3
.
And
(
[
z3
.
Implies
(
ra
.
loctype
(
q
)
==
False
,
ra
.
transition
(
q
,
ra
.
labels
[
l
],
r
)
==
ra
.
sink
)
for
q
,
r
in
itertools
.
product
(
ra
.
locations
,
ra
.
registers
)
]
)
for
l
in
self
.
input_labels
])
# Input enabled
axioms
.
extend
([
z3
.
And
(
[
z3
.
Implies
(
z3
.
And
(
ra
.
loctype
(
q
)
==
True
,
q
!=
ra
.
sink
),
ra
.
transition
(
q
,
ra
.
labels
[
l
],
r
)
!=
ra
.
sink
)
for
q
,
r
in
itertools
.
product
(
ra
.
locations
,
ra
.
registers
)]
)
for
l
in
self
.
input_labels
])
# parameter-less labels don't result in register updates
for
l
in
itertools
.
chain
(
self
.
input_labels
,
self
.
output_labels
):
if
self
.
param_size
[
l
]
==
0
:
axioms
.
append
(
z3
.
And
([
ra
.
update
(
q
,
ra
.
labels
[
l
])
==
ra
.
fresh
for
q
in
ra
.
locations
]
)
)
# parameter-less input labels lead to the same transition for all registers
for
l
in
self
.
input_labels
:
if
self
.
param_size
[
l
]
==
0
:
axioms
.
append
(
z3
.
And
(
[
ra
.
transition
(
q
,
ra
.
labels
[
l
],
r
)
==
ra
.
transition
(
q
,
ra
.
labels
[
l
],
ra
.
fresh
)
for
q
,
r
in
itertools
.
product
(
ra
.
locations
,
ra
.
registers
)]
)
)
for
l
in
self
.
output_labels
:
if
self
.
param_size
[
l
]
==
0
:
axioms
.
append
(
z3
.
And
(
[
z3
.
Implies
(
r
!=
ra
.
fresh
,
ra
.
transition
(
q
,
ra
.
labels
[
l
],
r
)
==
ra
.
sink
)
for
q
,
r
in
itertools
.
product
(
ra
.
locations
,
ra
.
registers
)]
)
)
return
axioms
def
node_constraints
(
self
,
ra
,
mapper
):
constraints
=
[]
for
node
in
self
.
tree
:
n
=
mapper
.
element
(
node
.
id
)
constraints
.
append
(
mapper
.
map
(
n
)
!=
ra
.
sink
)
return
constraints
def
transition_constraints
(
self
,
ra
,
mapper
):
constraints
=
[
ra
.
start
==
mapper
.
map
(
mapper
.
start
),
ra
.
sink
!=
ra
.
start
]
values
=
{
mapper
.
init
}
for
node
,
(
label
,
value
),
child
in
self
.
tree
.
transitions
():
n
=
mapper
.
element
(
node
.
id
)
l
=
ra
.
labels
[
label
]
v
=
mapper
.
value
(
value
)
if
value
is
not
None
else
None
c
=
mapper
.
element
(
child
.
id
)
# r, rp = z3.Consts('r rp', ra.Register)
if
value
is
not
None
:
constraints
.
extend
([
# If a non-fresh register has changed, it must have been updated
z3
.
And
(
[
z3
.
Implies
(
z3
.
And
(
r
!=
ra
.
fresh
,
mapper
.
valuation
(
c
,
r
)
!=
mapper
.
valuation
(
n
,
r
)
),
ra
.
update
(
mapper
.
map
(
n
),
l
)
==
r
)
for
r
in
ra
.
registers
]
),
# If a used, non-fresh register keeps its value, then it was not updated.
z3
.
And
(
[
z3
.
Implies
(
z3
.
And
(
r
!=
ra
.
fresh
,
mapper
.
valuation
(
c
,
r
)
==
mapper
.
valuation
(
n
,
r
),
ra
.
used
(
mapper
.
map
(
n
),
r
)
==
True
),
ra
.
update
(
mapper
.
map
(
n
),
l
)
!=
r
)
for
r
in
ra
.
registers
]
),
])
if
value
is
not
None
:
# If a non-fresh register is updated, and c and n are connected by fresh,
# then the register contains the value
# else the valuation is maintained.
constraints
.
append
(
z3
.
And
(
[
z3
.
If
(
z3
.
And
(
r
!=
ra
.
fresh
,
ra
.
update
(
mapper
.
map
(
n
),
l
)
==
r
,
ra
.
transition
(
mapper
.
map
(
n
),
l
,
ra
.
fresh
)
==
mapper
.
map
(
c
)
),
mapper
.
valuation
(
c
,
r
)
==
v
,
mapper
.
valuation
(
c
,
r
)
==
mapper
.
valuation
(
n
,
r
)
)
for
r
in
ra
.
registers
]
))
else
:
constraints
.
append
(
z3
.
And
(
[
mapper
.
valuation
(
c
,
r
)
==
mapper
.
valuation
(
n
,
r
)
for
r
in
ra
.
registers
]
)
)
# Map to the right transition
path
=
[
v
for
(
_
,
v
)
in
node
.
path
()
if
v
is
not
None
]
if
value
in
path
:
if
label
in
self
.
input_labels
:
constraints
.
append
(
z3
.
If
(
z3
.
Or
(
[
z3
.
And
(
r
!=
ra
.
fresh
,
mapper
.
valuation
(
n
,
r
)
==
v
,
ra
.
used
(
mapper
.
map
(
n
),
r
)
==
True
)
for
r
in
ra
.
registers
]
),
z3
.
And
(
[
z3
.
Implies
(
z3
.
And
(
r
!=
ra
.
fresh
,
mapper
.
valuation
(
n
,
r
)
==
v
,
ra
.
used
(
mapper
.
map
(
n
),
r
)
==
True
),