test_ralearner.py 1.43 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 z3
7
8
9
10

class RaTest(unittest.TestCase):

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

13

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

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

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

    def check_scenario(self, test_scenario : RaTestScenario):
25
26
27
28
        print("Scenario " + test_scenario.description)
        #result = self.learn_model(test_scenario)
        (succ, ra, model) = self.learn_model(test_scenario)
        self.assertTrue(succ, msg="Register Automaton could not be inferred")
29
        self.assertEqual(len(ra.locations), test_scenario.nr_locations,
30
                         "Wrong number of locations." )
31
        self.assertEqual(len(ra.locations), test_scenario.nr_locations,
32
33
34
                         "Wrong number of registers.")
    
    def learn_model(self, test_scenario : RaTestScenario):
35
        for trace in test_scenario.traces:
36
            self.ralearner.add(trace)
37
38
39
40
41
42
43
        #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
44
45
46