20198569605

Committed 13 Dec 2025 10:10PM UTC coverage: 94.914% (+0.4%) from 94.471%

Build # 20198569605

Build Type

Pull #153

github

Committed by

web-flow

Commit Message

Merge 6a71fc929 into 879958926

Pull Request Pull Request #153: Implementation for learning MMLTs, new model for collecting statistics

Run Details

1823 of 1873 new or added lines in 77 files covered. (97.33%)

1 existing line in 1 file now uncovered.

14258 of 15022 relevant lines covered (94.91%)

1.73 hits per line

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

99.12

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

import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;

import de.learnlib.oracle.SingleQueryOracle.SingleQueryOracleMMLT;
import de.learnlib.oracle.TimedQueryOracle;
import de.learnlib.sul.TimedSUL;
import de.learnlib.time.MMLTModelParams;
import net.automatalib.automaton.mmlt.TimerInfo;
import net.automatalib.symbol.time.InputSymbol;
import net.automatalib.symbol.time.TimeStepSequence;
import net.automatalib.symbol.time.TimedInput;
import net.automatalib.symbol.time.TimedOutput;
import net.automatalib.symbol.time.TimeoutSymbol;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * Implements a {@link TimedQueryOracle} given a {@link TimedSUL}.
 *
 * @param <I>
 *         input symbol type (of non-delaying inputs)
 * @param <O>
 *         output symbol type
 */
public class TimedSULOracle<I, O> implements SingleQueryOracleMMLT<I, O> {

    private static final Logger LOGGER = LoggerFactory.getLogger(TimedSULOracle.class);

    /**
     * To ensure globally unique timer names, we index them according to this counter.
     */
    private int timerCounter;

    private final TimedSUL<I, O> sul;
    private final MMLTModelParams<O> modelParams;

    public TimedSULOracle(TimedSUL<I, O> sul, MMLTModelParams<O> modelParams) {
        this.sul = sul;
        this.modelParams = modelParams;
        this.timerCounter = 0;
    }

    @Override
    public Word<TimedOutput<O>> answerQuery(Word<TimedInput<I>> prefix, Word<TimedInput<I>> suffix) {
        sul.pre();
        sul.follow(prefix, this.modelParams.maxTimeoutWaitingTime());

        // Query the SUL, one symbol at a time:
        WordBuilder<TimedOutput<O>> wbOutput = new WordBuilder<>();
        for (TimedInput<I> s : suffix) {
            if (s instanceof TimeoutSymbol<I>) {
                TimedOutput<O> output = sul.timeoutStep(this.modelParams.maxTimeoutWaitingTime());
                if (output != null) {
                    wbOutput.append(output);
                } else {
                    wbOutput.append(new TimedOutput<>(this.modelParams.silentOutput())); // no output in time -> silent
                }
            } else if (s instanceof InputSymbol<I> ndi) {
                TimedOutput<O> output = sul.step(ndi);
                wbOutput.append(output);
            } else if (s instanceof TimeStepSequence<I> ws) {
                if (ws.timeSteps() > 1) {
                    throw new IllegalArgumentException("Only single wait step allowed in suffix.");
                }

                // Wait for a single time step:
                TimedOutput<O> output = sul.timeStep();
                if (output != null) {
                    wbOutput.append(output);
                } else {
                    wbOutput.append(new TimedOutput<>(this.modelParams.silentOutput())); // no output in time -> silent
                }

            } else {
                throw new IllegalArgumentException("Only timeout or untimed symbols allowed in suffix.");
            }
        }

        sul.post();
        return wbOutput.toWord();
    }

    @Override
    public TimerQueryResult<O> queryTimers(Word<TimedInput<I>> prefix, long maxTotalWaitingTime) {
        this.sul.pre();

        // Go to location:
        this.sul.follow(prefix);

        // Collect timeouts:
        TimerQueryResult<O> timers = this.collectTimeouts(maxTotalWaitingTime);

        this.sul.post();
        return timers;
    }

    /**
     * Identifies the time at which the next known timeout(s) are expected.
     *
     * @param timeouts
     *         the known timeouts
     * @param currentTime
     *         the current time
     *
     * @return the next timeout time
     */
    private long calcNextExpectedTimeout(List<TimerInfo<?, O>> timeouts, long currentTime) {
        assert !timeouts.isEmpty();

        long minNext = Long.MAX_VALUE;
        for (TimerInfo<?, O> to : timeouts) {
            long occurrences = currentTime / to.initial();
            long nextOcc = (occurrences + 1) * to.initial(); // time of next occ

            if (nextOcc < minNext) {
                minNext = nextOcc;
            }
        }

        assert minNext != Long.MAX_VALUE;

        return minNext;
    }

