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

Some more edits, specifically targetting FA encoders.

parent 2d24010b
......@@ -6,12 +6,12 @@ from define import enum, Automaton
import model.fa
def FSM(Automaton,metaclass=ABCMeta):
class FSM(Automaton,metaclass=ABCMeta):
def __init__(self, num_states):
self.State, self.states = enum('State', ['state{0}'.format(i) for i in range(num_states)])
def DFA(FSM):
class DFA(FSM):
def __init__(self, labels, num_states):
self.Label, elements = enum('Label', labels)
......@@ -26,7 +26,7 @@ def DFA(FSM):
#return dfa
def MealyMachine(FSM):
class MealyMachine(FSM):
def __init__(self, input_labels, output_labels, num_states):
self.Input, elements = enum('Input', input_labels)
......@@ -49,48 +49,20 @@ class MealyMachineBuilder(object):
def build_mealy(self, model : z3.ModelRef) -> model.fa.MealyMachine:
tr = FATranslator()
mut_mm = MutableMealyMachine()
def _add_state(self, model, translator, mut_ra, z3state):
z3acc = model.eval(model.eval(self.ra.output(z3state)))
mut_ra.add_state(translator.z3_to_state(z3state), translator.z3_to_bool(z3acc) )
def _add_transitions(self, model, translator, mut_ra, z3state, z3label):
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
if self.ra.fresh not in enabled_z3guards:
for z3guard in enabled_z3guards:
z3end_state = model.eval(self.ra.transition(z3state, z3label, z3guard))
if z3end_state not in z3end_state_to_guards:
z3end_state_to_guards[z3end_state] = []
update = model.eval(self.ra.update(z3state, z3label))
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 not translator.z3_to_bool(model.eval(update == self.ra.fresh)):
self._add_transition(translator, mut_ra, z3state, z3label,
[self.ra.fresh], update, z3end_state, used_z3regs)
if len(z3guards) > 0:
self._add_transition(translator, mut_ra, z3state, z3label,
z3guards, None, z3end_state, used_z3regs)
def _add_transition(self, translator, mut_ra, z3start_state, z3label, z3guards, z3update, z3end_state, used_z3regs):
transition = RATransition(translator.z3_to_state(z3start_state), # start state
translator.z3_to_label(z3label), # label
translator.z3_to_guard(z3guards, used_z3regs), # guard
translator.z3_to_assignment(z3update), # assignment
translator.z3_to_state(z3end_state) # end state
mut_mm = model.fa.MutableMealyMachine()
for state in
for state in
for inp in
output = model.eval(, inp))
to_state = model.eval(, inp))
trans = model.fa.IOTransition(
return mut_mm.to_immutable()
class FATranslator(object):
......@@ -33,7 +33,7 @@ class MealyLearner(Learner):
"""generates the definition and model for an ra whose traces include the traces added so far"""
num_values = len(self.encoder.values)
for num_locations in range(min_states, max_states + 1):
ra, constraints =, num_registers)
ra, constraints =
result = self.solver.check()
if self.verbose:
......@@ -64,3 +64,5 @@ class MutableMealyMachine(MealyMachine, MutableAutomatonMixin):
def __init__(self):
super().__init__([], {})
def to_immutable(self) -> MealyMachine:
return MealyMachine(self._states, self._state_to_trans)
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