__init__.py 6.85 KB
Newer Older
1
from abc import ABCMeta, abstractmethod
2
from typing import List, Generator, Iterable, Tuple
3
import itertools
4

5
from model import Automaton, Acceptor, Transducer
6
from model.fa import Symbol
7
from model.ra import IORegisterAutomaton, Action
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
8
9
from sut import SUT
from sut.scalable import ActionSignature
10
11
12
13
from utils import determinize


class Test(metaclass=ABCMeta):
14
15
16
17
    """A test is based on a trace/observation on the actual SUT. The test verifies that
    the model exhibits behavior corresponding to this observation."""
    def __init__(self, trace):
        self.tr = trace
18
19

    def check(self, model:Automaton):
20
        """checks if the hyp passes the test. On failure, it returns a minimal trace to be added by the learner.
21
        On success it return None"""
22
        return self._check_trace(model, self.tr)
23
24

    @abstractmethod
25
    def _check_trace(self, model, trace):
26
27
28
        pass

    def trace(self):
29
        """returns the trace/observation of the SUT the Test is based on"""
30
        return self.tr
31
32

    @abstractmethod
33
34
    def size(self) -> int:
        """returns the size (in terms of inputs) of the test"""
35
36
        pass

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
37
38
39
40
    @abstractmethod
    def covers(self, test) -> bool:
        pass

41
42
43
44
45
46
47
48
49
50
51
52
53
class EqualTestsMixin(metaclass=ABCMeta):
    """doesn't work unfortunately"""
    def __eq__(self, other):
        return other and  type(other) is type(self) and other.tr == self.tr

    def __ne__(self, other):
        return not self.__eq__(other)

    def __hash__(self):
        return hash((type(self), frozenset(self.tr)))



54
class TestGenerator(metaclass=ABCMeta):
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
55
    #TODO gen_test should take the sut as param (relieving the testgens of having to store it in a field)
56
57
58
59
60
    @abstractmethod
    def gen_test(self, model: Automaton) -> Test:
        """generates a Test. Returns None if the test suite is exhausted"""
        pass

61
    def gen_test_iter(self, model: Automaton) -> Iterable[Test]:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
62
        self.initialize(model)
63
64
65
66
        test = self.gen_test(model)
        while test is not None:
            yield test
            test = self.gen_test(model)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
67
68
        self.terminate()

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
69
    def gen_blind_inp_seq(self, sut:SUT):
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
        """generates a sequence covering all input elements in the sut interface"""
        seq = []
        for abs_inp in self.sut.input_interface():
            cnt = 0
            # if it's RA stuff
            if isinstance(abs_inp, ActionSignature):
                if abs_inp.num_params == 0:
                    val = None
                else:
                    val = cnt
                    cnt += 1
                seq.append(Action(abs_inp.label, val))
            elif isinstance(abs_inp, str):
                seq.append(abs_inp)
            else:
                raise Exception("Unrecognized type")
        return seq

    def initialize(self, model: Automaton):
        """feeds the tests generator the supplied automaton in an initialization step"""
        pass

    def terminate(self):
        pass
94
95
96
97
98
99
100
101
102

class TracesGenerator(metaclass=ABCMeta):
    def __init__(self, traces = list()):
        self.traces = traces

    def gen_test(self, model:Automaton):
        if len(self.traces) > 0:
            return self.traces.pop(0)
        return None
103
104

class Tester(metaclass=ABCMeta):
105
106
107
108
109
    def __init__(self, test_generator:TestGenerator):
        self.generator = test_generator

    def find_ce(self, model:Automaton):
        """generates an observation which exposes a counterexample"""
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
110
111
        self.generator.initialize(model)
        ce = None
112
113
114
        while True:
            test = self.generator.gen_test(model)
            if test is None:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
115
                break
116
117
            trace = test.check(model)
            if trace is not None:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
118
119
120
                ce = trace
                break
        self.generator.terminate()
121
122
123
124
125
126
127
128
129


def determinize_act_io(tuple_seq):
    seq = list(itertools.chain.from_iterable(tuple_seq))
    det_seq = determinize(seq)
    det_act_seq = [Action(l, v) for (l, v) in det_seq]
    det_duple_seq = [(det_act_seq[i], det_act_seq[i + 1]) for i in range(0, len(det_act_seq), 2)]
    return det_duple_seq

130
131
class TransducerTest(Test):
    def __init__(self, trace:List[Tuple[object, object]]):
132
133
        super().__init__(trace)

134
    def _check_trace(self, model: Transducer, trace:List[Tuple[object, object]]):
135
136
137
138
139
140
141
142
        test_trace = []
        for (inp_act, out_act) in trace:
            test_trace.append((inp_act, out_act))
            output = model.output([inp for (inp, _) in test_trace])
            if output != out_act:
                return  test_trace
        return None

143
144
145
146
147
148
149
150
151
    def __hash__(self):
        return hash((type(self), frozenset(self.tr)))

    def __eq__(self, other):
        return other and type(other) is type(self) and other.tr == self.tr

    def __ne__(self, other):
        return not self.__eq__(other)

152
    def size(self):
153
        return len(self.tr)
154

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
155
156
157
158
159
160
161
162
163
    def covers(self, test):
        if type(test) is type(self) and len(test.trace()) <= len(self.trace()):
            for ((inp, _),(inp2, _)) in zip(self.trace(), test.trace()):
                if inp != inp2:
                    return  False
            return True
        return False


164
165
166
167
class MealyTest(TransducerTest):
    def __init__(self, trace:List[Tuple[Symbol, Symbol]]):
        super().__init__(trace)

168
169
170
171
172
173
174
175
176
    def __eq__(self, other):
        return super().__eq__(other)

    def __ne__(self, other):
        return super().__ne__(other)

    def __hash__(self):
        return super().__hash__()

177
178
179
180
181
182
183
184
185
class IORATest(TransducerTest):
    def __init__(self, trace: List[Tuple[Action, Action]]):
        super().__init__(trace)

    def _check_trace(self, model: IORegisterAutomaton, trace: List[Tuple[Action, Action]]):
        # any observation trace has to be first determinized
        trace = determinize_act_io(trace)
        return super()._check_trace(model, trace)

186
187
188
189
190
191
192
193
    def __eq__(self, other):
        return super().__eq__(other)

    def __ne__(self, other):
        return super().__ne__(other)

    def __hash__(self):
        return super().__hash__()
194

195
# Acceptor Test observations are tuples comprising sequences of Actions/Symbols joined by an accept/reject booleans
196
197
class AcceptorTest(Test):
    def __init__(self, trace:Tuple[List[object], bool]):
198
199
200
201
        super().__init__(trace)

    def _check_trace(self, model: Acceptor, trace):
        (seq, acc) = trace
202
203
        if model.accepts(seq) != acc:
            return trace
204
205
206
        return None

    def size(self):
207
        (seq, acc) = self.tr
208
209
210
211
212
213
214
215
216
217
218
        return len(seq)

    def __hash__(self):
        (seq, acc) = self.tr
        return hash((type(self), frozenset(seq), acc))

    def __eq__(self, other):
        return other and type(other) is type(self) and other.tr == self.tr

    def __ne__(self, other):
        return not self.__eq__(other)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
219
220
221
222
223
224
225
226

    def covers(self, test):
        if type(test) is type(self) and self.size() <= test.size():
            (seq, _) =  self.trace()
            (seq2, _) = test.trace()
            return seq == seq2
        return False