    private String newUniqueTimerName() {
        return "t_" + (++this.timerCounter);
    }

    /**
     * Identifies timeouts in the current location by waiting at most {@code maxTotalWaitingTime}.
     * <p>
     * All inferred timers are initially considered periodic. Stops when reaching {@code maxTotalWaitingTime} or when an
     * expected timeout does not occur. In the latter case, the {@link TimerQueryResult#aborted()}} flag is set.
     *
     * @param maxTotalWaitingTime
     *         the maximum time until timeouts are collected
     *
     * @return the list of periodic timeouts or {@code null} if none observed
     */
    private TimerQueryResult<O> collectTimeouts(long maxTotalWaitingTime) {
        if (maxTotalWaitingTime < this.modelParams.maxTimeoutWaitingTime()) {
            throw new IllegalArgumentException(
                    "Timer query waiting time must be at least maximum waiting time for a single timeout.");
        }

        List<TimerInfo<?, O>> knownTimers = new ArrayList<>();

        // Wait for the first timeout:
        TimedOutput<O> firstTimeout = this.sul.timeoutStep(this.modelParams.maxTimeoutWaitingTime());
        if (firstTimeout == null) {
            return new TimerQueryResult<>(false, Collections.emptyList()); // no timeouts found
        }

        List<O> firstTimeoutOutputs = this.modelParams.outputCombiner().separateSymbols(firstTimeout.symbol());
        if (firstTimeoutOutputs.size() > 1) {
            LOGGER.warn("Multiple timers expiring at first timeout, automaton may not be minimal.");
        }

        knownTimers.add(new TimerInfo<>(newUniqueTimerName(), firstTimeout.delay(), firstTimeoutOutputs, null, true));

        // Wait for further timeouts:
        long currentTimeStep = firstTimeout.delay(); // already waited for first timeout

        boolean inconsistent = false;
        while (currentTimeStep < maxTotalWaitingTime) {
            // Identify time of next expected timeout:
            long nextExpectedTime = this.calcNextExpectedTimeout(knownTimers, currentTimeStep);

            // Wait either until next timeout OR until maximum waiting time reached:
            long nextWaiting = Math.min(nextExpectedTime, maxTotalWaitingTime) - currentTimeStep;

            // Wait until next timeout:
            TimedOutput<O> nextOutput = this.sul.timeoutStep(nextWaiting);
            if (nextOutput == null) {
                if (nextExpectedTime <= maxTotalWaitingTime) {
                    // Expected a timeout within maximum waiting time but nothing happened:
                    inconsistent = true;
                }

                break; // either max time exceeded OR missing timeout (-> inconsistent)
            }

            // Compare observed timeout with expectation:
            long nextActualTime = nextOutput.delay() + currentTimeStep;

            TimerCheckResult<O> evalResult =
                    evaluateNextTimer(nextActualTime, nextExpectedTime, nextOutput, knownTimers);
            if (evalResult.newTimer() != null) {
                knownTimers.add(evalResult.newTimer());
            } else if (evalResult.inconsistent()) {
                inconsistent = true;
                break;
            }

            currentTimeStep = nextActualTime;
        }

        knownTimers.sort(Comparator.comparingLong(TimerInfo::initial));
        return new TimerQueryResult<>(inconsistent, knownTimers);
    }

