13034511199

Committed 29 Jan 2025 03:18PM UTC coverage: 94.304% (-0.09%) from 94.389%

Build # 13034511199

Build Type

push

github

Committed by

mtf90

Commit Message

spmm: improve assertions

Run Details

2 of 2 new or added lines in 1 file covered. (100.0%)

24 existing lines in 7 files now uncovered.

12417 of 13167 relevant lines covered (94.3%)

1.72 hits per line

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

81.82

/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/SampleSetEQOracle.java

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of LearnLib <https://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.oracle.equivalence;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Objects;

import de.learnlib.oracle.EquivalenceOracle;
import de.learnlib.oracle.MembershipOracle;
import de.learnlib.query.DefaultQuery;
import de.learnlib.query.Query;
import net.automatalib.automaton.concept.SuffixOutput;
import net.automatalib.word.Word;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * An equivalence oracle that tests a hypothesis against a fixed set of sample queries.
 * <p>
 * Sample queries are provided through one of the {@code add(...)} or {@code addAll(...)} methods of this class. A query
 * consists of an <i>input word</i> (split into a <i>prefix</i> and a <i>suffix</i>), and an expected <i>output</i>.
 * During an equivalence query, for each of those queries if the respective actual suffix output of the hypothesis
 * equals the expected output.
 * <p>
 * This oracle will always repeatedly test queries from the sample set if they turned out to be counterexamples.
 * However, the oracle can be configured to remove queries from the sample set if they did not serve as
 * counterexamples.
 *
 * @param <I>
 *         input symbol type
 * @param <D>
 *         output domain type
 */
public class SampleSetEQOracle<I, D> implements EquivalenceOracle<SuffixOutput<I, D>, I, D> {

    private final boolean removeUnsuccessful;
    private final List<DefaultQuery<I, D>> testQueries;

    /**
     * Constructor. Convenience method for {@link #SampleSetEQOracle(boolean)} that does not remove unsuccessful
     * samples.
     */
    public SampleSetEQOracle() {
        this(false);
    }

    /**
     * Constructor. Initializes the oracle with an empty sample set.
     *
     * @param removeUnsuccessful
     *         if set to {@code true}, queries will be removed from the sample set if they did not reveal a
     *         counterexample. Otherwise, all queries from the sample set will always be tested upon each invocation of
     *         {@link #findCounterExample(SuffixOutput, Collection)}.
     */
    public SampleSetEQOracle(boolean removeUnsuccessful) {
        this.removeUnsuccessful = removeUnsuccessful;
        if (removeUnsuccessful) {
            testQueries = new LinkedList<>(); // for O(1) removal of elements
        } else {
            testQueries = new ArrayList<>();
        }
    }

    /**
     * Adds a query word along with its expected output to the sample set.
     *
     * @param input
     *         the input word
     * @param expectedOutput
     *         the expected output for this word
     *
     * @return {@code this}, to enable chained {@code add} or {@code addAll} calls
     */
    public SampleSetEQOracle<I, D> add(Word<I> input, D expectedOutput) {
        testQueries.add(new DefaultQuery<>(input, expectedOutput));
        return this;
    }

    /**
     * Adds several query words to the sample set. The expected output is determined by means of the specified
     * membership oracle.
     *
     * @param oracle
     *         the membership oracle used to determine expected outputs
     * @param words
     *         the words to be added to the sample set
     *
     * @return {@code this}, to enable chained {@code add} or {@code addAll} calls
     */
    @SafeVarargs
    public final SampleSetEQOracle<I, D> addAll(MembershipOracle<I, D> oracle, Word<I>... words) {
        return addAll(oracle, Arrays.asList(words));
    }

    /**
     * Adds words to the sample set. The expected output is determined by means of the specified membership oracle.
     *
     * @param oracle
     *         the membership oracle used to determine the expected output
     * @param words
     *         the words to add
     *
     * @return {@code this}, to enable chained {@code add} or {@code addAll} calls
     */
    public SampleSetEQOracle<I, D> addAll(MembershipOracle<I, D> oracle, Collection<? extends Word<I>> words) {
        if (words.isEmpty()) {
            return this;
        }
        List<DefaultQuery<I, D>> newQueries = new ArrayList<>(words.size());
        for (Word<I> w : words) {
            newQueries.add(new DefaultQuery<>(w));
        }
        oracle.processQueries(newQueries);

        testQueries.addAll(newQueries);
        return this;
    }

    /**
     * Adds queries to the sample set. These must be {@link DefaultQuery}s, which allow for retrieving the corresponding
     * (expected) output.
     *
     * @param newTestQueries
     *         the queries to add to the sample set
     *
     * @return {@code this}, to enable chained {@code add} or {@code addAll} calls
     */
    @SafeVarargs
    public final SampleSetEQOracle<I, D> addAll(DefaultQuery<I, D>... newTestQueries) {
        return addAll(Arrays.asList(newTestQueries));
    }

