Commit 8f9b222d authored by Rick Smetsers's avatar Rick Smetsers
Browse files

Added unique valuedness constraints

parent c3b5abba
......@@ -130,13 +130,17 @@ axioms = [
z3.Implies(
z3.And(
r != fresh,
ra.transition(q, l, fresh) == ra.transition(q, l, r)
#ra.update(q, l) == r
ra.transition(q, l, fresh) == ra.transition(q, l, r),
),
ra.guard(q, l, r) == False
z3.And(
ra.update(q, l) != fresh,
ra.update(q, l) != r
)
)
),
z3.ForAll(
[q],
ra.used(q, fresh) == False
......@@ -153,24 +157,60 @@ axioms = [
)
),
# z3.ForAll(
# [q, qp, l, r],
# z3.Implies(
# z3.And(
# ra.transition(q, l, r) == qp,
# ra.guard(q, l, r) == True,
# ra.used(qp, r) == True
# ),
# z3.Or(
# ra.used(q, r) == True,
# z3.And(
# ra.transition(q, l, fresh) == qp,
# ra.update(q, l) == r
# )
# )
# )
# ),
z3.ForAll(
[q, qp, l, r],
[q, l, r, rp],
z3.Implies(
z3.And(
ra.transition(q, l, r) == qp,
ra.guard(q, l, r) == True,
ra.used(qp, r) == True
),
z3.Or(
ra.used(q, r) == True,
z3.And(
ra.transition(q, l, fresh) == qp,
ra.update(q, l) == r
)
)
ra.guard(q, l, rp) == True
),
ra.used(ra.transition(q, l, rp), r) == True
)
),
z3.ForAll(
[q, l, r],
z3.Implies(
z3.And(
r != fresh,
ra.update(q, l) == r
),
ra.used(ra.transition(q, l, fresh), r) == True
)
),
z3.ForAll(
[q, l, r, rp],
z3.Implies(
z3.And(
r != rp,
r != fresh,
rp != fresh,
ra.used(q, r),
ra.update(q, l) == rp
),
ra.guard(q, l, r) == True
)
)
# Frits' type RA's (uncomment this)
# z3.ForAll(
# [r],
......@@ -355,6 +395,33 @@ data_m5 = [
([act(0), act(1), act(2), act(3), act(4)], True),
]
data_m6 = [
([], False),
([act(0)], True),
([act(0), act(0)], False),
([act(0), act(1)], False),
#([act(0), act(0), act(0)], ???),
([act(0), act(0), act(1)], False),
([act(0), act(1), act(0)], True),
([act(0), act(1), act(1)], False),
([act(0), act(1), act(2)], False),
#([act(0), act(0), act(0), act(0)], ???),
#([act(0), act(0), act(0), act(1)], ???),
#([act(0), act(0), act(1), act(0)], ???),
([act(0), act(0), act(1), act(1)], False),
([act(0), act(0), act(1), act(2)], False),
([act(0), act(1), act(0), act(0)], False),
([act(0), act(1), act(0), act(1)], True),
([act(0), act(1), act(0), act(2)], False),
([act(0), act(1), act(1), act(0)], True),
([act(0), act(1), act(1), act(1)], True),
([act(0), act(1), act(1), act(2)], True),
([act(0), act(1), act(2), act(0)], True),
([act(0), act(1), act(2), act(1)], False),
([act(0), act(1), act(2), act(2)], False),
([act(0), act(1), act(2), act(3)], False),
]
data = data_m5
# from random import shuffle
# shuffle(data)
......
......@@ -43,16 +43,19 @@ class RAEncoder(Encoder):
)
),
# An active non-fresh transition and a fresh transition from a location can not go to the same location.
# If two locations are connected with both register and fresh transitions,
# then you have to do an update on a different register (otherwise you should merge the two transitions)
z3.ForAll(
[q, l, r],
z3.Implies(
z3.And(
r != ra.fresh,
ra.transition(q, l, ra.fresh) == ra.transition(q, l, r),
ra.update(q, l) == r
),
ra.guard(q, l, r) == False
z3.And(
ra.update(q, l) != ra.fresh,
ra.update(q, l) != r
)
)
),
......@@ -74,24 +77,42 @@ class RAEncoder(Encoder):
)
),
# If a register is used after a transition,
# then it was either used before the transition
# or it stores the value carried by the transition.
# If a register was used in a state, then it is used in any state that can be reached from this state.
z3.ForAll(
[q, qp, l, r],
[q, l, r, rp],
z3.Implies(
z3.And(
ra.transition(q, l, r) == qp,
ra.guard(q, l, r) == True,
ra.used(qp, r) == True
),
z3.Or(
ra.used(q, r) == True,
z3.And(
ra.transition(q, l, ra.fresh) == qp,
ra.update(q, l) == r
)
)
ra.guard(q, l, rp) == True
),
ra.used(ra.transition(q, l, rp), r) == True
)
),
# If a register is updated, it is used in the state that is reached.
z3.ForAll(
[q, l, r],
z3.Implies(
z3.And(
r != ra.fresh,
ra.update(q, l) == r
),
ra.used(ra.transition(q, l, ra.fresh), r) == True
)
),
# The automaton we learn is unique valued.
z3.ForAll(
[q, l, r, rp],
z3.Implies(
z3.And(
r != rp,
r != ra.fresh,
rp != ra.fresh,
ra.used(q, r),
ra.update(q, l) == rp
),
ra.guard(q, l, r) == True
)
)
]
......
from z3gi.learn import Learner
class RALearner(Learner):
def model(self):
pass
def add(self, trace):
pass
def __init__(self):
pass
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