    private TimerCheckResult<O> evaluateNextTimer(long nextActualTime,
                                                  long nextExpectedTime,
                                                  TimedOutput<O> nextOutput,
                                                  List<TimerInfo<?, O>> knownTimers) {

        List<O> nextOutputSymbols = this.modelParams.outputCombiner().separateSymbols(nextOutput.symbol());

        if (nextActualTime < nextExpectedTime) {
            // A timeout occurred before we expected one -> new timer:
            TimerInfo<?, O> newTimer =
                    new TimerInfo<>(newUniqueTimerName(), nextActualTime, nextOutputSymbols, null, true);
            return new TimerCheckResult<>(newTimer, false);
        } else {
            assert nextActualTime == nextExpectedTime;
            // Timeout occurred at expected time -> check if matching expected output:
            Map<O, Long> expectedOutputs = new HashMap<>();
            for (TimerInfo<?, O> t : knownTimers) {
                if (nextExpectedTime % t.initial() == 0) {
                    for (O o : t.outputs()) {
                        expectedOutputs.merge(o, 1L, Long::sum);
                    }
                }
            }

            Map<O, Long> actualOutputs = new HashMap<>();
            for (O o : nextOutputSymbols) {
                actualOutputs.merge(o, 1L, Long::sum);
            }

            // Any outputs that were expected but are not present?
            for (Entry<O, Long> e : expectedOutputs.entrySet()) {
                if (actualOutputs.getOrDefault(e.getKey(), 0L) < e.getValue()) {
                    // Same time but missing output -> missed location change:
                    return new TimerCheckResult<>(null, true);
                }
            }

            // At least all expected outputs are present.
            // Check for additional outputs:
            List<O> newOutputs = new ArrayList<>();
            for (Entry<O, Long> e : actualOutputs.entrySet()) {
                O output = e.getKey();
                long expectedCount = expectedOutputs.getOrDefault(output, 0L);
                long actualCount = e.getValue();

                long additional = actualCount - expectedCount;
                for (int i = 0; i < additional; i++) {
                    newOutputs.add(output);
                }
            }

            if (!newOutputs.isEmpty()) {
                // Same time and more outputs -> add new timer that uses the new outputs:
                TimerInfo<?, O> newTimer =
                        new TimerInfo<>(newUniqueTimerName(), nextActualTime, newOutputs, null, true);
                return new TimerCheckResult<>(newTimer, false);
            }
        }

        return new TimerCheckResult<>(null, false);
    }

