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

An alternative encoding. Doesn't work fully, but it is already more reliable.

parent c2dd19af
......@@ -26,6 +26,25 @@ class RegisterAutomaton(Automaton):
ra = builder.build_ra(model, self.locations, list(self.labels.values()), self.registers)
return ra
class SimpleRegisterAutomaton(Automaton):
def __init__(self, labels, num_locations, num_registers):
self.Label, elements = enum('Label', labels)
self.labels = {labels[i]: elements[i] for i in range(len(labels))}
self.Location, self.locations = enum('Location', ['location{0}'.format(i) for i in range(num_locations)])
self.Register, self.registers = enum('Register', ['register{0}'.format(i) for i in range(num_registers)] + ['fresh'])
self.start = self.locations[0]
self.fresh = self.registers[-1]
self.transition = z3.Function('transition', self.Location, self.Label, self.Register, self.Location)
self.output = z3.Function('output', self.Location, z3.BoolSort())
self.used = z3.Function('used', self.Location, self.Register, z3.BoolSort())
self.update = z3.Function('update', self.Location, self.Label, self.Register)
def export(self, model : z3.ModelRef) -> RegisterAutomaton:
builder = SimpleRegisterAutomatonBuilder(self)
ra = builder.build_ra(model, self.locations, list(self.labels.values()), self.registers)
return ra
class IORegisterAutomaton(RegisterAutomaton):
......@@ -101,6 +120,61 @@ class RegisterAutomatonBuilder():
guard, asg, end_state)
mut_ra.add_transition(start_state, transition)
class SimpleRegisterAutomatonBuilder():
"""
Builder class that construct a register automaton out of a model definition.
"""
def __init__(self, ra : SimpleRegisterAutomaton):
super().__init__()
self.ra = ra
def build_ra(self, model, states, labels, regs):
mut_ra = MutableRegisterAutomaton()
translator = Translator(self.ra)
for z3state in states:
self._add_state(model, translator, mut_ra, z3state)
for z3label in labels:
self._add_transitions(model, translator, mut_ra, z3state, z3label, regs)
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):
z3end_state_to_guards = dict()
enabled_z3guards = [guard for guard in z3regs if
translator.z3_to_bool(model.eval(self.ra.used(z3state, guard)))]
if self.ra.fresh not in enabled_z3guards:
enabled_z3guards.append(self.ra.fresh)
for z3guard in enabled_z3guards:
z3end_state = model.eval(self.ra.transition(z3state, z3label, z3guard))
if z3end_state not in z3end_state_to_guards:
z3end_state_to_guards[z3end_state] = []
z3end_state_to_guards[z3end_state].append(z3guard)
update = model.eval(self.ra.update(z3state, z3label))
start_state = translator.z3_to_state(z3state)
enabled_z3regs = [reg for reg in enabled_z3guards if reg is not self.ra.fresh]
for (z3end_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, start_state, z3label,
[self.ra.fresh], update, z3end_state, enabled_z3regs)
z3guards.remove(self.ra.fresh)
if len(z3guards) > 0:
self._add_transition(translator, mut_ra, start_state, z3label,
z3guards, None, z3end_state, enabled_z3regs)
def _add_transition(self, translator, mut_ra, start_state, z3label, z3guards, z3asg, z3end_state, enabled_z3regs):
guard = translator.z3_to_guard(z3guards, enabled_z3regs)
asg = translator.z3_to_assignment(z3asg)
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)
class Translator():
"""Provides translation from z3 constants to RA elements. """
def __init__(self, ra):
......
......@@ -22,6 +22,9 @@ class RAEncoder(Encoder):
self.output_constraints(ra, mapper) + \
self.transition_constraints(ra, mapper)
def print_tree(self):
print(self.trie)
@staticmethod
def axioms(ra, mapper, initialized):
l = z3.Const('l', ra.Label)
......@@ -110,13 +113,14 @@ class RAEncoder(Encoder):
r != rp,
r != ra.fresh,
rp != ra.fresh,
ra.used(q, r),
ra.used(q, r) == True,
ra.update(q, l) == rp
),
ra.guard(q, l, r) == True
)
)
]
if not initialized:
# Registers are not used in the start state
axioms.append(z3.ForAll([r], ra.used(ra.start, r) == False))
......@@ -124,6 +128,22 @@ class RAEncoder(Encoder):
return axioms
def output_constraints(self, ra, mapper):
# r = z3.Const('r', ra.Register)
# rp = z3.Const('rp', ra.Register)
# constraints = []
# 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(
# # mapper.valuation(n, r) == mapper.valuation(n, rp),
# # z3.Or(r == rp, mapper.valuation(n, r) == mapper.init, r == ra.fresh, rp == ra.fresh)
# # )
# # ),
# ])
# return constraints
return [ra.output(mapper.map(mapper.element(node.id))) == accept for node, accept in self.cache.items()]
def transition_constraints(self, ra, mapper):
......@@ -135,6 +155,7 @@ class RAEncoder(Encoder):
v = mapper.value(value)
c = mapper.element(child.id)
r = z3.Const('r', ra.Register)
#rp = z3.Const('rp', ra.Register)
constraints.extend([
# The guard on this transition is active.
......@@ -221,6 +242,16 @@ class RAEncoder(Encoder):
for label, value in node.children:
yield node, label, value, node.children[(label, value)]
def __str__(self, tabs=0):
space = "".join(["\t" for _ in range(0,tabs)])
# print(space, "n", self.id)
tree = "(n{0}".format(self.id)
for label, value in self.children:
tree+= "\n" + space + " {0} -> {1}".format(value, self.children[(label, value)].__str__(tabs=tabs+1))
tree += ")"
return tree
@staticmethod
class Mapper(object):
def __init__(self, ra):
......
import itertools
import z3
from encode import Encoder
from define.ra import SimpleRegisterAutomaton
class RANEncoder(Encoder):
def __init__(self):
self.trie = RANEncoder.Trie(itertools.count(0))
self.cache = {}
self.values = set()
def add(self, trace):
seq, accept = trace
node = self.trie[determinize(seq)]
self.cache[node] = accept
self.values.update([action.value for action in seq])
def build(self, ra, initialized=True):
mapper = RANEncoder.Mapper(ra)
return self.axioms(ra, mapper, initialized) + \
self.output_constraints(ra, mapper) + \
self.transition_constraints(ra, mapper)
def print_tree(self):
print(self.trie)
@staticmethod
def axioms(ra : SimpleRegisterAutomaton, mapper, initialized):
l = z3.Const('l', ra.Label)
q, qp = z3.Consts('q qp', ra.Location)
r, rp = z3.Consts('r rp', ra.Register)
axioms = [
# In the start state of the mapper,
# all registers contain an uninitialized value.
z3.ForAll(
[r],
z3.Implies(
r != ra.fresh,
mapper.valuation(mapper.start, r) == mapper.init
)
),
# 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),
),
z3.And(
ra.update(q, l) != ra.fresh,
ra.update(q, l) != r
)
)
),
# The fresh register is never used
z3.ForAll(
[q],
ra.used(q, ra.fresh) == False
),
# If a variable is used after a transition, it means it was either used before, or it was assigned
z3.ForAll(
[q, l, r, rp],
z3.Implies(
z3.And(
ra.used(ra.transition(q, l, rp), r) == True
),
z3.Or(
ra.used(q, r) == True,
ra.update(q, l) == r
)
)
),
# If a variable is updated, then it should have been used.
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
)
)
]
#if not initialized:
# Registers are not used in the start state
axioms.append(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()]
def transition_constraints(self, ra, mapper):
constraints = [ra.start == mapper.map(mapper.start)]
values = {mapper.init}
for node, label, value, child in self.trie.transitions():
n = mapper.element(node.id)
l = ra.labels[label]
v = mapper.value(value)
c = mapper.element(child.id)
r = z3.Const('r', ra.Register)
#rp = z3.Const('rp', ra.Register)
constraints.extend([
# If the transition is over a register, then the register is in use.
z3.ForAll(
[r],
z3.Implies(
z3.And(
r!= ra.fresh,
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
# what if not used?
z3.ForAll(
[r],
z3.Implies(
z3.And(
r != ra.fresh,
mapper.valuation(c, r) != mapper.valuation(n, r)),
ra.update(mapper.map(n), l) == r
)
),
# 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
)
),
# 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,
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)),
])
values.add(v)
constraints.append(z3.Distinct(list(values)))
return constraints
@staticmethod
class Trie(object):
def __init__(self, counter):
self.id = next(counter)
self.counter = counter
self.children = {}
def __getitem__(self, seq):
trie = self
for label, value in seq:
if (label, value) not in trie.children:
trie.children[(label, value)] = RANEncoder.Trie(self.counter)
trie = trie.children[(label, value)]
return trie
def __iter__(self):
yield self
for node in itertools.chain(*map(iter, self.children.values())):
yield node
def transitions(self):
for node in self:
for label, value in node.children:
yield node, label, value, node.children[(label, value)]
def __str__(self, tabs=0):
space = "".join(["\t" for _ in range(0,tabs)])
# print(space, "n", self.id)
tree = "(n{0}".format(self.id)
for label, value in self.children:
tree+= "\n" + space + " {0} -> {1}".format(value, self.children[(label, value)].__str__(tabs=tabs+1))
tree += ")"
return tree
@staticmethod
class Mapper(object):
def __init__(self, ra):
self.Value = z3.DeclareSort('Value')
self.Element = z3.DeclareSort('Element')
self.start = self.element(0)
self.init = self.value("_")
self.map = z3.Function('map', self.Element, ra.Location)
self.valuation = z3.Function('valuation', self.Element, ra.Register, self.Value)
def value(self, name):
return z3.Const("v"+str(name), self.Value)
def element(self, name):
return z3.Const("n"+str(name), self.Element)
def determinize(seq):
neat = {}
i = 0
for (label, value) in seq:
if value not in neat:
neat[value] = i
i = i + 1
return [(label, neat[value]) for label, value in seq]
import z3
from define.ra import RegisterAutomaton, IORegisterAutomaton
from define.ra import RegisterAutomaton, IORegisterAutomaton, SimpleRegisterAutomaton
from encode.ra import RAEncoder
from learn import Learner
import model.ra
......@@ -33,6 +33,9 @@ class RALearner(Learner):
return ra_def.export(m)
return None
def print_tree(self):
self.encoder.print_tree()
def _learn_model(self, min_locations, max_locations, num_registers) -> \
(bool, RegisterAutomaton, z3.ModelRef):
"""generates the definition and model for an ra whose traces include the traces added so far"""
......@@ -46,7 +49,7 @@ class RALearner(Learner):
if self.io:
ra = IORegisterAutomaton(inputs=self.labels, outputs=self.outputs, num_locations=num_locations, num_registers=num_registers)
else:
ra = RegisterAutomaton(labels=self.labels, num_locations=num_locations, num_registers=num_registers)
ra = SimpleRegisterAutomaton(labels=self.labels, num_locations=num_locations, num_registers=num_registers)
constraints = self.encoder.build(ra)
self.solver.add(constraints)
result = self.solver.check()
......
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