algorithm.py 4.95 KB
Newer Older
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
1
import copy
2
from typing import List, Tuple, Union,cast
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
3

4
5
from model import Automaton
from learn import Learner
6
from test import TestGenerator, Test
7
import time
8

9
10
11
12
13
__all__ = [
    "learn",
    "learn_mbt"
    ]

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
14

15
class Statistics():
16
    """We only refe"""
17
    def __init__(self):
18
        self.learning_times = []
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
19
        self.model_stats = None
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
20
21
        self.resets = 0
        self.inputs = 0
22

23
24
25
    def add_learning_time(self, time):
        self.learning_times.append(time)

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
26
27
28
29
30
31
32
33
34
35
36
37
38
    def set_num_resets(self, test_num):
        self.resets = test_num

    def set_num_inputs(self, inp_num):
        self.inputs = inp_num

    def __str__(self):        return \
        "Tests until last hyp: {} \n" \
        "Inputs until last hyp: {} \n " \
        "Hypotheses used in learning: {} \n " \
        "Learning time for each model: {} \n " \
        "Total learning time: {} ".format(        self.resets,
                                                  self.inputs,
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
39
                                                   len(self.learning_times),
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
40
                                                  self.learning_times,
41
                                                   sum(self.learning_times))
42
43
44


def learn(learner:Learner, test_type:type, traces: List[object]) -> Tuple[Automaton, Statistics]:
45
    """ takes learner and a list of traces and generates a model"""
46
47
48
49
50
    statistics = Statistics()
    if len(traces) == 0:
        return (None, statistics)
    else:
        statistics.set_suite_size(len(traces))
51
        test = cast(Test, test_type(traces.pop(0)))
52
        definition = None
53
        learner.add(test.tr)
54
        statistics.add_learner_test(test)
55
56
        done = False
        model = None
57
        learn_traces = [test.tr]
58
        while not done:
59
            start_time = int(time.time() * 1000)
60
            (model, definition) = learner.model(old_definition=definition)
61
62
            end_time = int(time.time() * 1000)
            statistics.add_learning_time(end_time-start_time)
63
64
            done = True
            for trace in traces:
65
                test = cast(Test, test_type(trace))
66
67
                ce = test.check(model)
                if ce is not None:
68
69
70
71
72
                    if ce not in learn_traces:
                        learn_traces.append(ce)
                    else:
                        raise Exception("The CE {0} has already been processed yet it "
                                        "is still a CE. \n CEs: {1} \n Model: {2}".format(ce, learn_traces, model))
73
                    learner.add(ce)
74
                    statistics.add_learner_test(test)
75
76
                    done = False
                    break
77
        statistics.set_suite_size(len(traces))
78
79
        return (model, statistics)

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
80
def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> Tuple[Union[Automaton,None], Statistics]:
81
    """ takes learner, a test generator, and bound on the number of tests and generates a model"""
82
83
84
85
86
87
88
89
90
91
    next_test = test_generator.gen_test(None)
    statistics = Statistics()
    if next_test is None:
        return (None, statistics)
    else:
        definition = None
        learner.add(next_test.trace())
        done = False
        learner_tests = [next_test]
        generated_tests = [next_test]
92
93
        last_ce = None
        ce = None
94
        while not done:
95
96
97
            if last_ce and ce == last_ce:
                raise Exception("Counterexample ", ce, " was not correctly processed")
            last_ce = ce
98
            start_time = int(time.time() * 1000)
99
100
101
102
            ret = learner.model(old_definition=definition)
            if ret is None:
                return (None, statistics)
            (model, definition) = ret
103
104
105
            end_time = int(time.time() * 1000)
            statistics.add_learning_time(end_time - start_time)
            done = True
106
            # we first check the tests that already have been generated
107
108
109
            for next_test in generated_tests:
                ce = next_test.check(model)
                if ce is not None:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
110
                    #print("TEST: ", next_test.trace())
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
111
                    print("CE: ", ce)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
112
                    #print(model)
113
                    learner.add(ce)
114
115
116
117
                    done = False
                    break
            if not done:
                continue
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
118
            test_generator.initialize(model)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
119

120
121
122
123
124
125
            # we then generate and check new tests, until either we find a CE,
            # or the suite is exhausted or we have run the intended number of tests
            for i in range(0, max_tests):
                next_test = test_generator.gen_test(model)
                if next_test is None:
                    break
126
127
128
                generated_tests.append(next_test)
                ce = next_test.check(model)
                if ce is not None:
129
                    learner_tests.append(next_test)
130
131
132
                    learner.add(ce)
                    done = False
                    break
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
133
            test_generator.terminate()
Paul Fiterau Brostean's avatar
Updates    
Paul Fiterau Brostean committed
134
135

        #print([str(test.trace() for test in learner_tests)])
136
        return (model, statistics)