12019076191

Committed 25 Nov 2024 09:09PM UTC coverage: 90.741%. Remained the same

Build # 12019076191

Build Type

push

github

Committed by

mtf90

Commit Message

add KTS abstraction

Run Details

15994 of 17626 relevant lines covered (90.74%)

1.68 hits per line

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

95.31

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

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

LearnLib / automatalib / 12019076191

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