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

One of the test fails for the RA case. I don't think it's the exporter.

parent 6f7c6bac
......@@ -32,6 +32,7 @@ class RaLearnerTest(unittest.TestCase):
self.assertEqual(len(ra.locations), test_scenario.nr_locations,
"Wrong number of registers.")
exported = ra.export(model)
print(model)
print("Learned model: \n",exported)
self.assertEqual(len(exported.states()), test_scenario.nr_locations,
"Wrong number of locations in exported model. ")
......
......@@ -79,22 +79,23 @@ class RegisterAutomatonBuilder():
if z3end_state not in z3end_state_to_guards:
z3end_state_to_guards[z3end_state] = []
z3end_state_to_guards[z3end_state].append(z3guard)
print(enabled_z3guards)
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,
z3guards, update, z3end_state)
z3guards, 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)
z3guards, None, z3end_state, enabled_z3regs)
def _add_transition(self, translator, mut_ra, start_state, z3label, z3guards, z3asg, z3end_state):
guard = translator.z3_to_guard(z3guards)
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),
......@@ -108,20 +109,20 @@ class Translator():
self.ra = ra
def z3_to_assignment(self, z3asg):
if z3asg is None or z3asg == self.ra.fresh:
if (z3asg is None) or (z3asg == self.ra.fresh):
asg = NoAssignment()
else:
asg = RegisterAssignment(self.z3_to_register(z3asg))
return asg
def z3_to_guard(self, z3guards):
guard_regs = [self.z3_to_register(z3reg) for z3reg in z3guards if z3reg is not self.ra.fresh]
def z3_to_guard(self, z3guards, enabled_z3regs):
z3guard_regs = [z3reg for z3reg in z3guards if z3reg is not self.ra.fresh]
if self.ra.fresh in z3guards:
diff_from = [self.z3_to_register(z3reg) for z3reg in self.ra.registers
if z3reg not in guard_regs and z3reg is not self.ra.fresh]
diff_from = [self.z3_to_register(z3reg) for z3reg in enabled_z3regs
if z3reg not in z3guard_regs and z3reg is not self.ra.fresh]
return FreshGuard(diff_from)
else:
equ_guards = [EqualityGuard(guard_reg) for guard_reg in guard_regs]
equ_guards = [EqualityGuard(self.z3_to_register(guard_reg)) for guard_reg in z3guard_regs]
if len(equ_guards) == 1:
return equ_guards[0]
else:
......@@ -131,12 +132,14 @@ class Translator():
return str(z3bool) == "True"
def z3_to_state(self, z3state):
return str(z3state)
return "l"+str(self.ra.locations.index(z3state))
def z3_to_label(self, z3label):
return str(z3label)
def z3_to_register(self, z3register):
if str(z3register) == "fresh":
raise Exception
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))
......
......@@ -23,6 +23,7 @@ class Automaton(metaclass=ABCMeta):
def state(self, trace):
pass
# Basic __str__ function which works for most FSMs.
def __str__(self):
str_rep = ""
for state in self.states():
......@@ -56,6 +57,9 @@ class Acceptor(Automaton, metaclass=ABCMeta):
is_acc = self.is_accepting(state)
return is_acc
def __str__(self):
return str(self._state_to_acc) + "\n" + super().__str__()
"""The most basic transition class available"""
class Transition():
def __init__(self, start_state, start_label, end_state):
......
......@@ -13,13 +13,13 @@ class RATransition(Transition):
self.guard = guard
self.assignment = assignment
def is_enabled(self, action, valuation):
if action.label is self.start_label:
satisfied = self.guard.is_satisfied(action.value, valuation)
def is_enabled(self, valuation, action):
if action.label == self.start_label:
satisfied = self.guard.is_satisfied(valuation, action.value)
return satisfied
return False
def update(self, action, valuation):
def update(self, valuation, action):
return self.assignment.update(valuation, action.value)
def __str__(self, shortened = False):
......@@ -43,6 +43,9 @@ class Register(SymbolicValue):
def __str__(self):
return "r" + str(self.index)
def __repr__(self):
return self.__str__()
class RegisterAutomaton(Acceptor):
def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
......@@ -62,9 +65,10 @@ class RegisterAutomaton(Acceptor):
reg_val[reg] = init
crt_state = self.start_state()
tr_str = "({0}:{1})".format(crt_state, reg_val)
for action in trace:
transitions = self.transitions(crt_state, action.label)
fired_transitions = [trans for trans in transitions if trans.is_enabled(action, reg_val)]
fired_transitions = [trans for trans in transitions if trans.is_enabled(reg_val, action)]
# the number of fired transitions can be more than one since we could have multiple equalities
# todo (merge into or guard?)
......@@ -77,7 +81,9 @@ class RegisterAutomaton(Acceptor):
fired_transition = fired_transitions[0]
reg_val = fired_transition.update(reg_val, action)
crt_state = fired_transition.end_state
tr_str += " {0} ({1}:{2})".format(action, crt_state, reg_val)
# print(tr_str)
return crt_state
class MutableRegisterAutomaton(RegisterAutomaton):
......@@ -190,22 +196,22 @@ class Assignment(metaclass=ABCMeta):
class RegisterAssignment(Assignment):
def __init__(self, register):
super().__init__()
self.register = register
self._register = register
def update(self, valuation, value):
new_valuation = dict(valuation)
new_valuation[self.register] = value
new_valuation[self._register] = value
return new_valuation
def __str__(self):
return "{0}:=p".format(str(self.register))
return "{0}:=p".format(str(self._register))
class NoAssignment(Assignment):
def __init__(self):
super().__init__()
def update(self, valuation):
def update(self, valuation, value):
return dict(valuation)
def __str__(self):
......
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