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

96.67

/examples/src/main/java/de/learnlib/example/mmlt/Example2.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.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.oracle.CounterEQOracle;
import de.learnlib.filter.statistic.sul.CounterTimedSUL;
import de.learnlib.oracle.equivalence.MMLTEQOracleChain;
import de.learnlib.oracle.equivalence.mmlt.RandomWpMethodEQOracle;
import de.learnlib.oracle.equivalence.mmlt.ResetSearchEQOracle;
import de.learnlib.oracle.equivalence.mmlt.SimulatorEQOracle;
import de.learnlib.oracle.membership.TimedSULOracle;
import de.learnlib.statistic.Statistics;
import de.learnlib.testsupport.example.mmlt.MMLTExamples;
import net.automatalib.symbol.time.TimedInput;
import net.automatalib.symbol.time.TimeoutSymbol;
import net.automatalib.word.Word;

/**
 * This example shows a basic set-up of the MMLT-learner for a black-box setting.
 * <p>
 * For this, we use a chain of different equivalence oracles that can be applied if the reference automaton is not
 * known.
 */
@SuppressWarnings("PMD.UseExplicitTypes") // allow magic numbers and vars in examples
public final class Example2 {

    private static final int BOUND = 100;
    private static final int MIN_SIZE = 16;
    private static final double PERCENTAGE = 1.0;
    private static final int SEED = 100;

    private Example2() {
        // prevent instantiation
    }

    public static void main(String[] args) {
        var model = MMLTExamples.sensorCollector();
        var mmlt = model.getReferenceAutomaton();
        var alphabet = mmlt.getInputAlphabet();

        // We first create a statistics container.
        // This container will store various statistical data during learning:
        var statistics = Statistics.getService();
        statistics.setText(Example1.KEY_MODEL, model.toString());
        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, model.getParams());
        var toReducerSul = new TimeoutReducerSUL<>(cacheSUL, model.getParams().maxTimeoutWaitingTime());
        var statsBeforeCache = new CounterTimedSUL<>(toReducerSul, "pre-cache");

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

        // We use a chain of different equivalence oracles to find counterexamples more efficiently:
        var chainOracle = new MMLTEQOracleChain<String, String>();
        // A cache oracle tests if the current hypothesis and the reference automaton give the same outputs
        // for all words that have already been queried. As the words have already been queried, this
        // executes no additional queries on the SUL:
        chainOracle.addOracle(new CounterEQOracle<>(cacheSUL.createCacheConsistencyTest(), "cache"));

        // A ResetSearchOracle tests for missing local resets, which often require many and/or long test words
        // when using random-based testing. We configure the tester to consider all transitions that might cause a reset:
        chainOracle.addOracle(new CounterEQOracle<>(new ResetSearchEQOracle<>(timeOracle, SEED, PERCENTAGE, PERCENTAGE),
                                                    "reset"));

        // Finally, we add an MMLT-specific RandomWp oracle:
        chainOracle.addOracle(new CounterEQOracle<>(new RandomWpMethodEQOracle<>(timeOracle, SEED, MIN_SIZE, 0, BOUND),
                                                    "wp"));

        // Set up our L* learner:
        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(model.getParams())
                                                                      .withTimeOracle(timeOracle)
                                                                      .withInitialSuffixes(suffixes)
                                                                      .create();

        // Start learning:
        var finalModel = ExampleRunner.runExperiment(learner, chainOracle, mmlt.getSemantics().getInputAlphabet());

        // In this set-up, we actually know the reference automaton.
        // This allows us to check that we learned an accurate model:
        var simOracle = new SimulatorEQOracle<>(mmlt);
        if (simOracle.findCounterExample(finalModel, finalModel.getSemantics().getInputAlphabet()) != null) {
            throw new IllegalStateException("Incorrect model learned.");
        }

