bisimulation.py 2.47 KB
Newer Older
1

2
3
4
5
def bisimilar(system1, system2, startState1=0, startState2=0):
    # starting from given states
    state1 = (startState1,)
    state2 = (startState2,)
6
7
8

    past = set()
    wait = set()
Michele's avatar
Michele committed
9
10
11
    trace = ()
    wait.add((state1, state2, trace))

12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
    while wait:
        current = wait.pop()
        past.add((current[0],current[1]))

        enabledLabels_1 = set()
        for state in current[0]:
            enabledLabels_1 = enabledLabels_1.union(system1.outputs(state))
            enabledLabels_1 = enabledLabels_1.union(system1.inputs(state))

        enabledLabels_2 = set()
        for state in current[1]:
            enabledLabels_2 = enabledLabels_2.union(system2.outputs(state))
            enabledLabels_2 = enabledLabels_2.union(system2.inputs(state))

        if enabledLabels_1 != enabledLabels_2:
            # Proved not bisimilar, return False
Michele's avatar
Michele committed
28
            return (current[0],current[1],enabledLabels_1,enabledLabels_2,current[2])
29
30
31
32
33
34
35
36
37
38
39
40
41
        else:
            # Add new pair of states for further checking bisimilarity
            transitions_1 = system1.getTransitions()
            transitions_2 = system2.getTransitions()
            for label in enabledLabels_1:
                newStates2 = set()
                newStates1 = set()
                for state in current[0]:
                    key = (state, label)
                    if key not in transitions_1:
                        if (label == system1.getQuiescence() and
                            label in system1.outputs(state)):
                            newStates1.add(state)
Michele's avatar
Michele committed
42
                        continue
43
44
45
46
47
48
49
50
51
52
53
                    for nextState in transitions_1[key]:
                        newStates1.add(nextState)
                tupledStates1 = tuple(newStates1)
                tupledStates1 = tuple(sorted(tupledStates1))

                for state in current[1]:
                    key = (state, label)
                    if key not in transitions_2:
                        if (label == system2.getQuiescence() and
                            label in system2.outputs(state)):
                            newStates2.add(state)
Michele's avatar
Michele committed
54
                        continue
55
56
57
58
59
60
                    for nextState in transitions_2[key]:
                        newStates2.add(nextState)
                tupledStates2 = tuple(newStates2)
                tupledStates2 = tuple(sorted(tupledStates2))

                if (tupledStates1, tupledStates2) not in past:
Michele's avatar
Michele committed
61
                    wait.add((tupledStates1, tupledStates2, current[2]+(label,)))
62
63

    return True