6433387082

Committed 06 Oct 2023 03:10PM UTC coverage: 92.296% (-0.007%) from 92.303%

Build # 6433387082

Build Type

push

github

Committed by

mtf90

Commit Message

update Falk's developer id

Run Details

11573 of 12539 relevant lines covered (92.3%)

1.67 hits per line

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

82.35

/commons/counterexamples/src/main/java/de/learnlib/counterexamples/GlobalSuffixFinders.java

/* Copyright (C) 2013-2023 TU Dortmund
 * This file is part of LearnLib, http://www.learnlib.de/.
 *
 * 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 de.learnlib.counterexamples;

import java.util.Collections;
import java.util.List;

import de.learnlib.api.AccessSequenceTransformer;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.Query;
import net.automatalib.automata.concepts.SuffixOutput;
import net.automatalib.words.Word;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * A collection of suffix-based global counterexample analyzers.
 *
 * @see GlobalSuffixFinder
 */
public final class GlobalSuffixFinders {

    /**
     * Adds all suffixes of the input word, as suggested by Maler &amp; Pnueli.
     *
     * @see #findMalerPnueli(Query)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> MALER_PNUELI =
            new GlobalSuffixFinder<@Nullable Object, @Nullable Object>() {

                @Override
                public <RI, RD> List<Word<RI>> findSuffixes(Query<RI, RD> ceQuery,
                                                            AccessSequenceTransformer<RI> asTransformer,
                                                            SuffixOutput<RI, RD> hypOutput,
                                                            MembershipOracle<RI, RD> oracle) {
                    return findMalerPnueli(ceQuery);
                }

                @Override
                public String toString() {
                    return "MalerPnueli";
                }
            };

    /**
     * Adds all suffixes of the remainder of the input word, after stripping a maximal one-letter extension of an access
     * sequence.
     *
     * @see #findShahbaz(Query, AccessSequenceTransformer)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> SHAHBAZ =
            new GlobalSuffixFinder<@Nullable Object, @Nullable Object>() {

                @Override
                public <RI, RD> List<Word<RI>> findSuffixes(Query<RI, RD> ceQuery,
                                                            AccessSequenceTransformer<RI> asTransformer,
                                                            SuffixOutput<RI, RD> hypOutput,
                                                            MembershipOracle<RI, RD> oracle) {
                    return findShahbaz(ceQuery, asTransformer);
                }

                @Override
                public String toString() {
                    return "Shahbaz";
                }
            };

    /**
     * Adds the single suffix found by the access sequence transformation in ascending linear order.
     *
     * @see #findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR =
            fromLocalFinder(LocalSuffixFinders.FIND_LINEAR, false);

    /**
     * Adds the suffix found by the access sequence transformation in ascending linear order, and all of its suffixes.
     *
     * @see #findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR_ALLSUFFIXES =
            fromLocalFinder(LocalSuffixFinders.FIND_LINEAR, true);

    /**
     * Adds the single suffix found by the access sequence transformation in descending linear order.
     *
     * @see #findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR_REVERSE =
            fromLocalFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, false);

    /**
     * Adds the suffix found by the access sequence transformation in descending linear order, and all of its suffixes.
     *
     * @see #findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR_REVERSE_ALLSUFFIXES =
            fromLocalFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, true);

    /**
     * Adds the single suffix found by the access sequence transformation using binary search.
     *
     * @see #findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> RIVEST_SCHAPIRE =
            fromLocalFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, false);

    /**
     * Adds the suffix found by the access sequence transformation using binary search, and all of its suffixes.
     *
     * @see #findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
     */
    public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> RIVEST_SCHAPIRE_ALLSUFFIXES =
            fromLocalFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, true);

    private GlobalSuffixFinders() {
        // prevent instantiation
    }

    /**
     * Transforms a {@link LocalSuffixFinder} into a global one. This is a convenience method, behaving like {@link
     * #fromLocalFinder(LocalSuffixFinder, boolean)}.
     *
     * @see #fromLocalFinder(LocalSuffixFinder, boolean)
     */
    public static <I, D> GlobalSuffixFinder<I, D> fromLocalFinder(LocalSuffixFinder<I, D> localFinder) {
        return fromLocalFinder(localFinder, false);
    }

    /**
     * Transforms a {@link LocalSuffixFinder} into a global one. Since local suffix finders only return a single suffix,
     * suffix-closedness of the set of distinguishing suffixes might not be preserved. Note that for correctly
     * implemented local suffix finders, this does not impair correctness of the learning algorithm. However, without
     * suffix closedness, intermediate hypothesis models might be non-canonical, if no additional precautions are taken.
     * For that reasons, the {@code allSuffixes} parameter can be specified to control whether the list returned by
     * {@link GlobalSuffixFinder#findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)} of the
     * returned global suffix finder should not only contain the single suffix, but also all of its suffixes, ensuring
     * suffix-closedness.
     *
     * @param localFinder
     *         the local suffix finder
     * @param allSuffixes
     *         whether all suffixes of the found local suffix should be added
     *
     * @return a global suffix finder using the analysis method from the specified local suffix finder
     */
    public static <I, D> GlobalSuffixFinder<I, D> fromLocalFinder(LocalSuffixFinder<I, D> localFinder,
                                                                  boolean allSuffixes) {

        return new GlobalSuffixFinder<I, D>() {

            @Override
            public <RI extends I, RD extends D> List<Word<RI>> findSuffixes(Query<RI, RD> ceQuery,
                                                                            AccessSequenceTransformer<RI> asTransformer,
                                                                            SuffixOutput<RI, RD> hypOutput,
                                                                            MembershipOracle<RI, RD> oracle) {
                int idx = localFinder.findSuffixIndex(ceQuery, asTransformer, hypOutput, oracle);
                return suffixesForLocalOutput(ceQuery, idx, allSuffixes);
            }

            @Override
            public String toString() {
                return localFinder.toString() + (allSuffixes ? "-AllSuffixes" : "");
            }
        };
    }

    /**
     * Transforms a suffix index returned by a {@link LocalSuffixFinder} into a list containing the single
     * distinguishing suffix.
     */
    public static <I, D> List<Word<I>> suffixesForLocalOutput(Query<I, D> ceQuery, int localSuffixIdx) {
        return suffixesForLocalOutput(ceQuery, localSuffixIdx, false);
    }

    /**
     * Transforms a suffix index returned by a {@link LocalSuffixFinder} into a list of distinguishing suffixes. This
     * list always contains the corresponding local suffix. Since local suffix finders only return a single suffix,
     * suffix-closedness of the set of distinguishing suffixes might not be preserved. Note that for correctly
     * implemented local suffix finders, this does not impair correctness of the learning algorithm. However, without
     * suffix closedness, intermediate hypothesis models might be non-canonical, if no additional precautions are taken.
     * For that reasons, the {@code allSuffixes} parameter can be specified to control whether the list returned by
     * {@link GlobalSuffixFinder#findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)} of the
     * returned global suffix finder should not only contain the single suffix, but also all of its suffixes, ensuring
     * suffix-closedness.
     */
    public static <I, D> List<Word<I>> suffixesForLocalOutput(Query<I, D> ceQuery,
                                                              int localSuffixIdx,
                                                              boolean allSuffixes) {

        if (localSuffixIdx == -1) {
            return Collections.emptyList();
        }

        Word<I> suffix = ceQuery.getInput().subWord(localSuffixIdx);

        if (!allSuffixes) {
            return Collections.singletonList(suffix);
        }

        return suffix.suffixes(false);
    }

    /**
     * Returns all suffixes of the counterexample word as distinguishing suffixes, as suggested by Maler &amp; Pnueli.
     *
     * @param ceQuery
     *         the counterexample query
     *
     * @return all suffixes of the counterexample input
     */
    public static <I, D> List<Word<I>> findMalerPnueli(Query<I, D> ceQuery) {
        return ceQuery.getInput().suffixes(false);
    }

    /**
     * Returns all suffixes of the counterexample word as distinguishing suffixes, after stripping a maximal one-letter
     * extension of an access sequence, as suggested by Shahbaz.
     *
     * @param ceQuery
     *         the counterexample query
     * @param asTransformer
     *         the access sequence transformer
     *
     * @return all suffixes from the counterexample after stripping a maximal one-letter extension of an access
     * sequence.
     */
    public static <I, D> List<Word<I>> findShahbaz(Query<I, D> ceQuery, AccessSequenceTransformer<I> asTransformer) {
        Word<I> queryWord = ceQuery.getInput();
        int queryLen = queryWord.length();

        Word<I> prefix = ceQuery.getPrefix();
        int i = prefix.length();

        while (i <= queryLen) {
            Word<I> nextPrefix = queryWord.prefix(i);

            if (!asTransformer.isAccessSequence(nextPrefix)) {
                break;
            }
            i++;
        }

        return queryWord.subWord(i).suffixes(false);
    }

    /**
     * Returns the suffix (plus all of its suffixes, if {@code allSuffixes} is true) found by the access sequence
     * transformation in ascending linear order.
     *
     * @param ceQuery
     *         the counterexample query
     * @param asTransformer
     *         the access sequence transformer
     * @param hypOutput
     *         interface to the hypothesis output
     * @param oracle
     *         interface to the SUL output
     * @param allSuffixes
     *         whether to include all suffixes of the found suffix
     *
     * @return the distinguishing suffixes
     *
     * @see LocalSuffixFinders#findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
     */
    public static <I, D> List<Word<I>> findLinear(Query<I, D> ceQuery,
                                                  AccessSequenceTransformer<I> asTransformer,
                                                  SuffixOutput<I, D> hypOutput,
                                                  MembershipOracle<I, D> oracle,
                                                  boolean allSuffixes) {
        int idx = LocalSuffixFinders.findLinear(ceQuery, asTransformer, hypOutput, oracle);
        return suffixesForLocalOutput(ceQuery, idx, allSuffixes);
    }

    /**
     * Returns the suffix (plus all of its suffixes, if {@code allSuffixes} is true) found by the access sequence
     * transformation in descending linear order.
     *
     * @param ceQuery
     *         the counterexample query
     * @param asTransformer
     *         the access sequence transformer
     * @param hypOutput
     *         interface to the hypothesis output
     * @param oracle
     *         interface to the SUL output
     * @param allSuffixes
     *         whether to include all suffixes of the found suffix
     *
     * @return the distinguishing suffixes
     *
     * @see LocalSuffixFinders#findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
     */
    public static <I, D> List<Word<I>> findLinearReverse(Query<I, D> ceQuery,
                                                         AccessSequenceTransformer<I> asTransformer,
                                                         SuffixOutput<I, D> hypOutput,
                                                         MembershipOracle<I, D> oracle,
                                                         boolean allSuffixes) {
        int idx = LocalSuffixFinders.findLinearReverse(ceQuery, asTransformer, hypOutput, oracle);
        return suffixesForLocalOutput(ceQuery, idx, allSuffixes);
    }

    /**
     * Returns the suffix (plus all of its suffixes, if {@code allSuffixes} is true) found by the binary search access
     * sequence transformation.
     *
     * @param ceQuery
     *         the counterexample query
     * @param asTransformer
     *         the access sequence transformer
     * @param hypOutput
     *         interface to the hypothesis output
     * @param oracle
     *         interface to the SUL output
     * @param allSuffixes
     *         whether to include all suffixes of the found suffix
     *
     * @return the distinguishing suffixes
     *
     * @see LocalSuffixFinders#findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
     */
    public static <I, O> List<Word<I>> findRivestSchapire(Query<I, O> ceQuery,
                                                          AccessSequenceTransformer<I> asTransformer,
                                                          SuffixOutput<I, O> hypOutput,
                                                          MembershipOracle<I, O> oracle,
                                                          boolean allSuffixes) {
        int idx = LocalSuffixFinders.findRivestSchapire(ceQuery, asTransformer, hypOutput, oracle);
        return suffixesForLocalOutput(ceQuery, idx, allSuffixes);
    }

    @SuppressWarnings("unchecked")
    public static GlobalSuffixFinder<@Nullable Object, @Nullable Object>[] values() {
        return new GlobalSuffixFinder[] {MALER_PNUELI,
                                         SHAHBAZ,
                                         FIND_LINEAR,
                                         FIND_LINEAR_ALLSUFFIXES,
                                         FIND_LINEAR_REVERSE,
                                         FIND_LINEAR_REVERSE_ALLSUFFIXES,
                                         RIVEST_SCHAPIRE,
                                         RIVEST_SCHAPIRE_ALLSUFFIXES};
    }

}

