test_ralearner.py 2.32 KB
Newer Older
1
2
import unittest

3
from tests.ra_testscenario import *
4
from z3gi.learn.ra import RALearner
5
from z3gi.define.ra import RegisterAutomaton
6
import model.ra
7
import z3
8

9
class RaLearnerTest(unittest.TestCase):
10
11

    def setUp(self):
12
        self.ralearner = RALearner(labels, verbose=True)
13

14

15
16
    def test_sut1(self):
        self.check_scenario(sut_m1)
17
18
19
20
        pass

    def test_sut2(self):
        self.check_scenario(sut_m2)
21

22
23
    def test_sut3(self):
        self.check_scenario(sut_m3)
24
25

    def check_scenario(self, test_scenario : RaTestScenario):
26
27
        print("Scenario " + test_scenario.description)
        (succ, ra, model) = self.learn_model(test_scenario)
28

29
        self.assertTrue(succ, msg="Register Automaton could not be inferred")
30
        self.assertEqual(len(ra.locations), test_scenario.nr_locations,
31
                         "Wrong number of locations." )
32
        self.assertEqual(len(ra.locations), test_scenario.nr_locations,
33
                         "Wrong number of registers.")
34
        exported = ra.export(model)
35
        print(model)
36
37
        print("Learned model:  \n",exported)
        self.assertEqual(len(exported.states()), test_scenario.nr_locations,
38
39
40
                          "Wrong number of locations in exported model. ")
        self.assertEqual(len(exported.registers()), test_scenario.nr_registers,
                          "Wrong number of registers in exported model. ")
41
42
43
44
45
46
47
        self.check_ra_against_obs(exported, test_scenario)


    def check_ra_against_obs(self, learned_ra: model.ra.RegisterAutomaton, test_scenario : RaTestScenario):
        """Checks if the learned RA corresponds to the scenario observations"""
        for trace, acc in test_scenario.traces:
            self.assertEqual(learned_ra.accepts(trace), acc,
48
                             "Register automaton output doesn't correspond to observation {0}".format(str(trace)))
49
    
50
51
    def learn_model(self, test_scenario : RaTestScenario) -> \
            (bool, RegisterAutomaton, z3.ModelRef):
52
        for trace in test_scenario.traces:
53
            self.ralearner.add(trace)
54
55
56
57
58
59
60
        #ra_def = None
        min_locations = 0
        max_locations = test_scenario.nr_locations + 1
        num_regs = 0
        #(_, ra_def, _) = self.ralearner._learn_model(2, 2, 1)
        result = self.ralearner._learn_model(min_locations, max_locations, num_regs)  #
        return result
61
62
63