Commit 9a3a6ca6 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Added untested IORA builder.

parent 306cd786
......@@ -64,7 +64,6 @@ class Mapper(object):
def element(self, name):
return z3.Const("n"+str(name), self.Element)
class RegisterAutomatonBuilder(object):
"""
Builder class that construct a register automaton out of a model definition.
......@@ -98,27 +97,107 @@ class RegisterAutomatonBuilder(object):
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]
used_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)
self._add_transition(translator, mut_ra, z3state, z3label,
[self.ra.fresh], update, z3end_state, used_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)
self._add_transition(translator, mut_ra, z3state, z3label,
z3guards, None, z3end_state, used_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)
def _add_transition(self, translator, mut_ra, z3start_state, z3label, z3guards, z3update, z3end_state, used_z3regs):
start_state = translator.z3_to_state(z3start_state)
guard = translator.z3_to_guard(z3guards, used_z3regs)
asg = translator.z3_to_assignment(z3update)
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 IORegisterAutomatonBuilder(object):
"""
Builder class that construct a register automaton out of a model definition.
"""
def __init__(self, ra : IORegisterAutomaton):
super().__init__()
self.ra = ra
def build_ra(self, model, input_labels, output_labels):
mut_ra = MutableIORegisterAutomaton()
translator = Translator(self.ra)
z3input_states = [z3state for z3state in self.ra.locations if
translator.z3_to_bool(model.eval(self.ra.loctype(z3state)))]
for z3state in z3input_states:
self._add_state(translator, mut_ra, z3state)
for z3label in input_labels:
self._add_transitions(model, translator, mut_ra, z3state, z3label, output_labels)
return mut_ra.to_immutable()
def _add_state(self, translator, mut_ra, z3state):
mut_ra.add_state(translator.z3_to_state(z3state))
def _add_transitions(self, model, translator, mut_ra, z3state, z3label, z3output_labels):
z3end_state_to_guards = dict()
enabled_z3guards = [guard for guard in self.ra.registers if
translator.z3_to_bool(model.eval(self.ra.used(z3state, guard))) or
guard is self.ra.fresh]
for z3guard in enabled_z3guards:
z3out_state = model.eval(self.ra.transition(z3state, z3label, z3guard))
if z3out_state not in z3end_state_to_guards:
z3end_state_to_guards[z3out_state] = []
z3end_state_to_guards[z3out_state].append(z3guard)
update = model.eval(self.ra.update(z3state, z3label))
used_z3regs = [reg for reg in enabled_z3guards if reg is not self.ra.fresh]
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 update is not self.ra.fresh:
self._add_transition(translator, mut_ra, z3state, z3label,
[self.ra.fresh], update, z3out_state,
z3output_labels, used_z3regs)
z3guards.remove(self.ra.fresh)
if len(z3guards) > 0:
self._add_transition(model, translator, mut_ra, z3state, z3label,
z3guards, None, z3out_state,
z3output_labels, used_z3regs)
def _add_transition(self, model, translator, mut_ra, z3start_state, z3label,
z3disjguards, z3input_update, z3out_state, output_labels, used_z3regs):
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]
active_z3action = [(output_label, guard) for output_label in output_labels for guard in enabled_z3guards
if model.eval(self.ra.transition(z3out_state, output_label, guard)) is not self.ra.sink]
if len(active_z3action) != 1:
raise Exception("Exactly one transition should not lead to sink state")
(z3output_label, z3output_guard) = active_z3action[0]
z3end_state = model.eval(self.ra.transitions(z3output_label, z3output_guard))
z3output_update = model.eval(self.ra.update(z3out_state))
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),
translator.z3_to_assignment(z3output_update),
translator.z3_to_state(z3end_state),
)
mut_ra.add_transition(z3start_state, transition)
class Translator(object):
"""Provides translation from z3 constants to RA elements. """
def __init__(self, ra):
......@@ -145,6 +224,12 @@ class Translator(object):
else:
return OrGuard(equ_guards)
def z3_to_mapping(self, z3guard):
if z3guard is self.ra.fresh:
return Fresh(0)
else:
return self.z3_to_register(z3guard)
def z3_to_bool(self, z3bool):
return str(z3bool) == "True"
......
......@@ -51,18 +51,15 @@ class Automaton(metaclass=ABCMeta):
return str_rep
class MutableAutomaton(Automaton):
def __init__(self):
super().__init__([], dict())
class MutableAutomatonMixin(metaclass=ABCMeta):
def add_state(self, state):
if state not in super()._states:
super()._states.append(state)
if state not in self._states:
self._states.append(state)
def add_transition(self, state, transition):
if state not in super()._state_to_trans:
super()._state_to_trans[state] = []
super()._state_to_trans[state].append(transition)
if state not in self._state_to_trans:
self._state_to_trans[state] = []
self._state_to_trans[state].append(transition)
@abstractmethod
def to_immutable(self) -> Automaton:
......@@ -94,6 +91,13 @@ class Acceptor(Automaton, metaclass=ABCMeta):
def __str__(self):
return str(self._state_to_acc) + "\n" + super().__str__()
class MutableAcceptorMixin(MutableAutomatonMixin, metaclass=ABCMeta):
def add_state(self, state, accepts):
super().add_state(state)
self._state_to_acc[state] = accepts
"""The most basic transition class available"""
class Transition():
def __init__(self, start_state, start_label, end_state):
......
from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired, Transducer
from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired, Transducer, \
MutableAcceptorMixin, MutableAutomatonMixin
from abc import ABCMeta, abstractmethod
import itertools
import collections
......@@ -131,8 +132,8 @@ class RegisterAutomaton(Acceptor, RegisterMachine):
class IORegisterAutomaton(Transducer, RegisterMachine):
def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
super().__init__(locations, loc_to_trans, loc_to_acc)
def __init__(self, locations, loc_to_trans, registers):
super().__init__(locations, loc_to_trans)
self._registers = registers
def registers(self) -> List[Register]:
......@@ -179,20 +180,12 @@ class IORegisterAutomaton(Transducer, RegisterMachine):
output = fired_transition.output(valuation, values)
return output
class MutableRegisterAutomaton(RegisterAutomaton):
class MutableRegisterAutomaton(RegisterAutomaton, MutableAcceptorMixin):
def __init__(self):
super().__init__([], dict(), dict(), [])
def add_state(self, state, accepts):
if state not in self._states:
self._states.append(state)
self._state_to_acc[state] = accepts
def add_transition(self, state, transition):
if state not in self._state_to_trans:
self._state_to_trans[state]=[]
self._state_to_trans[state].append(transition)
def add_transition(self, state:str, transition:RATransition):
super().add_transition(state, transition)
for reg in transition.guard.registers():
if reg not in self._registers:
self._registers.append(reg)
......@@ -200,6 +193,20 @@ class MutableRegisterAutomaton(RegisterAutomaton):
def to_immutable(self) -> RegisterAutomaton:
return RegisterAutomaton(self._states, self._state_to_acc, self._state_to_trans, self._registers)
class MutableIORegisterAutomaton(IORegisterAutomaton, MutableAutomatonMixin):
def __init__(self):
super().__init__([], dict(), [])
def add_transition(self, state:str, transition:IORATransition):
super().add_transition(state, transition)
for reg in transition.guard.registers():
if reg not in self._registers:
self._registers.append(reg)
def to_immutable(self):
return IORegisterAutomaton(self._states, self._state_to_trans, self._registers)
class Guard(metaclass=ABCMeta):
"""A guard with is_satisfied implements a predicate over the current register valuation and the parameter value. """
def __init__(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