    private record TimerCheckResult<O>(@Nullable TimerInfo<?, O> newTimer, boolean inconsistent) {}
}

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.membership;
17
18	import java.util.ArrayList;
19	import java.util.Collections;
20	import java.util.Comparator;
21	import java.util.HashMap;
22	import java.util.List;
23	import java.util.Map;
24	import java.util.Map.Entry;
25
26	import de.learnlib.oracle.SingleQueryOracle.SingleQueryOracleMMLT;
27	import de.learnlib.oracle.TimedQueryOracle;
28	import de.learnlib.sul.TimedSUL;
29	import de.learnlib.time.MMLTModelParams;
30	import net.automatalib.automaton.mmlt.TimerInfo;
31	import net.automatalib.symbol.time.InputSymbol;
32	import net.automatalib.symbol.time.TimeStepSequence;
33	import net.automatalib.symbol.time.TimedInput;
34	import net.automatalib.symbol.time.TimedOutput;
35	import net.automatalib.symbol.time.TimeoutSymbol;
36	import net.automatalib.word.Word;
37	import net.automatalib.word.WordBuilder;
38	import org.checkerframework.checker.nullness.qual.Nullable;
39	import org.slf4j.Logger;
40	import org.slf4j.LoggerFactory;
41
42	/**
43	* Implements a {@link TimedQueryOracle} given a {@link TimedSUL}.
44	*
45	* @param <I>
46	* input symbol type (of non-delaying inputs)
47	* @param <O>
48	* output symbol type
49	*/
50	public class TimedSULOracle<I, O> implements SingleQueryOracleMMLT<I, O> {
51
52	private static final Logger LOGGER = LoggerFactory.getLogger(TimedSULOracle.class);	2✔
53
54	/**
55	* To ensure globally unique timer names, we index them according to this counter.
56	*/
57	private int timerCounter;
58
59	private final TimedSUL<I, O> sul;
60	private final MMLTModelParams<O> modelParams;
61
62	public TimedSULOracle(TimedSUL<I, O> sul, MMLTModelParams<O> modelParams) {	2✔
63	this.sul = sul;	2✔
64	this.modelParams = modelParams;	2✔
65	this.timerCounter = 0;	2✔
66	}	2✔
67
68	@Override
69	public Word<TimedOutput<O>> answerQuery(Word<TimedInput<I>> prefix, Word<TimedInput<I>> suffix) {
70	sul.pre();	2✔
71	sul.follow(prefix, this.modelParams.maxTimeoutWaitingTime());	2✔
72
73	// Query the SUL, one symbol at a time:
74	WordBuilder<TimedOutput<O>> wbOutput = new WordBuilder<>();	2✔
75	for (TimedInput<I> s : suffix) {	2✔
76	if (s instanceof TimeoutSymbol<I>) {	2✔
77	TimedOutput<O> output = sul.timeoutStep(this.modelParams.maxTimeoutWaitingTime());	2✔
78	if (output != null) {	2✔
79	wbOutput.append(output);	1✔
80	} else {
81	wbOutput.append(new TimedOutput<>(this.modelParams.silentOutput())); // no output in time -> silent	2✔
82	}
83	} else if (s instanceof InputSymbol<I> ndi) {	2✔
84	TimedOutput<O> output = sul.step(ndi);	1✔
85	wbOutput.append(output);	1✔
86	} else if (s instanceof TimeStepSequence<I> ws) {	2✔
87	if (ws.timeSteps() > 1) {	2✔
88	throw new IllegalArgumentException("Only single wait step allowed in suffix.");	2✔
89	}
90
91	// Wait for a single time step:
92	TimedOutput<O> output = sul.timeStep();	1✔
93	if (output != null) {	1✔
94	wbOutput.append(output);	1✔
95	} else {
96	wbOutput.append(new TimedOutput<>(this.modelParams.silentOutput())); // no output in time -> silent	1✔
97	}
98
99	} else {	1✔
NEW 100	throw new IllegalArgumentException("Only timeout or untimed symbols allowed in suffix.");	×
101	}
102	}	2✔
103
104	sul.post();	2✔
105	return wbOutput.toWord();	2✔
106	}
107
108	@Override
109	public TimerQueryResult<O> queryTimers(Word<TimedInput<I>> prefix, long maxTotalWaitingTime) {
110	this.sul.pre();	2✔
111
112	// Go to location:
113	this.sul.follow(prefix);	2✔
114
115	// Collect timeouts:
116	TimerQueryResult<O> timers = this.collectTimeouts(maxTotalWaitingTime);	1✔
117
118	this.sul.post();	1✔
119	return timers;	1✔
120	}
121
122	/**
123	* Identifies the time at which the next known timeout(s) are expected.
124	*
125	* @param timeouts
126	* the known timeouts
127	* @param currentTime
128	* the current time
129	*
130	* @return the next timeout time
131	*/
132	private long calcNextExpectedTimeout(List<TimerInfo<?, O>> timeouts, long currentTime) {
133	assert !timeouts.isEmpty();	1✔
134
135	long minNext = Long.MAX_VALUE;	1✔
136	for (TimerInfo<?, O> to : timeouts) {	1✔
137	long occurrences = currentTime / to.initial();	1✔
138	long nextOcc = (occurrences + 1) * to.initial(); // time of next occ	1✔
139
140	if (nextOcc < minNext) {	1✔
141	minNext = nextOcc;	1✔
142	}
143	}	1✔
144
145	assert minNext != Long.MAX_VALUE;	1✔
146
147	return minNext;	1✔
148	}
149
150	private String newUniqueTimerName() {
151	return "t_" + (++this.timerCounter);	1✔
152	}
153
154	/**
155	* Identifies timeouts in the current location by waiting at most {@code maxTotalWaitingTime}.
156	* <p>
157	* All inferred timers are initially considered periodic. Stops when reaching {@code maxTotalWaitingTime} or when an
158	* expected timeout does not occur. In the latter case, the {@link TimerQueryResult#aborted()}} flag is set.
159	*
160	* @param maxTotalWaitingTime
161	* the maximum time until timeouts are collected
162	*
163	* @return the list of periodic timeouts or {@code null} if none observed
164	*/
165	private TimerQueryResult<O> collectTimeouts(long maxTotalWaitingTime) {
166	if (maxTotalWaitingTime < this.modelParams.maxTimeoutWaitingTime()) {	2✔
167	throw new IllegalArgumentException(	2✔
168	"Timer query waiting time must be at least maximum waiting time for a single timeout.");
169	}
170
171	List<TimerInfo<?, O>> knownTimers = new ArrayList<>();	1✔
172
173	// Wait for the first timeout:
174	TimedOutput<O> firstTimeout = this.sul.timeoutStep(this.modelParams.maxTimeoutWaitingTime());	1✔
175	if (firstTimeout == null) {	1✔
176	return new TimerQueryResult<>(false, Collections.emptyList()); // no timeouts found	1✔
177	}
178
179	List<O> firstTimeoutOutputs = this.modelParams.outputCombiner().separateSymbols(firstTimeout.symbol());	1✔
180	if (firstTimeoutOutputs.size() > 1) {	1✔
181	LOGGER.warn("Multiple timers expiring at first timeout, automaton may not be minimal.");	1✔
182	}
183
184	knownTimers.add(new TimerInfo<>(newUniqueTimerName(), firstTimeout.delay(), firstTimeoutOutputs, null, true));	1✔
185
186	// Wait for further timeouts:
187	long currentTimeStep = firstTimeout.delay(); // already waited for first timeout	1✔
188
189	boolean inconsistent = false;	1✔
190	while (currentTimeStep < maxTotalWaitingTime) {	1✔
191	// Identify time of next expected timeout:
192	long nextExpectedTime = this.calcNextExpectedTimeout(knownTimers, currentTimeStep);	1✔
193
194	// Wait either until next timeout OR until maximum waiting time reached:
195	long nextWaiting = Math.min(nextExpectedTime, maxTotalWaitingTime) - currentTimeStep;	1✔
196
197	// Wait until next timeout:
198	TimedOutput<O> nextOutput = this.sul.timeoutStep(nextWaiting);	1✔
199	if (nextOutput == null) {	1✔
200	if (nextExpectedTime <= maxTotalWaitingTime) {	1✔
201	// Expected a timeout within maximum waiting time but nothing happened:
202	inconsistent = true;	1✔
203	}
204
205	break; // either max time exceeded OR missing timeout (-> inconsistent)
206	}
207
208	// Compare observed timeout with expectation:
209	long nextActualTime = nextOutput.delay() + currentTimeStep;	1✔
210
211	TimerCheckResult<O> evalResult =	1✔
212	evaluateNextTimer(nextActualTime, nextExpectedTime, nextOutput, knownTimers);	1✔
213	if (evalResult.newTimer() != null) {	1✔
214	knownTimers.add(evalResult.newTimer());	1✔
215	} else if (evalResult.inconsistent()) {	1✔
216	inconsistent = true;	1✔
217	break;	1✔
218	}
219
220	currentTimeStep = nextActualTime;	1✔
221	}	1✔
222
223	knownTimers.sort(Comparator.comparingLong(TimerInfo::initial));	1✔
224	return new TimerQueryResult<>(inconsistent, knownTimers);	1✔
225	}
226
227	private TimerCheckResult<O> evaluateNextTimer(long nextActualTime,
228	long nextExpectedTime,
229	TimedOutput<O> nextOutput,
230	List<TimerInfo<?, O>> knownTimers) {
231
232	List<O> nextOutputSymbols = this.modelParams.outputCombiner().separateSymbols(nextOutput.symbol());	1✔
233
234	if (nextActualTime < nextExpectedTime) {	1✔
235	// A timeout occurred before we expected one -> new timer:
236	TimerInfo<?, O> newTimer =	1✔
237	new TimerInfo<>(newUniqueTimerName(), nextActualTime, nextOutputSymbols, null, true);	1✔
238	return new TimerCheckResult<>(newTimer, false);	1✔
239	} else {
240	assert nextActualTime == nextExpectedTime;	1✔
241	// Timeout occurred at expected time -> check if matching expected output:
242	Map<O, Long> expectedOutputs = new HashMap<>();	1✔
243	for (TimerInfo<?, O> t : knownTimers) {	1✔
244	if (nextExpectedTime % t.initial() == 0) {	1✔
245	for (O o : t.outputs()) {	1✔
246	expectedOutputs.merge(o, 1L, Long::sum);	1✔
247	}	1✔
248	}
249	}	1✔
250
251	Map<O, Long> actualOutputs = new HashMap<>();	1✔
252	for (O o : nextOutputSymbols) {	1✔
253	actualOutputs.merge(o, 1L, Long::sum);	1✔
254	}	1✔
255
256	// Any outputs that were expected but are not present?
257	for (Entry<O, Long> e : expectedOutputs.entrySet()) {	1✔
258	if (actualOutputs.getOrDefault(e.getKey(), 0L) < e.getValue()) {	1✔
259	// Same time but missing output -> missed location change:
260	return new TimerCheckResult<>(null, true);	1✔
261	}
262	}	1✔
263
264	// At least all expected outputs are present.
265	// Check for additional outputs:
266	List<O> newOutputs = new ArrayList<>();	1✔
267	for (Entry<O, Long> e : actualOutputs.entrySet()) {	1✔
268	O output = e.getKey();	1✔
269	long expectedCount = expectedOutputs.getOrDefault(output, 0L);	1✔
270	long actualCount = e.getValue();	1✔
271
272	long additional = actualCount - expectedCount;	1✔
273	for (int i = 0; i < additional; i++) {	1✔
274	newOutputs.add(output);	1✔
275	}
276	}	1✔
277
278	if (!newOutputs.isEmpty()) {	1✔
279	// Same time and more outputs -> add new timer that uses the new outputs:
280	TimerInfo<?, O> newTimer =	1✔
281	new TimerInfo<>(newUniqueTimerName(), nextActualTime, newOutputs, null, true);	1✔
282	return new TimerCheckResult<>(newTimer, false);	1✔
283	}
284	}
285
286	return new TimerCheckResult<>(null, false);	1✔
287	}
288
289	private record TimerCheckResult<O>(@Nullable TimerInfo<?, O> newTimer, boolean inconsistent) {}	1✔
290	}

LearnLib / learnlib / 20198569605

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