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

94.12

/examples/src/main/java/de/learnlib/example/mmlt/Example4.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.example.mmlt;

import java.io.IOException;
import java.io.InputStream;
import java.util.ArrayList;
import java.util.List;

import de.learnlib.algorithm.lstar.mmlt.ExtensibleLStarMMLTBuilder;
import de.learnlib.driver.simulator.MMLTSimulatorSUL;
import de.learnlib.filter.cache.mmlt.TimedSULTreeCache;
import de.learnlib.filter.cache.mmlt.TimeoutReducerSUL;
import de.learnlib.filter.statistic.sul.CounterTimedSUL;
import de.learnlib.oracle.equivalence.mmlt.SimulatorEQOracle;
import de.learnlib.oracle.membership.TimedSULOracle;
import de.learnlib.statistic.Statistics;
import de.learnlib.time.MMLTModelParams;
import net.automatalib.alphabet.Alphabet;
import net.automatalib.automaton.mmlt.MMLT;
import net.automatalib.automaton.mmlt.impl.StringSymbolCombiner;
import net.automatalib.exception.FormatException;
import net.automatalib.serialization.dot.DOTMMLTParser;
import net.automatalib.serialization.dot.DOTParsers;
import net.automatalib.symbol.time.TimedInput;
import net.automatalib.symbol.time.TimeoutSymbol;
import net.automatalib.util.automaton.mmlt.MMLTs;
import net.automatalib.word.Word;

/**
 * This example demonstrates how to load an {@link MMLT} from a dot-file and learn it using the L* algorithm.
 * <p>
 * A description of the dot-file syntax for MMLTs can be found in AutomataLib (see {@link DOTMMLTParser}).
 */
@SuppressWarnings("PMD.UseExplicitTypes") // allow vars in examples
public final class Example4 {

    private Example4() {
        // prevent instantiation
    }

