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

95.31

/util/src/main/java/net/automatalib/util/automaton/equivalence/NearLinearEquivalenceTest.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.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;

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

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