Commit 64f7b14f authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Some more updates. The setup works but scalability is a real issue.

parent 11813c0d
import itertools
from learn.algorithm import learn
from learn.ra import RALearner
from test import IORATest
from tests.iora_testscenario import *
from encode.iora import IORAEncoder
learner = RALearner(IORAEncoder())
test_type = IORATest
exp = sut_m5
(model, statistics) = learn(learner, test_type, exp.traces)
print(model)
print(statistics)
......@@ -30,8 +30,8 @@ def check_ra_against_obs(learner: RALearner, learned_ra:IORegisterAutomaton, m,
for i in range(1,2):
print("Experiment ",i)
learner = RALearner(labels, encoder=IORAEncoder(), verbose=True)
exp = sut_m5
learner = RALearner(IORAEncoder(), verbose=True)
exp = sut_m6
for trace in exp.traces:
learner.add(trace)
(_, ra, m) = learner._learn_model(exp.nr_locations-1,exp.nr_locations+1,exp.nr_registers)
......@@ -39,6 +39,5 @@ for i in range(1,2):
model = ra.export(m)
print(model)
check_ra_against_obs(learner, model, m, exp)
to_dot(model, None)
else:
print("unsat")
\ No newline at end of file
......@@ -33,6 +33,7 @@ sut_m1 = RaTestScenario("Accept everything", [
2, 1
)
sut_m2 = RaTestScenario("OK first then always NOK", [
[io(0, 'in', 100, 'OK')],
[io(0, 'in', 100, 'OK'), io(0, 'in', 101, 'NOK')],
......@@ -118,3 +119,36 @@ sut_m5 = RaTestScenario("Login model", [
],
9, 1)
# login model (incomplete traces)
sut_m6 = RaTestScenario("Stack model", [
[io(0, 'put', None, 'OK') ],
[io(None, 'get', None, 'NOK') ],
[io(0, 'put', None, 'OK'), io(1, 'put', None, 'NOK') ],
[io(0, 'put', None, 'OK'), io(None, 'get', 0, 'oget') ],
[io(None, 'get', None, 'NOK'), io(0, 'put', None, 'OK')],
[io(None, 'get', None, 'NOK'), io(None, 'get', None, 'NOK')],
[io(0, 'put', None, 'OK'), io(None, 'get', 0, 'oget'), io(None, 'get', None, 'NOK') ],
[io(0, 'put', None, 'OK'), io(None, 'get', 0, 'oget'), io(1, 'put', None, 'OK') ],
[io(0, 'put', None, 'OK'), io(None, 'get', 0, 'oget'), io(None, 'get', None, 'NOK') ],
[io(0, 'put', None, 'OK') ],
], 6, 1)
sut_m7 = RaTestScenario("Accept everything. Return same output", [
[io(0, 'in', 0, 'OK')],
[io(0, 'in', 0, 'OK'), io(0, 'in', 0, 'OK')],
[io(0, 'in', 0, 'OK'), io(1, 'in', 1, 'OK')]
], 3, 1)
sut_m8 = RaTestScenario("Accept everything. None output", [
[io(0, 'in', None, 'OK')],
[io(0, 'in', None, 'OK'), io(0, 'in', None, 'OK')],
[io(0, 'in', None, 'OK'), io(1, 'in', None, 'OK')]
], 3, 1)
sut_m9 = RaTestScenario("Accept everything. None input", [
[io(None, 'in', 0, 'OK')],
[io(None, 'in', 0, 'OK'), io(None, 'in', 1, 'OK')],
], 3, 1)
\ No newline at end of file
......@@ -34,12 +34,13 @@ class RegisterAutomaton(RegisterMachine):
class IORegisterAutomaton(RegisterMachine):
def __init__(self, input_labels, output_labels, num_locations, num_registers):
def __init__(self, input_labels, output_labels, param_size, num_locations, num_registers):
super().__init__(num_locations, num_registers)
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.param_size = param_size
self.sink = self.locations[-1]
self.start = self.locations[0]
self.fresh = self.registers[-1]
......@@ -195,7 +196,7 @@ class IORegisterAutomatonBuilder(object):
update = model.eval(self.ra.update(z3state, z3label))
used_z3regs = [reg for reg in enabled_z3guards if reg is not self.ra.fresh]
print("For {0} we have the transitions \n {1}".format(z3state, z3end_state_to_guards))
#print("For {0} we have the transitions \n {1}".format(z3state, z3end_state_to_guards))
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 not translator.z3_to_bool(model.eval(update == self.ra.fresh)):
......@@ -214,25 +215,30 @@ class IORegisterAutomatonBuilder(object):
enabled_z3guards = [guard for guard in self.ra.registers if
translator.z3_to_bool(model.eval(self.ra.used(z3out_state, guard))) or
guard is self.ra.fresh]
#print("From ", z3out_state, " enabled ", enabled_z3guards, " labels ", output_labels)
active_z3action = [(output_label, guard) for output_label in output_labels for guard in enabled_z3guards
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. "
"From location {0} there are {1} transitions which lead to sink {2}"
.format(z3out_state, len(active_z3action), self.ra.sink))
"From location {0} there are {1} transitions which don't lead to sink {2}. \n"
"Namely: {3}"
"\n\n Model: {4}"
.format(z3out_state, len(active_z3action), self.ra.sink, enabled_z3guards, model))
(z3output_label, z3output_guard) = active_z3action[0]
z3end_state = model.eval(self.ra.transition(z3out_state, z3output_label, z3output_guard))
z3output_update = model.eval(self.ra.update(z3out_state, z3output_label))
output_mapping = None if self.ra.param_size[translator.z3_to_label(z3output_label)] == 0 \
else translator.z3_to_mapping(z3output_guard)
transition = IORATransition(translator.z3_to_state(z3start_state),
translator.z3_to_label(z3label),
translator.z3_to_guard(z3disjguards, used_z3regs),
translator.z3_to_assignment(z3input_update),
translator.z3_to_label(z3output_label),
translator.z3_to_mapping(z3output_guard),
output_mapping,
translator.z3_to_assignment(z3output_update),
translator.z3_to_state(z3end_state),
)
......
......@@ -4,6 +4,7 @@ import z3
from define.ra import IORegisterAutomaton, Mapper
from encode import Encoder
from sut import ActionSignature
from utils import Tree, determinize
......@@ -13,16 +14,26 @@ class IORAEncoder(Encoder):
self.values = set()
self.input_labels = set()
self.output_labels = set()
self.param_size = dict()
def add(self, trace):
seq = list(itertools.chain(*map(iter, trace)))
_ = self.tree[determinize(seq)]
self.values.update([action.value for action in seq])
self.input_labels.update([action.label for action in [i for (i, o) in trace]])
self.output_labels.update([action.label for action in [o for (i, o) in trace]])
self.input_labels.update([action.label for action in [i for (i, _) in trace]])
self.output_labels.update([action.label for action in [o for (_, o) in trace]])
for action in seq:
if action.label not in self.param_size:
self.param_size[action.label] = action.param_size()
else:
if self.param_size[action.label] != action.param_size():
raise Exception("It is not allowed to have actions with different param sizes."
"Problem action: "+str(action))
def build(self, num_locations, num_registers):
ra = IORegisterAutomaton(list(self.input_labels), list(self.output_labels), num_locations, num_registers)
ra = IORegisterAutomaton(list(self.input_labels), list(self.output_labels), self.param_size,
num_locations, num_registers)
mapper = Mapper(ra)
constraints = []
constraints.extend(self.axioms(ra, mapper))
......@@ -123,21 +134,50 @@ class IORAEncoder(Encoder):
ra.loctype(ra.start) == True,
# In output locations, there's only one transition possible
# z3.ForAll(
# [q, l, lp, r, rp],
# z3.Implies(
# z3.And(
# q != ra.sink,
# ra.loctype(q) == False,
# ra.transition(q, l, r) != ra.sink,
# z3.Or(
# r != rp,
# l != lp
# )
# ),
# z3.Or(
# ra.transition(q, lp, rp) == ra.sink,
# rp != ra.fresh
# )
# )
# ),
# more readable version
z3.ForAll(
[q, l, lp, r, rp],
[q],
z3.Implies(
z3.And(
q != ra.sink,
ra.loctype(q) == False,
ra.transition(q, l, r) != ra.sink,
z3.Or(
r != rp,
l != lp
)
),
z3.Or(
ra.transition(q, lp, rp) == ra.sink,
rp != ra.fresh
z3.And(
z3.Exists(
[r,l],
ra.transition(q, l, r) != ra.sink,
),
z3.ForAll(
[r, l, rp,lp],
z3.Implies(
z3.And(
ra.transition(q, l, r) != ra.sink,
z3.Or(
rp != r,
lp != l,
)
),
ra.transition(q, lp, rp) == ra.sink
)
)
)
)
),
......@@ -207,7 +247,7 @@ class IORAEncoder(Encoder):
for node, (label, value), child in self.tree.transitions():
n = mapper.element(node.id)
l = ra.labels[label]
v = mapper.value(value)
v = mapper.value(value) if value is not None else None
c = mapper.element(child.id)
r, rp = z3.Consts('r rp', ra.Register)
......@@ -249,10 +289,12 @@ class IORAEncoder(Encoder):
)
),
])
if value is not None:
# If a non-fresh register is updated, and c and n are connected by fresh,
# then the register contains the value
# else the valuation is maintained.
z3.ForAll(
constraints.append(z3.ForAll(
[r],
z3.If(
z3.And(
......@@ -263,11 +305,20 @@ class IORAEncoder(Encoder):
mapper.valuation(c, r) == v,
mapper.valuation(c, r) == mapper.valuation(n, r)
)
),
])
))
else:
constraints.append(
z3.ForAll(
[r],
z3.And(
mapper.valuation(c, r) == mapper.valuation(n, r),
ra.update(mapper.map(n), l) == ra.fresh,
)
)
)
# Map to the right transition
path = [v for (l, v) in node.path()]
path = [v for (_, v) in node.path() if v is not None]
if value in path:
if label in self.input_labels:
constraints.append(
......@@ -296,12 +347,13 @@ class IORAEncoder(Encoder):
)
elif label in self.output_labels:
constraints.append(
z3.Exists(
[r],
z3.And(
r != ra.fresh,
mapper.valuation(n, r) == v
mapper.valuation(n, r) == v,
ra.used(mapper.map(n), r) == True, # this proved necessary
ra.transition(mapper.map(n), l, r) == mapper.map(c)
)
)
)
......@@ -309,11 +361,18 @@ class IORAEncoder(Encoder):
raise Exception("We did something wrong")
else:
constraints.append(
ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c)
)
values.add(v)
constraints.append(
ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c)
)
if value is None and label in self.input_labels:
constraints.append(
z3.ForAll(
[r],
ra.transition(mapper.map(n), l, r) == mapper.map(c)
)
)
if v is not None:
values.add(v)
constraints.append(z3.Distinct(list(values)))
return constraints
......@@ -41,6 +41,7 @@ def learn(learner:Learner, test_type:type, traces: List[object]) -> Tuple[Automa
statistics.add_inputs(test.size())
done = False
model = None
learn_traces = [test.trace]
while not done:
(model, definition) = learner.model(old_definition=definition)
done = True
......@@ -48,6 +49,11 @@ def learn(learner:Learner, test_type:type, traces: List[object]) -> Tuple[Automa
test = cast(TestTemplate, test_type(trace))
ce = test.check(model)
if ce is not None:
if ce not in learn_traces:
learn_traces.append(ce)
else:
raise Exception("The CE {0} has already been processed yet it "
"is still a CE. \n CEs: {1} \n Model: {2}".format(ce, learn_traces, model))
learner.add(ce)
statistics.add_tests(1)
statistics.add_inputs(test.size())
......
from encode.iora import IORAEncoder
from learn.algorithm import learn
from learn.ra import RALearner
from sut.stack import new_stack_sut
from sut.fifoset import new_fifoset_sut
from test import IORATest
from test.generation import ExhaustiveRAGenerator
# stack_sut = new_stack_sut(2)
# gen = ExhaustiveRAGenerator(stack_sut)
# obs = gen.generate_observations(4, max_registers=2)
# print("\n".join( [str(obs) for obs in obs]))
# learner = RALearner(IORAEncoder())
# (model, stats) = learn(learner, IORATest, obs)
# print(model, "\n \n", stats)
set_sut = new_fifoset_sut(2)
gen = ExhaustiveRAGenerator(set_sut)
obs = gen.generate_observations(4, max_registers=2)
print("\n".join( [str(obs) for obs in obs]))
learner = RALearner(IORAEncoder())
(model, stats) = learn(learner, IORATest, obs)
print(model, "\n \n", stats)
\ No newline at end of file
......@@ -5,7 +5,9 @@ import itertools
import collections
from typing import List
Action = collections.namedtuple('Action', ('label', 'value'))
class Action(collections.namedtuple('Action', ('label', 'value'))):
def param_size(self):
return 0 if self.value is None else 1
class RATransition(Transition):
def __init__(self, start_state, start_label, guard, assignment, end_state):
......@@ -60,7 +62,8 @@ class Register(SymbolicValue):
class IORATransition(RATransition):
def __init__(self, start_state, start_label, guard, assignment, output_label, output_mapping, output_assignment, end_state):
def __init__(self, start_state, start_label, guard, assignment, output_label,
output_mapping, output_assignment, end_state):
super().__init__(start_state, start_label, guard, assignment, end_state)
self.guard = guard
self.assignment = assignment
......@@ -69,7 +72,10 @@ class IORATransition(RATransition):
self.output_assignment =output_assignment
def output(self, valuation, values):
if type(self.output_mapping) == Fresh:
"""if the output mapping is None, it means that the output was parameter-less"""
if self.output_mapping is None:
return Action(self.output_label, None)
elif type(self.output_mapping) == Fresh:
return Action(self.output_label, max(values) + 1 if len(values) > 0 else 0)
else:
return Action(self.output_label, valuation[self.output_mapping])
......@@ -135,8 +141,9 @@ class RegisterAutomaton(Acceptor, RegisterMachine):
class IORegisterAutomaton(Transducer, RegisterMachine):
def __init__(self, locations, loc_to_trans, registers):
super().__init__(locations, loc_to_trans)
self._registers = registers
super().__init__(locations, loc_to_trans)
self._registers = registers
def registers(self) -> List[Register]:
return self._registers
......@@ -158,7 +165,8 @@ class IORegisterAutomaton(Transducer, RegisterMachine):
crt_state = self.start_state()
for action in trace:
values.add(action.value)
if action.value is not None:
values.add(action.value)
transitions = self.transitions(crt_state, action.label)
fired_transition = super()._fired_transition(transitions, reg_val, action)
reg_val = fired_transition.update(reg_val, action)
......@@ -167,7 +175,8 @@ class IORegisterAutomaton(Transducer, RegisterMachine):
output_action = fired_transition.output(reg_val, values)
# based on this output, the transition should update the set of registers
reg_val = fired_transition.output_update(reg_val, output_action)
values.add(output_action.value)
if output_action.value is not None:
values.add(output_action.value)
crt_state = fired_transition.end_state
return (crt_state, reg_val, values)
......@@ -180,7 +189,9 @@ class IORegisterAutomaton(Transducer, RegisterMachine):
action = trace[-1]
transitions = super().transitions(reached_state, action.label)
fired_transition = super()._fired_transition(transitions, valuation, action)
values.add(action.value)
valuation = fired_transition.update(valuation, action)
if action.value is not None:
values.add(action.value)
output = fired_transition.output(valuation, values)
return output
......
from sut import SUT, ObjectSUT, ActionSignature
class FIFOSet():
INTERFACE = [ActionSignature("get", 0), ActionSignature("put", 1)]
def __init__(self, size):
super()
self.size = size
self.list = list()
def get(self):
if len(self.list) == 0:
return SUT.NOK
else:
return ("OGET", self.list.pop(len(self.list)-1))
def put(self, val):
if len(self.list) < self.size and val not in self.list:
self.list.append(val)
return SUT.OK
else:
return SUT.NOK
def new_fifoset_sut(size):
return ObjectSUT(FIFOSet.INTERFACE, lambda : FIFOSet(size))
......@@ -82,6 +82,7 @@ class IORATest(TestTemplate):
return test_trace
output = model.output([inp for (inp, _) in test_trace])
if output != out_act:
# print("Expected: ", out_act, " Got: ", output, "\n Trace: ", trace)
return test_trace
return None
......
......@@ -5,15 +5,7 @@ from encode.iora import IORAEncoder
from learn.algorithm import learn
from learn.ra import RALearner
from model.ra import Action
from sut import SUT, ActionSignature, RASUT
# class RAObservation():
# def __init__(self, trace):
# self.trace = trace
#
# def values(self):
# for
from sut import RASUT
from sut.stack import new_stack_sut
from test import IORATest
......@@ -61,11 +53,3 @@ class ExhaustiveRAGenerator(ObservationGeneration):
extended_obs = self._generate_observations(new_obs, crt_depth + 1, max_depth, max_values)
new_obs.extend(extended_obs)
return new_obs
stack_sut = new_stack_sut(1)
gen = ExhaustiveRAGenerator(stack_sut)
obs = gen.generate_observations(2)
print("\n".join( [str(obs) for obs in obs]))
learner = RALearner(IORAEncoder())
learn(learner, IORATest, obs)
......@@ -53,6 +53,7 @@ class Tree(object):
def determinize(seq):
neat = {}
neat[None] = None
i = 0
for (label, value) in seq:
if value not in neat:
......
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