ra.py 6.85 KB
Newer Older
1
from z3gi.model import Transition, Acceptor, NoTransitionFired, MultipleTransitionsFired
2
from abc import ABCMeta, abstractmethod
3
import itertools
4
import collections
5
from typing import List
6
7

Action = collections.namedtuple('Action', ('label', 'value'))
8

9
10
11

class RATransition(Transition):
    def __init__(self, start_state, start_label, guard, assignment, end_state):
12
        super().__init__(start_state, start_label, end_state)
13
14
15
16
17
18
19
20
21
22
23
24
        self.guard = guard
        self.assignment = assignment

    def is_enabled(self, action, valuation):
        if action.label is self.start_label:
            satisfied = self.guard.is_satisfied(action.value, valuation)
            return satisfied
        return False

    def update(self, action, valuation):
        return self.assignment.update(valuation, action.value)

25
26
27
28
29
30
31
32
    def __str__(self, shortened = False):
        if not shortened:
            return "{0} {1}({2}) -> {3} {4}".format(self.start_state, self.start_label, self.guard,
                                               self.assignment, self.end_state)
        else:
            return "{0}({1}) -> {2} {3}".format(self.start_label, self.guard,
                                                    self.assignment, self.end_state)

33
34
35
class SymbolicValue(metaclass=ABCMeta):
    """Symbolic values can be used to symbolically express registers, constants and parameters."""
    def __init__(self, index):
36
        super().__init__()
37
38
39
40
        self.index = index

class Register(SymbolicValue):
    def __init__(self, index):
41
        super().__init__(index)
42
43
44
45
46

    def __str__(self):
        return "r" + str(self.index)


47
class RegisterAutomaton(Acceptor):
48
    def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
49
      super().__init__(locations, loc_to_trans, loc_to_acc)
50
51
      self._registers = registers

52
    def registers(self) -> List[Register]:
53
        return self._registers
54

55
56
    def transitions(self, state: str, label:str = None) -> List[RATransition]:
        return super().transitions(state, label)
57

58
    def state(self, trace: List[Action]) -> str:
59
60
        init = -1
        reg_val = dict()
61
        for reg in self.registers():
62
63
64
65
66
67
68
69
70
71
72
73
            reg_val[reg] = init

        crt_state = self.start_state()
        for action in trace:
            transitions = self.transitions(crt_state, action.label)
            fired_transitions = [trans for trans in transitions if trans.is_enabled(action, reg_val)]

            # the number of fired transitions can be more than one since we could have multiple equalities
            # todo (merge into or guard?)
            if len(fired_transitions) == 0:
                raise NoTransitionFired

74
75
76
            if len(fired_transitions) > 1:
                raise MultipleTransitionsFired

77
78
79
80
81
82
            fired_transition = fired_transitions[0]
            reg_val = fired_transition.update(reg_val, action)
            crt_state = fired_transition.end_state

        return crt_state

83
84
class MutableRegisterAutomaton(RegisterAutomaton):
    def __init__(self):
85
        super().__init__([], dict(), dict(), [])
86
87
88
89
90
91
92
93
94
95
96

    def add_state(self, state, accepts):
        if state not in self._states:
            self._states.append(state)
        self._state_to_acc[state] = accepts


    def add_transition(self, state, transition):
        if state not in self._state_to_trans:
            self._state_to_trans[state]=[]
        self._state_to_trans[state].append(transition)
97
        for reg in transition.guard.registers():
98
99
100
            if reg not in self._registers:
                self._registers.append(reg)

101
    def to_immutable(self) -> RegisterAutomaton:
102
103
        return RegisterAutomaton(self._states, self._state_to_acc, self._state_to_trans, self._registers)

104
class Guard(metaclass=ABCMeta):
105
    """A guard with is_satisfied implements a predicate over the current register valuation and the parameter value. """
106
107
108
    def __init__(self):
        pass

109

110
111
    @abstractmethod
    def get_registers(self):
112
        """Returns the registers/constants over which the guard is formed"""
113
114
        pass

115
    # to make this more abstract, value would have to be replaced by param valuation
116
117
118
119
    @abstractmethod
    def is_satisfied(self, valuation, value):
        pass

120
class EqualityGuard(Guard):
121
    """An equality guard holds iff. the parameter value is equal to the value assigned to its register."""
122
    def __init__(self, register):
123
        super().__init__()
124
125
126
127
128
        self.register = register

    def is_satisfied(self, valuation, value):
        return valuation[self.register] == value

129
130
131
    def get_registers(self):
        return [self.register]

132
133
    def __str__(self):
        return "p=={0}".format(str(self.register))
134

135
136
137
138
139
140
141
142
143
144
class OrGuard(Guard):
    def __init__(self, guards):
        self.guards = guards

    def is_satisfied(self, valuation, value):
        for guard in self.guards:
            if guard.is_satisfied(valuation, value):
                return True
        return False

145
    def get_registers(self):
146
        regs_of_guards = [guard.registers() for guard in self.guards]
147
148
149
150
151
        regs = itertools.chain.from_iterable(regs_of_guards)
        seen = set()
        distinct_regs = [x for x in regs if x not in seen and not seen.add(x)]
        return list(distinct_regs)

152
153
154
155
    def __str__(self):
        all_guards = [str(guard) for guard in self.guards]
        return "\\/".join(all_guards)

156

157
class FreshGuard(Guard):
158
    """An fresh guard holds if the parameter value is different from the value assigned to any of its registers."""
159
    def __init__(self, guarded_registers = []):
160
        super().__init__()
161
162
163
164
165
166
167
168
        self.registers = guarded_registers

    def is_satisfied(self, valuation, value):
        for register in self.registers:
            if valuation[register] == value:
                return False
        return True

169
170
    def get_registers(self):
        return self.registers
171

172
173
174
175
176
177
178
    def __str__(self):
        if len(self.registers) == 0:
            return "True"
        else:
            all_deq = ["p!={0}".format(str(reg)) for reg in self.registers]
            return "/\\".join(all_deq)

179
class Assignment(metaclass=ABCMeta):
180
    """An assignment updates the valuation of registers using the old valuation and the current parameter value"""
181
182
183
    def __init__(self):
        pass

184
    # to make this more general, value would have to be replaced by variable(reg/param) mapping and par valuation
185
186
187
188
189
190
191
    @abstractmethod
    def update(self, valuation, value):
        pass


class RegisterAssignment(Assignment):
    def __init__(self, register):
192
        super().__init__()
193
194
195
        self.register = register

    def update(self, valuation, value):
196
197
198
        new_valuation = dict(valuation)
        new_valuation[self.register] = value
        return new_valuation
199

200
201
202
    def __str__(self):
        return "{0}:=p".format(str(self.register))

203

204
205
class NoAssignment(Assignment):
    def __init__(self):
206
        super().__init__()
207

208
    def update(self, valuation):
209
210
        return dict(valuation)

211
212
    def __str__(self):
        return "r:=r"
213