ra.py 13.2 KB
Newer Older
1
2
from collections import namedtuple

Rick Smetsers's avatar
Rick Smetsers committed
3
import z3
4
from model.ra import *
5

Rick Smetsers's avatar
Rick Smetsers committed
6

Rick Smetsers's avatar
Rick Smetsers committed
7
8
from define import Automaton

Rick Smetsers's avatar
Rick Smetsers committed
9
10
11
12

class RegisterAutomaton(Automaton):

    def __init__(self, labels, num_locations, num_registers):
13
14
        self.Label, elements = enum('Label', labels)
        self.labels = {labels[i]: elements[i] for i in range(len(labels))}
Rick Smetsers's avatar
Rick Smetsers committed
15
16
17
        self.Location, self.locations = enum('Location', ['location{0}'.format(i) for i in range(num_locations)])
        self.Register, self.registers = enum('Register', ['register{0}'.format(i) for i in range(num_registers)] + ['fresh'])
        self.start = self.locations[0]
18
        self.fresh = self.registers[-1]
Rick Smetsers's avatar
Rick Smetsers committed
19
20
21
22
23
        self.transition = z3.Function('transition', self.Location, self.Label, self.Register, self.Location)
        self.output = z3.Function('output', self.Location, z3.BoolSort())
        self.used = z3.Function('used', self.Location, self.Register, z3.BoolSort())
        self.update = z3.Function('update', self.Location, self.Label, self.Register)

24
    def export(self, model : z3.ModelRef) -> RegisterAutomaton:
25
        builder = RegisterAutomatonBuilder(self)
26
        ra = builder.build_ra(model)
27
        return ra
Rick Smetsers's avatar
Rick Smetsers committed
28

Rick Smetsers's avatar
Rick Smetsers committed
29

Rick Smetsers's avatar
Rick Smetsers committed
30
31
32
33
34
35
class IORegisterAutomaton(Automaton):

    def __init__(self, input_labels, output_labels, num_locations, num_registers):
        labels = input_labels + output_labels
        self.Label, elements = enum('Label', input_labels + output_labels)
        self.labels = {labels[i]: elements[i] for i in range(len(labels))}
36
        self._input_labels =  [self.labels[lbl] for lbl in input_labels]
Rick Smetsers's avatar
Rick Smetsers committed
37
38
39
40
41
42
43
44
45
46
47
48
49
        self.Location, self.locations = enum('Location', ['location{0}'.format(i) for i in range(num_locations + 1)])
        self.sink = self.locations[-1]
        self.Register, self.registers = enum('Register', ['register{0}'.format(i) for i in range(num_registers)] + ['fresh'])
        self.start = self.locations[0]
        self.fresh = self.registers[-1]
        self.transition = z3.Function('transition', self.Location, self.Label, self.Register, self.Location)
        self.output = z3.Function('output', self.Location, z3.BoolSort())
        self.used = z3.Function('used', self.Location, self.Register, z3.BoolSort())
        self.update = z3.Function('update', self.Location, self.Label, self.Register)
        self.loctype = z3.Function('loctype', self.Location, z3.BoolSort())


    def export(self, model : z3.ModelRef) -> RegisterAutomaton:
50
51
52
        builder = IORegisterAutomatonBuilder(self)
        ra = builder.build_ra(model)
        return ra
Rick Smetsers's avatar
Rick Smetsers committed
53
54


Rick Smetsers's avatar
Rick Smetsers committed
55
class Mapper(object):
56
    def __init__(self, ra):
Rick Smetsers's avatar
Rick Smetsers committed
57
58
59
60
61
62
        self.Value = z3.DeclareSort('Value')
        self.Element = z3.DeclareSort('Element')
        self.start = self.element(0)
        self.init = self.value("_")
        self.map = z3.Function('map', self.Element, ra.Location)
        self.valuation = z3.Function('valuation', self.Element, ra.Register, self.Value)
63

Rick Smetsers's avatar
Rick Smetsers committed
64
65
    def value(self, name):
        return z3.Const("v"+str(name), self.Value)
66

Rick Smetsers's avatar
Rick Smetsers committed
67
68
    def element(self, name):
        return z3.Const("n"+str(name), self.Element)
69

Rick Smetsers's avatar
Rick Smetsers committed
70
class RegisterAutomatonBuilder(object):
71
72
73
    """
    Builder class that construct a register automaton out of a model definition.
    """
Rick Smetsers's avatar
Rick Smetsers committed
74
    def __init__(self, ra : RegisterAutomaton):
75
76
77
        super().__init__()
        self.ra = ra

78
    def build_ra(self, model):
