Commit 158e9d26 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Removed unused scraps. Will continue tomorrow.

parent 074777c0
# Encoding of Frits' first suggestion
import collections
import z3
# states
n = 3
State = z3.Datatype('State')
for i in range(n):
State.declare('state{0}'.format(i))
State = State.create()
state = z3.Const('state', State)
# registers
k = 1
Register = z3.Datatype('Register')
Register.declare('fresh')
for i in range(1, k+1):
Register.declare('register{0}'.format(i))
Register = Register.create()
registers = [Register.fresh, Register.register1]
register = z3.Const('register', Register)
fresh = Register.fresh
print(registers)
# inputs
Value = z3.DeclareSort('Value')
val = z3.Const('val', Value)
other = z3.Const('other', Value)
RegisterAutomaton = collections.namedtuple('RegisterAutomaton', 'start transition output registers set select store')
ra = RegisterAutomaton(start=z3.Const('start', State),
transition=z3.Function('transition', State, Value, State),
output=z3.Function('output', State, z3.BoolSort()),
registers=registers,
set=z3.Function('set', State, Register, z3.BoolSort()),
select=z3.Function('select', State, Value, Register),
store=z3.Function('store', State, Value, Register))
axioms = [z3.ForAll([register],
z3.Implies(register != fresh, ra.set(ra.start, register) == False)),
z3.ForAll([state, val],
z3.And([
z3.And(
# a (non-fresh) guard on transition implies that it is set in the source
z3.Implies(ra.select(state, val) == register,
ra.set(state, register) == True),
# an update of a (non-perp) register on a transition implies
# that there is no guard on that register on that transition
z3.Implies(ra.store(state, val) == register,
ra.select(state, val) == fresh),
# if a register is updated is must be used
z3.Implies(ra.store(state, val) == register,
ra.set(ra.transition(state, val), register) == True),
# If a variable is used after a transition, then it was either used before the transition,
# or it stores the parameter carried by the transition
z3.Implies(ra.set(ra.transition(state, val), register) == True,
z3.Or(ra.set(state, register) == True,
z3.And(ra.select(state, val) == fresh,
ra.store(state, val) == register))))
# Explictly adding that we can not update registers that are already set
# -> Is this a logical consequence of the other axioms?
#z3.Implies(ra.store(state, val) == register,
# ra.set(state, register) == False))
for register in registers[1:]]),
patterns = [ra.transition(state, val)]),
z3.ForAll([state, val, other],
z3.Implies(z3.And([val != other, ra.transition(state, val) != ra.transition(state, other)]),
ra.select(state, val) != ra.select(state, other)))]
def _state(aut, access):
if not access:
return aut.start
return aut.transition(_state(aut, access[:-1]), access[-1])
def canonical(seq):
values = {}
i = 0
for input in seq:
if input not in values:
values[input] = z3.Const('val{0}'.format(i), Value)
i = i + 1
return [values[input] for input in seq]
constraints = [ra.output(_state(ra, canonical('11'))) == True,
ra.output(_state(ra, canonical('10'))) == False,
ra.output(_state(ra, canonical('110'))) == False,
ra.output(_state(ra, canonical('111'))) == True,
ra.output(_state(ra, canonical('11101'))) == True,
ra.output(_state(ra, canonical('111011'))) == True,
# bijection
ra.output(_state(ra, canonical('00'))) == True,
ra.output(_state(ra, canonical('88555'))) == True,
z3.Distinct([z3.Const('val{0}'.format(i), Value) for i in range(2)])
]
solver = z3.Solver()
solver.add(axioms + constraints)
#solver.add(axioms) # Useful if we want to see if additional axioms are a logical consequence of the ones we have
if solver.check() == z3.sat:
model = solver.model()
print(model)
print()
# Proof that we do not update registers that are already set.
eval = model.evaluate(z3.Implies(ra.store(state, val) == register, ra.set(state, register) == False))
print(eval)
else:
print(solver.unsat_core())
print(z3.simplify(z3.And(axioms + constraints)))
# Improved encoding
import collections
import itertools
import z3
num_locations = 3
num_labels = 1
num_registers = 1
def enum(type, names):
dt = z3.Datatype(type)
for name in names:
dt.declare(name)
dt = dt.create()
fields = [dt.__getattribute__(name) for name in names]
return (dt, fields)
Location, locations = enum('Location', ['location{0}'.format(i) for i in range(num_locations)])
Label, labels = enum('Label', ['label{0}'.format(i) for i in range(num_labels)])
Register, registers = enum('Register', ['register{0}'.format(i) for i in range(num_registers)] + ['fresh'])
Value = z3.DeclareSort('Value')
Node = z3.DeclareSort('Node')
RegisterAutomaton = collections.namedtuple('RegisterAutomaton',
'start transition output used update')
def register_automaton(Location, Label, Register, start):
return RegisterAutomaton(start = start,
transition = z3.Function('transition', Location, Label, Register, Location),
output = z3.Function('output', Location, z3.BoolSort()),
used = z3.Function('used', Location, Register, z3.BoolSort()),
update = z3.Function('update', Location, Label, Register))
Mapper = collections.namedtuple('Mapper',
'map valuation')
def mapper(Node, Location, Value, Register):
return Mapper(map = z3.Function('map', Node, Location),
valuation = z3.Function('valuation', Node, Register, Value))
ra = register_automaton(Location, Label, Register, locations[0])
m = mapper(Node, Location, Value, Register)
q = z3.Const('q', Location)
l = z3.Const('l', Label)
r = z3.Const('r', Register)
rp = z3.Const('rp', Register)
fresh = registers[-1]
# Register automaton axioms
ra_axioms = [
# Updating a non-fresh register for a label in a location,
# means that the register is used in any location reached from this location with a fresh guard.
z3.ForAll([q, l, r],
z3.Implies(z3.And(ra.update(q, l) == r, r != fresh),
ra.used(ra.transition(q, l, fresh), r) == True)),
# If a non-fresh register is used in a state,
# it was either used in the previous state,
# or it was updated on the previous transition.
z3.ForAll([q, l, r, rp],
z3.Implies(ra.used(ra.transition(q, l, rp), r) == True,
z3.Or(ra.used(q, r) == True,
z3.And(ra.update(q, l) == r,
rp == fresh)))),
# None of the registers are in use in the start state.
z3.ForAll([r],
ra.used(ra.start, r) == False)
]
n = z3.Const('n', Node)
np = z3.Const('np', Node)
v = z3.Const('v', Value)
# Mapper axioms
m_axioms = [
# If we update a register on a transition from a state,
# then the register is assigned the value.
# Else, the register keeps its previous value.
z3.ForAll([n, np, r, v, l],
z3.If(z3.And(ra.transition(m.map(n), l, r) == m.map(np),
ra.update(m.map(n), l) == r),
m.valuation(np, r) == v,
m.valuation(np, r) == m.valuation(n, r))),
# If there is a transition from a state, label and (non-fresh) register,
# then the valuation of that register should be kept.
z3.ForAll([n, np, l, r, v],
z3.Implies(z3.And(ra.transition(m.map(n), l, r) == m.map(np),
r != fresh),
m.valuation(np, r) == m.valuation(n, r)))
]
Action = collections.namedtuple('Action',
'label value')
def determinize(seq):
neat = {}
i = 0
for action in seq:
if action.value not in neat:
neat[action.value] = z3.Const('val{0}'.format(i), Value)
i = i + 1
return [Action(action.label, neat[action.value]) for action in seq]
# Trie data structure
class Trie(object):
def __init__(self, counter):
self.id = next(counter)
self.node = z3.Const('node{0}'.format(self.id), Node)
self.counter = counter
self.children = {}
def __getitem__(self, seq):
seq = determinize(seq)
trie = self
for action in seq:
if action not in trie.children:
trie.children[action] = Trie(self.counter)
trie = trie.children[action]
return trie
def __iter__(self):
yield self
for child in itertools.chain(*map(iter, self.children.values())):
yield child
def transitions(self):
for node in self:
for action in node.children:
yield node, action, node.children[action]
trie = Trie(itertools.count(0))
label = labels[0]
act = lambda x: Action(label, x)
# Define data
data = [([act(5), act(5)], True),
([act(6), act(6)], True),
([act(1), act(7)], False),
([act(9)], True),
([act(1), act(2), act(2), act(6), act(9), act(9)], True),
]
# Add output constraints for data
output_constraints = []
for seq, accept in data:
node = trie[seq]
output_constraints.append(ra.output(m.map(node.node)) == accept)
# Add transition constraints for all transitions in trie
transition_constraints = [ra.start == m.map(trie.node)]
for n, a, c in trie.transitions():
transition_constraints.append(z3.Exists([r], ra.transition(m.map(n.node), a.label, r) == m.map(c.node)))
# Create an empty value and assert that all (neat) values are different
init = z3.Const('init', Value)
values = {init}
for n, a, c in trie.transitions():
values.add(a.value)
value_constraints = [z3.Distinct(list(values)),
#z3.ForAll([r],
# z3.Implies(r != fresh,
# m.valuation(trie.node, r) == init)),
]
s = z3.Solver()
s.add(ra_axioms)
s.add(m_axioms)
s.add(transition_constraints)
s.add(output_constraints)
s.add(value_constraints)
print(s.check())
model = s.model()
print(model)
for seq, accept in data:
print(model.eval(ra.output(m.map(trie[seq].node)) == accept))
for n in trie:
print('{0} maps to {1}'.format(n.node, model.eval(m.map(n.node))))
# Improved encoding
import collections
import itertools
import z3
num_locations = 2
num_labels = 1
num_registers = 1
def enum(type, names):
dt = z3.Datatype(type)
for name in names:
dt.declare(name)
dt = dt.create()
fields = [dt.__getattribute__(name) for name in names]
return (dt, fields)
Location, locations = enum('Location', ['location{0}'.format(i) for i in range(num_locations)])
Label, labels = enum('Label', ['label{0}'.format(i) for i in range(num_labels)])
Register, registers = enum('Register', ['register{0}'.format(i) for i in range(num_registers)] + ['perp'])
perp = registers[-1]
Value = z3.DeclareSort('Value')
Node = z3.DeclareSort('Node')
RegisterAutomaton = collections.namedtuple('RegisterAutomaton',
'start transition output guard update')
def register_automaton(Location, Label, Register, start):
return RegisterAutomaton(start = start,
# For r != perp, transition(q, l, r) only makes sense if guard(q, l, r) == true.
# In this case there is a transition q -- l(v), v==r -> transition(q, l, r),
# Otherwise, use q -- l(v), perp -> transition(q, l, perp).
transition = z3.Function('transition', Location, Label, Register, Location),
# If there is an l such that guard(q, l, r) == True, then used(q, r) == true.
guard=z3.Function('guard', Location, Label, Register, z3.BoolSort()),
# TODO: does used still make sense if we have guard?
# TODO: does used make sense at all?
# Since we can't lose registers, there will never be transitions (back) to states that use less registers
# Can't we just assume all registers are used all the time, but sometimes we don't care what's in them?
#used = z3.Function('used', Location, Register, z3.BoolSort()),
# !!!! if update(q, l) = r, then (for all r', r'!= fresh -> guard(q, l, r') == False)
update = z3.Function('update', Location, Label, Register),
output=z3.Function('output', Location, z3.BoolSort()),
)
Mapper = collections.namedtuple('Mapper',
'map valuation')
def mapper(Node, Location, Value, Register):
return Mapper(map = z3.Function('map', Node, Location),
valuation = z3.Function('valuation', Node, Register, Value))
Action = collections.namedtuple('Action',
'label value')
label = labels[0]
act = lambda x: Action(label, x)
def determinize(seq):
neat = {}
i = 0
for action in seq:
if action.value not in neat:
neat[action.value] = z3.Const('val{0}'.format(i), Value)
i = i + 1
return [Action(action.label, neat[action.value]) for action in seq]
# Trie data structure
class Trie(object):
def __init__(self, counter):
self.id = next(counter)
self.node = z3.Const('node{0}'.format(self.id), Node)
self.counter = counter
self.children = {}
def __getitem__(self, seq):
seq = determinize(seq)
trie = self
for action in seq:
if action not in trie.children:
trie.children[action] = Trie(self.counter)
trie = trie.children[action]
return trie
def __iter__(self):
yield self
for child in itertools.chain(*map(iter, self.children.values())):
yield child
def transitions(self):
for node in self:
for action in node.children:
yield node, action, node.children[action]
trie = Trie(itertools.count(0))
ra = register_automaton(Location, Label, Register, locations[0])
m = mapper(Node, Location, Value, Register)
q = z3.Const('q', Location)
l = z3.Const('l', Label)
r = z3.Const('r', Register)
rp = z3.Const('rp', Register)
n = z3.Const('n', Node)
np = z3.Const('np', Node)
v = z3.Const('v', Value)
init = z3.Const('init', Value)
root = trie.node
# Axioms
axioms = [
# if update(q, l) = r, then (for all r', r'!= perp -> guard(q, l, r') == False)
# q -- l(p) r := p -> q' then q -- l(p) r == p -> q'' if q' != q'' is problematic
z3.ForAll([q, l, r],
z3.Implies(ra.update(q, l) == r,
z3.ForAll([rp],
z3.Implies(rp != perp,
ra.guard(q, l, rp) == False # THIS IS WRONG, WE ALSO NEED VALUATION
)
)
)
),
# If we update a non-fresh register on a transition from a state,
# then the register is assigned the value.
# Else, the register keeps its previous value.
z3.ForAll([n, np, r, v, l],
z3.Implies(ra.transition(m.map(n), l, r) == m.map(np),
z3.If(r != perp,
z3.Implies(m.valuation(np, r) != m.valuation(n, r),
ra.update(m.map(n), l) == r),
m.valuation(np, r) == m.valuation(n, r)
)
)
),
# In the start state of the mapper,
# all registers contain a value outside the domain of plausible values.
z3.ForAll([r],
z3.Implies(r != perp,
m.valuation(root, r) == init)
),
]
# Define data
# Data for M1
data_m1 = [([act(5), act(5)], True),
([act(6), act(6)], True),
([act(1), act(7)], False),
([act(9)], True),
([act(8), act(4)], False),
([act(8), act(2), act(2)], True),
([act(4), act(3), act(3), act(1)], False),
([act(0), act(1), act(1), act(6), act(4)], True),
([act(1), act(2), act(2), act(6), act(9), act(9)], True),
]
data_m2 = [
([act(1)], True),
([act(1), act(2)], False),
([act(1), act(2), act(1)], True),
([act(1), act(2), act(3)], False),
([act(1), act(2), act(1), act(1)], False),
]
data = data_m2
# Add output constraints for data
output_constraints = []
for seq, accept in data:
node = trie[seq]
output_constraints.append(ra.output(m.map(node.node)) == accept)
# Add transition constraints for all transitions in trie
transition_constraints = [ra.start == m.map(trie.node)]
for n, a, c in trie.transitions():
transition_constraints.append(z3.Exists([r], ra.transition(m.map(n.node), a.label, r) == m.map(c.node)))
# Create an empty value and assert that all (neat) values are different
values = {init}
for n, a, c in trie.transitions():
values.add(a.value)
distinct_values = z3.Distinct(list(values))
s = z3.Solver()
s.add(axioms)
s.add(transition_constraints)
s.add(output_constraints)
s.add(distinct_values)
print(s.check())
model = s.model()
print(model)
for seq, accept in data:
print(model.eval(ra.output(m.map(trie[seq].node)) == accept))
for n in trie:
print('{0} maps to {1}'.format(n.node, model.eval(m.map(n.node))))
# WORKING! encoding
import collections
import itertools
import z3
num_locations = 4
num_registers = 2
def enum(type, names):
dt = z3.Datatype(type)
for name in names:
dt.declare(name)
dt = dt.create()
fields = [dt.__getattribute__(name) for name in names]
return (dt, fields)
Location, locations = enum('Location', ['location{0}'.format(i) for i in range(num_locations)])
Register, registers = enum('Register', ['register{0}'.format(i) for i in range(num_registers)] + ['fresh'])
fresh = registers[-1]
Value = z3.DeclareSort('Value')
Node = z3.DeclareSort('Node')
RegisterAutomaton = collections.namedtuple('RegisterAutomaton',
'start transition output guard update')
def register_automaton(Location, Register, start):
return RegisterAutomaton(start = start,
# For r != fresh, transition(q, l, r) only makes sense if guard(q, l, r) == true.
# In this case there is a transition q -- l(v), v==r -> transition(q, l, r),
# Otherwise, use q -- l(v), fresh -> transition(q, l, fresh).
transition = z3.Function('transition', Location, Register, Location),
guard=z3.Function('guard', Location, Register, z3.BoolSort()),
update = z3.Function('update', Location, Register, Register),
output=z3.Function('output', Location, z3.BoolSort()),
)
Mapper = collections.namedtuple('Mapper',
'map val')
def mapper(Node, Location, Value, Register):
return Mapper(map = z3.Function('map', Node, Location),
val = z3.Function('valuation', Node, Register, Value))
Action = collections.namedtuple('Action',
'value')
act = lambda x: Action(x)
def determinize(seq):
neat = {}
i = 0
for action in seq:
if action.value not in neat:
neat[action.value] = z3.Const('val{0}'.format(i), Value)
i = i + 1
return [Action(neat[action.value]) for action in seq]
# Trie data structure
class Trie(object):
def __init__(self, counter):
self.id = next(counter)
self.node = z3.Const('node{0}'.format(self.id), Node)
self.counter = counter
self.children = {}
def __getitem__(self, seq):
seq = determinize(seq)
trie = self
for action in seq:
if action not in trie.children:
trie.children[action] = Trie(self.counter)
trie = trie.children[action]
return trie