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

91.84

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

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

import net.automatalib.alphabet.ProceduralInputAlphabet;
import net.automatalib.automaton.procedural.SPMM;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Operations on {@link SPMM}s.
 */
public final class SPMMs {

    private SPMMs() {
        // prevent instantiation
    }

    /**
     * Computes a set of access sequences and terminating sequences for a given {@link SPMM}.  This is a convenience
     * method for {@link #computeATSequences(SPMM, ProceduralInputAlphabet)} that automatically uses the
     * {@link SPMM#getInputAlphabet() input alphabet} of the given {@code spmm}.
     *
     * @param spmm
     *         the {@link SPMM} for which the sequences should be computed
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return an {@link ATSequences} object which contains the respective sequences.
     *
     * @see #computeATSequences(SPMM, ProceduralInputAlphabet)
     */
    public static <I, O> ATSequences<I> computeATSequences(SPMM<?, I, ?, O> spmm) {
        return computeATSequences(spmm, spmm.getInputAlphabet());
    }

    /**
     * Computes a set of access sequences and return sequences for a given {@link SPMM} limited to the symbols of the
     * given {@link ProceduralInputAlphabet}.
     *
     * @param spmm
     *         the {@link SPMM} for which the sequences should be computed
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for computing the respective sequences
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return an {@link ATSequences} object which contains the respective sequences.
     *
     * @see #computeAccessSequences(SPMM, ProceduralInputAlphabet, Map)
     * @see #computeTerminatingSequences(SPMM, ProceduralInputAlphabet)
     */
    public static <I, O> ATSequences<I> computeATSequences(SPMM<?, I, ?, O> spmm, ProceduralInputAlphabet<I> alphabet) {

        assert isValid(spmm, alphabet);

        final Map<I, Word<I>> terminatingSequences = computeTerminatingSequences(spmm, alphabet);
        final Map<I, Word<I>> accessSequences = computeAccessSequences(spmm, alphabet, terminatingSequences);

        return new ATSequences<>(accessSequences, terminatingSequences);
    }

    /**
     * Computes for a given {@link SPMM} the set of terminating sequences using the given
     * {@link ProceduralInputAlphabet alphabet}. Terminating sequences transfer a procedure from its initial state to a
     * returnable state. This method furthermore checks that the hierarchy of calls is well-defined, i.e. it only
     * includes procedural invocations <i>p</i> for determining a terminating sequence if <i>p</i> has a valid
     * terminating sequence itself.
     *
     * @param spmm
     *         the {@link SPMM} to analyze
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for computing the terminating sequences
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return A map from procedures (restricted to the call symbols of the given alphabet) to the terminating
     * sequences. This map may be partial as some procedures may not have a well-defined terminating sequence for the
     * given alphabet.
     */
    public static <I, O> Map<I, Word<I>> computeTerminatingSequences(SPMM<?, I, ?, O> spmm,
                                                                     ProceduralInputAlphabet<I> alphabet) {
        final Word<I> returnWord = Word.fromLetter(alphabet.getReturnSymbol());

        return ProceduralUtil.computeTerminatingSequences(spmm.getProcedures(), alphabet, (mealy, trace) -> {
            final Word<O> output = mealy.computeSuffixOutput(trace, returnWord);
            return !output.isEmpty() && !spmm.isErrorOutput(output.lastSymbol());
        });
    }