    /**
     * Adds queries to the sample set. These must be {@link DefaultQuery}s, which allow for retrieving the corresponding
     * (expected) output.
     *
     * @param newTestQueries
     *         the queries to add to the sample set
     *
     * @return {@code this}, to enable chained {@code add} or {@code addAll} calls
     */
    public SampleSetEQOracle<I, D> addAll(Collection<? extends DefaultQuery<I, D>> newTestQueries) {
        testQueries.addAll(newTestQueries);
        return this;
    }

    @Override
    public @Nullable DefaultQuery<I, D> findCounterExample(SuffixOutput<I, D> hypothesis,
                                                           Collection<? extends I> inputs) {
        Iterator<DefaultQuery<I, D>> queryIt = testQueries.iterator();

        while (queryIt.hasNext()) {
            DefaultQuery<I, D> query = queryIt.next();

            if (checkInputs(query, inputs)) {
                if (!test(query, hypothesis)) {
                    return query;
                } else if (removeUnsuccessful) {
                    queryIt.remove();
                }
            }
        }
        return null;
    }

    /**
     * Tests if the input word of the given {@link Query} consists entirely of symbols in {@code inputs}.
     *
     * @param query
     *         the query to test
     * @param inputs
     *         the set of allowed inputs
     *
     * @return {@code true} if the input word of {@code query} consists entirely of symbols in {@code inputs},
     * {@code false} otherwise
     */
    private static <I> boolean checkInputs(Query<I, ?> query, Collection<? extends I> inputs) {
        for (I sym : query.getPrefix()) {
            if (!inputs.contains(sym)) {
                return false;
            }
        }
        for (I sym : query.getSuffix()) {
            if (!inputs.contains(sym)) {
                return false;
            }
        }
        return true;
    }

