Commit 486e4922 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Updated FA definitions

parent d5a13967
...@@ -4,6 +4,7 @@ from abc import ABCMeta, abstractmethod ...@@ -4,6 +4,7 @@ from abc import ABCMeta, abstractmethod
import z3 import z3
from define import enum, Automaton from define import enum, Automaton
import model.fa import model.fa
from model import Transition
class FSM(Automaton,metaclass=ABCMeta): class FSM(Automaton,metaclass=ABCMeta):
...@@ -20,10 +21,9 @@ class DFA(FSM): ...@@ -20,10 +21,9 @@ class DFA(FSM):
self.output = z3.Function('output', self.State, z3.BoolSort()) self.output = z3.Function('output', self.State, z3.BoolSort())
def export(self, model : z3.ModelRef) -> model.fa.DFA: def export(self, model : z3.ModelRef) -> model.fa.DFA:
pass builder = DFABuilder(self)
#builder = DFABuilder(self) dfa = builder.build_dfa(self)
#dfa = builder.build_dfa(self) return dfa
#return dfa
class MealyMachine(FSM): class MealyMachine(FSM):
...@@ -47,15 +47,15 @@ class MealyMachineBuilder(object): ...@@ -47,15 +47,15 @@ class MealyMachineBuilder(object):
super().__init__() super().__init__()
self.mm = mm self.mm = mm
def build_mealy(self, model : z3.ModelRef) -> model.fa.MealyMachine: def build_mealy(self, m : z3.ModelRef) -> model.fa.MealyMachine:
tr = FATranslator() tr = FATranslator()
mut_mm = model.fa.MutableMealyMachine() mut_mm = model.fa.MutableMealyMachine()
for state in self.mm.states: for state in self.mm.states:
mut_mm.add_state(tr.z3_to_state(state)) mut_mm.add_state(tr.z3_to_state(state))
for state in self.mm.states: for state in self.mm.states:
for inp in self.mm.inputs: for inp in self.mm.inputs:
output = model.eval(self.mm.output(state, inp)) output = m.eval(self.mm.output(state, inp))
to_state = model.eval(self.mm.transition(state, inp)) to_state = m.eval(self.mm.transition(state, inp))
trans = model.fa.IOTransition( trans = model.fa.IOTransition(
tr.z3_to_state(state), tr.z3_to_state(state),
tr.z3_to_label(inp), tr.z3_to_label(inp),
...@@ -64,6 +64,26 @@ class MealyMachineBuilder(object): ...@@ -64,6 +64,26 @@ class MealyMachineBuilder(object):
return mut_mm.to_immutable() return mut_mm.to_immutable()
class DFABuilder(object):
def __init__(self, dfa : DFA):
super().__init__()
self.dfa = dfa
def build_dfa(self, m : z3.ModelRef) -> model.fa.DFA:
tr = FATranslator()
mut_dfa = model.fa.MutableDFA()
for state in self.dfa.states:
accepting = m.eval(self.dfa.output(state))
mut_dfa.add_state(tr.z3_to_state(state), tr.z3_to_bool(accepting))
for state in self.dfa.states:
for labels in self.dfa.labels:
to_state = m.eval(self.dfa.transition(state, labels))
trans = Transition(
tr.z3_to_state(state),
tr.z3_to_label(labels),
tr.z3_to_state(to_state))
return mut_dfa.to_immutable()
class FATranslator(object): class FATranslator(object):
"""Provides translation from z3 constants to RA elements. """ """Provides translation from z3 constants to RA elements. """
......
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