    public static void main(String[] args) {
        // First, we load the file "mmlt_example.dot" from the "resources" folder:
        MMLT<?, String, ?, String> mmlt;
        Alphabet<String> alphabet;
        MMLTModelParams<String> params;

        // We define the output that represents silence:
        var silentOutput = "void";

        // In an MMLT, a timeout may yield multiple outputs.
        // We use a symbol combiner to combine them into a single output.
        // Here, we use a StringSymbolCombiner that sorts symbols and then concatenates them with a pipe:
        var outputCombiner = StringSymbolCombiner.getInstance();
        var parser = DOTParsers.mmlt(silentOutput, outputCombiner);

        try (InputStream is = Example4.class.getResourceAsStream("/mmlt_example.dot")) {
            var parsedModel = parser.readModel(is);
            mmlt = parsedModel.model;
            alphabet = parsedModel.alphabet;

            // During learning, we use a symbolic "timeout" symbol to indicate that the
            // teacher should wait for the next timeout. To avoid an infinite runtime,
            // we set a maximum waiting time for these symbols.
            // This time should be at least the maximum time to the next timeout in any
            // state of the system. We configure this as follows:
            long maxTimeoutDelay = MMLTs.getMaximumTimeoutDelay(mmlt);

            // After adding a new location, the learner infers timers for it by watching the SUL for timeouts.
            // To learn an accurate model, the maximum time to watch for these timeouts must be at
            // least the value of "maxTimeoutDelay".
            // If the maximum initial value of timers in the SUL is known or can be reasonably estimated,
            // setting the watch time to twice that value usually yields good results:
            long maxTimerQueryWaitingFinal = MMLTs.getMaximumInitialTimerValue(mmlt) * 2;

            params = new MMLTModelParams<>(silentOutput, outputCombiner, maxTimeoutDelay, maxTimerQueryWaitingFinal);
        } catch (IOException | FormatException e) {
            throw new IllegalStateException("Unable to load model from file.", e);
        }

        // Proceed as in Example1:

        var statistics = Statistics.getService();
        statistics.setText(Example1.KEY_MODEL, "mmlt_example.dot");
        statistics.setCounter(Example1.KEY_LOCS, mmlt.getStates().size());
        statistics.setCounter(Example1.KEY_SYMS, alphabet.size());

        // Set up the pipeline:
        // We use a simulator SUL to simulate our automaton:
        var sul = new MMLTSimulatorSUL<>(mmlt);

        // We count all operations that are performed on the SUL with a stats-SUL:
        var statsAfterCache = new CounterTimedSUL<>(sul, "post-cache");

        // We use a cache to avoid redundant operations:
        var cacheSUL = new TimedSULTreeCache<>(statsAfterCache, params);
        var toReducerSul = new TimeoutReducerSUL<>(cacheSUL, params.maxTimeoutWaitingTime());
        var statsBeforeCache = new CounterTimedSUL<>(toReducerSul, "pre-cache");

        // We use a query oracle to answer queries from the learner:
        var timeOracle = new TimedSULOracle<>(statsBeforeCache, params);

        // In the basic set-up, we use a simulator oracle to answer equivalence queries.
        // This oracle has perfect knowledge of the reference automaton.
        var eqOracle = new SimulatorEQOracle<>(mmlt);

        // Set up our L* learner:

        // We provide the learner with an initial set of suffixes.
        // We include all untimed inputs and the symbolic timeout symbol, which causes the learner to wait
        // until the next timeout (but no longer than params.maxTimeoutWaitingTime()).
        List<Word<TimedInput<String>>> suffixes = new ArrayList<>();
        alphabet.forEach(s -> suffixes.add(Word.fromLetter(TimedInput.input(s))));
        suffixes.add(Word.fromLetter(new TimeoutSymbol<>()));

        var learner = new ExtensibleLStarMMLTBuilder<String, String>().withAlphabet(alphabet)
                                                                      .withModelParams(params)
                                                                      .withTimeOracle(timeOracle)
                                                                      .withInitialSuffixes(suffixes)
                                                                      .create();

        // Start learning:
        ExampleRunner.runExperiment(learner, eqOracle, mmlt.getSemantics().getInputAlphabet());
    }

}

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.example.mmlt;
17
18	import java.io.IOException;
19	import java.io.InputStream;
20	import java.util.ArrayList;
21	import java.util.List;
22
23	import de.learnlib.algorithm.lstar.mmlt.ExtensibleLStarMMLTBuilder;
24	import de.learnlib.driver.simulator.MMLTSimulatorSUL;
25	import de.learnlib.filter.cache.mmlt.TimedSULTreeCache;
26	import de.learnlib.filter.cache.mmlt.TimeoutReducerSUL;
27	import de.learnlib.filter.statistic.sul.CounterTimedSUL;
28	import de.learnlib.oracle.equivalence.mmlt.SimulatorEQOracle;
29	import de.learnlib.oracle.membership.TimedSULOracle;
30	import de.learnlib.statistic.Statistics;
31	import de.learnlib.time.MMLTModelParams;
32	import net.automatalib.alphabet.Alphabet;
33	import net.automatalib.automaton.mmlt.MMLT;
34	import net.automatalib.automaton.mmlt.impl.StringSymbolCombiner;
35	import net.automatalib.exception.FormatException;
36	import net.automatalib.serialization.dot.DOTMMLTParser;
37	import net.automatalib.serialization.dot.DOTParsers;
38	import net.automatalib.symbol.time.TimedInput;
39	import net.automatalib.symbol.time.TimeoutSymbol;
40	import net.automatalib.util.automaton.mmlt.MMLTs;
41	import net.automatalib.word.Word;
42
43	/**
44	* This example demonstrates how to load an {@link MMLT} from a dot-file and learn it using the L* algorithm.
45	* <p>
46	* A description of the dot-file syntax for MMLTs can be found in AutomataLib (see {@link DOTMMLTParser}).
47	*/
48	@SuppressWarnings("PMD.UseExplicitTypes") // allow vars in examples
49	public final class Example4 {
50
51	private Example4() {
52	// prevent instantiation
53	}
54
55	public static void main(String[] args) {
56	// First, we load the file "mmlt_example.dot" from the "resources" folder:
57	MMLT<?, String, ?, String> mmlt;
58	Alphabet<String> alphabet;
59	MMLTModelParams<String> params;
60
61	// We define the output that represents silence:
62	var silentOutput = "void";	1✔
63
64	// In an MMLT, a timeout may yield multiple outputs.
65	// We use a symbol combiner to combine them into a single output.
66	// Here, we use a StringSymbolCombiner that sorts symbols and then concatenates them with a pipe:
67	var outputCombiner = StringSymbolCombiner.getInstance();	1✔
68	var parser = DOTParsers.mmlt(silentOutput, outputCombiner);	1✔
69
70	try (InputStream is = Example4.class.getResourceAsStream("/mmlt_example.dot")) {	1✔
71	var parsedModel = parser.readModel(is);	1✔
72	mmlt = parsedModel.model;	1✔
73	alphabet = parsedModel.alphabet;	1✔
74
75	// During learning, we use a symbolic "timeout" symbol to indicate that the
76	// teacher should wait for the next timeout. To avoid an infinite runtime,
77	// we set a maximum waiting time for these symbols.
78	// This time should be at least the maximum time to the next timeout in any
79	// state of the system. We configure this as follows:
80	long maxTimeoutDelay = MMLTs.getMaximumTimeoutDelay(mmlt);	1✔
81
82	// After adding a new location, the learner infers timers for it by watching the SUL for timeouts.
83	// To learn an accurate model, the maximum time to watch for these timeouts must be at
84	// least the value of "maxTimeoutDelay".
85	// If the maximum initial value of timers in the SUL is known or can be reasonably estimated,
86	// setting the watch time to twice that value usually yields good results:
87	long maxTimerQueryWaitingFinal = MMLTs.getMaximumInitialTimerValue(mmlt) * 2;	1✔
88
89	params = new MMLTModelParams<>(silentOutput, outputCombiner, maxTimeoutDelay, maxTimerQueryWaitingFinal);	1✔
NEW 90	} catch (IOException \| FormatException e) {	×
NEW 91	throw new IllegalStateException("Unable to load model from file.", e);	×
92	}	1✔
93
94	// Proceed as in Example1:
95
96	var statistics = Statistics.getService();	1✔
97	statistics.setText(Example1.KEY_MODEL, "mmlt_example.dot");	1✔
98	statistics.setCounter(Example1.KEY_LOCS, mmlt.getStates().size());	1✔
99	statistics.setCounter(Example1.KEY_SYMS, alphabet.size());	1✔
100
101	// Set up the pipeline:
102	// We use a simulator SUL to simulate our automaton:
103	var sul = new MMLTSimulatorSUL<>(mmlt);	1✔
104
105	// We count all operations that are performed on the SUL with a stats-SUL:
106	var statsAfterCache = new CounterTimedSUL<>(sul, "post-cache");	1✔
107
108	// We use a cache to avoid redundant operations:
109	var cacheSUL = new TimedSULTreeCache<>(statsAfterCache, params);	1✔
110	var toReducerSul = new TimeoutReducerSUL<>(cacheSUL, params.maxTimeoutWaitingTime());	1✔
111	var statsBeforeCache = new CounterTimedSUL<>(toReducerSul, "pre-cache");	1✔
112
113	// We use a query oracle to answer queries from the learner:
114	var timeOracle = new TimedSULOracle<>(statsBeforeCache, params);	1✔
115
116	// In the basic set-up, we use a simulator oracle to answer equivalence queries.
117	// This oracle has perfect knowledge of the reference automaton.
118	var eqOracle = new SimulatorEQOracle<>(mmlt);	1✔
119
120	// Set up our L* learner:
121
122	// We provide the learner with an initial set of suffixes.
123	// We include all untimed inputs and the symbolic timeout symbol, which causes the learner to wait
124	// until the next timeout (but no longer than params.maxTimeoutWaitingTime()).
125	List<Word<TimedInput<String>>> suffixes = new ArrayList<>();	1✔
126	alphabet.forEach(s -> suffixes.add(Word.fromLetter(TimedInput.input(s))));	1✔
127	suffixes.add(Word.fromLetter(new TimeoutSymbol<>()));	1✔
128
129	var learner = new ExtensibleLStarMMLTBuilder<String, String>().withAlphabet(alphabet)	1✔
130	.withModelParams(params)	1✔
131	.withTimeOracle(timeOracle)	1✔
132	.withInitialSuffixes(suffixes)	1✔
133	.create();	1✔
134
135	// Start learning:
136	ExampleRunner.runExperiment(learner, eqOracle, mmlt.getSemantics().getInputAlphabet());	1✔
137	}	1✔
138
139	}

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