ra.py 3.28 KB
Newer Older
1
from z3gi.model import Transition, Acceptor, NoTransitionFired, NonDeterminism
2
3
4
from abc import ABCMeta, abstractmethod

class RegisterAutomaton(Acceptor):
5
    def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
6
7
8
      super.__init__(locations, loc_to_trans, loc_to_acc)
      self.register = registers

9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
    def state(self, trace):
        init = -1
        reg_val = dict()
        for reg in self.ra.get_registers():
            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

            fired_transition = fired_transitions[0]
            reg_val = fired_transition.update(reg_val, action)
            crt_state = fired_transition.end_state

        return crt_state

31
32
33
34
35
36
37
38
39
40
41
42
class RATransition(Transition):
    def __init__(self, start_state, start_label, guard, assignment, end_state):
        Transition.__init__(start_state, start_label, end_state)
        self.guard = guard
        self.assignment = assignment

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

43
44
    def update(self, action, valuation):
        return self.assignment.update(valuation, action.value)
45
46
47
48
49
50


class Guard(metaclass=ABCMeta):
    def __init__(self):
        pass

51
    # to make this more abstract, value would have to be replaced by param valuation
52
53
54
55
    @abstractmethod
    def is_satisfied(self, valuation, value):
        pass

56
57

class EqualityGuard(Guard):
58
59
60
61
62
63
64
    def __init__(self, register):
        super.__init__()
        self.register = register

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

65

66
67
68
69
70
71
72
73
74
75
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

76

77
78
79
80
81
82
83
84
85
86
87
class FreshGuard(Guard):
    def __init__(self, guarded_registers = []):
        super.__init__()
        self.registers = guarded_registers

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

88

89
90
91
92
class Assignment(metaclass=ABCMeta):
    def __init__(self):
        pass

93
    # to make this more general, value would have to be replaced by variable(reg/param) mapping and par valuation
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
    @abstractmethod
    def update(self, valuation, value):
        pass


class RegisterAssignment(Assignment):
    def __init__(self, register):
        super.__init__()
        self.register = register

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

class NoAssignment(Assignment):
    def __init__(self):
        super.__init__()
    def update(self, valuation):
        return valuation