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

98.48

/oracles/membership-oracles/src/main/java/de/learnlib/oracle/membership/AbstractSULOmegaOracle.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.membership;

import java.util.ArrayList;
import java.util.Collection;
import java.util.List;

import de.learnlib.api.ObservableSUL;
import de.learnlib.api.SUL;
import de.learnlib.api.oracle.MembershipOracle.MealyMembershipOracle;
import de.learnlib.api.oracle.OmegaMembershipOracle;
import de.learnlib.api.oracle.OmegaMembershipOracle.MealyOmegaMembershipOracle;
import de.learnlib.api.query.OmegaQuery;
import net.automatalib.commons.util.Pair;
import net.automatalib.words.Word;
import net.automatalib.words.WordBuilder;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * An omega membership oracle for an {@link ObservableSUL}.
 * <p>
 * The behavior is similar to a {@link SULOracle}, except that this class answers {@link OmegaQuery}s.
 * <p>
 * After some symbols (i.e. after {@link OmegaQuery#getPrefix()}, and after each {@link OmegaQuery#getLoop()}) the state
 * of the {@link ObservableSUL} is retrieved, and used to answer the query.
 * <p>
 * This class is <b>not</b> thread-safe.
 *
 * @param <S>
 *         the state type of the {@link ObservableSUL}
 * @param <I>
 *         the input type
 * @param <O>
 *         the output type
 * @param <Q>
 *         the state information type that is used to answer {@link OmegaQuery}s
 */
public abstract class AbstractSULOmegaOracle<S extends Object, I, O, Q> implements MealyOmegaMembershipOracle<Q, I, O> {

    private final ObservableSUL<S, I, O> sul;

    protected AbstractSULOmegaOracle(ObservableSUL<S, I, O> sul) {
        this.sul = sul;
    }

    /**
     * Gets the {@link ObservableSUL}.
     *
     * @return the {@link ObservableSUL}.
     */
    public ObservableSUL<S, I, O> getSul() {
        return sul;
    }

    @Override
    public void processQueries(Collection<? extends OmegaQuery<I, Word<O>>> queries) {
        for (OmegaQuery<I, Word<O>> q : queries) {
            final Pair<@Nullable Word<O>, Integer> output = answerQuery(q.getPrefix(), q.getLoop(), q.getRepeat());
            q.answer(output.getFirst(), output.getSecond());
        }
    }

    protected abstract Q getQueryState(ObservableSUL<S, I, O> sul);

    @Override
    public Pair<@Nullable Word<O>, Integer> answerQuery(Word<I> prefix, Word<I> loop, int repeat) {
        assert repeat > 0;
        sul.pre();
        try {
            final int traceLength = prefix.length() + loop.length() * repeat;
            final WordBuilder<I> inputBuilder = new WordBuilder<>(traceLength, prefix);
            final WordBuilder<O> outputBuilder = new WordBuilder<>(traceLength);
            final List<Q> states = new ArrayList<>(repeat + 1);

            for (int i = 0; i < prefix.length(); i++) {
                outputBuilder.append(sul.step(prefix.getSymbol(i)));
            }
            states.add(getQueryState(sul));

            for (int i = 0; i < repeat; i++) {
                inputBuilder.append(loop);
                for (int j = 0; j < loop.length(); j++) {
                    outputBuilder.append(sul.step(loop.getSymbol(j)));
                }
                final Q nextState = getQueryState(sul);

                int prefixLength = prefix.length();
                for (Q q: states) {
                    if (isSameState(inputBuilder.toWord(), nextState, inputBuilder.toWord(0, prefixLength), q)) {
                        return Pair.of(outputBuilder.toWord(), i + 1);
                    }
                    prefixLength += loop.length();
                }
                states.add(nextState);
            }

            return Pair.of(null, -1);
        } finally {
            sul.post();
        }
    }

    @Override
    public MealyMembershipOracle<I, O> getMembershipOracle() {
        return new SULOracle<>(sul);
    }

    /**
     * Creates a new {@link AbstractSULOmegaOracle}, while making sure the invariants of the {@link ObservableSUL} are
     * satisfied.
     *
     * @param sul the {@link ObservableSUL} to wrap around.
     * @param deepCopies whether to test for state equivalence directly on the retrieved state.
     *
     * @param <S> the state type
     * @param <I> the input type
     * @param <O> the output type
     *
     * @return the {@link AbstractSULOmegaOracle}.
     */
    public static <S extends Object, I, O> AbstractSULOmegaOracle<S, I, O, ?> newOracle(ObservableSUL<S, I, O> sul,
                                                                                        boolean deepCopies) {
        final AbstractSULOmegaOracle<S, I, O, ?> abstractSulOmegaOracle;
        if (deepCopies) {
            if (!sul.deepCopies()) {
                throw new IllegalArgumentException("SUL can not make deep copies of states.");
            } else {
                abstractSulOmegaOracle = new DeepCopySULOmegaOracle<>(sul);
            }
        } else {
            if (!sul.canFork()) {
                throw new IllegalArgumentException("SUL must be forkable.");
            } else {
                abstractSulOmegaOracle = new ShallowCopySULOmegaOracle<>(sul);
            }
        }

        return abstractSulOmegaOracle;
    }

    /**
     * Creates a new {@link AbstractSULOmegaOracle} that assumes the {@link SUL} can not make deep copies.
     *
     * @see #newOracle(ObservableSUL, boolean)
     *
     * @param <S> the state type
     * @param <I> the input type
     * @param <O> the output type
     */
    public static <S extends Object, I, O> AbstractSULOmegaOracle<S, I, O, ?> newOracle(ObservableSUL<S, I, O> sul) {
        return newOracle(sul, !sul.canFork());
    }

    /**
     * A {@link AbstractSULOmegaOracle} that uses {@link Object#hashCode()}, and {@link Object#equals(Object)} to test
     * for state equivalence. When the hash codes of two states are equal this class will use two access sequences to
     * move two {@link ObservableSUL}s to those states and perform an equality check.
     * <p>
     * The state information used to answer {@link OmegaQuery}s is of type {@link Integer}. The values of those integers
     * are actually hash codes of states of the {@link ObservableSUL}.
     *
     * @param <S> the state type
     * @param <I> the input type
     * @param <O> the output type
     */
    private static final class ShallowCopySULOmegaOracle<S extends Object, I, O>
            extends AbstractSULOmegaOracle<S, I, O, Integer> {

        /**
         * A forked {@link SUL} is necessary when we need to step to two particular states at the same time.
         */
        private final ObservableSUL<S, I, O> forkedSUL;

        /**
         * Constructs a new {@link ShallowCopySULOmegaOracle}, use {@link #newOracle(ObservableSUL)} to create an
         * instance. This method makes sure the invariants of the {@link ObservableSUL} are satisfied (i.e., the {@link
         * ObservableSUL} must be forkable, i.e. ({@code {@link SUL#canFork()} == true}).
         *
         * @param sul the SUL
         */
        ShallowCopySULOmegaOracle(ObservableSUL<S, I, O> sul) {
            super(sul);
            assert sul.canFork();
            forkedSUL = sul.fork();
        }

        /**
         * Returns the state as a hash code.
         *
         * @param sul the {@link ObservableSUL} to retrieve the current state from.
         *
         * @return the hash code of the state.
         */
        @Override
        protected Integer getQueryState(ObservableSUL<S, I, O> sul) {
            return sul.getState().hashCode();
        }

        /**
         * Test for state equivalence, by means of {@link Object#hashCode()}, and {@link Object#equals(Object)}.
         *
         * @see OmegaMembershipOracle#isSameState(Word, Object, Word, Object)
         *
         * @return whether the following conditions hold:
         *  1. the hash codes are the same, i.e. {@code s1.equals(s2)}, and
         *  2. the two access sequences lead to the same state.
         */
        @Override
        public boolean isSameState(Word<I> input1, Integer s1, Word<I> input2, Integer s2) {
            if (!s1.equals(s2)) {
                return false;
            } else {
                // in this case the hash codes are equal, now we must check if we accidentally had a hash-collision.
                final ObservableSUL<S, I, O> sul1 = getSul();
                final ObservableSUL<S, I, O> sul2 = forkedSUL;

                // assert sul1 is already in the correct state
                assert s1.equals(sul1.getState().hashCode());

                sul2.pre();
                try {
                    // step through the second SUL
                    for (I sym : input2) {
                        sul2.step(sym);
                    }

                    assert sul1.getState().hashCode() == sul2.getState().hashCode();
                    assert s2.equals(sul2.getState().hashCode());

                    // check for state equivalence
                    return sul1.getState().equals(sul2.getState());
                } finally {
                    sul2.post();
                }
            }
        }
    }

    /**
     * A {@link AbstractSULOmegaOracle} for states that are deep copies. When a state is a deep copy, this means we can
     * simply invoke {@link Object#equals(Object)} on both.
     * <p>
     * The state information used to answer {@link OmegaQuery}s is of type {@link S}.
     *
     * @param <S> the state type
     * @param <I> the input type
     * @param <O> the output type
     */
    private static final class DeepCopySULOmegaOracle<S extends Object, I, O>
            extends AbstractSULOmegaOracle<S, I, O, S> {

        /**
         * Constructs a {@link DeepCopySULOmegaOracle}, use {@link #newOracle(ObservableSUL, boolean)} to create an
         * actual instance. This method will make sure the invariants of the {@link ObservableSUL} are satisfied.
         *
         * @param sul the {@link ObservableSUL}.
         */
        DeepCopySULOmegaOracle(ObservableSUL<S, I, O> sul) {
            super(sul);
        }

        /**
         * Returns the current state of the {@link ObservableSUL}.
         *
         * @param sul the {@link ObservableSUL} to retrieve the current state from.
         *
         * @return the current state.
         */
        @Override
        protected S getQueryState(ObservableSUL<S, I, O> sul) {
            return sul.getState();
        }

        /**
         * Test for state equivalence using {@link Object#equals(Object)}.
         *
         * @see OmegaMembershipOracle#isSameState(Word, Object, Word, Object)
         */
        @Override
        public boolean isSameState(Word<I> input1, S s1, Word<I> input2, S s2) {
            return s1.equals(s2);
        }
    }
}

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.membership;
17
18	import java.util.ArrayList;
19	import java.util.Collection;
20	import java.util.List;
21
22	import de.learnlib.api.ObservableSUL;
23	import de.learnlib.api.SUL;
24	import de.learnlib.api.oracle.MembershipOracle.MealyMembershipOracle;
25	import de.learnlib.api.oracle.OmegaMembershipOracle;
26	import de.learnlib.api.oracle.OmegaMembershipOracle.MealyOmegaMembershipOracle;
27	import de.learnlib.api.query.OmegaQuery;
28	import net.automatalib.commons.util.Pair;
29	import net.automatalib.words.Word;
30	import net.automatalib.words.WordBuilder;
31	import org.checkerframework.checker.nullness.qual.Nullable;
32
33	/**
34	* An omega membership oracle for an {@link ObservableSUL}.
35	* <p>
36	* The behavior is similar to a {@link SULOracle}, except that this class answers {@link OmegaQuery}s.
37	* <p>
38	* After some symbols (i.e. after {@link OmegaQuery#getPrefix()}, and after each {@link OmegaQuery#getLoop()}) the state
39	* of the {@link ObservableSUL} is retrieved, and used to answer the query.
40	* <p>
41	* This class is <b>not</b> thread-safe.
42	*
43	* @param <S>
44	* the state type of the {@link ObservableSUL}
45	* @param <I>
46	* the input type
47	* @param <O>
48	* the output type
49	* @param <Q>
50	* the state information type that is used to answer {@link OmegaQuery}s
51	*/
52	public abstract class AbstractSULOmegaOracle<S extends Object, I, O, Q> implements MealyOmegaMembershipOracle<Q, I, O> {	2✔
53
54	private final ObservableSUL<S, I, O> sul;
55
56	protected AbstractSULOmegaOracle(ObservableSUL<S, I, O> sul) {	2✔
57	this.sul = sul;	2✔
58	}	2✔
59
60	/**
61	* Gets the {@link ObservableSUL}.
62	*
63	* @return the {@link ObservableSUL}.
64	*/
65	public ObservableSUL<S, I, O> getSul() {
66	return sul;	2✔
67	}
68
69	@Override
70	public void processQueries(Collection<? extends OmegaQuery<I, Word<O>>> queries) {
71	for (OmegaQuery<I, Word<O>> q : queries) {	2✔
72	final Pair<@Nullable Word<O>, Integer> output = answerQuery(q.getPrefix(), q.getLoop(), q.getRepeat());	2✔
73	q.answer(output.getFirst(), output.getSecond());	2✔
74	}	2✔
75	}	2✔
76
77	protected abstract Q getQueryState(ObservableSUL<S, I, O> sul);
78
79	@Override
80	public Pair<@Nullable Word<O>, Integer> answerQuery(Word<I> prefix, Word<I> loop, int repeat) {
81	assert repeat > 0;	2✔
82	sul.pre();	2✔
83	try {
84	final int traceLength = prefix.length() + loop.length() * repeat;	2✔
85	final WordBuilder<I> inputBuilder = new WordBuilder<>(traceLength, prefix);	2✔
86	final WordBuilder<O> outputBuilder = new WordBuilder<>(traceLength);	2✔
87	final List<Q> states = new ArrayList<>(repeat + 1);	2✔
88
89	for (int i = 0; i < prefix.length(); i++) {	2✔
90	outputBuilder.append(sul.step(prefix.getSymbol(i)));	2✔
91	}
92	states.add(getQueryState(sul));	2✔
93
94	for (int i = 0; i < repeat; i++) {	2✔
95	inputBuilder.append(loop);	2✔
96	for (int j = 0; j < loop.length(); j++) {	2✔
97	outputBuilder.append(sul.step(loop.getSymbol(j)));	2✔
98	}
99	final Q nextState = getQueryState(sul);	2✔
100
101	int prefixLength = prefix.length();	2✔
102	for (Q q: states) {	2✔
103	if (isSameState(inputBuilder.toWord(), nextState, inputBuilder.toWord(0, prefixLength), q)) {	2✔
104	return Pair.of(outputBuilder.toWord(), i + 1);	2✔
105	}
106	prefixLength += loop.length();	2✔
107	}	2✔
108	states.add(nextState);	2✔
109	}
110
111	return Pair.of(null, -1);	2✔
112	} finally {
113	sul.post();	2✔
114	}
115	}
116
117	@Override
118	public MealyMembershipOracle<I, O> getMembershipOracle() {
119	return new SULOracle<>(sul);	×
120	}
121
122	/**
123	* Creates a new {@link AbstractSULOmegaOracle}, while making sure the invariants of the {@link ObservableSUL} are
124	* satisfied.
125	*
126	* @param sul the {@link ObservableSUL} to wrap around.
127	* @param deepCopies whether to test for state equivalence directly on the retrieved state.
128	*
129	* @param <S> the state type
130	* @param <I> the input type
131	* @param <O> the output type
132	*
133	* @return the {@link AbstractSULOmegaOracle}.
134	*/
135	public static <S extends Object, I, O> AbstractSULOmegaOracle<S, I, O, ?> newOracle(ObservableSUL<S, I, O> sul,
136	boolean deepCopies) {
137	final AbstractSULOmegaOracle<S, I, O, ?> abstractSulOmegaOracle;
138	if (deepCopies) {	2✔
139	if (!sul.deepCopies()) {	2✔
140	throw new IllegalArgumentException("SUL can not make deep copies of states.");	2✔
141	} else {
142	abstractSulOmegaOracle = new DeepCopySULOmegaOracle<>(sul);	2✔
143	}
144	} else {
145	if (!sul.canFork()) {	2✔
146	throw new IllegalArgumentException("SUL must be forkable.");	2✔
147	} else {
148	abstractSulOmegaOracle = new ShallowCopySULOmegaOracle<>(sul);	2✔
149	}
150	}
151
152	return abstractSulOmegaOracle;	2✔
153	}
154
155	/**
156	* Creates a new {@link AbstractSULOmegaOracle} that assumes the {@link SUL} can not make deep copies.
157	*
158	* @see #newOracle(ObservableSUL, boolean)
159	*
160	* @param <S> the state type
161	* @param <I> the input type
162	* @param <O> the output type
163	*/
164	public static <S extends Object, I, O> AbstractSULOmegaOracle<S, I, O, ?> newOracle(ObservableSUL<S, I, O> sul) {
165	return newOracle(sul, !sul.canFork());	2✔
166	}
167
168	/**
169	* A {@link AbstractSULOmegaOracle} that uses {@link Object#hashCode()}, and {@link Object#equals(Object)} to test
170	* for state equivalence. When the hash codes of two states are equal this class will use two access sequences to
171	* move two {@link ObservableSUL}s to those states and perform an equality check.
172	* <p>
173	* The state information used to answer {@link OmegaQuery}s is of type {@link Integer}. The values of those integers
174	* are actually hash codes of states of the {@link ObservableSUL}.
175	*
176	* @param <S> the state type
177	* @param <I> the input type
178	* @param <O> the output type
179	*/
180	private static final class ShallowCopySULOmegaOracle<S extends Object, I, O>	2✔
181	extends AbstractSULOmegaOracle<S, I, O, Integer> {
182
183	/**
184	* A forked {@link SUL} is necessary when we need to step to two particular states at the same time.
185	*/
186	private final ObservableSUL<S, I, O> forkedSUL;
187
188	/**
189	* Constructs a new {@link ShallowCopySULOmegaOracle}, use {@link #newOracle(ObservableSUL)} to create an
190	* instance. This method makes sure the invariants of the {@link ObservableSUL} are satisfied (i.e., the {@link
191	* ObservableSUL} must be forkable, i.e. ({@code {@link SUL#canFork()} == true}).
192	*
193	* @param sul the SUL
194	*/
195	ShallowCopySULOmegaOracle(ObservableSUL<S, I, O> sul) {
196	super(sul);	2✔
197	assert sul.canFork();	2✔
198	forkedSUL = sul.fork();	2✔
199	}	2✔
200
201	/**
202	* Returns the state as a hash code.
203	*
204	* @param sul the {@link ObservableSUL} to retrieve the current state from.
205	*
206	* @return the hash code of the state.
207	*/
208	@Override
209	protected Integer getQueryState(ObservableSUL<S, I, O> sul) {
210	return sul.getState().hashCode();	2✔
211	}
212
213	/**
214	* Test for state equivalence, by means of {@link Object#hashCode()}, and {@link Object#equals(Object)}.
215	*
216	* @see OmegaMembershipOracle#isSameState(Word, Object, Word, Object)
217	*
218	* @return whether the following conditions hold:
219	* 1. the hash codes are the same, i.e. {@code s1.equals(s2)}, and
220	* 2. the two access sequences lead to the same state.
221	*/
222	@Override
223	public boolean isSameState(Word<I> input1, Integer s1, Word<I> input2, Integer s2) {
224	if (!s1.equals(s2)) {	2✔
225	return false;	2✔
226	} else {
227	// in this case the hash codes are equal, now we must check if we accidentally had a hash-collision.
228	final ObservableSUL<S, I, O> sul1 = getSul();	2✔
229	final ObservableSUL<S, I, O> sul2 = forkedSUL;	2✔
230
231	// assert sul1 is already in the correct state
232	assert s1.equals(sul1.getState().hashCode());	2✔
233
234	sul2.pre();	2✔
235	try {
236	// step through the second SUL
237	for (I sym : input2) {	2✔
238	sul2.step(sym);	2✔
239	}	2✔
240
241	assert sul1.getState().hashCode() == sul2.getState().hashCode();	2✔
242	assert s2.equals(sul2.getState().hashCode());	2✔
243
244	// check for state equivalence
245	return sul1.getState().equals(sul2.getState());	2✔
246	} finally {
247	sul2.post();	2✔
248	}
249	}
250	}
251	}
252
253	/**
254	* A {@link AbstractSULOmegaOracle} for states that are deep copies. When a state is a deep copy, this means we can
255	* simply invoke {@link Object#equals(Object)} on both.
256	* <p>
257	* The state information used to answer {@link OmegaQuery}s is of type {@link S}.
258	*
259	* @param <S> the state type
260	* @param <I> the input type
261	* @param <O> the output type
262	*/
263	private static final class DeepCopySULOmegaOracle<S extends Object, I, O>
264	extends AbstractSULOmegaOracle<S, I, O, S> {
265
266	/**
267	* Constructs a {@link DeepCopySULOmegaOracle}, use {@link #newOracle(ObservableSUL, boolean)} to create an
268	* actual instance. This method will make sure the invariants of the {@link ObservableSUL} are satisfied.
269	*
270	* @param sul the {@link ObservableSUL}.
271	*/
272	DeepCopySULOmegaOracle(ObservableSUL<S, I, O> sul) {
273	super(sul);	2✔
274	}	2✔
275
276	/**
277	* Returns the current state of the {@link ObservableSUL}.
278	*
279	* @param sul the {@link ObservableSUL} to retrieve the current state from.
280	*
281	* @return the current state.
282	*/
283	@Override
284	protected S getQueryState(ObservableSUL<S, I, O> sul) {
285	return sul.getState();	2✔
286	}
287
288	/**
289	* Test for state equivalence using {@link Object#equals(Object)}.
290	*
291	* @see OmegaMembershipOracle#isSameState(Word, Object, Word, Object)
292	*/
293	@Override
294	public boolean isSameState(Word<I> input1, S s1, Word<I> input2, S s2) {
295	return s1.equals(s2);	2✔
296	}
297	}
298	}

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