fa.py 1.51 KB
Newer Older
1
2
3
4
5
6
import z3

from encode.ra import RAEncoder
from learn import Learner
import model.fa

Rick Smetsers's avatar
Rick Smetsers committed
7
8
9
10
11
import z3

from encode.fa import DFAEncoder, MealyEncoder
from learn import Learner
import model.fa
12

Rick Smetsers's avatar
Rick Smetsers committed
13
14
class FALearner(Learner):
    def __init__(self, labels, encoder, solver=None, verbose=False):
15
16
17
        if not solver:
            solver = z3.Solver()
        self.solver = solver
Rick Smetsers's avatar
Rick Smetsers committed
18
        self.encoder = encoder
19
20
21
22
23
        self.verbose = verbose

    def add(self, trace):
        self.encoder.add(trace)

Rick Smetsers's avatar
Rick Smetsers committed
24
25
    def model(self, min_states=1, max_states=20):
        (succ, fa, m) = self._learn_model(min_states=min_states,
26
27
                                        max_states=max_states)
        if succ:
Rick Smetsers's avatar
Rick Smetsers committed
28
            return fa.export(m)
29
30
31
        return None

    def _learn_model(self, min_states=1, max_states=20):
Rick Smetsers's avatar
Rick Smetsers committed
32
33
34
        """generates the definition and model for an fa whose traces include the traces added so far"""
        for num_states in range(min_states, max_states + 1):
            fa, constraints = self.encoder.build(num_states)
35
36
37
38
            self.solver.add(constraints)
            result = self.solver.check()
            if self.verbose:
                print("Learning with {0} states. Result: {1}"
Rick Smetsers's avatar
Rick Smetsers committed
39
                  .format(num_states, result))
40
41
42
            if result == z3.sat:
                model = self.solver.model()
                self.solver.reset()
Rick Smetsers's avatar
Rick Smetsers committed
43
                return (True, fa, model)
44
45
46
47
48
            else:
                self.solver.reset()
                # TODO: process the unsat core?
                pass
        return (False, None, None)