    /**
     * Computes for a given {@link SPMM} a set of access sequences using the SPMM
     * {@link ProceduralInputAlphabet alphabet}. An access sequence (for procedure <i>p</i>) transfers an {@link SPMM}
     * from its initial state to a state that is able to successfully execute a run of <i>p</i>. This method furthermore
     * checks that potentially nested calls are well-defined, i.e. it only includes procedural invocations
     * <i>p</i> for determining access sequences if <i>p</i> has a valid terminating sequence and therefore can
     * be expanded correctly.
     *
     * @param spmm
     *         the {@link SPMM} to analyze
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for computing the access sequences
     * @param terminatingSequences
     *         a {@link Map} of call symbols to terminating sequences used to expand nested invocations in access
     *         sequences
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return A map from procedures (restricted to the call symbols of the given alphabet) to the access sequences.
     * This map may be partial as some procedures may not have well-defined access sequences for the given alphabet.
     */
    public static <I, O> Map<I, Word<I>> computeAccessSequences(SPMM<?, I, ?, O> spmm,
                                                                ProceduralInputAlphabet<I> alphabet,
                                                                Map<I, Word<I>> terminatingSequences) {
        return ProceduralUtil.computeAccessSequences(spmm.getProcedures(),
                                                     alphabet,
                                                     spmm.getProceduralInputs(alphabet),
                                                     spmm.getInitialProcedure(),
                                                     terminatingSequences,
                                                     (mealy, trace) -> !spmm.isErrorOutput(mealy.computeOutput(trace)
                                                                                                .lastSymbol()));
    }

    /**
     * Checks whether the given {@link SPMM} is valid, This is a convenience method for
     * {@link #isValid(SPMM, ProceduralInputAlphabet)} that uses the {@link SPMM#getInputAlphabet() input alphabet} of
     * the given {@link SPMM}.
     *
     * @param spmm
     *         the {@link SPMM} to analyze
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return {@code true} if {@code spmm} is valid, {@code false} otherwise.
     *
     * @see #isValid(SPMM, ProceduralInputAlphabet)
     */
    public static <I, O> boolean isValid(SPMM<?, I, ?, O> spmm) {
        return isValid(spmm, spmm.getInputAlphabet());
    }

    /**
     * Checks whether the given {@link SPMM} is valid with respect to the given {@link ProceduralInputAlphabet}, i.e.,
     * whether its {@link SPMM#getProcedures() procedures} are error-closed, return-closed, and call-closed.
     * <p>
     * A procedure is considered error-closed iff any transition that emits an
     * {@link SPMM#getErrorOutput() error output} transitions the procedure into a sink state that continues to output
     * the {@link SPMM#getErrorOutput() error output}.
     * <p>
     * A procedure is considered return-closed iff the {@link ProceduralInputAlphabet#getReturnSymbol() return symbol}
     * transitions the procedure into a sink state that continues to output the
     * {@link SPMM#getErrorOutput() error output}.
     * <p>
     * A procedure is considered call-closed iff any transition labeled with a non-terminating
     * {@link ProceduralInputAlphabet#getCallAlphabet() call symbol} transitions the procedure into a sink state that
     * continues to output the {@link SPMM#getErrorOutput() error output}.
     *
     * @param spmm
     *         the {@link SPMM} to analyze
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for checking validity
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return {@code true} if {@code spmm} is valid, {@code false} otherwise.
     */
    public static <I, O> boolean isValid(SPMM<?, I, ?, O> spmm, ProceduralInputAlphabet<I> alphabet) {

        final Map<I, Word<I>> ts = computeTerminatingSequences(spmm, alphabet);
        final Collection<I> proceduralInputs = spmm.getProceduralInputs(alphabet);
        final Set<I> nonContinuableSymbols = new HashSet<>(alphabet.getCallAlphabet());
        nonContinuableSymbols.removeAll(ts.keySet());
        nonContinuableSymbols.retainAll(proceduralInputs);
        nonContinuableSymbols.add(alphabet.getReturnSymbol());

        for (MealyMachine<?, I, ?, O> p : spmm.getProcedures().values()) {
            if (!isErrorReturnAndCallClosed(p, proceduralInputs, nonContinuableSymbols, spmm.getErrorOutput())) {
                return false;
            }
        }

        return true;
    }

    private static <S, I, O> boolean isErrorReturnAndCallClosed(MealyMachine<S, I, ?, O> procedure,
                                                                Collection<I> inputs,
                                                                Collection<I> nonContinuableInputs,
                                                                O errorOutput) {

        for (I i : inputs) {

            boolean isNonContinuable = nonContinuableInputs.contains(i);

            for (S s : procedure) {

                final O output = procedure.getOutput(s, i);
                final S succ = procedure.getSuccessor(s, i);

                if (succ != null && (isNonContinuable || Objects.equals(output, errorOutput)) &&
                    !isSink(procedure, inputs, succ, errorOutput)) {
                    return false;
                }
            }
        }

        return true;
    }

