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

97.26

/util/src/main/java/net/automatalib/util/automaton/equivalence/DeterministicEquivalenceTest.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.ArrayDeque;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.Objects;
import java.util.Queue;

import net.automatalib.automaton.UniversalDeterministicAutomaton;
import net.automatalib.automaton.concept.StateIDs;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.Nullable;

public final class DeterministicEquivalenceTest {

    private static final int MAP_THRESHOLD = 10_000;

    private DeterministicEquivalenceTest() {
        // prevent instantiation
    }

    public static <I, S, T, SP, TP, S2, T2, SP2, TP2> @Nullable Word<I> findSeparatingWord(
            UniversalDeterministicAutomaton<S, I, T, SP, TP> reference,
            UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
            Collection<? extends I> inputs) {
        int refSize = reference.size();
        int totalStates = refSize * other.size();

        if (totalStates > MAP_THRESHOLD) {
            return findSeparatingWordLarge(reference, other, inputs);
        }

        S refInit = reference.getInitialState();
        S2 otherInit = other.getInitialState();

        if (refInit == null || otherInit == null) {
            return refInit == null && otherInit == null ? null : Word.epsilon();
        }

        SP refStateProp = reference.getStateProperty(refInit);
        SP2 otherStateProp = other.getStateProperty(otherInit);

        if (!Objects.equals(refStateProp, otherStateProp)) {
            return Word.epsilon();
        }

        Queue<StatePair<S, S2>> bfsQueue = new ArrayDeque<>();
        bfsQueue.add(new StatePair<>(refInit, otherInit));

        StateIDs<S> refStateIds = reference.stateIDs();
        StateIDs<S2> otherStateIds = other.stateIDs();

        StatePair<S, S2> currPair;
        int lastId = otherStateIds.getStateId(otherInit) * refSize + refStateIds.getStateId(refInit);

        @SuppressWarnings("unchecked")
        Pred<I>[] preds = new Pred[totalStates];
        preds[lastId] = new Pred<>();

        int currDepth = 0;
        int inCurrDepth = 1;
        int inNextDepth = 0;

        I lastSym = null;

        bfs:
        while ((currPair = bfsQueue.poll()) != null) {
            S refState = currPair.ref;
            S2 otherState = currPair.other;

            int currId = otherStateIds.getStateId(otherState) * refSize + refStateIds.getStateId(refState);
            lastId = currId;

            for (I in : inputs) {
                lastSym = in;
                T refTrans = reference.getTransition(refState, in);
                T2 otherTrans = other.getTransition(otherState, in);

                if (refTrans == null || otherTrans == null) {
                    if (refTrans == null && otherTrans == null) {
                        continue;
                    } else {
                        break bfs;
                    }
                }

                TP refProp = reference.getTransitionProperty(refTrans);
                TP2 otherProp = other.getTransitionProperty(otherTrans);
                if (!Objects.equals(refProp, otherProp)) {
                    break bfs;
                }

                S refSucc = reference.getSuccessor(refTrans);
                S2 otherSucc = other.getSuccessor(otherTrans);

                int succId = otherStateIds.getStateId(otherSucc) * refSize + refStateIds.getStateId(refSucc);

                if (preds[succId] == null) {
                    refStateProp = reference.getStateProperty(refSucc);
                    otherStateProp = other.getStateProperty(otherSucc);

                    if (!Objects.equals(refStateProp, otherStateProp)) {
                        break bfs;
                    }

                    preds[succId] = new Pred<>(currId, in);
                    bfsQueue.add(new StatePair<>(refSucc, otherSucc));
                    inNextDepth++;
                }
            }

            lastSym = null;

            // Next level in BFS reached
            if (--inCurrDepth == 0) {
                inCurrDepth = inNextDepth;
                inNextDepth = 0;
                currDepth++;
            }
        }

        if (lastSym == null) {
            return null;
        }

        @SuppressWarnings("nullness") // we make sure to set each index to a value of type I
        WordBuilder<I> sep = new WordBuilder<>(null, currDepth + 1);
        int index = currDepth;
        sep.setSymbol(index--, lastSym);

        Pred<I> pred = preds[lastId];
        while (pred.id >= 0) {
            sep.setSymbol(index--, pred.symbol);
            pred = preds[pred.id];
        }

        return sep.toWord();
    }

