scrap_test.py 1.03 KB
Newer Older
1
from z3gi.learn.ra import RALearner
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
2
3
from tests.ra_testscenario import *
from encode.ran import RANEncoder
4
5


Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
6
def check_ra_against_obs(learner, learned_ra, m,  test_scenario):
7
8
9
    """Checks if the learned RA corresponds to the scenario observations"""
    for trace, acc in test_scenario.traces:
        if learned_ra.accepts(trace) != acc:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
10
            learner.print_tree()
11
12
13
14
            print("Register automaton {0} \n\n with model {1} \n doesn't correspond to the observation {2}"
                  .format(learned_ra, m, str((trace, acc))))
            return

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
15
16
17
18
for i in range(1,10):
    print("Experiment ",i)
    learner = RALearner(labels, encoder=RANEncoder())
    exp = sut_m1
19
20
    for trace in exp.traces:
        learner.add(trace)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
21
22
23
24
25
26
27
28
29
    (_, ra, m) = learner._learn_model(exp.nr_locations,exp.nr_locations+1,exp.nr_registers)
    if m is not None:
        model = ra.export(m)
        loc = ra.locations
        lbl = ra.labels[labels[0]]
        fresh = ra.fresh
        check_ra_against_obs(learner, model, m, exp)
    else:
        print("unsat")