79
80
        mut_ra = MutableRegisterAutomaton()
        translator = Translator(self.ra)
81
        for z3state in self.ra.locations:
82
            self._add_state(model, translator, mut_ra, z3state)
83
84
            for z3label in self.ra.labels.values():
                self._add_transitions(model, translator, mut_ra, z3state, z3label)
85
86
87
88
89
90
        return mut_ra.to_immutable()

    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) )

91
    def _add_transitions(self, model, translator, mut_ra, z3state, z3label):
92
        z3end_state_to_guards = dict()
93
94
95
96
        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
                            ]
97
98
99
100
101
        if self.ra.fresh not in enabled_z3guards:
            enabled_z3guards.append(self.ra.fresh)
        for z3guard in enabled_z3guards:
            z3end_state = model.eval(self.ra.transition(z3state, z3label, z3guard))
            if z3end_state not in z3end_state_to_guards:
102
103
104
                z3end_state_to_guards[z3end_state] = []
            z3end_state_to_guards[z3end_state].append(z3guard)
        update = model.eval(self.ra.update(z3state, z3label))
105
        used_z3regs = [reg for reg in enabled_z3guards if reg is not self.ra.fresh]
106

107
        for (z3end_state, z3guards) in z3end_state_to_guards.items():
108
            # a transition which makes an assignment is never merged
109
            if self.ra.fresh in z3guards and not translator.z3_to_bool(model.eval(update == self.ra.fresh)):
110
111
                self._add_transition(translator, mut_ra, z3state, z3label,
                                     [self.ra.fresh], update, z3end_state, used_z3regs)
112
113
                z3guards.remove(self.ra.fresh)
            if len(z3guards) > 0:
114
115
                self._add_transition(translator, mut_ra, z3state, z3label,
                                     z3guards, None, z3end_state, used_z3regs)
116

117
    def _add_transition(self, translator, mut_ra, z3start_state, z3label, z3guards, z3update, z3end_state, used_z3regs):
118
119
120
121
122
123
124
        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_ra.add_transition(translator.z3_to_state(z3start_state),transition)
125

126
127
128
129
130
131
132
133
134
135

class IORegisterAutomatonBuilder(object):
    """
    Builder class that construct a register automaton out of a model definition.
    """
    def __init__(self, ra : IORegisterAutomaton):
        super().__init__()
        self.ra = ra


136
    def build_ra(self, model):
137
138
        mut_ra = MutableIORegisterAutomaton()
        translator = Translator(self.ra)
139

140
        z3input_states = [z3state for z3state in self.ra.locations if
141
142
143
144
145
146
147
148
149
150
            translator.z3_to_bool(model.eval(
                z3.And(self.ra.loctype(z3state), z3state != self.ra.sink)))]

        # we cannot use 'is not', since 'is not' compares references, not values and model.eval produces a
        # different reference
        z3input_labels = [z3label for z3label in self.ra.labels.values() if
                          translator.z3_to_bool(model.eval(
                              self.ra.transition(self.ra.start, z3label, self.ra.fresh) != self.ra.sink))
                          ]
        z3output_labels = [z3label for z3label in self.ra.labels.values() if z3label not in z3input_labels]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
151
152
153
        print("Input labels ", z3input_labels, "; Output labels", z3output_labels,
              "Input states ", z3input_states, "; Output and sink states",
              [z3state for z3state in self.ra.locations if z3state not in z3input_states])
154
155
156

        for z3state in z3input_states:
            self._add_state(translator, mut_ra, z3state)
157
158
            for z3label in z3input_labels:
                self._add_transitions(model, translator, mut_ra, z3state, z3label, z3output_labels)
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
        return mut_ra.to_immutable()

    def _add_state(self, translator, mut_ra, z3state):
        mut_ra.add_state(translator.z3_to_state(z3state))

    def _add_transitions(self, model, translator, mut_ra, z3state, z3label, z3output_labels):
        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]

        for z3guard in enabled_z3guards:
            z3out_state = model.eval(self.ra.transition(z3state, z3label, z3guard))

            if z3out_state not in z3end_state_to_guards:
                z3end_state_to_guards[z3out_state] = []
            z3end_state_to_guards[z3out_state].append(z3guard)
        update = model.eval(self.ra.update(z3state, z3label))
        used_z3regs = [reg for reg in enabled_z3guards if reg is not self.ra.fresh]

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
179
        print("For {0} we have the transitions \n {1}".format(z3state, z3end_state_to_guards))
180
181
        for (z3out_state, z3guards) in z3end_state_to_guards.items():
            # a transition which makes an assignment is never merged
