6685076669

Committed 29 Oct 2023 06:24PM UTC coverage: 89.857% (+0.06%) from 89.796%

Build # 6685076669

Build Type

push

github

Committed by

mtf90

Commit Message

align core packages with api packages

Run Details

15814 of 17599 relevant lines covered (89.86%)

1.67 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

89.06

/util/src/main/java/net/automatalib/util/automaton/equivalence/Bisimulation.java

/* Copyright (C) 2013-2023 TU Dortmund
 * This file is part of AutomataLib, http://www.automatalib.net/.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package net.automatalib.util.automaton.equivalence;

import java.util.Collection;
import java.util.Objects;
import java.util.Set;

import com.google.common.collect.Sets;
import net.automatalib.automaton.Automaton;
import net.automatalib.common.util.Pair;

public final class Bisimulation {

    private Bisimulation() {
        // prevent instantiation
    }

    public static <AS, I, AT, A extends Automaton<AS, I, AT>, BS, BT, B extends Automaton<BS, I, BT>> Set<Pair<AS, BS>> bisimulationEquivalenceRelation(
            A a,
            B b,
            Collection<I> inputs) {

        Set<Pair<AS, BS>> bisim = Sets.newHashSetWithExpectedSize(a.size() * b.size());
        Set<Pair<AS, BS>> change = Sets.newHashSetWithExpectedSize(a.size() * b.size());

        boolean empty;

        for (AS p : a.getStates()) {
            for (BS q : b.getStates()) {

                empty = true;
                for (I sym : inputs) {
                    empty &= a.getTransitions(p, sym).isEmpty() && b.getTransitions(q, sym).isEmpty();
                    if (!a.getTransitions(p, sym).isEmpty() && !b.getTransitions(q, sym).isEmpty()) {
                        change.add(Pair.of(p, q));
                        break;
                    }
                }

                if (empty) {
                    change.add(Pair.of(p, q));
                }
            }
        }

        Set<Pair<AS, BS>> swap;
        boolean forall, exists;
        while (!bisim.equals(change)) {
            swap = change;
            change = bisim;
            bisim = swap;
            change.clear();

            for (Pair<AS, BS> p : bisim) {

                forall = true;
                for (I sym : inputs) {
                    for (AT t : a.getTransitions(p.getFirst(), sym)) {

                        exists = false;
                        for (BT f : b.getTransitions(p.getSecond(), sym)) {
                            for (Pair<AS, BS> s : bisim) {
                                if (Objects.equals(a.getSuccessor(t), s.getFirst()) &&
                                    Objects.equals(b.getSuccessor(f), s.getSecond())) {
                                    exists = true;
                                    break;
                                }
                            }
                            if (exists) {
                                break;
                            }
                        }
                        if (!exists) {
                            forall = false;
                            break;
                        }
                    }
                }

                if (!forall) {
                    continue;
                }

                for (I sym : inputs) {
                    for (BT f : b.getTransitions(p.getSecond(), sym)) {

                        exists = false;
                        for (AT t : a.getTransitions(p.getFirst(), sym)) {
                            for (Pair<AS, BS> s : bisim) {
                                if (Objects.equals(b.getSuccessor(f), s.getSecond()) &&
                                    Objects.equals(a.getSuccessor(t), s.getFirst())) {
                                    exists = true;
                                    break;
                                }
                            }
                            if (exists) {
                                break;
                            }
                        }
                        if (!exists) {
                            forall = false;
                            break;
                        }
                    }
                }

                if (forall) {
                    change.add(p);
                }
            }
        }

        return change;
    }
}

1	/* Copyright (C) 2013-2023 TU Dortmund
2	* This file is part of AutomataLib, http://www.automatalib.net/.
3	*
4	* Licensed under the Apache License, Version 2.0 (the "License");
5	* you may not use this file except in compliance with the License.
6	* You may obtain a copy of the License at
7	*
8	* http://www.apache.org/licenses/LICENSE-2.0
9	*
10	* Unless required by applicable law or agreed to in writing, software
11	* distributed under the License is distributed on an "AS IS" BASIS,
12	* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13	* See the License for the specific language governing permissions and
14	* limitations under the License.
15	*/
16	package net.automatalib.util.automaton.equivalence;
17
18	import java.util.Collection;
19	import java.util.Objects;
20	import java.util.Set;
21
22	import com.google.common.collect.Sets;
23	import net.automatalib.automaton.Automaton;
24	import net.automatalib.common.util.Pair;
25
26	public final class Bisimulation {
27
28	private Bisimulation() {
29	// prevent instantiation
30	}
31
32	public static <AS, I, AT, A extends Automaton<AS, I, AT>, BS, BT, B extends Automaton<BS, I, BT>> Set<Pair<AS, BS>> bisimulationEquivalenceRelation(
33	A a,
34	B b,
35	Collection<I> inputs) {
36
37	Set<Pair<AS, BS>> bisim = Sets.newHashSetWithExpectedSize(a.size() * b.size());	2✔
38	Set<Pair<AS, BS>> change = Sets.newHashSetWithExpectedSize(a.size() * b.size());	2✔
39
40	boolean empty;
41
42	for (AS p : a.getStates()) {	2✔
43	for (BS q : b.getStates()) {	2✔
44
45	empty = true;	2✔
46	for (I sym : inputs) {	2✔
47	empty &= a.getTransitions(p, sym).isEmpty() && b.getTransitions(q, sym).isEmpty();	2✔
48	if (!a.getTransitions(p, sym).isEmpty() && !b.getTransitions(q, sym).isEmpty()) {	2✔
49	change.add(Pair.of(p, q));	2✔
50	break;	2✔
51	}
52	}	×
53
54	if (empty) {	2✔
55	change.add(Pair.of(p, q));	×
56	}
57	}	2✔
58	}	2✔
59
60	Set<Pair<AS, BS>> swap;
61	boolean forall, exists;
62	while (!bisim.equals(change)) {	2✔
63	swap = change;	2✔
64	change = bisim;	2✔
65	bisim = swap;	2✔
66	change.clear();	2✔
67
68	for (Pair<AS, BS> p : bisim) {	2✔
69
70	forall = true;	2✔
71	for (I sym : inputs) {	2✔
72	for (AT t : a.getTransitions(p.getFirst(), sym)) {	2✔
73
74	exists = false;	2✔
75	for (BT f : b.getTransitions(p.getSecond(), sym)) {	2✔
76	for (Pair<AS, BS> s : bisim) {	2✔
77	if (Objects.equals(a.getSuccessor(t), s.getFirst()) &&	2✔
78	Objects.equals(b.getSuccessor(f), s.getSecond())) {	2✔
79	exists = true;	2✔
80	break;	2✔
81	}
82	}	2✔
83	if (exists) {	2✔
84	break;	2✔
85	}
86	}	×
87	if (!exists) {	2✔
88	forall = false;	×
89	break;	×
90	}
91	}	2✔
92	}	2✔
93
94	if (!forall) {	2✔
95	continue;	×
96	}
97
98	for (I sym : inputs) {	2✔
99	for (BT f : b.getTransitions(p.getSecond(), sym)) {	2✔
100
101	exists = false;	2✔
102	for (AT t : a.getTransitions(p.getFirst(), sym)) {	2✔
103	for (Pair<AS, BS> s : bisim) {	2✔
104	if (Objects.equals(b.getSuccessor(f), s.getSecond()) &&	2✔
105	Objects.equals(a.getSuccessor(t), s.getFirst())) {	2✔
106	exists = true;	2✔
107	break;	2✔
108	}
109	}	2✔
110	if (exists) {	2✔
111	break;	2✔
112	}
113	}	×
114	if (!exists) {	2✔
115	forall = false;	2✔
116	break;	2✔
117	}
118	}	2✔
119	}	2✔
120
121	if (forall) {	2✔
122	change.add(p);	2✔
123	}
124	}	2✔
125	}
126
127	return change;	2✔
128	}
129	}

LearnLib / automatalib / 6685076669

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous