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

Added FA models.

parent 9b3fd88d
......@@ -19,9 +19,27 @@ class Automaton(metaclass=ABCMeta):
else:
return list([trans for trans in self._state_to_trans[state] if trans.start_label == label])
@abstractmethod
def state(self, trace):
pass
"""state function which also provides a basic implementation"""
crt_state = self.start_state()
tr_str = crt_state
for symbol in trace:
transitions = self.transitions(crt_state, symbol)
fired_transitions = [trans for trans in transitions if trans.start_label == symbol]
# the number of fired transitions can be more than one since we could have multiple equalities
if len(fired_transitions) == 0:
raise NoTransitionFired
if len(fired_transitions) > 1:
raise MultipleTransitionsFired
fired_transition = fired_transitions[0]
crt_state = fired_transition.end_state
tr_str += " {0} {1}".format(symbol, crt_state)
# print(tr_str)
return crt_state
# Basic __str__ function which works for most FSMs.
def __str__(self):
......@@ -40,7 +58,7 @@ class Transducer(Automaton, metaclass=ABCMeta):
super().__init__(states, state_to_trans)
@abstractmethod
def outputs(self, trace):
def output(self, trace):
pass
"""An automaton model whose states are accepting/rejecting"""
......
from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired
from z3gi.model import Transition, Acceptor, Transducer, NoTransitionFired, MultipleTransitionsFired, Automaton
from abc import ABCMeta, abstractmethod
import itertools
import collections
......@@ -7,35 +7,60 @@ from typing import List
Symbol = str
State = str
Label = str
Output = str
class DFA(Acceptor):
def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
super().__init__(locations, loc_to_trans, loc_to_acc)
self._registers = registers
def __init__(self, states, state_to_trans, state_to_acc):
super().__init__(states, state_to_trans, state_to_acc)
def transitions(self, state: State, label:Label = None) -> List[Transition]:
return super().transitions(state, label)
def state(self, trace: List[Symbol]) -> State:
crt_state = super().state(trace)
# print(tr_str)
return crt_state
crt_state = self.start_state()
tr_str = crt_state
for symbol in trace:
transitions = self.transitions(crt_state, symbol)
fired_transitions = [trans for trans in transitions if trans.start_label == symbol]
class MooreMachine(Transducer):
def __init__(self, states, state_to_trans, state_to_out):
super().__init__(states, state_to_trans)
self.state_to_out = state_to_out
# the number of fired transitions can be more than one since we could have multiple equalities
if len(fired_transitions) == 0:
raise NoTransitionFired
def transitions(self, state: State, label:Label = None) -> List[Transition]:
return super().transitions(state, label)
if len(fired_transitions) > 1:
raise MultipleTransitionsFired
def state(self, trace: List[Symbol]) -> State:
crt_state = super().state(trace)
return crt_state
fired_transition = fired_transitions[0]
crt_state = fired_transition.end_state
tr_str += " {0} {1}".format(symbol, crt_state)
def output(self, trace: List[Symbol]) -> Output:
crt_state = self.state(trace)
return self.state_to_out[crt_state]
# print(tr_str)
class MealyMachine(Transducer):
def __init__(self, states, state_to_trans, state_to_out):
super().__init__(states, state_to_trans)
self.state_to_out = state_to_out
def transitions(self, state: State, label: Label = None) -> List[IOTransition]:
return super().transitions(state, label)
def state(self, trace: List[Symbol]) -> State:
crt_state = super().state(trace)
return crt_state
def output(self, trace: List[Symbol]) -> Output:
if len(trace) == 0:
return None
else:
state_before = self.state(trace[:-1])
trans = self.transitions(state_before, trace[-1])
return trans.output
class IOTransition(Transition):
def __init__(self, start_state, start_label, output, end_state):
super().__init__(start_state, start_label, end_state)
self.output = output
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