Commit 306cd786 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Added IO models. Will need to add export.

parent 9dfe83c9
......@@ -51,6 +51,22 @@ class Automaton(metaclass=ABCMeta):
return str_rep
class MutableAutomaton(Automaton):
def __init__(self):
super().__init__([], dict())
def add_state(self, state):
if state not in super()._states:
super()._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)
@abstractmethod
def to_immutable(self) -> Automaton:
pass
"""An automaton model that generates output"""
class Transducer(Automaton, metaclass=ABCMeta):
......@@ -97,5 +113,4 @@ class NoTransitionFired(Exception):
"""Exception raised when several transitions can be fired in a deterministic machine"""
class MultipleTransitionsFired(Exception):
pass
pass
\ No newline at end of file
......@@ -62,5 +62,3 @@ class IOTransition(Transition):
super().__init__(start_state, start_label, end_state)
self.output = output
from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired
from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired, Transducer
from abc import ABCMeta, abstractmethod
import itertools
import collections
......@@ -6,7 +6,6 @@ from typing import List
Action = collections.namedtuple('Action', ('label', 'value'))
class RATransition(Transition):
def __init__(self, start_state, start_label, guard, assignment, end_state):
super().__init__(start_state, start_label, end_state)
......@@ -30,12 +29,23 @@ class RATransition(Transition):
return "{0}({1}) -> {2} {3}".format(self.start_label, self.guard,
self.assignment, self.end_state)
class SymbolicValue(metaclass=ABCMeta):
"""Symbolic values can be used to symbolically express registers, constants and parameters."""
def __init__(self, index):
super().__init__()
self.index = index
class Fresh(SymbolicValue):
def __init__(self, index):
super().__init__(index)
def __str__(self):
return "f" + str(self.index)
def __repr__(self):
return self.__str__()
class Register(SymbolicValue):
def __init__(self, index):
super().__init__(index)
......@@ -47,7 +57,50 @@ class Register(SymbolicValue):
return self.__str__()
class RegisterAutomaton(Acceptor):
class IORATransition(RATransition):
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
self.output_label = output_label
self.output_mapping = output_mapping
self.output_assignment =output_assignment
def output(self, valuation, values):
if type(self.output_mapping) == Fresh:
return Action(self.output_label, max(values) + 1)
else:
return Action(self.output_label, valuation[self.output_mapping])
def output_update(self, valuation, action):
return self.output_assignment.update(valuation, action.value)
def __str__(self, shortened=False):
trans_str = "{0}({1}) {2} {3} / {4}({5}) {6} {7}"\
.format(self.start_label, self.guard, self.assignment, self.output_label,\
self.output_mapping, self.output_mapping, self.end_state)
if not shortened:
trans_str = self.start_label + " " + trans_str
return trans_str
# some methods shared between the different register automatas
class RegisterMachine():
def _fired_transition(self, transitions, reg_val, action):
"""Retrieves the transition fired based on the action and valuation"""
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?)
if len(fired_transitions) == 0:
raise NoTransitionFired
if len(fired_transitions) > 1:
raise MultipleTransitionsFired
return fired_transitions[0]
class RegisterAutomaton(Acceptor, RegisterMachine):
def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
super().__init__(locations, loc_to_trans, loc_to_acc)
self._registers = registers
......@@ -68,17 +121,7 @@ class RegisterAutomaton(Acceptor):
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(reg_val, action)]
# the number of fired transitions can be more than one since we could have multiple equalities
# todo (merge into or guard?)
if len(fired_transitions) == 0:
raise NoTransitionFired
if len(fired_transitions) > 1:
raise MultipleTransitionsFired
fired_transition = fired_transitions[0]
fired_transition = super()._fired_transition(transitions, reg_val, action)
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)
......@@ -86,6 +129,56 @@ class RegisterAutomaton(Acceptor):
# print(tr_str)
return crt_state
class IORegisterAutomaton(Transducer, RegisterMachine):
def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
super().__init__(locations, loc_to_trans, loc_to_acc)
self._registers = registers
def registers(self) -> List[Register]:
return self._registers
def transitions(self, state: str, label:str = None) -> List[IORATransition]:
return super().transitions(state, label)
def state(self, trace: List[Action]) -> str:
(reached_state, valuation, values) = self._machine_state(trace)
return reached_state
def _machine_state(self, trace: List[Action]) -> (str, dict, set):
init = -1
# maintains the set of values encountered
values = set()
reg_val = dict()
for reg in self.registers():
reg_val[reg] = init
crt_state = self.start_state()
for action in trace:
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)
# the transition should give us the output action
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)
crt_state = fired_transition.end_state
return (crt_state, reg_val, values)
def output(self, trace: List[Action]) -> Action:
if len(trace) == 0:
return None
else:
(reached_state, valuation, values) = self._machine_state(trace[:-1])
action = trace[-1]
transitions = super().transitions(reached_state, action.label)
fired_transition = super()._fired_transition(transitions, valuation, action)
output = fired_transition.output(valuation, values)
return output
class MutableRegisterAutomaton(RegisterAutomaton):
def __init__(self):
super().__init__([], dict(), dict(), [])
......@@ -182,6 +275,7 @@ class FreshGuard(Guard):
all_deq = ["p!={0}".format(str(reg)) for reg in self._registers]
return " /\\ ".join(all_deq)
class Assignment(metaclass=ABCMeta):
"""An assignment updates the valuation of registers using the old valuation and the current 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