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

80.95

/oracles/equivalence-oracles/src/main/java/de/learnlib/oracle/equivalence/SampleSetEQOracle.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.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.api.oracle.EquivalenceOracle;
import de.learnlib.api.oracle.MembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import de.learnlib.api.query.Query;
import net.automatalib.automata.concepts.SuffixOutput;
import net.automatalib.words.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. 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 ArrayList<>();
        } else {
            testQueries = new LinkedList<>(); // for O(1) removal of elements
        }
    }

    /**
     * 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-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.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.api.oracle.EquivalenceOracle;
27	import de.learnlib.api.oracle.MembershipOracle;
28	import de.learnlib.api.query.DefaultQuery;
29	import de.learnlib.api.query.Query;
30	import net.automatalib.automata.concepts.SuffixOutput;
31	import net.automatalib.words.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. Initializes the oracle with an empty sample set.
58	*
59	* @param removeUnsuccessful
60	* if set to {@code true}, queries will be removed from the sample set if they did not reveal a
61	* counterexample. Otherwise, all queries from the sample set will always be tested upon each invocation of
62	* {@link #findCounterExample(SuffixOutput, Collection)}.
63	*/
64	public SampleSetEQOracle(boolean removeUnsuccessful) {	2✔
65	this.removeUnsuccessful = removeUnsuccessful;	2✔
66	if (!removeUnsuccessful) {	2✔
67	testQueries = new ArrayList<>();	1✔
68	} else {
69	testQueries = new LinkedList<>(); // for O(1) removal of elements	2✔
70	}
71	}	2✔
72
73	/**
74	* Adds a query word along with its expected output to the sample set.
75	*
76	* @param input
77	* the input word
78	* @param expectedOutput
79	* the expected output for this word
80	*
81	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
82	*/
83	public SampleSetEQOracle<I, D> add(Word<I> input, D expectedOutput) {
84	testQueries.add(new DefaultQuery<>(input, expectedOutput));	2✔
85	return this;	2✔
86	}
87
88	/**
89	* Adds several query words to the sample set. The expected output is determined by means of the specified
90	* membership oracle.
91	*
92	* @param oracle
93	* the membership oracle used to determine expected outputs
94	* @param words
95	* the words to be added to the sample set
96	*
97	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
98	*/
99	@SafeVarargs
100	public final SampleSetEQOracle<I, D> addAll(MembershipOracle<I, D> oracle, Word<I>... words) {
101	return addAll(oracle, Arrays.asList(words));	1✔
102	}
103
104	/**
105	* Adds words to the sample set. The expected output is determined by means of the specified membership oracle.
106	*
107	* @param oracle
108	* the membership oracle used to determine the expected output
109	* @param words
110	* the words to add
111	*
112	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
113	*/
114	public SampleSetEQOracle<I, D> addAll(MembershipOracle<I, D> oracle, Collection<? extends Word<I>> words) {
115	if (words.isEmpty()) {	2✔
116	return this;	×
117	}
118	List<DefaultQuery<I, D>> newQueries = new ArrayList<>(words.size());	2✔
119	for (Word<I> w : words) {	2✔
120	newQueries.add(new DefaultQuery<>(w));	2✔
121	}	2✔
122	oracle.processQueries(newQueries);	2✔
123
124	testQueries.addAll(newQueries);	2✔
125	return this;	2✔
126	}
127
128	/**
129	* Adds queries to the sample set. These must be {@link DefaultQuery}s, which allow for retrieving the corresponding
130	* (expected) output.
131	*
132	* @param newTestQueries
133	* the queries to add to the sample set
134	*
135	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
136	*/
137	@SafeVarargs
138	public final SampleSetEQOracle<I, D> addAll(DefaultQuery<I, D>... newTestQueries) {
139	return addAll(Arrays.asList(newTestQueries));	×
140	}
141
142	/**
143	* Adds queries to the sample set. These must be {@link DefaultQuery}s, which allow for retrieving the corresponding
144	* (expected) output.
145	*
146	* @param newTestQueries
147	* the queries to add to the sample set
148	*
149	* @return {@code this}, to enable chained {@code add} or {@code addAll} calls
150	*/
151	public SampleSetEQOracle<I, D> addAll(Collection<? extends DefaultQuery<I, D>> newTestQueries) {
152	testQueries.addAll(newTestQueries);	×
153	return this;	×
154	}
155
156	@Override
157	public @Nullable DefaultQuery<I, D> findCounterExample(SuffixOutput<I, D> hypothesis,
158	Collection<? extends I> inputs) {
159	Iterator<DefaultQuery<I, D>> queryIt = testQueries.iterator();	2✔
160
161	while (queryIt.hasNext()) {	2✔
162	DefaultQuery<I, D> query = queryIt.next();	2✔
163
164	if (checkInputs(query, inputs)) {	2✔
165	if (!test(query, hypothesis)) {	2✔
166	return query;	1✔
167	} else if (removeUnsuccessful) {	2✔
168	queryIt.remove();	2✔
169	}
170	}
171	}	2✔
172	return null;	2✔
173	}
174
175	/**
176	* Tests if the input word of the given {@link Query} consists entirely of symbols in {@code inputs}.
177	*
178	* @param query
179	* the query to test
180	* @param inputs
181	* the set of allowed inputs
182	*
183	* @return {@code true} if the input word of {@code query} consists entirely of symbols in {@code inputs}, {@code
184	* false} otherwise
185	*/
186	private static <I> boolean checkInputs(Query<I, ?> query, Collection<? extends I> inputs) {
187	for (I sym : query.getPrefix()) {	2✔
188	if (!inputs.contains(sym)) {	×
189	return false;	×
190	}
191	}	×
192	for (I sym : query.getSuffix()) {	2✔
193	if (!inputs.contains(sym)) {	2✔
194	return false;	×
195	}
196	}	2✔
197	return true;	2✔
198	}
199
200	/**
201	* Tests if the suffix output of the given hypothesis matches the expected output stored in the query.
202	*
203	* @param query
204	* the query, containing the expected output
205	* @param hypOutput
206	* the suffix output portion of the hypothesis
207	*
208	* @return {@code true} if the suffix output by {@code hypOutput} matches the expected output stored in {@code
209	* query}, {@code false} otherwise.
210	*/
211	private static <I, D> boolean test(DefaultQuery<I, D> query, SuffixOutput<I, D> hypOutput) {
212	D hypOut = hypOutput.computeSuffixOutput(query.getPrefix(), query.getSuffix());	2✔
213
214	return Objects.equals(hypOut, query.getOutput());	2✔
215	}
216
217	}

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