fa.py 3.54 KB
Newer Older
1
2
3
4
5
6
import collections
from abc import ABCMeta, abstractmethod

import z3
from define import enum, Automaton
import model.fa
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
7
from model import Transition
8
9


10
class FSM(Automaton,metaclass=ABCMeta):
11
12
13
14
    @abstractmethod
    def __init__(self, num_states):
        self.State, self.states = enum('State', ['state{0}'.format(i) for i in range(num_states)])

15
class DFA(FSM):
16
17
18
19
20
21
22
23
    def __init__(self, labels, num_states):
        super.__init__(num_states)
        self.Label, elements = enum('Label', labels)
        self.labels = {labels[i]: elements[i] for i in range(len(labels))}
        self.transition = z3.Function('transition', self.State, self.Label, self.State)
        self.output = z3.Function('output', self.State, z3.BoolSort())

    def export(self, model : z3.ModelRef) -> model.fa.DFA:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
24
25
26
        builder = DFABuilder(self)
        dfa = builder.build_dfa(self)
        return dfa
27
28


29
class MealyMachine(FSM):
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
    def __init__(self, input_labels, output_labels, num_states):
        super.__init__(num_states)
        self.Input, elements = enum('Input', input_labels)
        self.inputs = {input_labels[i]: elements[i] for i in range(len(input_labels))}
        self.Output, elements = enum('Output', output_labels)
        self.outputs = {output_labels[i]: elements[i] for i in range(len(output_labels))}
        self.transition = z3.Function('transition', self.State, self.Input, self.State)
        self.output = z3.Function('output', self.State, self.Input, self.Output)

    def export(self, model : z3.ModelRef) -> model.fa.MealyMachine:
        builder = MealyMachineBuilder(self)
        mealy = builder.build_mealy(model)
        return mealy


class MealyMachineBuilder(object):
    def __init__(self, mm : MealyMachine):
        super().__init__()
        self.mm = mm

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
50
    def build_mealy(self, m : z3.ModelRef) -> model.fa.MealyMachine:
51
        tr = FATranslator()
52
53
54
55
56
        mut_mm =  model.fa.MutableMealyMachine()
        for state in self.mm.states:
            mut_mm.add_state(tr.z3_to_state(state))
        for state in self.mm.states:
            for inp in self.mm.inputs:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
57
58
                output = m.eval(self.mm.output(state, inp))
                to_state = m.eval(self.mm.transition(state, inp))
59
60
61
62
63
64
65
                trans = model.fa.IOTransition(
                    tr.z3_to_state(state),
                    tr.z3_to_label(inp),
                    tr.z3_to_label(output),
                    tr.z3_to_state(to_state))

        return mut_mm.to_immutable()
66

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
class DFABuilder(object):
    def __init__(self, dfa : DFA):
        super().__init__()
        self.dfa = dfa

    def build_dfa(self, m : z3.ModelRef) -> model.fa.DFA:
        tr = FATranslator()
        mut_dfa =  model.fa.MutableDFA()
        for state in self.dfa.states:
            accepting = m.eval(self.dfa.output(state))
            mut_dfa.add_state(tr.z3_to_state(state), tr.z3_to_bool(accepting))
        for state in self.dfa.states:
            for labels in self.dfa.labels:
                to_state = m.eval(self.dfa.transition(state, labels))
                trans = Transition(
                    tr.z3_to_state(state),
                    tr.z3_to_label(labels),
                    tr.z3_to_state(to_state))

        return mut_dfa.to_immutable()
87
88
89
90
91
92
93
94
95
96
97
98
99
100

class FATranslator(object):
    """Provides translation from z3 constants to RA elements. """
    def __init__(self, fa:FSM ):
        self.fa = fa

    def z3_to_bool(self, z3bool):
        return str(z3bool) == "True"

    def z3_to_state(self, z3state):
        return "q"+str(self.fa.states.index(z3state))

    def z3_to_label(self, z3label):
        return str(z3label)