    /**
     * Tests if the suffix output of the given hypothesis matches the expected output stored in the query.
     *
     * @param query
     *         the query, containing the expected output
     * @param hypOutput
     *         the suffix output portion of the hypothesis
     *
     * @return {@code true} if the suffix output by {@code hypOutput} matches the expected output stored in
     * {@code query}, {@code false} otherwise.
     */
    private static <I, D> boolean test(DefaultQuery<I, D> query, SuffixOutput<I, D> hypOutput) {
        D hypOut = hypOutput.computeSuffixOutput(query.getPrefix(), query.getSuffix());

        return Objects.equals(hypOut, query.getOutput());
    }

}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of LearnLib <https://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.oracle.equivalence;
17
18	import java.util.ArrayList;
19	import java.util.Arrays;
20	import java.util.Collection;
21	import java.util.Iterator;
22	import java.util.LinkedList;
23	import java.util.List;
24	import java.util.Objects;
25
26	import de.learnlib.oracle.EquivalenceOracle;
27	import de.learnlib.oracle.MembershipOracle;
28	import de.learnlib.query.DefaultQuery;
29	import de.learnlib.query.Query;
30	import net.automatalib.automaton.concept.SuffixOutput;
31	import net.automatalib.word.Word;
32	import org.checkerframework.checker.nullness.qual.Nullable;
33
34	/**
35	* An equivalence oracle that tests a hypothesis against a fixed set of sample queries.
36	* <p>
37	* Sample queries are provided through one of the {@code add(...)} or {@code addAll(...)} methods of this class. A query
38	* consists of an <i>input word</i> (split into a <i>prefix</i> and a <i>suffix</i>), and an expected <i>output</i>.
39	* During an equivalence query, for each of those queries if the respective actual suffix output of the hypothesis
40	* equals the expected output.
41	* <p>
42	* This oracle will always repeatedly test queries from the sample set if they turned out to be counterexamples.
43	* However, the oracle can be configured to remove queries from the sample set if they did not serve as
44	* counterexamples.
45	*
46	* @param <I>
47	* input symbol type
48	* @param <D>
49	* output domain type
50	*/
51	public class SampleSetEQOracle<I, D> implements EquivalenceOracle<SuffixOutput<I, D>, I, D> {
52
53	private final boolean removeUnsuccessful;
54	private final List<DefaultQuery<I, D>> testQueries;
55
56	/**
57	* Constructor. Convenience method for {@link #SampleSetEQOracle(boolean)} that does not remove unsuccessful
58	* samples.
59	*/
60	public SampleSetEQOracle() {
61	this(false);	1✔
62	}	1✔
63
64	/**
65	* Constructor. Initializes the oracle with an empty sample set.
66	*
67	* @param removeUnsuccessful
68	* if set to {@code true}, queries will be removed from the sample set if they did not reveal a
69	* counterexample. Otherwise, all queries from the sample set will always be tested upon each invocation of
70	* {@link #findCounterExample(SuffixOutput, Collection)}.
71	*/
72	public SampleSetEQOracle(boolean removeUnsuccessful) {	2✔
73	this.removeUnsuccessful = removeUnsuccessful;	2✔
74	if (removeUnsuccessful) {	2✔
75	testQueries = new LinkedList<>(); // for O(1) removal of elements	2✔
76	} else {
77	testQueries = new ArrayList<>();	1✔
78	}
79	}	2✔
80
81	/**
82	* Adds a query word along with its expected output to the sample set.
83	*
84	* @param input
85	* the input word
86	* @param expectedOutput
87	* the expected output for this word
88	*
89	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
90	*/
91	public SampleSetEQOracle<I, D> add(Word<I> input, D expectedOutput) {
92	testQueries.add(new DefaultQuery<>(input, expectedOutput));	2✔
93	return this;	2✔
94	}
95
96	/**
97	* Adds several query words to the sample set. The expected output is determined by means of the specified
98	* membership oracle.
99	*
100	* @param oracle
101	* the membership oracle used to determine expected outputs
102	* @param words
103	* the words to be added to the sample set
104	*
105	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
106	*/
107	@SafeVarargs
108	public final SampleSetEQOracle<I, D> addAll(MembershipOracle<I, D> oracle, Word<I>... words) {
109	return addAll(oracle, Arrays.asList(words));	1✔
110	}
111
112	/**
113	* Adds words to the sample set. The expected output is determined by means of the specified membership oracle.
114	*
115	* @param oracle
116	* the membership oracle used to determine the expected output
117	* @param words
118	* the words to add
119	*
120	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
121	*/
122	public SampleSetEQOracle<I, D> addAll(MembershipOracle<I, D> oracle, Collection<? extends Word<I>> words) {
123	if (words.isEmpty()) {	2✔
UNCOV 124	return this;	×
125	}
126	List<DefaultQuery<I, D>> newQueries = new ArrayList<>(words.size());	2✔
127	for (Word<I> w : words) {	2✔
128	newQueries.add(new DefaultQuery<>(w));	2✔
129	}	2✔
130	oracle.processQueries(newQueries);	2✔
131
132	testQueries.addAll(newQueries);	2✔
133	return this;	2✔
134	}
135
136	/**
137	* Adds queries to the sample set. These must be {@link DefaultQuery}s, which allow for retrieving the corresponding
138	* (expected) output.
139	*
140	* @param newTestQueries
141	* the queries to add to the sample set
142	*
143	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
144	*/
145	@SafeVarargs
146	public final SampleSetEQOracle<I, D> addAll(DefaultQuery<I, D>... newTestQueries) {
UNCOV 147	return addAll(Arrays.asList(newTestQueries));	×
148	}
149
150	/**
151	* Adds queries to the sample set. These must be {@link DefaultQuery}s, which allow for retrieving the corresponding
152	* (expected) output.
153	*
154	* @param newTestQueries
155	* the queries to add to the sample set
156	*
157	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
158	*/
159	public SampleSetEQOracle<I, D> addAll(Collection<? extends DefaultQuery<I, D>> newTestQueries) {
UNCOV 160	testQueries.addAll(newTestQueries);	×
UNCOV 161	return this;	×
162	}
163
164	@Override
165	public @Nullable DefaultQuery<I, D> findCounterExample(SuffixOutput<I, D> hypothesis,
166	Collection<? extends I> inputs) {
167	Iterator<DefaultQuery<I, D>> queryIt = testQueries.iterator();	2✔
168
169	while (queryIt.hasNext()) {	2✔
170	DefaultQuery<I, D> query = queryIt.next();	2✔
171
172	if (checkInputs(query, inputs)) {	2✔
173	if (!test(query, hypothesis)) {	2✔
174	return query;	1✔
175	} else if (removeUnsuccessful) {	2✔
176	queryIt.remove();	2✔
177	}
178	}
179	}	2✔
180	return null;	2✔
181	}
182
183	/**
184	* Tests if the input word of the given {@link Query} consists entirely of symbols in {@code inputs}.
185	*
186	* @param query
187	* the query to test
188	* @param inputs
189	* the set of allowed inputs
190	*
191	* @return {@code true} if the input word of {@code query} consists entirely of symbols in {@code inputs},
192	* {@code false} otherwise
193	*/
194	private static <I> boolean checkInputs(Query<I, ?> query, Collection<? extends I> inputs) {
195	for (I sym : query.getPrefix()) {	2✔
UNCOV 196	if (!inputs.contains(sym)) {	×
UNCOV 197	return false;	×
198	}
UNCOV 199	}	×
200	for (I sym : query.getSuffix()) {	2✔
201	if (!inputs.contains(sym)) {	2✔
UNCOV 202	return false;	×
203	}
204	}	2✔
205	return true;	2✔
206	}
207
208	/**
209	* Tests if the suffix output of the given hypothesis matches the expected output stored in the query.
210	*
211	* @param query
212	* the query, containing the expected output
213	* @param hypOutput
214	* the suffix output portion of the hypothesis
215	*
216	* @return {@code true} if the suffix output by {@code hypOutput} matches the expected output stored in
217	* {@code query}, {@code false} otherwise.
218	*/
219	private static <I, D> boolean test(DefaultQuery<I, D> query, SuffixOutput<I, D> hypOutput) {
220	D hypOut = hypOutput.computeSuffixOutput(query.getPrefix(), query.getSuffix());	2✔
221
222	return Objects.equals(hypOut, query.getOutput());	2✔
223	}
224
225	}

LearnLib / learnlib / 13034511199

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