Commit f67529ed authored by Rick Smetsers's avatar Rick Smetsers
Browse files

Fixed everyting

parent a796a5b3
from z3gi.learn.ra import RALearner
from tests.ra_testscenario import *
from encode.ran import RANEncoder
from encode.ra import RAEncoder
def check_ra_against_obs(learner, learned_ra, m, test_scenario):
......@@ -14,7 +14,7 @@ def check_ra_against_obs(learner, learned_ra, m, test_scenario):
for i in range(1,10):
print("Experiment ",i)
learner = RALearner(labels, encoder=RANEncoder())
learner = RALearner(labels, encoder=RAEncoder())
exp = sut_m1
for trace in exp.traces:
learner.add(trace)
......
# TODO make standalone
from define import Automaton
class IORegisterAutomaton(Automaton):
def __init__(self, inputs, outputs, num_locations, num_registers):
super().__init__(inputs + outputs, num_locations + 1, num_registers)
del self.output
self.sink = self.locations[-1]
self.statetype = z3.Function('statetype', self.Location, z3.BoolSort())
def export(self, model):
raise NotImplementedError()
......@@ -4,7 +4,8 @@ import z3
from model.ra import *
from z3gi.define import Automaton
from define import Automaton
class RegisterAutomaton(Automaton):
......@@ -18,7 +19,6 @@ class RegisterAutomaton(Automaton):
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.guard = z3.Function('guard', self.Location, self.Label, self.Register, z3.BoolSort())
self.update = z3.Function('update', self.Location, self.Label, self.Register)
def export(self, model : z3.ModelRef) -> RegisterAutomaton:
......@@ -26,109 +26,31 @@ 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):
def __init__(self, inputs, outputs, num_locations, num_registers):
super().__init__(inputs + outputs, num_locations + 1, num_registers)
del self.output
self.sink = self.locations[-1]
self.statetype = z3.Function('statetype', self.Location, z3.BoolSort())
def export(self, model):
raise NotImplementedError()
def enum(name, elements):
d = z3.Datatype(name)
for element in elements:
d.declare(element)
d = d.create()
return d, [d.__getattribute__(element) for element in elements]
class RegisterAutomatonBuilder():
"""
Builder class that construct a register automaton out of a model definition.
"""
class Mapper(object):
def __init__(self, ra):
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()
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 _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 value(self, name):
return z3.Const("v"+str(name), self.Value)
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.guard(z3state, z3label, guard)))]
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]
def element(self, name):
return z3.Const("n"+str(name), self.Element)
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 SimpleRegisterAutomatonBuilder():
class RegisterAutomatonBuilder(object):
"""
Builder class that construct a register automaton out of a model definition.
"""
def __init__(self, ra : SimpleRegisterAutomaton):
def __init__(self, ra : RegisterAutomaton):
super().__init__()
self.ra = ra
def build_ra(self, model, states, labels, regs):
mut_ra = MutableRegisterAutomaton()
translator = Translator(self.ra)
......@@ -175,7 +97,7 @@ class SimpleRegisterAutomatonBuilder():
guard, asg, end_state)
mut_ra.add_transition(start_state, transition)
class Translator():
class Translator(object):
"""Provides translation from z3 constants to RA elements. """
def __init__(self, ra):
self.reg_context = dict()
......@@ -216,4 +138,12 @@ class Translator():
assert z3register is not self.ra.fresh
if str(z3register) not in self.reg_context:
self.reg_context[str(z3register)] = Register(self.ra.registers.index(z3register))
return self.reg_context[str(z3register)]
\ No newline at end of file
return self.reg_context[str(z3register)]
def enum(name, elements):
d = z3.Datatype(name)
for element in elements:
d.declare(element)
d = d.create()
return d, [d.__getattribute__(element) for element in elements]
......@@ -6,5 +6,5 @@ class Encoder(metaclass=ABCMeta):
pass
@abstractmethod
def build(self, automaton):
def build(self, *args):
pass
\ No newline at end of file
......@@ -15,7 +15,7 @@ class IORAEncoder(RAEncoder):
def add(self, trace):
seq = list(itertools.chain(*map(iter, trace)))
print(list(seq))
node = self.trie[determinize(seq)]
node = self.tree[determinize(seq)]
self.values.update([action.value for action in seq])
self.inputs.update([action.label for action in [i for (i, o) in trace]])
self.outputs.update([action.label for action in [o for (i, o) in trace]])
......
......@@ -2,49 +2,44 @@ import itertools
import z3
from encode import Encoder
from define.ra import RegisterAutomaton, Mapper
from utils import Tree, determinize
class RAEncoder(Encoder):
def __init__(self):
self.trie = RAEncoder.Trie(itertools.count(0))
self.tree = Tree(itertools.count(0))
self.cache = {}
self.values = set()
self.labels = set()
def add(self, trace):
seq, accept = trace
node = self.trie[determinize(seq)]
node = self.tree[determinize(seq)]
self.cache[node] = accept
self.values.update([action.value for action in seq])
self.labels.update([action.label for action in seq])
def build(self, ra, initialized=True):
mapper = RAEncoder.Mapper(ra)
return self.axioms(ra, mapper, initialized) + \
self.output_constraints(ra, mapper) + \
self.transition_constraints(ra, mapper)
def build(self, num_locations, num_registers):
ra = RegisterAutomaton(list(self.labels), num_locations, num_registers)
mapper = Mapper(ra)
constraints = self.axioms(ra, mapper) + \
self.output_constraints(ra, mapper) + \
self.transition_constraints(ra, mapper)
return ra, constraints
def print_tree(self):
print(self.trie)
@staticmethod
def axioms(ra, mapper, initialized):
def axioms(ra : RegisterAutomaton, mapper):
l = z3.Const('l', ra.Label)
q, qp = z3.Consts('q qp', ra.Location)
r, rp = z3.Consts('r rp', ra.Register)
axioms = [
# Fresh guards are always active
z3.ForAll(
[q, l],
ra.guard(q, l, ra.fresh) == True
),
# 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
)
mapper.valuation(mapper.start, r) == mapper.init
),
# If two locations are connected with both register and fresh transitions,
......@@ -63,37 +58,28 @@ class RAEncoder(Encoder):
)
),
# The fresh register never has a memorable value.
# The fresh register is never used
z3.ForAll(
[q],
ra.used(q, ra.fresh) == False
),
# If a register is not used, then there are no guards defined over it.
z3.ForAll(
[q, l, r],
z3.Implies(
z3.And(
r != ra.fresh,
ra.used(q, r) == False
),
ra.guard(q, l, r) == False
)
),
# If a register was used in a state, then it is used in any state that can be reached from this state.
# 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.guard(q, l, rp) == True
),
ra.used(ra.transition(q, l, rp), r) == True
z3.And(
ra.update(q, l) == r,
rp == ra.fresh
),
)
)
),
# If a register is updated, it is used in the state that is reached.
# If a variable is updated, then it should have been used.
z3.ForAll(
[q, l, r],
z3.Implies(
......@@ -105,65 +91,45 @@ class RAEncoder(Encoder):
)
),
# The automaton we learn is unique valued.
# Registers are not used in the start state
z3.ForAll(
[q, l, r, rp],
z3.Implies(
z3.And(
r != rp,
r != ra.fresh,
rp != ra.fresh,
ra.used(q, r) == True,
ra.update(q, l) == rp
),
ra.guard(q, l, r) == True
)
[r],
ra.used(ra.start, r) == False
)
]
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):
# 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()]
constraints = []
for node, accept in self.cache.items():
n = mapper.element(node.id)
constraints.extend(
[ra.output(mapper.map(n)) == accept]
)
return constraints
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():
for node, label, value, child in self.tree.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)
r, rp = z3.Consts('r rp', ra.Register)
constraints.extend([
# The guard on this transition is active.
# If the transition is over a register, then the register is in use.
z3.ForAll(
[r],
z3.Implies(
ra.transition(mapper.map(n), l, r) == mapper.map(c),
ra.guard(mapper.map(n), l, r) == True
z3.And(
r!= ra.fresh,
ra.transition(mapper.map(n), l, r) == mapper.map(c)
),
ra.used(mapper.map(n), r) == True
)
),
......@@ -173,17 +139,44 @@ class RAEncoder(Encoder):
z3.Implies(
z3.And(
r != ra.fresh,
mapper.valuation(c, r) != mapper.valuation(n, r)),
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
# If a used, non-fresh register keeps its value, then it was not updated.
z3.ForAll(
[r],
z3.Implies(
z3.And(r != ra.fresh, ra.update(mapper.map(n), l) == r),
mapper.valuation(c, r) == v
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
)
),
# If a non-fresh register is updated, and c and n are connect by fresh,
# then in c there is a register whose value is v,
# else the valuation is maintained.
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)
)
),
......@@ -204,7 +197,8 @@ class RAEncoder(Encoder):
mapper.valuation(n, r) == v
),
z3.If(
ra.guard(mapper.map(n), l, r) == True,
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),
)
......@@ -216,64 +210,3 @@ class RAEncoder(Encoder):
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)] = RAEncoder.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 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],
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