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

The export function works and we get the right model. Still needs some testing.

parent 9a3a6ca6
......@@ -4,4 +4,4 @@ class Automaton(metaclass=ABCMeta):
@abstractmethod
def export(self, model):
"""Returns a z3gi.model for this automaton."""
pass
\ No newline at end of file
pass
......@@ -23,7 +23,7 @@ class RegisterAutomaton(Automaton):
def export(self, model : z3.ModelRef) -> RegisterAutomaton:
builder = RegisterAutomatonBuilder(self)
ra = builder.build_ra(model, self.locations, list(self.labels.values()), self.registers)
ra = builder.build_ra(model)
return ra
......@@ -33,6 +33,7 @@ class IORegisterAutomaton(Automaton):
labels = input_labels + output_labels
self.Label, elements = enum('Label', input_labels + output_labels)
self.labels = {labels[i]: elements[i] for i in range(len(labels))}
self._input_labels = [self.labels[lbl] for lbl in input_labels]
self.Location, self.locations = enum('Location', ['location{0}'.format(i) for i in range(num_locations + 1)])
self.sink = self.locations[-1]
self.Register, self.registers = enum('Register', ['register{0}'.format(i) for i in range(num_registers)] + ['fresh'])
......@@ -46,7 +47,9 @@ class IORegisterAutomaton(Automaton):
def export(self, model : z3.ModelRef) -> RegisterAutomaton:
raise NotImplementedError()
builder = IORegisterAutomatonBuilder(self)
ra = builder.build_ra(model)
return ra
class Mapper(object):
......@@ -72,23 +75,25 @@ class RegisterAutomatonBuilder(object):
super().__init__()
self.ra = ra
def build_ra(self, model, states, labels, regs):
def build_ra(self, model):
mut_ra = MutableRegisterAutomaton()
translator = Translator(self.ra)
for z3state in states:
for z3state in self.ra.locations:
self._add_state(model, translator, mut_ra, z3state)
for z3label in labels:
self._add_transitions(model, translator, mut_ra, z3state, z3label, regs)
for z3label in self.ra.labels.values():
self._add_transitions(model, translator, mut_ra, z3state, z3label)
return mut_ra.to_immutable()
def _add_state(self, model, translator, mut_ra, z3state):
z3acc = model.eval(model.eval(self.ra.output(z3state)))
mut_ra.add_state(translator.z3_to_state(z3state), translator.z3_to_bool(z3acc) )
def _add_transitions(self, model, translator, mut_ra, z3state, z3label, z3regs):
def _add_transitions(self, model, translator, mut_ra, z3state, z3label):
z3end_state_to_guards = dict()
enabled_z3guards = [guard for guard in z3regs if
translator.z3_to_bool(model.eval(self.ra.used(z3state, guard)))]
enabled_z3guards = [guard for guard in self.ra.registers if
translator.z3_to_bool(model.eval(self.ra.used(z3state, guard))) or
guard is self.ra.fresh
]
if self.ra.fresh not in enabled_z3guards:
enabled_z3guards.append(self.ra.fresh)
for z3guard in enabled_z3guards:
......@@ -110,13 +115,13 @@ class RegisterAutomatonBuilder(object):
z3guards, None, z3end_state, used_z3regs)
def _add_transition(self, translator, mut_ra, z3start_state, z3label, z3guards, z3update, z3end_state, used_z3regs):
start_state = translator.z3_to_state(z3start_state)
guard = translator.z3_to_guard(z3guards, used_z3regs)
asg = translator.z3_to_assignment(z3update)
end_state = translator.z3_to_state(z3end_state)
transition = RATransition(start_state, translator.z3_to_label(z3label),
guard, asg, end_state)
mut_ra.add_transition(start_state, transition)
transition = RATransition(translator.z3_to_state(z3start_state), # start state
translator.z3_to_label(z3label), # label
translator.z3_to_guard(z3guards, used_z3regs), # guard
translator.z3_to_assignment(z3update), # assignment
translator.z3_to_state(z3end_state) # end state
)
mut_ra.add_transition(translator.z3_to_state(z3start_state),transition)
class IORegisterAutomatonBuilder(object):
......@@ -128,16 +133,27 @@ class IORegisterAutomatonBuilder(object):
self.ra = ra
def build_ra(self, model, input_labels, output_labels):
def build_ra(self, model):
mut_ra = MutableIORegisterAutomaton()
translator = Translator(self.ra)
z3input_states = [z3state for z3state in self.ra.locations if
translator.z3_to_bool(model.eval(self.ra.loctype(z3state)))]
translator.z3_to_bool(model.eval(
z3.And(self.ra.loctype(z3state), z3state != self.ra.sink)))]
# we cannot use 'is not', since 'is not' compares references, not values and model.eval produces a
# different reference
z3input_labels = [z3label for z3label in self.ra.labels.values() if
translator.z3_to_bool(model.eval(
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)
for z3state in z3input_states:
self._add_state(translator, mut_ra, z3state)
for z3label in input_labels:
self._add_transitions(model, translator, mut_ra, z3state, z3label, output_labels)
for z3label in z3input_labels:
self._add_transitions(model, translator, mut_ra, z3state, z3label, z3output_labels)
return mut_ra.to_immutable()
def _add_state(self, translator, mut_ra, z3state):
......@@ -162,7 +178,7 @@ class IORegisterAutomatonBuilder(object):
for (z3out_state, z3guards) in z3end_state_to_guards.items():
# a transition which makes an assignment is never merged
if self.ra.fresh in z3guards and update is not self.ra.fresh:
self._add_transition(translator, mut_ra, z3state, z3label,
self._add_transition(model, translator, mut_ra, z3state, z3label,
[self.ra.fresh], update, z3out_state,
z3output_labels, used_z3regs)
z3guards.remove(self.ra.fresh)
......@@ -179,13 +195,16 @@ class IORegisterAutomatonBuilder(object):
guard is self.ra.fresh]
active_z3action = [(output_label, guard) for output_label in output_labels for guard in enabled_z3guards
if model.eval(self.ra.transition(z3out_state, output_label, guard)) is not self.ra.sink]
if translator.z3_to_bool(model.eval(self.ra.transition(z3out_state, output_label, guard)
!= self.ra.sink))]
if len(active_z3action) != 1:
raise Exception("Exactly one transition should not lead to sink state")
raise Exception("Exactly one transition should not lead to sink state. "
"From location {0} there are {1} transitions which lead to sink"
.format(z3out_state, len(active_z3action)))
(z3output_label, z3output_guard) = active_z3action[0]
z3end_state = model.eval(self.ra.transitions(z3output_label, z3output_guard))
z3output_update = model.eval(self.ra.update(z3out_state))
z3end_state = model.eval(self.ra.transition(z3out_state, z3output_label, z3output_guard))
z3output_update = model.eval(self.ra.update(z3out_state, z3output_label))
transition = IORATransition(translator.z3_to_state(z3start_state),
translator.z3_to_label(z3label),
......@@ -196,7 +215,7 @@ class IORegisterAutomatonBuilder(object):
translator.z3_to_assignment(z3output_update),
translator.z3_to_state(z3end_state),
)
mut_ra.add_transition(z3start_state, transition)
mut_ra.add_transition(translator.z3_to_state(z3start_state), transition)
class Translator(object):
"""Provides translation from z3 constants to RA elements. """
......
......@@ -44,20 +44,20 @@ class IORAEncoder(Encoder):
# # 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.transition(q, l, ra.fresh) != ra.sink
),
z3.And(
ra.update(q, l) != ra.fresh,
ra.update(q, l) != r
)
)
),
# z3.ForAll(
# [q, l, r],
# z3.Implies(
# z3.And(
# r != ra.fresh,
# ra.transition(q, l, ra.fresh) == ra.transition(q, l, r),
# ra.transition(q, l, ra.fresh) != ra.sink
# ),
# z3.And(
# ra.update(q, l) != ra.fresh,
# ra.update(q, l) != r
# )
# )
# ),
# The fresh register is never used
z3.ForAll(
......@@ -74,7 +74,8 @@ class IORAEncoder(Encoder):
z3.Implies(
z3.And(
ra.used(ra.transition(q, l, rp), r) == True,
q != ra.sink
q != ra.sink,
r != ra.fresh
),
z3.Or(
ra.used(q, r) == True,
......@@ -150,7 +151,10 @@ class IORAEncoder(Encoder):
l != lp
)
),
ra.transition(q, lp, rp) == ra.sink
z3.Or(
ra.transition(q, lp, rp) == ra.sink,
rp != ra.fresh
)
)
),
......@@ -184,7 +188,7 @@ class IORAEncoder(Encoder):
[q, r],
z3.Implies(
ra.loctype(q) == False,
ra.transition(q, ra. labels[l], r) == ra.sink
ra.transition(q, ra.labels[l], r) == ra.sink
)
)
for l in self.input_labels])
......@@ -317,64 +321,20 @@ class IORAEncoder(Encoder):
)
elif label in self.output_labels:
constraints.append(
z3.If(
z3.Exists(
z3.Exists(
[r],
z3.And(
r != ra.fresh,
mapper.valuation(n, r) == v
)
),
z3.ForAll(
[r],
z3.Implies(
z3.And(
r != ra.fresh,
mapper.valuation(n, r) == v
),
z3.And(
ra.used(mapper.map(n), r) == True,
ra.transition(mapper.map(n), l, r) == mapper.map(c),
)
)
),
False
)
)
)
else:
raise Exception("We did something wrong")
else:
# Take the fresh transition
constraints.append(ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c))
# # Map to the right transition
# z3.If(
# z3.Exists(
# [r],
# z3.And(
# r != ra.fresh,
# mapper.valuation(n, r) == v
# )
# ),
# z3.ForAll(
# [r],
# z3.Implies(
# z3.And(
# r != ra.fresh,
# mapper.valuation(n, r) == v
# ),
# 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)
# )
# )
# ),
# ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c)
# )
constraints.append(ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c))
values.add(v)
......
......@@ -78,9 +78,9 @@ class IORATransition(RATransition):
return self.output_assignment.update(valuation, action.value)
def __str__(self, shortened=False):
trans_str = "{0}({1}) {2} {3} / {4}({5}) {6} {7}"\
trans_str = "{0}({1}) {2} / {3}({4}) {5} {6}"\
.format(self.start_label, self.guard, self.assignment, self.output_label,\
self.output_mapping, self.output_mapping, self.end_state)
self.output_mapping, self.output_assignment, self.end_state)
if not shortened:
trans_str = self.start_label + " " + trans_str
......
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