    public static <I, S, T, SP, TP, S2, T2, SP2, TP2> @Nullable Word<I> findSeparatingWordLarge(
            UniversalDeterministicAutomaton<S, I, T, SP, TP> reference,
            UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
            Collection<? extends I> inputs) {
        S refInit = reference.getInitialState();
        S2 otherInit = other.getInitialState();

        if (refInit == null || otherInit == null) {
            return refInit == null && otherInit == null ? null : Word.epsilon();
        }

        SP refStateProp = reference.getStateProperty(refInit);
        SP2 otherStateProp = other.getStateProperty(otherInit);

        if (!Objects.equals(refStateProp, otherStateProp)) {
            return Word.epsilon();
        }

        Queue<StatePair<S, S2>> bfsQueue = new ArrayDeque<>();
        bfsQueue.add(new StatePair<>(refInit, otherInit));

        int refSize = reference.size();

        StateIDs<S> refStateIds = reference.stateIDs();
        StateIDs<S2> otherStateIds = other.stateIDs();

        StatePair<S, S2> currPair;
        int lastId = otherStateIds.getStateId(otherInit) * refSize + refStateIds.getStateId(refInit);

        //TIntObjectMap<Pred<I>> preds = new TIntObjectHashMap<>();
        Map<Integer, Pred<I>> preds = new HashMap<>(); // TODO: replace by primitive specialization
        preds.put(lastId, new Pred<>());

        int currDepth = 0;
        int inCurrDepth = 1;
        int inNextDepth = 0;

        I lastSym = null;

        bfs:
        while ((currPair = bfsQueue.poll()) != null) {
            S refState = currPair.ref;
            S2 otherState = currPair.other;

            int currId = otherStateIds.getStateId(otherState) * refSize + refStateIds.getStateId(refState);
            lastId = currId;

            for (I in : inputs) {
                lastSym = in;
                T refTrans = reference.getTransition(refState, in);
                T2 otherTrans = other.getTransition(otherState, in);

                if (refTrans == null || otherTrans == null) {
                    if (refTrans == null && otherTrans == null) {
                        continue;
                    } else {
                        break bfs;
                    }
                }

                TP refProp = reference.getTransitionProperty(refTrans);
                TP2 otherProp = other.getTransitionProperty(otherTrans);
                if (!Objects.equals(refProp, otherProp)) {
                    break bfs;
                }

                S refSucc = reference.getSuccessor(refTrans);
                S2 otherSucc = other.getSuccessor(otherTrans);

                int succId = otherStateIds.getStateId(otherSucc) * refSize + refStateIds.getStateId(refSucc);

                if (preds.get(succId) == null) {
                    refStateProp = reference.getStateProperty(refSucc);
                    otherStateProp = other.getStateProperty(otherSucc);

                    if (!Objects.equals(refStateProp, otherStateProp)) {
                        break bfs;
                    }

                    preds.put(succId, new Pred<>(currId, in));
                    bfsQueue.add(new StatePair<>(refSucc, otherSucc));
                    inNextDepth++;
                }
            }

            lastSym = null;

            // Next level in BFS reached
            if (--inCurrDepth == 0) {
                inCurrDepth = inNextDepth;
                inNextDepth = 0;
                currDepth++;
            }
        }

        if (lastSym == null) {
            return null;
        }

        @SuppressWarnings("nullness") // we make sure to set each index to a value of type I
        WordBuilder<I> sep = new WordBuilder<>(null, currDepth + 1);
        int index = currDepth;
        sep.setSymbol(index--, lastSym);

        Pred<I> pred = preds.get(lastId);
        assert pred != null;
        while (pred.id >= 0) {
            sep.setSymbol(index--, pred.symbol);
            pred = preds.get(pred.id);
            assert pred != null;
        }

        return sep.toWord();
    }

    private static final class StatePair<S, S2> {

        public final S ref;
        public final S2 other;

        StatePair(S ref, S2 other) {
            this.ref = ref;
            this.other = other;
        }
    }

    private static final class Pred<I> {

        public final int id;
        public final I symbol;

        @SuppressWarnings("nullness") // we check this special element using its id value
        Pred() {
            this.id = -1;
            this.symbol = null;
        }

        Pred(int id, I input) {
            this.id = id;
            this.symbol = input;
        }
    }
}

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.ArrayDeque;
19	import java.util.Collection;
20	import java.util.HashMap;
21	import java.util.Map;
22	import java.util.Objects;
23	import java.util.Queue;
24
25	import net.automatalib.automaton.UniversalDeterministicAutomaton;
26	import net.automatalib.automaton.concept.StateIDs;
27	import net.automatalib.word.Word;
28	import net.automatalib.word.WordBuilder;
29	import org.checkerframework.checker.nullness.qual.Nullable;
30
31	public final class DeterministicEquivalenceTest {	2✔
32
33	private static final int MAP_THRESHOLD = 10_000;
34
35	private DeterministicEquivalenceTest() {
36	// prevent instantiation
37	}
38
39	public static <I, S, T, SP, TP, S2, T2, SP2, TP2> @Nullable Word<I> findSeparatingWord(
40	UniversalDeterministicAutomaton<S, I, T, SP, TP> reference,
41	UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
42	Collection<? extends I> inputs) {
43	int refSize = reference.size();	2✔
44	int totalStates = refSize * other.size();	2✔
45
46	if (totalStates > MAP_THRESHOLD) {	2✔
47	return findSeparatingWordLarge(reference, other, inputs);	2✔
48	}
49
50	S refInit = reference.getInitialState();	2✔
51	S2 otherInit = other.getInitialState();	2✔
52
53	if (refInit == null \|\| otherInit == null) {	2✔
54	return refInit == null && otherInit == null ? null : Word.epsilon();	2✔
55	}
56
57	SP refStateProp = reference.getStateProperty(refInit);	2✔
58	SP2 otherStateProp = other.getStateProperty(otherInit);	2✔
59
60	if (!Objects.equals(refStateProp, otherStateProp)) {	2✔
61	return Word.epsilon();	2✔
62	}
63
64	Queue<StatePair<S, S2>> bfsQueue = new ArrayDeque<>();	2✔
65	bfsQueue.add(new StatePair<>(refInit, otherInit));	2✔
66
67	StateIDs<S> refStateIds = reference.stateIDs();	2✔
68	StateIDs<S2> otherStateIds = other.stateIDs();	2✔
69
70	StatePair<S, S2> currPair;
71	int lastId = otherStateIds.getStateId(otherInit) * refSize + refStateIds.getStateId(refInit);	2✔
72
73	@SuppressWarnings("unchecked")
74	Pred<I>[] preds = new Pred[totalStates];	2✔
75	preds[lastId] = new Pred<>();	2✔
76
77	int currDepth = 0;	2✔
78	int inCurrDepth = 1;	2✔
79	int inNextDepth = 0;	2✔
80
81	I lastSym = null;	2✔
82
83	bfs:
84	while ((currPair = bfsQueue.poll()) != null) {	2✔
85	S refState = currPair.ref;	2✔
86	S2 otherState = currPair.other;	2✔
87
88	int currId = otherStateIds.getStateId(otherState) * refSize + refStateIds.getStateId(refState);	2✔
89	lastId = currId;	2✔
90
91	for (I in : inputs) {	2✔
92	lastSym = in;	2✔
93	T refTrans = reference.getTransition(refState, in);	2✔
94	T2 otherTrans = other.getTransition(otherState, in);	2✔
95
96	if (refTrans == null \|\| otherTrans == null) {	2✔
97	if (refTrans == null && otherTrans == null) {	2✔
98	continue;	2✔
99	} else {
100	break bfs;
101	}
102	}
103
104	TP refProp = reference.getTransitionProperty(refTrans);	2✔
105	TP2 otherProp = other.getTransitionProperty(otherTrans);	2✔
106	if (!Objects.equals(refProp, otherProp)) {	2✔
107	break bfs;	2✔
108	}
109
110	S refSucc = reference.getSuccessor(refTrans);	2✔
111	S2 otherSucc = other.getSuccessor(otherTrans);	2✔
112
113	int succId = otherStateIds.getStateId(otherSucc) * refSize + refStateIds.getStateId(refSucc);	2✔
114
115	if (preds[succId] == null) {	2✔
116	refStateProp = reference.getStateProperty(refSucc);	2✔
117	otherStateProp = other.getStateProperty(otherSucc);	2✔
118
119	if (!Objects.equals(refStateProp, otherStateProp)) {	2✔
120	break bfs;	1✔
121	}
122
123	preds[succId] = new Pred<>(currId, in);	2✔
124	bfsQueue.add(new StatePair<>(refSucc, otherSucc));	2✔
125	inNextDepth++;	2✔
126	}
127	}	2✔
128
129	lastSym = null;	2✔
130
131	// Next level in BFS reached
132	if (--inCurrDepth == 0) {	2✔
133	inCurrDepth = inNextDepth;	2✔
134	inNextDepth = 0;	2✔
135	currDepth++;	2✔
136	}
137	}	2✔
138
139	if (lastSym == null) {	2✔
140	return null;	2✔
141	}
142
143	@SuppressWarnings("nullness") // we make sure to set each index to a value of type I
144	WordBuilder<I> sep = new WordBuilder<>(null, currDepth + 1);	2✔
145	int index = currDepth;	2✔
146	sep.setSymbol(index--, lastSym);	2✔
147
148	Pred<I> pred = preds[lastId];	2✔
149	while (pred.id >= 0) {	2✔
150	sep.setSymbol(index--, pred.symbol);	1✔
151	pred = preds[pred.id];	1✔
152	}
153
154	return sep.toWord();	2✔
155	}
156
157	public static <I, S, T, SP, TP, S2, T2, SP2, TP2> @Nullable Word<I> findSeparatingWordLarge(
158	UniversalDeterministicAutomaton<S, I, T, SP, TP> reference,
159	UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
160	Collection<? extends I> inputs) {
161	S refInit = reference.getInitialState();	2✔
162	S2 otherInit = other.getInitialState();	2✔
163
164	if (refInit == null \|\| otherInit == null) {	2✔
165	return refInit == null && otherInit == null ? null : Word.epsilon();	2✔
166	}
167
168	SP refStateProp = reference.getStateProperty(refInit);	2✔
169	SP2 otherStateProp = other.getStateProperty(otherInit);	2✔
170
171	if (!Objects.equals(refStateProp, otherStateProp)) {	2✔
172	return Word.epsilon();	×
173	}
174
175	Queue<StatePair<S, S2>> bfsQueue = new ArrayDeque<>();	2✔
176	bfsQueue.add(new StatePair<>(refInit, otherInit));	2✔
177
178	int refSize = reference.size();	2✔
179
180	StateIDs<S> refStateIds = reference.stateIDs();	2✔
181	StateIDs<S2> otherStateIds = other.stateIDs();	2✔
182
183	StatePair<S, S2> currPair;
184	int lastId = otherStateIds.getStateId(otherInit) * refSize + refStateIds.getStateId(refInit);	2✔
185
186	//TIntObjectMap<Pred<I>> preds = new TIntObjectHashMap<>();
187	Map<Integer, Pred<I>> preds = new HashMap<>(); // TODO: replace by primitive specialization	2✔
188	preds.put(lastId, new Pred<>());	2✔
189
190	int currDepth = 0;	2✔
191	int inCurrDepth = 1;	2✔
192	int inNextDepth = 0;	2✔
193
194	I lastSym = null;	2✔
195
196	bfs:
197	while ((currPair = bfsQueue.poll()) != null) {	2✔
198	S refState = currPair.ref;	2✔
199	S2 otherState = currPair.other;	2✔
200
201	int currId = otherStateIds.getStateId(otherState) * refSize + refStateIds.getStateId(refState);	2✔
202	lastId = currId;	2✔
203
204	for (I in : inputs) {	2✔
205	lastSym = in;	2✔
206	T refTrans = reference.getTransition(refState, in);	2✔
207	T2 otherTrans = other.getTransition(otherState, in);	2✔
208
209	if (refTrans == null \|\| otherTrans == null) {	2✔
210	if (refTrans == null && otherTrans == null) {	2✔
211	continue;	2✔
212	} else {
213	break bfs;
214	}
215	}
216
217	TP refProp = reference.getTransitionProperty(refTrans);	2✔
218	TP2 otherProp = other.getTransitionProperty(otherTrans);	2✔
219	if (!Objects.equals(refProp, otherProp)) {	2✔
220	break bfs;	2✔
221	}
222
223	S refSucc = reference.getSuccessor(refTrans);	2✔
224	S2 otherSucc = other.getSuccessor(otherTrans);	2✔
225
226	int succId = otherStateIds.getStateId(otherSucc) * refSize + refStateIds.getStateId(refSucc);	2✔
227
228	if (preds.get(succId) == null) {	2✔
229	refStateProp = reference.getStateProperty(refSucc);	2✔
230	otherStateProp = other.getStateProperty(otherSucc);	2✔
231
232	if (!Objects.equals(refStateProp, otherStateProp)) {	2✔
233	break bfs;	2✔
234	}
235
236	preds.put(succId, new Pred<>(currId, in));	2✔
237	bfsQueue.add(new StatePair<>(refSucc, otherSucc));	2✔
238	inNextDepth++;	2✔
239	}
240	}	2✔
241
242	lastSym = null;	2✔
243
244	// Next level in BFS reached
245	if (--inCurrDepth == 0) {	2✔
246	inCurrDepth = inNextDepth;	2✔
247	inNextDepth = 0;	2✔
248	currDepth++;	2✔
249	}
250	}	2✔
251
252	if (lastSym == null) {	2✔
253	return null;	2✔
254	}
255
256	@SuppressWarnings("nullness") // we make sure to set each index to a value of type I
257	WordBuilder<I> sep = new WordBuilder<>(null, currDepth + 1);	2✔
258	int index = currDepth;	2✔
259	sep.setSymbol(index--, lastSym);	2✔
260
261	Pred<I> pred = preds.get(lastId);	2✔
262	assert pred != null;	2✔
263	while (pred.id >= 0) {	2✔
264	sep.setSymbol(index--, pred.symbol);	×
265	pred = preds.get(pred.id);	×
266	assert pred != null;	×
267	}
268
269	return sep.toWord();	2✔
270	}
271
272	private static final class StatePair<S, S2> {
273
274	public final S ref;
275	public final S2 other;
276
277	StatePair(S ref, S2 other) {	2✔
278	this.ref = ref;	2✔
279	this.other = other;	2✔
280	}	2✔
281	}
282
283	private static final class Pred<I> {
284
285	public final int id;
286	public final I symbol;
287
288	@SuppressWarnings("nullness") // we check this special element using its id value
289	Pred() {	2✔
290	this.id = -1;	2✔
291	this.symbol = null;	2✔
292	}	2✔
293
294	Pred(int id, I input) {	2✔
295	this.id = id;	2✔
296	this.symbol = input;	2✔
297	}	2✔
298	}
299	}

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