    private static <S, I, T, O> boolean isSink(MealyMachine<S, I, T, O> m,
                                               Collection<? extends I> inputs,
                                               S state,
                                               O output) {
        for (I i : inputs) {
            final T t = m.getTransition(state, i);
            if (t != null &&
                (!Objects.equals(m.getSuccessor(t), state) || !Objects.equals(m.getTransitionOutput(t), output))) {
                return false;
            }
        }
        return true;
    }

    /**
     * Checks if the two given {@link SPMM}s are equivalent, i.e. whether there exists a
     * {@link #findSeparatingWord(SPMM, SPMM, ProceduralInputAlphabet) separating word} for them.
     *
     * @param spmm1
     *         the first {@link SPMM}
     * @param spmm2
     *         the second {@link SPMM}
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for checking equivalence
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return {@code true} if the two {@link SPMM}s are equivalent, {@code false} otherwise.
     *
     * @see #findSeparatingWord(SPMM, SPMM, ProceduralInputAlphabet)
     */
    public static <I, O> boolean testEquivalence(SPMM<?, I, ?, O> spmm1,
                                                 SPMM<?, I, ?, O> spmm2,
                                                 ProceduralInputAlphabet<I> alphabet) {
        return findSeparatingWord(spmm1, spmm2, alphabet) == null;
    }