1	/* Copyright (C) 2013-2023 TU Dortmund
2	* This file is part of LearnLib, http://www.learnlib.de/.
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 de.learnlib.counterexamples;
17
18	import java.util.Collections;
19	import java.util.List;
20
21	import de.learnlib.api.AccessSequenceTransformer;
22	import de.learnlib.api.oracle.MembershipOracle;
23	import de.learnlib.api.query.Query;
24	import net.automatalib.automata.concepts.SuffixOutput;
25	import net.automatalib.words.Word;
26	import org.checkerframework.checker.nullness.qual.Nullable;
27
28	/**
29	* A collection of suffix-based global counterexample analyzers.
30	*
31	* @see GlobalSuffixFinder
32	*/
33	public final class GlobalSuffixFinders {
34
35	/**
36	* Adds all suffixes of the input word, as suggested by Maler & Pnueli.
37	*
38	* @see #findMalerPnueli(Query)
39	*/
40	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> MALER_PNUELI =	1✔
41	new GlobalSuffixFinder<@Nullable Object, @Nullable Object>() {	1✔
42
43	@Override
44	public <RI, RD> List<Word<RI>> findSuffixes(Query<RI, RD> ceQuery,
45	AccessSequenceTransformer<RI> asTransformer,
46	SuffixOutput<RI, RD> hypOutput,
47	MembershipOracle<RI, RD> oracle) {
48	return findMalerPnueli(ceQuery);	1✔
49	}
50
51	@Override
52	public String toString() {
53	return "MalerPnueli";	1✔
54	}
55	};
56
57	/**
58	* Adds all suffixes of the remainder of the input word, after stripping a maximal one-letter extension of an access
59	* sequence.
60	*
61	* @see #findShahbaz(Query, AccessSequenceTransformer)
62	*/
63	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> SHAHBAZ =	1✔
64	new GlobalSuffixFinder<@Nullable Object, @Nullable Object>() {	1✔
65
66	@Override
67	public <RI, RD> List<Word<RI>> findSuffixes(Query<RI, RD> ceQuery,
68	AccessSequenceTransformer<RI> asTransformer,
69	SuffixOutput<RI, RD> hypOutput,
70	MembershipOracle<RI, RD> oracle) {
71	return findShahbaz(ceQuery, asTransformer);	1✔
72	}
73
74	@Override
75	public String toString() {
76	return "Shahbaz";	1✔
77	}
78	};
79
80	/**
81	* Adds the single suffix found by the access sequence transformation in ascending linear order.
82	*
83	* @see #findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
84	*/
85	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR =	1✔
86	fromLocalFinder(LocalSuffixFinders.FIND_LINEAR, false);	1✔
87
88	/**
89	* Adds the suffix found by the access sequence transformation in ascending linear order, and all of its suffixes.
90	*
91	* @see #findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
92	*/
93	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR_ALLSUFFIXES =	1✔
94	fromLocalFinder(LocalSuffixFinders.FIND_LINEAR, true);	1✔
95
96	/**
97	* Adds the single suffix found by the access sequence transformation in descending linear order.
98	*
99	* @see #findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
100	*/
101	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR_REVERSE =	1✔
102	fromLocalFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, false);	1✔
103
104	/**
105	* Adds the suffix found by the access sequence transformation in descending linear order, and all of its suffixes.
106	*
107	* @see #findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
108	*/
109	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> FIND_LINEAR_REVERSE_ALLSUFFIXES =	1✔
110	fromLocalFinder(LocalSuffixFinders.FIND_LINEAR_REVERSE, true);	1✔
111
112	/**
113	* Adds the single suffix found by the access sequence transformation using binary search.
114	*
115	* @see #findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
116	*/
117	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> RIVEST_SCHAPIRE =	1✔
118	fromLocalFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, false);	1✔
119
120	/**
121	* Adds the suffix found by the access sequence transformation using binary search, and all of its suffixes.
122	*
123	* @see #findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle, boolean)
124	*/
125	public static final GlobalSuffixFinder<@Nullable Object, @Nullable Object> RIVEST_SCHAPIRE_ALLSUFFIXES =	1✔
126	fromLocalFinder(LocalSuffixFinders.RIVEST_SCHAPIRE, true);	1✔
127
128	private GlobalSuffixFinders() {
129	// prevent instantiation
130	}
131
132	/**
133	* Transforms a {@link LocalSuffixFinder} into a global one. This is a convenience method, behaving like {@link
134	* #fromLocalFinder(LocalSuffixFinder, boolean)}.
135	*
136	* @see #fromLocalFinder(LocalSuffixFinder, boolean)
137	*/
138	public static <I, D> GlobalSuffixFinder<I, D> fromLocalFinder(LocalSuffixFinder<I, D> localFinder) {
139	return fromLocalFinder(localFinder, false);	×
140	}
141
142	/**
143	* Transforms a {@link LocalSuffixFinder} into a global one. Since local suffix finders only return a single suffix,
144	* suffix-closedness of the set of distinguishing suffixes might not be preserved. Note that for correctly
145	* implemented local suffix finders, this does not impair correctness of the learning algorithm. However, without
146	* suffix closedness, intermediate hypothesis models might be non-canonical, if no additional precautions are taken.
147	* For that reasons, the {@code allSuffixes} parameter can be specified to control whether the list returned by
148	* {@link GlobalSuffixFinder#findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)} of the
149	* returned global suffix finder should not only contain the single suffix, but also all of its suffixes, ensuring
150	* suffix-closedness.
151	*
152	* @param localFinder
153	* the local suffix finder
154	* @param allSuffixes
155	* whether all suffixes of the found local suffix should be added
156	*
157	* @return a global suffix finder using the analysis method from the specified local suffix finder
158	*/
159	public static <I, D> GlobalSuffixFinder<I, D> fromLocalFinder(LocalSuffixFinder<I, D> localFinder,
160	boolean allSuffixes) {
161
162	return new GlobalSuffixFinder<I, D>() {	1✔
163
164	@Override
165	public <RI extends I, RD extends D> List<Word<RI>> findSuffixes(Query<RI, RD> ceQuery,
166	AccessSequenceTransformer<RI> asTransformer,
167	SuffixOutput<RI, RD> hypOutput,
168	MembershipOracle<RI, RD> oracle) {
169	int idx = localFinder.findSuffixIndex(ceQuery, asTransformer, hypOutput, oracle);	1✔
170	return suffixesForLocalOutput(ceQuery, idx, allSuffixes);	1✔
171	}
172
173	@Override
174	public String toString() {
175	return localFinder.toString() + (allSuffixes ? "-AllSuffixes" : "");	1✔
176	}
177	};
178	}
179
180	/**
181	* Transforms a suffix index returned by a {@link LocalSuffixFinder} into a list containing the single
182	* distinguishing suffix.
183	*/
184	public static <I, D> List<Word<I>> suffixesForLocalOutput(Query<I, D> ceQuery, int localSuffixIdx) {
185	return suffixesForLocalOutput(ceQuery, localSuffixIdx, false);	×
186	}
187
188	/**
189	* Transforms a suffix index returned by a {@link LocalSuffixFinder} into a list of distinguishing suffixes. This
190	* list always contains the corresponding local suffix. Since local suffix finders only return a single suffix,
191	* suffix-closedness of the set of distinguishing suffixes might not be preserved. Note that for correctly
192	* implemented local suffix finders, this does not impair correctness of the learning algorithm. However, without
193	* suffix closedness, intermediate hypothesis models might be non-canonical, if no additional precautions are taken.
194	* For that reasons, the {@code allSuffixes} parameter can be specified to control whether the list returned by
195	* {@link GlobalSuffixFinder#findSuffixes(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)} of the
196	* returned global suffix finder should not only contain the single suffix, but also all of its suffixes, ensuring
197	* suffix-closedness.
198	*/
199	public static <I, D> List<Word<I>> suffixesForLocalOutput(Query<I, D> ceQuery,
200	int localSuffixIdx,
201	boolean allSuffixes) {
202
203	if (localSuffixIdx == -1) {	1✔
204	return Collections.emptyList();	×
205	}
206
207	Word<I> suffix = ceQuery.getInput().subWord(localSuffixIdx);	1✔
208
209	if (!allSuffixes) {	1✔
210	return Collections.singletonList(suffix);	1✔
211	}
212
213	return suffix.suffixes(false);	1✔
214	}
215
216	/**
217	* Returns all suffixes of the counterexample word as distinguishing suffixes, as suggested by Maler & Pnueli.
218	*
219	* @param ceQuery
220	* the counterexample query
221	*
222	* @return all suffixes of the counterexample input
223	*/
224	public static <I, D> List<Word<I>> findMalerPnueli(Query<I, D> ceQuery) {
225	return ceQuery.getInput().suffixes(false);	1✔
226	}
227
228	/**
229	* Returns all suffixes of the counterexample word as distinguishing suffixes, after stripping a maximal one-letter
230	* extension of an access sequence, as suggested by Shahbaz.
231	*
232	* @param ceQuery
233	* the counterexample query
234	* @param asTransformer
235	* the access sequence transformer
236	*
237	* @return all suffixes from the counterexample after stripping a maximal one-letter extension of an access
238	* sequence.
239	*/
240	public static <I, D> List<Word<I>> findShahbaz(Query<I, D> ceQuery, AccessSequenceTransformer<I> asTransformer) {
241	Word<I> queryWord = ceQuery.getInput();	1✔
242	int queryLen = queryWord.length();	1✔
243
244	Word<I> prefix = ceQuery.getPrefix();	1✔
245	int i = prefix.length();	1✔
246
247	while (i <= queryLen) {	1✔
248	Word<I> nextPrefix = queryWord.prefix(i);	1✔
249
250	if (!asTransformer.isAccessSequence(nextPrefix)) {	1✔
251	break;	1✔
252	}
253	i++;	1✔
254	}	1✔
255
256	return queryWord.subWord(i).suffixes(false);	1✔
257	}
258
259	/**
260	* Returns the suffix (plus all of its suffixes, if {@code allSuffixes} is true) found by the access sequence
261	* transformation in ascending linear order.
262	*
263	* @param ceQuery
264	* the counterexample query
265	* @param asTransformer
266	* the access sequence transformer
267	* @param hypOutput
268	* interface to the hypothesis output
269	* @param oracle
270	* interface to the SUL output
271	* @param allSuffixes
272	* whether to include all suffixes of the found suffix
273	*
274	* @return the distinguishing suffixes
275	*
276	* @see LocalSuffixFinders#findLinear(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
277	*/
278	public static <I, D> List<Word<I>> findLinear(Query<I, D> ceQuery,
279	AccessSequenceTransformer<I> asTransformer,
280	SuffixOutput<I, D> hypOutput,
281	MembershipOracle<I, D> oracle,
282	boolean allSuffixes) {
283	int idx = LocalSuffixFinders.findLinear(ceQuery, asTransformer, hypOutput, oracle);	×
284	return suffixesForLocalOutput(ceQuery, idx, allSuffixes);	×
285	}
286
287	/**
288	* Returns the suffix (plus all of its suffixes, if {@code allSuffixes} is true) found by the access sequence
289	* transformation in descending linear order.
290	*
291	* @param ceQuery
292	* the counterexample query
293	* @param asTransformer
294	* the access sequence transformer
295	* @param hypOutput
296	* interface to the hypothesis output
297	* @param oracle
298	* interface to the SUL output
299	* @param allSuffixes
300	* whether to include all suffixes of the found suffix
301	*
302	* @return the distinguishing suffixes
303	*
304	* @see LocalSuffixFinders#findLinearReverse(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
305	*/
306	public static <I, D> List<Word<I>> findLinearReverse(Query<I, D> ceQuery,
307	AccessSequenceTransformer<I> asTransformer,
308	SuffixOutput<I, D> hypOutput,
309	MembershipOracle<I, D> oracle,
310	boolean allSuffixes) {
311	int idx = LocalSuffixFinders.findLinearReverse(ceQuery, asTransformer, hypOutput, oracle);	×
312	return suffixesForLocalOutput(ceQuery, idx, allSuffixes);	×
313	}
314
315	/**
316	* Returns the suffix (plus all of its suffixes, if {@code allSuffixes} is true) found by the binary search access
317	* sequence transformation.
318	*
319	* @param ceQuery
320	* the counterexample query
321	* @param asTransformer
322	* the access sequence transformer
323	* @param hypOutput
324	* interface to the hypothesis output
325	* @param oracle
326	* interface to the SUL output
327	* @param allSuffixes
328	* whether to include all suffixes of the found suffix
329	*
330	* @return the distinguishing suffixes
331	*
332	* @see LocalSuffixFinders#findRivestSchapire(Query, AccessSequenceTransformer, SuffixOutput, MembershipOracle)
333	*/
334	public static <I, O> List<Word<I>> findRivestSchapire(Query<I, O> ceQuery,
335	AccessSequenceTransformer<I> asTransformer,
336	SuffixOutput<I, O> hypOutput,
337	MembershipOracle<I, O> oracle,
338	boolean allSuffixes) {
339	int idx = LocalSuffixFinders.findRivestSchapire(ceQuery, asTransformer, hypOutput, oracle);	×
340	return suffixesForLocalOutput(ceQuery, idx, allSuffixes);	×
341	}
342
343	@SuppressWarnings("unchecked")
344	public static GlobalSuffixFinder<@Nullable Object, @Nullable Object>[] values() {
345	return new GlobalSuffixFinder[] {MALER_PNUELI,	1✔
346	SHAHBAZ,
347	FIND_LINEAR,
348	FIND_LINEAR_ALLSUFFIXES,
349	FIND_LINEAR_REVERSE,
350	FIND_LINEAR_REVERSE_ALLSUFFIXES,
351	RIVEST_SCHAPIRE,
352	RIVEST_SCHAPIRE_ALLSUFFIXES};
353	}
354
355	}

LearnLib / learnlib / 6433387082

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