20199022329

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

Build # 20199022329

Build Type

push

github

Committed by

web-flow

Commit Message

Implementation for learning MMLTs, new model for collecting statistics (#153)

* Made RowImpl public to enable access in custom observation table implementations.

* Made several methods of RowImpl public, to enable external access from observation tables that are defined in the learner module.

* Started with integration of MMLT.

* Extended EquivalenceOracle.java with LocalTimerMealyEquivalenceOracle.

* Created module for symbol filters; added tests for counterexample handling for MMLT learner.

* Functions for printing stats as JSON/YAML.

* Renamed statsContainer; exporting mmlt caches.

* Included symbol-filters module in dependency management.

* Renamed fast cache to cache for MMLTs; added integration tests for MMLTs; allow access to stats during testing of learner.

* Added more test models for the MMLT learner.

* Added more test models for the MMLT learner.

* Added cache consistency test for MMLT learning.

* Removed location type parameter from LocalTimerMealyEquivalenceOracle.

* Cache for MMLTs now inherits LearningCache

* Multiple EQ tests for MMLTs can now respect the provided list of inputs for counterexamples.

* Added tests for the cache; cleaned-up some files.

* Added tests for the MMLT cache consistency test.

* Made the MMLT SUL an interface with default methods.

* Made symbol filters more independent from MMLTs

* StatisticsSymbolFilter has stats container as constructor parameter.

* Moved several MMLT examples to test-support.

* Added an example for learning MMLTs; added module info for symbol filter module.

* Added an example for learning MMLTs; added module info for symbol filter module.

* Added more descriptions for included MMLT models

* More info on model params

* Updated reset search oracle to check if it can return a counterexample with the provided inputs.

* adjust to AutomataLib refactorings

* adjust to AutomataLib refactorings

* adjust to AutomataLib refactorings

* Using correct function to render MMLT i... (continued)

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

97.73

/filters/cache/src/main/java/de/learnlib/filter/cache/mmlt/TimedSULTreeCache.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.filter.cache.mmlt;

import java.util.ArrayDeque;
import java.util.Deque;
import java.util.Iterator;

import de.learnlib.filter.cache.LearningCache.MMLTLearningCache;
import de.learnlib.filter.cache.mmlt.CacheTreeNode.CacheTreeTransition;
import de.learnlib.oracle.EquivalenceOracle.MMLTEquivalenceOracle;
import de.learnlib.sul.TimedSUL;
import de.learnlib.time.MMLTModelParams;
import net.automatalib.common.util.collection.AbstractSimplifiedIterator;
import net.automatalib.common.util.collection.IteratorUtil;
import net.automatalib.symbol.time.InputSymbol;
import net.automatalib.symbol.time.TimedInput;
import net.automatalib.symbol.time.TimedOutput;
import net.automatalib.word.Word;
import net.automatalib.word.WordBuilder;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Caches queries sent to a {@link TimedSUL}.
 *
 * @param <I>
 *         input symbol type (of non-delaying inputs)
 * @param <O>
 *         output symbol type
 */
public class TimedSULTreeCache<I, O> implements TimedSUL<I, O>, MMLTLearningCache<I, O> {

    private final TimedSUL<I, O> delegate;

    private final CacheTreeNode<I, O> cacheRoot;
    private CacheTreeNode<I, O> currentState;

    private final MMLTModelParams<O> modelParams;
    private final TimedOutput<O> silentOutput;
    private boolean cacheMiss;
    private boolean init;

    public TimedSULTreeCache(TimedSUL<I, O> delegate, MMLTModelParams<O> modelParams) {
        this.delegate = delegate;
        this.modelParams = modelParams;
        this.silentOutput = new TimedOutput<>(modelParams.silentOutput());

        // Init cache:
        this.cacheRoot = new CacheTreeNode<>(null, null);
        this.currentState = this.cacheRoot;
    }

    private void followCurrentPrefix(CacheTreeNode<I, O> current) {
        Word<TimedInput<I>> prefix = extractWord(current);
        this.delegate.pre();
        this.delegate.follow(prefix);
    }

    @Override
    public TimedOutput<O> step(InputSymbol<I> input) {
        if (!init) {
            throw new IllegalStateException();
        }

        if (!cacheMiss) {
            if (this.currentState.hasChild(input)) {
                TimedOutput<O> output = this.currentState.getOutput(input);
                this.currentState = this.currentState.getChild(input);
                return output;
            }
            this.followCurrentPrefix(this.currentState);
            this.cacheMiss = true;
        }

        // Cache miss -> query + insert:
        TimedOutput<O> output = this.delegate.step(input);
        this.currentState = this.currentState.addUntimedChild(input, output);
        return output;
    }

    @Override
    public @Nullable TimedOutput<O> timeoutStep(long maxTime) {
        if (!init) {
            throw new IllegalStateException();
        }

        long remaining = maxTime;
        if (!this.cacheMiss) {
            // Move to closest state in cache:
            while (remaining > 0) {
                if (!currentState.hasTimeChild()) {
                    break; // cache miss
                }

                if (currentState.getTimeout() > remaining) {
                    // Split current timeout:
                    this.currentState = this.currentState.splitTimeout(remaining, this.silentOutput);
                    return null; // no timer in this state
                }

                TimedOutput<O> currentOutput = currentState.getTimeoutOutput();
                remaining -= currentState.getTimeout();
                this.currentState = this.currentState.getTimeoutChild();

                if (!currentOutput.equals(this.silentOutput)) {
                    // Found valid timeout:
                    return new TimedOutput<>(currentOutput.symbol(), maxTime - remaining);
                }
            }

            if (remaining == 0) {
                return null; // no timer in this state
            }

            this.followCurrentPrefix(this.currentState);
            this.cacheMiss = true;
        }

        TimedOutput<O> timeoutStepResult = this.delegate.timeoutStep(remaining);
        if (timeoutStepResult == null) { // no timers here
            this.currentState = this.currentState.addTimeChild(remaining, this.silentOutput);
            return null;
        } else {
            this.currentState = this.currentState.addTimeChild(timeoutStepResult.delay(),
                                                               new TimedOutput<>(timeoutStepResult.symbol()));
            return new TimedOutput<>(timeoutStepResult.symbol(), maxTime - remaining + timeoutStepResult.delay());
        }

    }

    @Override
    public void pre() {
        this.currentState = this.cacheRoot;
        this.cacheMiss = false;
        this.init = true;
    }

    @Override
    public void post() {
        this.init = false;
        if (this.cacheMiss) {
            this.delegate.post();
        }
    }

    @Override
    public MMLTEquivalenceOracle<I, O> createCacheConsistencyTest() {
        return new MMLTCacheConsistencyTest<>(this, this.modelParams);
    }

    /**
     * Returns an iterator that traverses all words (leaves of this tree) in a BFS-style fashion.
     *
     * @return an iterator over all words of this tree
     */
    public Iterator<Word<TimedInput<I>>> allWordsIterator() {
        return IteratorUtil.map(new LeavesIterator<>(this.cacheRoot), this::extractWord);
    }

    private Word<TimedInput<I>> extractWord(CacheTreeNode<I, O> leaf) {
        final WordBuilder<TimedInput<I>> wb = new WordBuilder<>();

        // Move towards the root:
        CacheTreeNode<I, O> nodeIter = leaf.getParent();
        TimedInput<I> inputIter = leaf.getParentInput();
        while (nodeIter != null && inputIter != null) {
            wb.append(inputIter);
            inputIter = nodeIter.getParentInput();
            nodeIter = nodeIter.getParent();
        }

        // Start at root -> flip buffer:
        wb.reverse();
        return wb.toWord();
    }

    private static final class LeavesIterator<I, O> extends AbstractSimplifiedIterator<CacheTreeNode<I, O>> {

        private final Deque<CacheTreeNode<I, O>> queue;

        private LeavesIterator(CacheTreeNode<I, O> root) {
            this.queue = new ArrayDeque<>();
            this.queue.add(root);
        }

        @Override
        protected boolean calculateNext() {

            while (!queue.isEmpty()) {
                @SuppressWarnings("nullness") //false positive https://github.com/typetools/checker-framework/issues/399
                final @NonNull CacheTreeNode<I, O> node = queue.poll();

                boolean hasChildren = false;

                if (node.hasTimeChild()) {
                    queue.add(node.getTimeoutChild());
                    hasChildren = true;
                }

                for (CacheTreeTransition<I, O> t : node.getUntimedChildren().values()) {
                    queue.add(t.target());
                    hasChildren = true;
                }

                if (!hasChildren) {
                    super.nextValue = node;
                    return true;
                }
            }

            return false;
        }
    }
}

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.filter.cache.mmlt;
17
18	import java.util.ArrayDeque;
19	import java.util.Deque;
20	import java.util.Iterator;
21
22	import de.learnlib.filter.cache.LearningCache.MMLTLearningCache;
23	import de.learnlib.filter.cache.mmlt.CacheTreeNode.CacheTreeTransition;
24	import de.learnlib.oracle.EquivalenceOracle.MMLTEquivalenceOracle;
25	import de.learnlib.sul.TimedSUL;
26	import de.learnlib.time.MMLTModelParams;
27	import net.automatalib.common.util.collection.AbstractSimplifiedIterator;
28	import net.automatalib.common.util.collection.IteratorUtil;
29	import net.automatalib.symbol.time.InputSymbol;
30	import net.automatalib.symbol.time.TimedInput;
31	import net.automatalib.symbol.time.TimedOutput;
32	import net.automatalib.word.Word;
33	import net.automatalib.word.WordBuilder;
34	import org.checkerframework.checker.nullness.qual.NonNull;
35	import org.checkerframework.checker.nullness.qual.Nullable;
36
37	/**
38	* Caches queries sent to a {@link TimedSUL}.
39	*
40	* @param <I>
41	* input symbol type (of non-delaying inputs)
42	* @param <O>
43	* output symbol type
44	*/
45	public class TimedSULTreeCache<I, O> implements TimedSUL<I, O>, MMLTLearningCache<I, O> {
46
47	private final TimedSUL<I, O> delegate;
48
49	private final CacheTreeNode<I, O> cacheRoot;
50	private CacheTreeNode<I, O> currentState;
51
52	private final MMLTModelParams<O> modelParams;
53	private final TimedOutput<O> silentOutput;
54	private boolean cacheMiss;
55	private boolean init;
56
57	public TimedSULTreeCache(TimedSUL<I, O> delegate, MMLTModelParams<O> modelParams) {	2✔
58	this.delegate = delegate;	2✔
59	this.modelParams = modelParams;	2✔
60	this.silentOutput = new TimedOutput<>(modelParams.silentOutput());	2✔
61
62	// Init cache:
63	this.cacheRoot = new CacheTreeNode<>(null, null);	2✔
64	this.currentState = this.cacheRoot;	2✔
65	}	2✔
66
67	private void followCurrentPrefix(CacheTreeNode<I, O> current) {
68	Word<TimedInput<I>> prefix = extractWord(current);	2✔
69	this.delegate.pre();	2✔
70	this.delegate.follow(prefix);	2✔
71	}	2✔
72
73	@Override
74	public TimedOutput<O> step(InputSymbol<I> input) {
75	if (!init) {	2✔
NEW 76	throw new IllegalStateException();	×
77	}
78
79	if (!cacheMiss) {	2✔
80	if (this.currentState.hasChild(input)) {	2✔
81	TimedOutput<O> output = this.currentState.getOutput(input);	2✔
82	this.currentState = this.currentState.getChild(input);	2✔
83	return output;	2✔
84	}
85	this.followCurrentPrefix(this.currentState);	2✔
86	this.cacheMiss = true;	2✔
87	}
88
89	// Cache miss -> query + insert:
90	TimedOutput<O> output = this.delegate.step(input);	2✔
91	this.currentState = this.currentState.addUntimedChild(input, output);	2✔
92	return output;	2✔
93	}
94
95	@Override
96	public @Nullable TimedOutput<O> timeoutStep(long maxTime) {
97	if (!init) {	2✔
NEW 98	throw new IllegalStateException();	×
99	}
100
101	long remaining = maxTime;	2✔
102	if (!this.cacheMiss) {	2✔
103	// Move to closest state in cache:
104	while (remaining > 0) {	2✔
105	if (!currentState.hasTimeChild()) {	2✔
106	break; // cache miss	2✔
107	}
108
109	if (currentState.getTimeout() > remaining) {	2✔
110	// Split current timeout:
111	this.currentState = this.currentState.splitTimeout(remaining, this.silentOutput);	1✔
112	return null; // no timer in this state	1✔
113	}
114
115	TimedOutput<O> currentOutput = currentState.getTimeoutOutput();	2✔
116	remaining -= currentState.getTimeout();	2✔
117	this.currentState = this.currentState.getTimeoutChild();	2✔
118
119	if (!currentOutput.equals(this.silentOutput)) {	2✔
120	// Found valid timeout:
121	return new TimedOutput<>(currentOutput.symbol(), maxTime - remaining);	2✔
122	}
123	}	2✔
124
125	if (remaining == 0) {	2✔
126	return null; // no timer in this state	2✔
127	}
128
129	this.followCurrentPrefix(this.currentState);	2✔
130	this.cacheMiss = true;	2✔
131	}
132
133	TimedOutput<O> timeoutStepResult = this.delegate.timeoutStep(remaining);	2✔
134	if (timeoutStepResult == null) { // no timers here	2✔
135	this.currentState = this.currentState.addTimeChild(remaining, this.silentOutput);	2✔
136	return null;	2✔
137	} else {
138	this.currentState = this.currentState.addTimeChild(timeoutStepResult.delay(),	2✔
139	new TimedOutput<>(timeoutStepResult.symbol()));	2✔
140	return new TimedOutput<>(timeoutStepResult.symbol(), maxTime - remaining + timeoutStepResult.delay());	2✔
141	}
142
143	}
144
145	@Override
146	public void pre() {
147	this.currentState = this.cacheRoot;	2✔
148	this.cacheMiss = false;	2✔
149	this.init = true;	2✔
150	}	2✔
151
152	@Override
153	public void post() {
154	this.init = false;	2✔
155	if (this.cacheMiss) {	2✔
156	this.delegate.post();	2✔
157	}
158	}	2✔
159
160	@Override
161	public MMLTEquivalenceOracle<I, O> createCacheConsistencyTest() {
162	return new MMLTCacheConsistencyTest<>(this, this.modelParams);	2✔
163	}
164
165	/**
166	* Returns an iterator that traverses all words (leaves of this tree) in a BFS-style fashion.
167	*
168	* @return an iterator over all words of this tree
169	*/
170	public Iterator<Word<TimedInput<I>>> allWordsIterator() {
171	return IteratorUtil.map(new LeavesIterator<>(this.cacheRoot), this::extractWord);	2✔
172	}
173
174	private Word<TimedInput<I>> extractWord(CacheTreeNode<I, O> leaf) {
175	final WordBuilder<TimedInput<I>> wb = new WordBuilder<>();	2✔
176
177	// Move towards the root:
178	CacheTreeNode<I, O> nodeIter = leaf.getParent();	2✔
179	TimedInput<I> inputIter = leaf.getParentInput();	2✔
180	while (nodeIter != null && inputIter != null) {	2✔
181	wb.append(inputIter);	2✔
182	inputIter = nodeIter.getParentInput();	2✔
183	nodeIter = nodeIter.getParent();	2✔
184	}
185
186	// Start at root -> flip buffer:
187	wb.reverse();	2✔
188	return wb.toWord();	2✔
189	}
190
191	private static final class LeavesIterator<I, O> extends AbstractSimplifiedIterator<CacheTreeNode<I, O>> {
192
193	private final Deque<CacheTreeNode<I, O>> queue;
194
195	private LeavesIterator(CacheTreeNode<I, O> root) {	2✔
196	this.queue = new ArrayDeque<>();	2✔
197	this.queue.add(root);	2✔
198	}	2✔
199
200	@Override
201	protected boolean calculateNext() {
202
203	while (!queue.isEmpty()) {	2✔
204	@SuppressWarnings("nullness") //false positive https://github.com/typetools/checker-framework/issues/399
205	final @NonNull CacheTreeNode<I, O> node = queue.poll();	2✔
206
207	boolean hasChildren = false;	2✔
208
209	if (node.hasTimeChild()) {	2✔
210	queue.add(node.getTimeoutChild());	2✔
211	hasChildren = true;	2✔
212	}
213
214	for (CacheTreeTransition<I, O> t : node.getUntimedChildren().values()) {	2✔
215	queue.add(t.target());	2✔
216	hasChildren = true;	2✔
217	}	2✔
218
219	if (!hasChildren) {	2✔
220	super.nextValue = node;	2✔
221	return true;	2✔
222	}
223	}	2✔
224
225	return false;	2✔
226	}
227	}
228	}

LearnLib / learnlib / 20199022329

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