        // Troubleshooting
        // If you attempt to learn a model of some application and the learner
        // throws assertion errors or illegal state exceptions,
        // your SUL likely has no MMLT semantics.
        // In this case, you can try to learn a partial model by excluding TimeStepSymbol
        // from the input alphabet for the counterexample search:
        // In your learn-loop (see ExampleUtil), replace
        // tester.findCounterExample(hyp, hyp.getSemantics().getInputAlphabet());
        // with: tester.findCounterExample(hyp, hyp.getSemantics().getInputAlphabet().stream().filter(s -> !(s instanceof TimeStepSymbol<String>)).toList());
    }

}

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.util.ArrayList;
19	import java.util.List;
20
21	import de.learnlib.algorithm.lstar.mmlt.ExtensibleLStarMMLTBuilder;
22	import de.learnlib.driver.simulator.MMLTSimulatorSUL;
23	import de.learnlib.filter.cache.mmlt.TimedSULTreeCache;
24	import de.learnlib.filter.cache.mmlt.TimeoutReducerSUL;
25	import de.learnlib.filter.statistic.oracle.CounterEQOracle;
26	import de.learnlib.filter.statistic.sul.CounterTimedSUL;
27	import de.learnlib.oracle.equivalence.MMLTEQOracleChain;
28	import de.learnlib.oracle.equivalence.mmlt.RandomWpMethodEQOracle;
29	import de.learnlib.oracle.equivalence.mmlt.ResetSearchEQOracle;
30	import de.learnlib.oracle.equivalence.mmlt.SimulatorEQOracle;
31	import de.learnlib.oracle.membership.TimedSULOracle;
32	import de.learnlib.statistic.Statistics;
33	import de.learnlib.testsupport.example.mmlt.MMLTExamples;
34	import net.automatalib.symbol.time.TimedInput;
35	import net.automatalib.symbol.time.TimeoutSymbol;
36	import net.automatalib.word.Word;
37
38	/**
39	* This example shows a basic set-up of the MMLT-learner for a black-box setting.
40	* <p>
41	* For this, we use a chain of different equivalence oracles that can be applied if the reference automaton is not
42	* known.
43	*/
44	@SuppressWarnings("PMD.UseExplicitTypes") // allow magic numbers and vars in examples
45	public final class Example2 {
46
47	private static final int BOUND = 100;
48	private static final int MIN_SIZE = 16;
49	private static final double PERCENTAGE = 1.0;
50	private static final int SEED = 100;
51
52	private Example2() {
53	// prevent instantiation
54	}
55
56	public static void main(String[] args) {
57	var model = MMLTExamples.sensorCollector();	1✔
58	var mmlt = model.getReferenceAutomaton();	1✔
59	var alphabet = mmlt.getInputAlphabet();	1✔
60
61	// We first create a statistics container.
62	// This container will store various statistical data during learning:
63	var statistics = Statistics.getService();	1✔
64	statistics.setText(Example1.KEY_MODEL, model.toString());	1✔
65	statistics.setCounter(Example1.KEY_LOCS, mmlt.getStates().size());	1✔
66	statistics.setCounter(Example1.KEY_SYMS, alphabet.size());	1✔
67
68	// ======================
69	// Set up the pipeline:
70	// We use a simulator SUL to simulate our automaton:
71	var sul = new MMLTSimulatorSUL<>(mmlt);	1✔
72
73	// We count all operations that are performed on the SUL with a stats-SUL:
74	var statsAfterCache = new CounterTimedSUL<>(sul, "post-cache");	1✔
75
76	// We use a cache to avoid redundant operations:
77	var cacheSUL = new TimedSULTreeCache<>(statsAfterCache, model.getParams());	1✔
78	var toReducerSul = new TimeoutReducerSUL<>(cacheSUL, model.getParams().maxTimeoutWaitingTime());	1✔
79	var statsBeforeCache = new CounterTimedSUL<>(toReducerSul, "pre-cache");	1✔
80
81	// We use a query oracle to answer queries from the learner:
82	var timeOracle = new TimedSULOracle<>(statsBeforeCache, model.getParams());	1✔
83
84	// We use a chain of different equivalence oracles to find counterexamples more efficiently:
85	var chainOracle = new MMLTEQOracleChain<String, String>();	1✔
86	// A cache oracle tests if the current hypothesis and the reference automaton give the same outputs
87	// for all words that have already been queried. As the words have already been queried, this
88	// executes no additional queries on the SUL:
89	chainOracle.addOracle(new CounterEQOracle<>(cacheSUL.createCacheConsistencyTest(), "cache"));	1✔
90
91	// A ResetSearchOracle tests for missing local resets, which often require many and/or long test words
92	// when using random-based testing. We configure the tester to consider all transitions that might cause a reset:
93	chainOracle.addOracle(new CounterEQOracle<>(new ResetSearchEQOracle<>(timeOracle, SEED, PERCENTAGE, PERCENTAGE),	1✔
94	"reset"));
95
96	// Finally, we add an MMLT-specific RandomWp oracle:
97	chainOracle.addOracle(new CounterEQOracle<>(new RandomWpMethodEQOracle<>(timeOracle, SEED, MIN_SIZE, 0, BOUND),	1✔
98	"wp"));
99
100	// Set up our L* learner:
101	List<Word<TimedInput<String>>> suffixes = new ArrayList<>();	1✔
102	alphabet.forEach(s -> suffixes.add(Word.fromLetter(TimedInput.input(s))));	1✔
103	suffixes.add(Word.fromLetter(new TimeoutSymbol<>()));	1✔
104
105	var learner = new ExtensibleLStarMMLTBuilder<String, String>().withAlphabet(alphabet)	1✔
106	.withModelParams(model.getParams())	1✔
107	.withTimeOracle(timeOracle)	1✔
108	.withInitialSuffixes(suffixes)	1✔
109	.create();	1✔
110
111	// Start learning:
112	var finalModel = ExampleRunner.runExperiment(learner, chainOracle, mmlt.getSemantics().getInputAlphabet());	1✔
113
114	// In this set-up, we actually know the reference automaton.
115	// This allows us to check that we learned an accurate model:
116	var simOracle = new SimulatorEQOracle<>(mmlt);	1✔
117	if (simOracle.findCounterExample(finalModel, finalModel.getSemantics().getInputAlphabet()) != null) {	1✔
NEW 118	throw new IllegalStateException("Incorrect model learned.");	×
119	}
120
121	// Troubleshooting
122	// If you attempt to learn a model of some application and the learner
123	// throws assertion errors or illegal state exceptions,
124	// your SUL likely has no MMLT semantics.
125	// In this case, you can try to learn a partial model by excluding TimeStepSymbol
126	// from the input alphabet for the counterexample search:
127	// In your learn-loop (see ExampleUtil), replace
128	// tester.findCounterExample(hyp, hyp.getSemantics().getInputAlphabet());
129	// with: tester.findCounterExample(hyp, hyp.getSemantics().getInputAlphabet().stream().filter(s -> !(s instanceof TimeStepSymbol<String>)).toList());
130	}	1✔
131
132	}

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