182
            if self.ra.fresh in z3guards and not translator.z3_to_bool(model.eval(update == self.ra.fresh)):
183
                self._add_transition(model, translator, mut_ra, z3state, z3label,
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
                                     [self.ra.fresh], update, z3out_state,
                                     z3output_labels, used_z3regs)
                z3guards.remove(self.ra.fresh)
            if len(z3guards) > 0:
                self._add_transition(model, translator, mut_ra, z3state, z3label,
                                     z3guards, None, z3out_state,
                                     z3output_labels, used_z3regs)

    def _add_transition(self, model, translator, mut_ra, z3start_state, z3label,
                        z3disjguards, z3input_update, z3out_state, output_labels, used_z3regs):

        enabled_z3guards = [guard for guard in self.ra.registers if
                            translator.z3_to_bool(model.eval(self.ra.used(z3out_state, guard))) or
                            guard is self.ra.fresh]

        active_z3action = [(output_label, guard) for output_label in output_labels for guard in enabled_z3guards
200
201
                         if translator.z3_to_bool(model.eval(self.ra.transition(z3out_state, output_label, guard)
                                                             != self.ra.sink))]
202
        if len(active_z3action) != 1:
203
            raise Exception("Exactly one transition should not lead to sink state. "
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
204
205
                            "From location {0} there are {1} transitions which lead to sink {2}"
                            .format(z3out_state, len(active_z3action), self.ra.sink))
206
207

        (z3output_label, z3output_guard) = active_z3action[0]
208
209
        z3end_state = model.eval(self.ra.transition(z3out_state, z3output_label, z3output_guard))
        z3output_update = model.eval(self.ra.update(z3out_state, z3output_label))
210
211
212
213
214
215
216
217
218
219

        transition = IORATransition(translator.z3_to_state(z3start_state),
                                    translator.z3_to_label(z3label),
                                    translator.z3_to_guard(z3disjguards, used_z3regs),
                                    translator.z3_to_assignment(z3input_update),
                                    translator.z3_to_label(z3output_label),
                                    translator.z3_to_mapping(z3output_guard),
                                    translator.z3_to_assignment(z3output_update),
                                    translator.z3_to_state(z3end_state),
                                    )
220
        mut_ra.add_transition(translator.z3_to_state(z3start_state), transition)
221

Rick Smetsers's avatar
Rick Smetsers committed
222
class Translator(object):
223
224
225
226
227
228
    """Provides translation from z3 constants to RA elements. """
    def __init__(self, ra):
        self.reg_context = dict()
        self.ra = ra

    def z3_to_assignment(self, z3asg):
229
        if (z3asg is None) or (z3asg == self.ra.fresh):
230
231
232
233
234
            asg = NoAssignment()
        else:
            asg = RegisterAssignment(self.z3_to_register(z3asg))
        return asg

235
236
    def z3_to_guard(self, z3guards, enabled_z3regs):
        z3guard_regs = [z3reg for z3reg in z3guards if z3reg is not self.ra.fresh]
237
        if self.ra.fresh in z3guards:
238
239
            diff_from = [self.z3_to_register(z3reg) for z3reg in enabled_z3regs
                         if z3reg not in z3guard_regs and z3reg is not self.ra.fresh]
240
            return FreshGuard(diff_from)
241
        else:
242
            equ_guards = [EqualityGuard(self.z3_to_register(guard_reg)) for guard_reg in z3guard_regs]
243
244
245
246
247
            if len(equ_guards) == 1:
                return equ_guards[0]
            else:
                return OrGuard(equ_guards)

248
249
250
251
252
253
    def z3_to_mapping(self, z3guard):
        if z3guard is self.ra.fresh:
            return Fresh(0)
        else:
            return self.z3_to_register(z3guard)

254
255
    def z3_to_bool(self, z3bool):
        return str(z3bool) == "True"
256
257

    def z3_to_state(self, z3state):
258
        return "l"+str(self.ra.locations.index(z3state))
259
260
261
262
263

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

    def z3_to_register(self, z3register):
264
265
        if str(z3register) == "fresh":
            raise Exception
266
        assert z3register is not self.ra.fresh
267
268
        if str(z3register) not in self.reg_context:
            self.reg_context[str(z3register)] = Register(self.ra.registers.index(z3register))
Rick Smetsers's avatar
Rick Smetsers committed
269
270
271
272
273
274
275
276
277
        return self.reg_context[str(z3register)]


def enum(name, elements):
    d = z3.Datatype(name)
    for element in elements:
        d.declare(element)
    d = d.create()
    return d, [d.__getattribute__(element) for element in elements]