fa.py 5.34 KB
Newer Older
1
2
3
4
from abc import ABCMeta, abstractmethod

import z3
import model.fa
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
5
from define import Automaton, dt_enum
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
6
from model import Transition
7
8


9
class FSM(Automaton,metaclass=ABCMeta):
10
    @abstractmethod
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
11
12
    def __init__(self, num_states, state_enum=dt_enum):
        self.State, self.states = state_enum('State', ['state{0}'.format(i) for i in range(num_states)])
Rick Smetsers's avatar
Rick Smetsers committed
13
        self.start = self.states[0]
14

15
class DFA(FSM):
16
    def __init__(self, labels, num_states):
Rick Smetsers's avatar
Rick Smetsers committed
17
18
        super().__init__(num_states)
        labels = list(labels)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
19
        self.Label, elements = dt_enum('Label', labels)
20
21
22
23
24
        self.labels = {labels[i]: elements[i] for i in range(len(labels))}
        self.transition = z3.Function('transition', self.State, self.Label, self.State)
        self.output = z3.Function('output', self.State, z3.BoolSort())

    def export(self, model : z3.ModelRef) -> model.fa.DFA:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
25
        builder = DFABuilder(self)
Rick Smetsers's avatar
Rick Smetsers committed
26
        dfa = builder.build_dfa(model)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
27
        return dfa
28
29


30
class MealyMachine(FSM):
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
31
32
33
    def __init__(self, input_labels, output_labels, num_states, state_enum=dt_enum, label_enum=dt_enum):
        super().__init__(num_states, state_enum=state_enum)
        self.Input, elements = label_enum('Input', input_labels)
34
        self.inputs = {input_labels[i]: elements[i] for i in range(len(input_labels))}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
35
        self.Output, elements = label_enum('Output', output_labels)
36
37
38
39
40
41
42
43
44
        self.outputs = {output_labels[i]: elements[i] for i in range(len(output_labels))}
        self.transition = z3.Function('transition', self.State, self.Input, self.State)
        self.output = z3.Function('output', self.State, self.Input, self.Output)

    def export(self, model : z3.ModelRef) -> model.fa.MealyMachine:
        builder = MealyMachineBuilder(self)
        mealy = builder.build_mealy(model)
        return mealy

Rick Smetsers's avatar
Rick Smetsers committed
45
46
47
48
class Mapper(object):
    def __init__(self, fa):
        self.Element = z3.DeclareSort('Element')
        self.start = self.element(0)
Rick Smetsers's avatar
Rick Smetsers committed
49
        self.map = z3.Function('map', self.Element, fa.State)
Rick Smetsers's avatar
Rick Smetsers committed
50
51
52
53

    def element(self, name):
        return z3.Const("n"+str(name), self.Element)

54

55

56
57
58
59
60
class MealyMachineBuilder(object):
    def __init__(self, mm : MealyMachine):
        super().__init__()
        self.mm = mm

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
61
    def build_mealy(self, m : z3.ModelRef) -> model.fa.MealyMachine:
62
        tr = MealyTranslator(m, self.mm)
63
64
65
66
        mut_mm =  model.fa.MutableMealyMachine()
        for state in self.mm.states:
            mut_mm.add_state(tr.z3_to_state(state))
        for state in self.mm.states:
67
            for inp in self.mm.inputs.values():
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
68
69
                output = m.eval(self.mm.output(state, inp))
                to_state = m.eval(self.mm.transition(state, inp))
70
71
                trans = model.fa.IOTransition(
                    tr.z3_to_state(state),
72
73
                    tr.z3_to_input(inp),
                    tr.z3_to_output(output),
74
                    tr.z3_to_state(to_state))
75
                mut_mm.add_transition(tr.z3_to_state(state), trans)
76
        mut_mm.generate_acc_seq()
77
        return mut_mm.to_immutable()
78

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
79
80
81
82
83
84
class DFABuilder(object):
    def __init__(self, dfa : DFA):
        super().__init__()
        self.dfa = dfa

    def build_dfa(self, m : z3.ModelRef) -> model.fa.DFA:
Rick Smetsers's avatar
Rick Smetsers committed
85
        tr = FATranslator(self.dfa)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
86
87
88
89
90
        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:
Rick Smetsers's avatar
Rick Smetsers committed
91
            for labels in self.dfa.labels.values():
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
92
93
94
95
96
                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))
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
97
                mut_dfa.add_transition(tr.z3_to_state(state), trans)
98
        mut_dfa.generate_acc_seq()
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
99
        return mut_dfa.to_immutable()
100

101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
class MealyTranslator(object):
    """Provides translation from z3 constants to RA elements. """
    def __init__(self, model, mm: MealyMachine):
        self._model = model
        self._mm = mm
        self._z3_to_inp = dict(map(reversed, mm.inputs.items()))
        self._z3_to_out = dict(map(reversed, mm.outputs.items()))


    def z3_to_state(self, z3state):
        if z3state in self._mm.states:
            return "q" + str(self._mm.states.index(z3state))
        else:
            return "q" + str(list(map(self._model.eval, self._mm.states)).index(z3state))

    def z3_to_input(self, z3label):
        if z3label in self._z3_to_inp:
            return self._z3_to_inp[z3label]
        else:
            for inp in self._z3_to_inp:
                if self._model.eval(inp) == self._model.eval(z3label):
                    return self._z3_to_inp[inp]

    def z3_to_output(self, z3label):
        if z3label in self._z3_to_out:
            return self._z3_to_out[z3label]
        else:
            for out in self._z3_to_out:
                if self._model.eval(out) == self._model.eval(z3label):
                    return self._z3_to_out[out]

132
133
class FATranslator(object):
    """Provides translation from z3 constants to RA elements. """
134
    def __init__(self, fa:FSM):
135
136
        self.fa = fa

137

138
139
140
141
142
143
144
145
    def z3_to_bool(self, z3bool):
        return str(z3bool) == "True"

    def z3_to_state(self, z3state):
        return "q"+str(self.fa.states.index(z3state))

    def z3_to_label(self, z3label):
        return str(z3label)