    /**
     * Computes a separating word for the two given {@link SPMM}s, if existent. A separating word is a {@link Word} such
     * that one {@link SPMM} {@link SPMM#computeOutput(Iterable) behaves} different from the other.
     *
     * @param spmm1
     *         the first {@link SPMM}
     * @param spmm2
     *         the second {@link SPMM}
     * @param alphabet
     *         the {@link ProceduralInputAlphabet} whose symbols should be used for computing the separating word
     * @param <I>
     *         input symbol type
     * @param <O>
     *         output symbol type
     *
     * @return a separating word, if existent, {@code null} otherwise.
     */
    public static <I, O> @Nullable Word<I> findSeparatingWord(SPMM<?, I, ?, O> spmm1,
                                                              SPMM<?, I, ?, O> spmm2,
                                                              ProceduralInputAlphabet<I> alphabet) {

        final ATSequences<I> at1 = computeATSequences(spmm1, alphabet);
        final ATSequences<I> at2 = computeATSequences(spmm2, alphabet);

        return ProceduralUtil.findSeparatingWord(spmm1.getProcedures(), at1, spmm2.getProcedures(), at2, alphabet);
    }
}

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.procedural;
17
18	import java.util.Collection;
19	import java.util.HashSet;
20	import java.util.Map;
21	import java.util.Objects;
22	import java.util.Set;
23
24	import net.automatalib.alphabet.ProceduralInputAlphabet;
25	import net.automatalib.automaton.procedural.SPMM;
26	import net.automatalib.automaton.transducer.MealyMachine;
27	import net.automatalib.word.Word;
28	import org.checkerframework.checker.nullness.qual.Nullable;
29
30	/**
31	* Operations on {@link SPMM}s.
32	*/
33	public final class SPMMs {	2✔
34
35	private SPMMs() {
36	// prevent instantiation
37	}
38
39	/**
40	* Computes a set of access sequences and terminating sequences for a given {@link SPMM}. This is a convenience
41	* method for {@link #computeATSequences(SPMM, ProceduralInputAlphabet)} that automatically uses the
42	* {@link SPMM#getInputAlphabet() input alphabet} of the given {@code spmm}.
43	*
44	* @param spmm
45	* the {@link SPMM} for which the sequences should be computed
46	* @param <I>
47	* input symbol type
48	* @param <O>
49	* output symbol type
50	*
51	* @return an {@link ATSequences} object which contains the respective sequences.
52	*
53	* @see #computeATSequences(SPMM, ProceduralInputAlphabet)
54	*/
55	public static <I, O> ATSequences<I> computeATSequences(SPMM<?, I, ?, O> spmm) {
56	return computeATSequences(spmm, spmm.getInputAlphabet());	2✔
57	}
58
59	/**
60	* Computes a set of access sequences and return sequences for a given {@link SPMM} limited to the symbols of the
61	* given {@link ProceduralInputAlphabet}.
62	*
63	* @param spmm
64	* the {@link SPMM} for which the sequences should be computed
65	* @param alphabet
66	* the {@link ProceduralInputAlphabet} whose symbols should be used for computing the respective sequences
67	* @param <I>
68	* input symbol type
69	* @param <O>
70	* output symbol type
71	*
72	* @return an {@link ATSequences} object which contains the respective sequences.
73	*
74	* @see #computeAccessSequences(SPMM, ProceduralInputAlphabet, Map)
75	* @see #computeTerminatingSequences(SPMM, ProceduralInputAlphabet)
76	*/
77	public static <I, O> ATSequences<I> computeATSequences(SPMM<?, I, ?, O> spmm, ProceduralInputAlphabet<I> alphabet) {
78
79	assert isValid(spmm, alphabet);	2✔
80
81	final Map<I, Word<I>> terminatingSequences = computeTerminatingSequences(spmm, alphabet);	2✔
82	final Map<I, Word<I>> accessSequences = computeAccessSequences(spmm, alphabet, terminatingSequences);	2✔
83
84	return new ATSequences<>(accessSequences, terminatingSequences);	2✔
85	}
86
87	/**
88	* Computes for a given {@link SPMM} the set of terminating sequences using the given
89	* {@link ProceduralInputAlphabet alphabet}. Terminating sequences transfer a procedure from its initial state to a
90	* returnable state. This method furthermore checks that the hierarchy of calls is well-defined, i.e. it only
91	* includes procedural invocations <i>p</i> for determining a terminating sequence if <i>p</i> has a valid
92	* terminating sequence itself.
93	*
94	* @param spmm
95	* the {@link SPMM} to analyze
96	* @param alphabet
97	* the {@link ProceduralInputAlphabet} whose symbols should be used for computing the terminating sequences
98	* @param <I>
99	* input symbol type
100	* @param <O>
101	* output symbol type
102	*
103	* @return A map from procedures (restricted to the call symbols of the given alphabet) to the terminating
104	* sequences. This map may be partial as some procedures may not have a well-defined terminating sequence for the
105	* given alphabet.
106	*/
107	public static <I, O> Map<I, Word<I>> computeTerminatingSequences(SPMM<?, I, ?, O> spmm,
108	ProceduralInputAlphabet<I> alphabet) {
109	final Word<I> returnWord = Word.fromLetter(alphabet.getReturnSymbol());	2✔
110
111	return ProceduralUtil.computeTerminatingSequences(spmm.getProcedures(), alphabet, (mealy, trace) -> {	2✔
112	final Word<O> output = mealy.computeSuffixOutput(trace, returnWord);	2✔
113	return !output.isEmpty() && !spmm.isErrorOutput(output.lastSymbol());	2✔
114	});
115	}
116
117	/**
118	* Computes for a given {@link SPMM} a set of access sequences using the SPMM
119	* {@link ProceduralInputAlphabet alphabet}. An access sequence (for procedure <i>p</i>) transfers an {@link SPMM}
120	* from its initial state to a state that is able to successfully execute a run of <i>p</i>. This method furthermore
121	* checks that potentially nested calls are well-defined, i.e. it only includes procedural invocations
122	* <i>p</i> for determining access sequences if <i>p</i> has a valid terminating sequence and therefore can
123	* be expanded correctly.
124	*
125	* @param spmm
126	* the {@link SPMM} to analyze
127	* @param alphabet
128	* the {@link ProceduralInputAlphabet} whose symbols should be used for computing the access sequences
129	* @param terminatingSequences
130	* a {@link Map} of call symbols to terminating sequences used to expand nested invocations in access
131	* sequences
132	* @param <I>
133	* input symbol type
134	* @param <O>
135	* output symbol type
136	*
137	* @return A map from procedures (restricted to the call symbols of the given alphabet) to the access sequences.
138	* This map may be partial as some procedures may not have well-defined access sequences for the given alphabet.
139	*/
140	public static <I, O> Map<I, Word<I>> computeAccessSequences(SPMM<?, I, ?, O> spmm,
141	ProceduralInputAlphabet<I> alphabet,
142	Map<I, Word<I>> terminatingSequences) {
143	return ProceduralUtil.computeAccessSequences(spmm.getProcedures(),	2✔
144	alphabet,
145	spmm.getProceduralInputs(alphabet),	2✔
146	spmm.getInitialProcedure(),	2✔
147	terminatingSequences,
148	(mealy, trace) -> !spmm.isErrorOutput(mealy.computeOutput(trace)	2✔
149	.lastSymbol()));	2✔
150	}
151
152	/**
153	* Checks whether the given {@link SPMM} is valid, This is a convenience method for
154	* {@link #isValid(SPMM, ProceduralInputAlphabet)} that uses the {@link SPMM#getInputAlphabet() input alphabet} of
155	* the given {@link SPMM}.
156	*
157	* @param spmm
158	* the {@link SPMM} to analyze
159	* @param <I>
160	* input symbol type
161	* @param <O>
162	* output symbol type
163	*
164	* @return {@code true} if {@code spmm} is valid, {@code false} otherwise.
165	*
166	* @see #isValid(SPMM, ProceduralInputAlphabet)
167	*/
168	public static <I, O> boolean isValid(SPMM<?, I, ?, O> spmm) {
169	return isValid(spmm, spmm.getInputAlphabet());	×
170	}
171
172	/**
173	* Checks whether the given {@link SPMM} is valid with respect to the given {@link ProceduralInputAlphabet}, i.e.,
174	* whether its {@link SPMM#getProcedures() procedures} are error-closed, return-closed, and call-closed.
175	* <p>
176	* A procedure is considered error-closed iff any transition that emits an
177	* {@link SPMM#getErrorOutput() error output} transitions the procedure into a sink state that continues to output
178	* the {@link SPMM#getErrorOutput() error output}.
179	* <p>
180	* A procedure is considered return-closed iff the {@link ProceduralInputAlphabet#getReturnSymbol() return symbol}
181	* transitions the procedure into a sink state that continues to output the
182	* {@link SPMM#getErrorOutput() error output}.
183	* <p>
184	* A procedure is considered call-closed iff any transition labeled with a non-terminating
185	* {@link ProceduralInputAlphabet#getCallAlphabet() call symbol} transitions the procedure into a sink state that
186	* continues to output the {@link SPMM#getErrorOutput() error output}.
187	*
188	* @param spmm
189	* the {@link SPMM} to analyze
190	* @param alphabet
191	* the {@link ProceduralInputAlphabet} whose symbols should be used for checking validity
192	* @param <I>
193	* input symbol type
194	* @param <O>
195	* output symbol type
196	*
197	* @return {@code true} if {@code spmm} is valid, {@code false} otherwise.
198	*/
199	public static <I, O> boolean isValid(SPMM<?, I, ?, O> spmm, ProceduralInputAlphabet<I> alphabet) {
200
201	final Map<I, Word<I>> ts = computeTerminatingSequences(spmm, alphabet);	2✔
202	final Collection<I> proceduralInputs = spmm.getProceduralInputs(alphabet);	2✔
203	final Set<I> nonContinuableSymbols = new HashSet<>(alphabet.getCallAlphabet());	2✔
204	nonContinuableSymbols.removeAll(ts.keySet());	2✔
205	nonContinuableSymbols.retainAll(proceduralInputs);	2✔
206	nonContinuableSymbols.add(alphabet.getReturnSymbol());	2✔
207
208	for (MealyMachine<?, I, ?, O> p : spmm.getProcedures().values()) {	2✔
209	if (!isErrorReturnAndCallClosed(p, proceduralInputs, nonContinuableSymbols, spmm.getErrorOutput())) {	2✔
210	return false;	×
211	}
212	}	2✔
213
214	return true;	2✔
215	}
216
217	private static <S, I, O> boolean isErrorReturnAndCallClosed(MealyMachine<S, I, ?, O> procedure,
218	Collection<I> inputs,
219	Collection<I> nonContinuableInputs,
220	O errorOutput) {
221
222	for (I i : inputs) {	2✔
223
224	boolean isNonContinuable = nonContinuableInputs.contains(i);	2✔
225
226	for (S s : procedure) {	2✔
227
228	final O output = procedure.getOutput(s, i);	2✔
229	final S succ = procedure.getSuccessor(s, i);	2✔
230
231	if (succ != null && (isNonContinuable \|\| Objects.equals(output, errorOutput)) &&	2✔
232	!isSink(procedure, inputs, succ, errorOutput)) {	2✔
233	return false;	×
234	}
235	}	2✔
236	}	2✔
237
238	return true;	2✔
239	}
240
241	private static <S, I, T, O> boolean isSink(MealyMachine<S, I, T, O> m,
242	Collection<? extends I> inputs,
243	S state,
244	O output) {
245	for (I i : inputs) {	2✔
246	final T t = m.getTransition(state, i);	2✔
247	if (t != null &&	2✔
248	(!Objects.equals(m.getSuccessor(t), state) \|\| !Objects.equals(m.getTransitionOutput(t), output))) {	2✔
249	return false;	×
250	}
251	}	2✔
252	return true;	2✔
253	}
254
255	/**
256	* Checks if the two given {@link SPMM}s are equivalent, i.e. whether there exists a
257	* {@link #findSeparatingWord(SPMM, SPMM, ProceduralInputAlphabet) separating word} for them.
258	*
259	* @param spmm1
260	* the first {@link SPMM}
261	* @param spmm2
262	* the second {@link SPMM}
263	* @param alphabet
264	* the {@link ProceduralInputAlphabet} whose symbols should be used for checking equivalence
265	* @param <I>
266	* input symbol type
267	* @param <O>
268	* output symbol type
269	*
270	* @return {@code true} if the two {@link SPMM}s are equivalent, {@code false} otherwise.
271	*
272	* @see #findSeparatingWord(SPMM, SPMM, ProceduralInputAlphabet)
273	*/
274	public static <I, O> boolean testEquivalence(SPMM<?, I, ?, O> spmm1,
275	SPMM<?, I, ?, O> spmm2,
276	ProceduralInputAlphabet<I> alphabet) {
277	return findSeparatingWord(spmm1, spmm2, alphabet) == null;	2✔
278	}
279
280	/**
281	* Computes a separating word for the two given {@link SPMM}s, if existent. A separating word is a {@link Word} such
282	* that one {@link SPMM} {@link SPMM#computeOutput(Iterable) behaves} different from the other.
283	*
284	* @param spmm1
285	* the first {@link SPMM}
286	* @param spmm2
287	* the second {@link SPMM}
288	* @param alphabet
289	* the {@link ProceduralInputAlphabet} whose symbols should be used for computing the separating word
290	* @param <I>
291	* input symbol type
292	* @param <O>
293	* output symbol type
294	*
295	* @return a separating word, if existent, {@code null} otherwise.
296	*/
297	public static <I, O> @Nullable Word<I> findSeparatingWord(SPMM<?, I, ?, O> spmm1,
298	SPMM<?, I, ?, O> spmm2,
299	ProceduralInputAlphabet<I> alphabet) {
300
301	final ATSequences<I> at1 = computeATSequences(spmm1, alphabet);	2✔
302	final ATSequences<I> at2 = computeATSequences(spmm2, alphabet);	2✔
303
304	return ProceduralUtil.findSeparatingWord(spmm1.getProcedures(), at1, spmm2.getProcedures(), at2, alphabet);	2✔
305	}
306	}

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