Commit a796a5b3 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Updated repo

parent fa9dd5a6
from z3gi.learn.ra import RALearner
from tests.ra_testscenario import sut_m3, labels
from tests.ra_testscenario import *
from encode.ran import RANEncoder
def check_ra_against_obs(learned_ra, m, test_scenario):
def check_ra_against_obs(learner, learned_ra, m, test_scenario):
"""Checks if the learned RA corresponds to the scenario observations"""
for trace, acc in test_scenario.traces:
if learned_ra.accepts(trace) != acc:
learner.print_tree()
print("Register automaton {0} \n\n with model {1} \n doesn't correspond to the observation {2}"
.format(learned_ra, m, str((trace, acc))))
return
for _ in range(1,50):
learner = RALearner(labels)
exp = sut_m3
for i in range(1,10):
print("Experiment ",i)
learner = RALearner(labels, encoder=RANEncoder())
exp = sut_m1
for trace in exp.traces:
learner.add(trace)
(_, ra, m) = learner._learn_model(4,4,2)
model = ra.export(m)
loc = ra.locations
lbl = ra.labels[labels[0]]
fresh = ra.fresh
check_ra_against_obs(model, m, exp)
\ No newline at end of file
(_, ra, m) = learner._learn_model(exp.nr_locations,exp.nr_locations+1,exp.nr_registers)
if m is not None:
model = ra.export(m)
loc = ra.locations
lbl = ra.labels[labels[0]]
fresh = ra.fresh
check_ra_against_obs(learner, model, m, exp)
else:
print("unsat")
\ No newline at end of file
......@@ -36,10 +36,7 @@ class RANEncoder(Encoder):
# all registers contain an uninitialized value.
z3.ForAll(
[r],
z3.Implies(
r != ra.fresh,
mapper.valuation(mapper.start, r) == mapper.init
)
mapper.valuation(mapper.start, r) == mapper.init
),
# If two locations are connected with both register and fresh transitions,
......@@ -73,7 +70,10 @@ class RANEncoder(Encoder):
),
z3.Or(
ra.used(q, r) == True,
ra.update(q, l) == r
z3.And(
ra.update(q, l) == r,
rp == ra.fresh
),
)
)
),
......@@ -88,17 +88,39 @@ class RANEncoder(Encoder):
),
ra.used(ra.transition(q, l, ra.fresh), r) == True
)
)
]
),
#if not initialized:
# Registers are not used in the start state
axioms.append(z3.ForAll([r], ra.used(ra.start, r) == False))
z3.ForAll(
[r],
ra.used(ra.start, r) == False
)
]
return axioms
def output_constraints(self, ra, mapper):
return [ra.output(mapper.map(mapper.element(node.id))) == accept for node, accept in self.cache.items()]
constraints = []
r = z3.Const('r', ra.Register)
rp = z3.Const('rp', ra.Register)
for node, accept in self.cache.items():
n = mapper.element(node.id)
constraints.extend(
[ra.output(mapper.map(n)) == accept,
# z3.ForAll([r,rp],
# z3.Implies(
# z3.And(
# r != rp,
# r != ra.fresh,
# rp != ra.fresh
# ),
# mapper.valuation(n, r) != mapper.valuation(n, rp)
# )
# )
]
)
return constraints
def transition_constraints(self, ra, mapper):
constraints = [ra.start == mapper.map(mapper.start)]
......@@ -109,7 +131,7 @@ class RANEncoder(Encoder):
v = mapper.value(value)
c = mapper.element(child.id)
r = z3.Const('r', ra.Register)
#rp = z3.Const('rp', ra.Register)
rp = z3.Const('rp', ra.Register)
constraints.extend([
# If the transition is over a register, then the register is in use.
......@@ -118,12 +140,14 @@ class RANEncoder(Encoder):
z3.Implies(
z3.And(
r!= ra.fresh,
ra.transition(mapper.map(n), l, r) == mapper.map(c)),
ra.transition(mapper.map(n), l, r) == mapper.map(c)
),
ra.used(mapper.map(n), r) == True
)
),
# If a non-fresh register has changed, it must have been updated
# and the transition
# what if not used?
z3.ForAll(
[r],
......@@ -135,17 +159,53 @@ class RANEncoder(Encoder):
)
),
# If a register is updated, it must contain the current value
z3.ForAll(
[r],
z3.Implies(
z3.And(
r != ra.fresh,
ra.update(mapper.map(n), l) == r),
mapper.valuation(c, r) == v
mapper.valuation(c, r) == mapper.valuation(n, r),
ra.used(mapper.map(n), r) == True
),
ra.update(mapper.map(n), l) != r
)
),
z3.ForAll(
[r],
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)
),
z3.Exists(
[rp],
z3.And(
rp != ra.fresh,
mapper.valuation(c, rp) == v
)
),
mapper.valuation(c, r) == mapper.valuation(n, r)
)
),
# If a register is updated, then the node reached with a fresh transition must contain the new value
# or
# z3.ForAll(
# [r],
# 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(n, r)
# )
# ),
# Map to the right transition
z3.If(
z3.Exists(
......@@ -164,6 +224,7 @@ class RANEncoder(Encoder):
),
z3.If(
ra.used(mapper.map(n), r) == True,
# it might not keep the valuation
ra.transition(mapper.map(n), l, r) == mapper.map(c),
ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c),
)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment