13138848026

Committed 04 Feb 2025 02:53PM UTC coverage: 92.108% (+2.2%) from 89.877%

Build # 13138848026

Build Type

push

github

Committed by

mtf90

Commit Message

[maven-release-plugin] prepare release automatalib-0.12.0

Run Details

16609 of 18032 relevant lines covered (92.11%)

1.7 hits per line

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

98.12

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

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of AutomataLib <https://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.Objects;
import java.util.Queue;

import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.UniversalDeterministicAutomaton;
import net.automatalib.automaton.concept.InputAlphabetHolder;
import net.automatalib.automaton.concept.StateIDs;
import net.automatalib.common.util.IntDisjointSets;
import net.automatalib.common.util.UnionFindRemSP;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Implements Hopcroft and Karp's equivalence test, as described in <a href="https://doi.org/1813/5958">A linear
 * algorithm for testing equivalence of finite automata</a>.
 */
@SuppressWarnings("PMD.TestClassWithoutTestCases") // not a traditional test class
public final class NearLinearEquivalenceTest {

    private NearLinearEquivalenceTest() {
        // prevent instantiation
    }

    public static <S, I> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<S, I, ?, ?, ?> target,
                                                              S init1,
                                                              S init2,
                                                              Collection<? extends I> inputs) {
        return findSeparatingWord(target, init1, init2, inputs, false);
    }

    /**
     * Find a separating word for two states in a given automaton.
     *
     * @param target
     *         the automaton
     * @param init1
     *         the first state
     * @param init2
     *         the second state
     * @param inputs
     *         the inputs to consider for a separating word
     * @param ignoreUndefinedTransitions
     *         if {@code true}, undefined transitions are not considered to distinguish two states, if {@code false} an
     *         undefined and defined transition are considered to distinguish two states
     * @param <S>
     *         automaton state type
     * @param <I>
     *         input alphabet type
     * @param <T>
     *         automaton transition type
     *
     * @return A word separating the two states, {@code null} if no such word can be found
     */
    public static <S, I, T> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<S, I, T, ?, ?> target,
                                                                 S init1,
                                                                 S init2,
                                                                 Collection<? extends I> inputs,
                                                                 boolean ignoreUndefinedTransitions) {

        Object sprop1 = target.getStateProperty(init1);
        Object sprop2 = target.getStateProperty(init2);

        if (!Objects.equals(sprop1, sprop2)) {
            return Word.epsilon();
        }

        IntDisjointSets uf = new UnionFindRemSP(target.size());

        StateIDs<S> stateIds = target.stateIDs();

        int id1 = stateIds.getStateId(init1), id2 = stateIds.getStateId(init2);

        uf.link(id1, id2);

        Queue<Record<S, S, I>> queue = new ArrayDeque<>();

        queue.add(new Record<>(init1, init2));

        I lastSym = null;
        Record<S, S, I> current;

        explore:
        while ((current = queue.poll()) != null) {
            S state1 = current.state1;
            S state2 = current.state2;

            for (I sym : inputs) {
                T trans1 = target.getTransition(state1, sym);
                T trans2 = target.getTransition(state2, sym);

                if (ignoreUndefinedTransitions && (trans1 == null || trans2 == null)) {
                    continue;
                } else if (trans1 == null) {
                    if (trans2 == null) {
                        continue;
                    }
                    lastSym = sym;
                    break explore;
                } else if (trans2 == null) {
                    lastSym = sym;
                    break explore;
                }

                Object tprop1 = target.getTransitionProperty(trans1);
                Object tprop2 = target.getTransitionProperty(trans2);

                if (!Objects.equals(tprop1, tprop2)) {
                    lastSym = sym;
                    break explore;
                }

                S succ1 = target.getSuccessor(trans1);
                S succ2 = target.getSuccessor(trans2);

                id1 = stateIds.getStateId(succ1);
                id2 = stateIds.getStateId(succ2);

                int r1 = uf.find(id1), r2 = uf.find(id2);

                if (r1 == r2) {
                    continue;
                }

                sprop1 = target.getStateProperty(succ1);
                sprop2 = target.getStateProperty(succ2);

                if (!Objects.equals(sprop1, sprop2)) {
                    lastSym = sym;
                    break explore;
                }

                uf.link(r1, r2);

                queue.add(new Record<>(succ1, succ2, sym, current));
            }
        }

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

        int position = current.depth + 1;

        @SuppressWarnings("argument") // we make sure to set each index to a value of type I
        WordBuilder<I> wb = new WordBuilder<>(null, position);
        wb.setSymbol(--position, lastSym);

        while (current.reachedFrom != null) {
            wb.setSymbol(--position, current.reachedBy);
            current = current.reachedFrom;
        }

        return wb.toWord();
    }

    public static <I> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<?, I, ?, ?, ?> target,
                                                           UniversalDeterministicAutomaton<?, I, ?, ?, ?> other,
                                                           Collection<? extends I> inputs) {
        return findSeparatingWord(target, other, inputs, false);
    }

    public static <S, S2, I, T, T2, SP, SP2, TP, TP2> @Nullable Word<I> findSeparatingWord(
            UniversalDeterministicAutomaton<S, I, T, SP, TP> target,
            UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
            Collection<? extends I> inputs,
            boolean ignoreUndefinedTransitions) {

        if (inputs instanceof Alphabet && target instanceof InputAlphabetHolder &&
            other instanceof InputAlphabetHolder) {
            @SuppressWarnings("unchecked")
            Alphabet<I> alphabet = (Alphabet<I>) inputs;
            @SuppressWarnings("unchecked")
            Alphabet<I> targetAlphabet = ((InputAlphabetHolder<I>) target).getInputAlphabet();
            if (alphabet.equals(targetAlphabet)) {
                @SuppressWarnings("unchecked")
                Alphabet<I> otherAlphabet = ((InputAlphabetHolder<I>) other).getInputAlphabet();
                if (alphabet.equals(otherAlphabet)) {
                    return findSeparatingWord(target, other, alphabet, ignoreUndefinedTransitions);
                }
            }
        }

        S init1 = target.getInitialState();
        S2 init2 = other.getInitialState();

        if (init1 == null && init2 == null) {
            return null;
        } else if (init1 == null || init2 == null) {
            return ignoreUndefinedTransitions ? null : Word.epsilon();
        }

        SP sprop1 = target.getStateProperty(init1);
        SP2 sprop2 = other.getStateProperty(init2);

        if (!Objects.equals(sprop1, sprop2)) {
            return Word.epsilon();
        }

        int targetStates = target.size();
        IntDisjointSets uf = new UnionFindRemSP(targetStates + other.size());

        StateIDs<S> targetStateIds = target.stateIDs();
        StateIDs<S2> otherStateIds = other.stateIDs();

        int id1 = targetStateIds.getStateId(init1);
        int id2 = otherStateIds.getStateId(init2) + targetStates;

        uf.link(id1, id2);

        Queue<Record<S, S2, I>> queue = new ArrayDeque<>();

        queue.add(new Record<>(init1, init2));

        I lastSym = null;

        Record<S, S2, I> current;

        explore:
        while ((current = queue.poll()) != null) {
            S state1 = current.state1;
            S2 state2 = current.state2;

            for (I sym : inputs) {
                T trans1 = target.getTransition(state1, sym);
                T2 trans2 = other.getTransition(state2, sym);

                if (ignoreUndefinedTransitions && (trans1 == null || trans2 == null)) {
                    continue;
                } else if (trans1 == null) {
                    if (trans2 == null) {
                        continue;
                    }
                    lastSym = sym;
                    break explore;
                } else if (trans2 == null) {
                    lastSym = sym;
                    break explore;
                }

                TP tprop1 = target.getTransitionProperty(trans1);
                TP2 tprop2 = other.getTransitionProperty(trans2);

                if (!Objects.equals(tprop1, tprop2)) {
                    lastSym = sym;
                    break explore;
                }

                S succ1 = target.getSuccessor(trans1);
                S2 succ2 = other.getSuccessor(trans2);

                id1 = targetStateIds.getStateId(succ1);
                id2 = otherStateIds.getStateId(succ2) + targetStates;

                if (!uf.union(id1, id2)) {
                    continue;
                }

                sprop1 = target.getStateProperty(succ1);
                sprop2 = other.getStateProperty(succ2);

                if (!Objects.equals(sprop1, sprop2)) {
                    lastSym = sym;
                    break explore;
                }

                queue.add(new Record<>(succ1, succ2, sym, current));
            }
        }

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

        int position = current.depth + 1;

        @SuppressWarnings("argument") // we make sure to set each index to a value of type I
        WordBuilder<I> wb = new WordBuilder<>(null, position);
        wb.setSymbol(--position, lastSym);

        while (current.reachedFrom != null) {
            wb.setSymbol(--position, current.reachedBy);
            current = current.reachedFrom;
        }

        return wb.toWord();
    }

    public static <I> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<?, I, ?, ?, ?> target,
                                                           UniversalDeterministicAutomaton<?, I, ?, ?, ?> other,
                                                           Alphabet<I> inputs) {
        return findSeparatingWord(target, other, inputs, false);
    }

    public static <S, S2, I, T, T2, SP, SP2, TP, TP2> @Nullable Word<I> findSeparatingWord(
            UniversalDeterministicAutomaton<S, I, T, SP, TP> target,
            UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
            Alphabet<I> inputs,
            boolean ignoreUndefinedTransitions) {
        UniversalDeterministicAutomaton.FullIntAbstraction<T, SP, TP> absTarget = target.fullIntAbstraction(inputs);
        UniversalDeterministicAutomaton.FullIntAbstraction<T2, SP2, TP2> absOther = other.fullIntAbstraction(inputs);

        int init1 = absTarget.getIntInitialState();
        int init2 = absOther.getIntInitialState();

        if (init1 < 0 && init2 < 0) {
            return null;
        } else if (init1 < 0 || init2 < 0) {
            return ignoreUndefinedTransitions ? null : Word.epsilon();
        }

        SP sprop1 = absTarget.getStateProperty(init1);
        SP2 sprop2 = absOther.getStateProperty(init2);

        if (!Objects.equals(sprop1, sprop2)) {
            return Word.epsilon();
        }

        int targetStates = target.size();
        IntDisjointSets uf = new UnionFindRemSP(targetStates + other.size());

        int id1 = init1;
        int id2 = targetStates + init2;

        uf.link(id1, id2);

        Queue<IntRecord> queue = new ArrayDeque<>();

        queue.add(new IntRecord(init1, init2));

        int lastSym = -1;
        int numInputs = inputs.size();

        IntRecord current;

        explore:
        while ((current = queue.poll()) != null) {
            int state1 = current.state1;
            int state2 = current.state2;

            for (int sym = 0; sym < numInputs; sym++) {
                T trans1 = absTarget.getTransition(state1, sym);
                T2 trans2 = absOther.getTransition(state2, sym);

                if (ignoreUndefinedTransitions && (trans1 == null || trans2 == null)) {
                    continue;
                } else if (trans1 == null) {
                    if (trans2 == null) {
                        continue;
                    }
                    lastSym = sym;
                    break explore;
                } else if (trans2 == null) {
                    lastSym = sym;
                    break explore;
                }

                TP tprop1 = target.getTransitionProperty(trans1);
                TP2 tprop2 = other.getTransitionProperty(trans2);

                if (!Objects.equals(tprop1, tprop2)) {
                    lastSym = sym;
                    break explore;
                }

                int succ1 = absTarget.getIntSuccessor(trans1);
                int succ2 = absOther.getIntSuccessor(trans2);

                id1 = succ1;
                id2 = succ2 + targetStates;

                if (!uf.union(id1, id2)) {
                    continue;
                }

                sprop1 = absTarget.getStateProperty(succ1);
                sprop2 = absOther.getStateProperty(succ2);

                if (!Objects.equals(sprop1, sprop2)) {
                    lastSym = sym;
                    break explore;
                }

                queue.add(new IntRecord(succ1, succ2, sym, current));
            }
        }

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

        int position = current.depth + 1;

        @SuppressWarnings("argument") // we make sure to set each index to a value of type I
        WordBuilder<I> wb = new WordBuilder<>(null, position);
        wb.setSymbol(--position, inputs.getSymbol(lastSym));

        while (current.reachedFrom != null) {
            wb.setSymbol(--position, inputs.getSymbol(current.reachedBy));
            current = current.reachedFrom;
        }

        return wb.toWord();
    }

    private static final class Record<S, S2, I> {

        private final S state1;
        private final S2 state2;
        private final I reachedBy;
        private final @Nullable Record<S, S2, I> reachedFrom;
        private final int depth;

        @SuppressWarnings("nullness") // we will only access reachedBy after checking reachedFrom for null
        Record(S state1, S2 state2) {
            this(state1, state2, null, null);
        }

        Record(S state1, S2 state2, I reachedBy, @Nullable Record<S, S2, I> reachedFrom) {
            this.state1 = state1;
            this.state2 = state2;
            this.reachedBy = reachedBy;
            this.reachedFrom = reachedFrom;
            this.depth = (reachedFrom != null) ? reachedFrom.depth + 1 : 0;
        }
    }

    private static final class IntRecord {

        private final int state1;
        private final int state2;
        private final int reachedBy;
        private final @Nullable IntRecord reachedFrom;
        private final int depth;

        IntRecord(int state1, int state2) {
            this(state1, state2, -1, null);
        }

        IntRecord(int state1, int state2, int reachedBy, @Nullable IntRecord reachedFrom) {
            this.state1 = state1;
            this.state2 = state2;
            this.reachedBy = reachedBy;
            this.reachedFrom = reachedFrom;
            this.depth = (reachedFrom != null) ? reachedFrom.depth + 1 : 0;
        }
    }
}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of AutomataLib <https://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.Objects;
21	import java.util.Queue;
22
23	import net.automatalib.alphabet.Alphabet;
24	import net.automatalib.automaton.UniversalDeterministicAutomaton;
25	import net.automatalib.automaton.concept.InputAlphabetHolder;
26	import net.automatalib.automaton.concept.StateIDs;
27	import net.automatalib.common.util.IntDisjointSets;
28	import net.automatalib.common.util.UnionFindRemSP;
29	import net.automatalib.word.Word;
30	import net.automatalib.word.WordBuilder;
31	import org.checkerframework.checker.nullness.qual.Nullable;
32
33	/**
34	* Implements Hopcroft and Karp's equivalence test, as described in <a href="https://doi.org/1813/5958">A linear
35	* algorithm for testing equivalence of finite automata</a>.
36	*/
37	@SuppressWarnings("PMD.TestClassWithoutTestCases") // not a traditional test class
38	public final class NearLinearEquivalenceTest {
39
40	private NearLinearEquivalenceTest() {
41	// prevent instantiation
42	}
43
44	public static <S, I> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<S, I, ?, ?, ?> target,
45	S init1,
46	S init2,
47	Collection<? extends I> inputs) {
48	return findSeparatingWord(target, init1, init2, inputs, false);	2✔
49	}
50
51	/**
52	* Find a separating word for two states in a given automaton.
53	*
54	* @param target
55	* the automaton
56	* @param init1
57	* the first state
58	* @param init2
59	* the second state
60	* @param inputs
61	* the inputs to consider for a separating word
62	* @param ignoreUndefinedTransitions
63	* if {@code true}, undefined transitions are not considered to distinguish two states, if {@code false} an
64	* undefined and defined transition are considered to distinguish two states
65	* @param <S>
66	* automaton state type
67	* @param <I>
68	* input alphabet type
69	* @param <T>
70	* automaton transition type
71	*
72	* @return A word separating the two states, {@code null} if no such word can be found
73	*/
74	public static <S, I, T> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<S, I, T, ?, ?> target,
75	S init1,
76	S init2,
77	Collection<? extends I> inputs,
78	boolean ignoreUndefinedTransitions) {
79
80	Object sprop1 = target.getStateProperty(init1);	2✔
81	Object sprop2 = target.getStateProperty(init2);	2✔
82
83	if (!Objects.equals(sprop1, sprop2)) {	2✔
84	return Word.epsilon();	2✔
85	}
86
87	IntDisjointSets uf = new UnionFindRemSP(target.size());	2✔
88
89	StateIDs<S> stateIds = target.stateIDs();	2✔
90
91	int id1 = stateIds.getStateId(init1), id2 = stateIds.getStateId(init2);	2✔
92
93	uf.link(id1, id2);	2✔
94
95	Queue<Record<S, S, I>> queue = new ArrayDeque<>();	2✔
96
97	queue.add(new Record<>(init1, init2));	2✔
98
99	I lastSym = null;	2✔
100	Record<S, S, I> current;
101
102	explore:
103	while ((current = queue.poll()) != null) {	2✔
104	S state1 = current.state1;	2✔
105	S state2 = current.state2;	2✔
106
107	for (I sym : inputs) {	2✔
108	T trans1 = target.getTransition(state1, sym);	2✔
109	T trans2 = target.getTransition(state2, sym);	2✔
110
111	if (ignoreUndefinedTransitions && (trans1 == null \|\| trans2 == null)) {	2✔
112	continue;	×
113	} else if (trans1 == null) {	2✔
114	if (trans2 == null) {	2✔
115	continue;	2✔
116	}
117	lastSym = sym;	2✔
118	break explore;	2✔
119	} else if (trans2 == null) {	2✔
120	lastSym = sym;	2✔
121	break explore;	2✔
122	}
123
124	Object tprop1 = target.getTransitionProperty(trans1);	2✔
125	Object tprop2 = target.getTransitionProperty(trans2);	2✔
126
127	if (!Objects.equals(tprop1, tprop2)) {	2✔
128	lastSym = sym;	2✔
129	break explore;	2✔
130	}
131
132	S succ1 = target.getSuccessor(trans1);	2✔
133	S succ2 = target.getSuccessor(trans2);	2✔
134
135	id1 = stateIds.getStateId(succ1);	2✔
136	id2 = stateIds.getStateId(succ2);	2✔
137
138	int r1 = uf.find(id1), r2 = uf.find(id2);	2✔
139
140	if (r1 == r2) {	2✔
141	continue;	2✔
142	}
143
144	sprop1 = target.getStateProperty(succ1);	2✔
145	sprop2 = target.getStateProperty(succ2);	2✔
146
147	if (!Objects.equals(sprop1, sprop2)) {	2✔
148	lastSym = sym;	2✔
149	break explore;	2✔
150	}
151
152	uf.link(r1, r2);	2✔
153
154	queue.add(new Record<>(succ1, succ2, sym, current));	2✔
155	}	2✔
156	}	2✔
157
158	if (current == null) {	2✔
159	return null;	×
160	}
161
162	int position = current.depth + 1;	2✔
163
164	@SuppressWarnings("argument") // we make sure to set each index to a value of type I
165	WordBuilder<I> wb = new WordBuilder<>(null, position);	2✔
166	wb.setSymbol(--position, lastSym);	2✔
167
168	while (current.reachedFrom != null) {	2✔
169	wb.setSymbol(--position, current.reachedBy);	2✔
170	current = current.reachedFrom;	2✔
171	}
172
173	return wb.toWord();	2✔
174	}
175
176	public static <I> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<?, I, ?, ?, ?> target,
177	UniversalDeterministicAutomaton<?, I, ?, ?, ?> other,
178	Collection<? extends I> inputs) {
179	return findSeparatingWord(target, other, inputs, false);	2✔
180	}
181
182	public static <S, S2, I, T, T2, SP, SP2, TP, TP2> @Nullable Word<I> findSeparatingWord(
183	UniversalDeterministicAutomaton<S, I, T, SP, TP> target,
184	UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
185	Collection<? extends I> inputs,
186	boolean ignoreUndefinedTransitions) {
187
188	if (inputs instanceof Alphabet && target instanceof InputAlphabetHolder &&	2✔
189	other instanceof InputAlphabetHolder) {
190	@SuppressWarnings("unchecked")
191	Alphabet<I> alphabet = (Alphabet<I>) inputs;	2✔
192	@SuppressWarnings("unchecked")
193	Alphabet<I> targetAlphabet = ((InputAlphabetHolder<I>) target).getInputAlphabet();	2✔
194	if (alphabet.equals(targetAlphabet)) {	2✔
195	@SuppressWarnings("unchecked")
196	Alphabet<I> otherAlphabet = ((InputAlphabetHolder<I>) other).getInputAlphabet();	2✔
197	if (alphabet.equals(otherAlphabet)) {	2✔
198	return findSeparatingWord(target, other, alphabet, ignoreUndefinedTransitions);	2✔
199	}
200	}
201	}
202
203	S init1 = target.getInitialState();	2✔
204	S2 init2 = other.getInitialState();	2✔
205
206	if (init1 == null && init2 == null) {	2✔
207	return null;	2✔
208	} else if (init1 == null \|\| init2 == null) {	2✔
209	return ignoreUndefinedTransitions ? null : Word.epsilon();	2✔
210	}
211
212	SP sprop1 = target.getStateProperty(init1);	2✔
213	SP2 sprop2 = other.getStateProperty(init2);	2✔
214
215	if (!Objects.equals(sprop1, sprop2)) {	2✔
216	return Word.epsilon();	2✔
217	}
218
219	int targetStates = target.size();	2✔
220	IntDisjointSets uf = new UnionFindRemSP(targetStates + other.size());	2✔
221
222	StateIDs<S> targetStateIds = target.stateIDs();	2✔
223	StateIDs<S2> otherStateIds = other.stateIDs();	2✔
224
225	int id1 = targetStateIds.getStateId(init1);	2✔
226	int id2 = otherStateIds.getStateId(init2) + targetStates;	2✔
227
228	uf.link(id1, id2);	2✔
229
230	Queue<Record<S, S2, I>> queue = new ArrayDeque<>();	2✔
231
232	queue.add(new Record<>(init1, init2));	2✔
233
234	I lastSym = null;	2✔
235
236	Record<S, S2, I> current;
237
238	explore:
239	while ((current = queue.poll()) != null) {	2✔
240	S state1 = current.state1;	2✔
241	S2 state2 = current.state2;	2✔
242
243	for (I sym : inputs) {	2✔
244	T trans1 = target.getTransition(state1, sym);	2✔
245	T2 trans2 = other.getTransition(state2, sym);	2✔
246
247	if (ignoreUndefinedTransitions && (trans1 == null \|\| trans2 == null)) {	2✔
248	continue;	2✔
249	} else if (trans1 == null) {	2✔
250	if (trans2 == null) {	2✔
251	continue;	2✔
252	}
253	lastSym = sym;	2✔
254	break explore;	2✔
255	} else if (trans2 == null) {	2✔
256	lastSym = sym;	2✔
257	break explore;	2✔
258	}
259
260	TP tprop1 = target.getTransitionProperty(trans1);	2✔
261	TP2 tprop2 = other.getTransitionProperty(trans2);	2✔
262
263	if (!Objects.equals(tprop1, tprop2)) {	2✔
264	lastSym = sym;	×
265	break explore;	×
266	}
267
268	S succ1 = target.getSuccessor(trans1);	2✔
269	S2 succ2 = other.getSuccessor(trans2);	2✔
270
271	id1 = targetStateIds.getStateId(succ1);	2✔
272	id2 = otherStateIds.getStateId(succ2) + targetStates;	2✔
273
274	if (!uf.union(id1, id2)) {	2✔
275	continue;	2✔
276	}
277
278	sprop1 = target.getStateProperty(succ1);	2✔
279	sprop2 = other.getStateProperty(succ2);	2✔
280
281	if (!Objects.equals(sprop1, sprop2)) {	2✔
282	lastSym = sym;	2✔
283	break explore;	2✔
284	}
285
286	queue.add(new Record<>(succ1, succ2, sym, current));	2✔
287	}	2✔
288	}	2✔
289
290	if (current == null) {	2✔
291	return null;	2✔
292	}
293
294	int position = current.depth + 1;	2✔
295
296	@SuppressWarnings("argument") // we make sure to set each index to a value of type I
297	WordBuilder<I> wb = new WordBuilder<>(null, position);	2✔
298	wb.setSymbol(--position, lastSym);	2✔
299
300	while (current.reachedFrom != null) {	2✔
301	wb.setSymbol(--position, current.reachedBy);	2✔
302	current = current.reachedFrom;	2✔
303	}
304
305	return wb.toWord();	2✔
306	}
307
308	public static <I> @Nullable Word<I> findSeparatingWord(UniversalDeterministicAutomaton<?, I, ?, ?, ?> target,
309	UniversalDeterministicAutomaton<?, I, ?, ?, ?> other,
310	Alphabet<I> inputs) {
311	return findSeparatingWord(target, other, inputs, false);	2✔
312	}
313
314	public static <S, S2, I, T, T2, SP, SP2, TP, TP2> @Nullable Word<I> findSeparatingWord(
315	UniversalDeterministicAutomaton<S, I, T, SP, TP> target,
316	UniversalDeterministicAutomaton<S2, I, T2, SP2, TP2> other,
317	Alphabet<I> inputs,
318	boolean ignoreUndefinedTransitions) {
319	UniversalDeterministicAutomaton.FullIntAbstraction<T, SP, TP> absTarget = target.fullIntAbstraction(inputs);	2✔
320	UniversalDeterministicAutomaton.FullIntAbstraction<T2, SP2, TP2> absOther = other.fullIntAbstraction(inputs);	2✔
321
322	int init1 = absTarget.getIntInitialState();	2✔
323	int init2 = absOther.getIntInitialState();	2✔
324
325	if (init1 < 0 && init2 < 0) {	2✔
326	return null;	2✔
327	} else if (init1 < 0 \|\| init2 < 0) {	2✔
328	return ignoreUndefinedTransitions ? null : Word.epsilon();	2✔
329	}
330
331	SP sprop1 = absTarget.getStateProperty(init1);	2✔
332	SP2 sprop2 = absOther.getStateProperty(init2);	2✔
333
334	if (!Objects.equals(sprop1, sprop2)) {	2✔
335	return Word.epsilon();	2✔
336	}
337
338	int targetStates = target.size();	2✔
339	IntDisjointSets uf = new UnionFindRemSP(targetStates + other.size());	2✔
340
341	int id1 = init1;	2✔
342	int id2 = targetStates + init2;	2✔
343
344	uf.link(id1, id2);	2✔
345
346	Queue<IntRecord> queue = new ArrayDeque<>();	2✔
347
348	queue.add(new IntRecord(init1, init2));	2✔
349
350	int lastSym = -1;	2✔
351	int numInputs = inputs.size();	2✔
352
353	IntRecord current;
354
355	explore:
356	while ((current = queue.poll()) != null) {	2✔
357	int state1 = current.state1;	2✔
358	int state2 = current.state2;	2✔
359
360	for (int sym = 0; sym < numInputs; sym++) {	2✔
361	T trans1 = absTarget.getTransition(state1, sym);	2✔
362	T2 trans2 = absOther.getTransition(state2, sym);	2✔
363
364	if (ignoreUndefinedTransitions && (trans1 == null \|\| trans2 == null)) {	2✔
365	continue;	2✔
366	} else if (trans1 == null) {	2✔
367	if (trans2 == null) {	2✔
368	continue;	2✔
369	}
370	lastSym = sym;	2✔
371	break explore;	2✔
372	} else if (trans2 == null) {	2✔
373	lastSym = sym;	2✔
374	break explore;	2✔
375	}
376
377	TP tprop1 = target.getTransitionProperty(trans1);	2✔
378	TP2 tprop2 = other.getTransitionProperty(trans2);	2✔
379
380	if (!Objects.equals(tprop1, tprop2)) {	2✔
381	lastSym = sym;	2✔
382	break explore;	2✔
383	}
384
385	int succ1 = absTarget.getIntSuccessor(trans1);	2✔
386	int succ2 = absOther.getIntSuccessor(trans2);	2✔
387
388	id1 = succ1;	2✔
389	id2 = succ2 + targetStates;	2✔
390
391	if (!uf.union(id1, id2)) {	2✔
392	continue;	2✔
393	}
394
395	sprop1 = absTarget.getStateProperty(succ1);	2✔
396	sprop2 = absOther.getStateProperty(succ2);	2✔
397
398	if (!Objects.equals(sprop1, sprop2)) {	2✔
399	lastSym = sym;	2✔
400	break explore;	2✔
401	}
402
403	queue.add(new IntRecord(succ1, succ2, sym, current));	2✔
404	}
405	}	2✔
406
407	if (current == null) {	2✔
408	return null;	2✔
409	}
410
411	int position = current.depth + 1;	2✔
412
413	@SuppressWarnings("argument") // we make sure to set each index to a value of type I
414	WordBuilder<I> wb = new WordBuilder<>(null, position);	2✔
415	wb.setSymbol(--position, inputs.getSymbol(lastSym));	2✔
416
417	while (current.reachedFrom != null) {	2✔
418	wb.setSymbol(--position, inputs.getSymbol(current.reachedBy));	2✔
419	current = current.reachedFrom;	2✔
420	}
421
422	return wb.toWord();	2✔
423	}
424
425	private static final class Record<S, S2, I> {
426
427	private final S state1;
428	private final S2 state2;
429	private final I reachedBy;
430	private final @Nullable Record<S, S2, I> reachedFrom;
431	private final int depth;
432
433	@SuppressWarnings("nullness") // we will only access reachedBy after checking reachedFrom for null
434	Record(S state1, S2 state2) {
435	this(state1, state2, null, null);	2✔
436	}	2✔
437
438	Record(S state1, S2 state2, I reachedBy, @Nullable Record<S, S2, I> reachedFrom) {	2✔
439	this.state1 = state1;	2✔
440	this.state2 = state2;	2✔
441	this.reachedBy = reachedBy;	2✔
442	this.reachedFrom = reachedFrom;	2✔
443	this.depth = (reachedFrom != null) ? reachedFrom.depth + 1 : 0;	2✔
444	}	2✔
445	}
446
447	private static final class IntRecord {
448
449	private final int state1;
450	private final int state2;
451	private final int reachedBy;
452	private final @Nullable IntRecord reachedFrom;
453	private final int depth;
454
455	IntRecord(int state1, int state2) {
456	this(state1, state2, -1, null);	2✔
457	}	2✔
458
459	IntRecord(int state1, int state2, int reachedBy, @Nullable IntRecord reachedFrom) {	2✔
460	this.state1 = state1;	2✔
461	this.state2 = state2;	2✔
462	this.reachedBy = reachedBy;	2✔
463	this.reachedFrom = reachedFrom;	2✔
464	this.depth = (reachedFrom != null) ? reachedFrom.depth + 1 : 0;	2✔
465	}	2✔
466	}
467	}

LearnLib / automatalib / 13138848026

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