MMLT-Learner now explicitly takes untimed inputs in constructor.

Author: tupaul

algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LStarLocalTimerMealy.java

@@ -29,6 +29,9 @@
 import de.learnlib.symbol_filter.SymbolFilterResponse;
 import de.learnlib.util.mealy.MealyUtil;
 import net.automatalib.alphabet.Alphabet;
+import net.automatalib.alphabet.GrowingAlphabet;
+import net.automatalib.alphabet.impl.Alphabets;
+import net.automatalib.alphabet.impl.GrowingMapAlphabet;
 import net.automatalib.automaton.mmlt.MMLT;
 import net.automatalib.automaton.mmlt.MealyTimerInfo;
 import net.automatalib.symbol.time.InputSymbol;
@@ -70,13 +73,13 @@ public class LStarLocalTimerMealy<I, O> implements OTLearner<MMLT<Integer, I, ?,
      * Uses the close-shortest strategy for closing the observation table and
      * binary-backwards search for decomposing counterexamples.
      *
-     * @param alphabet        Input alphabet for the semantic automaton
+     * @param alphabet        Alphabet of non-delaying inputs
      * @param modelParams     LocalTimerMealyModel parameters
      * @param initialSuffixes Initial set of suffixes. May be empty.
      * @param timeOracle      The output query oracle for MMLTs.
      * @param symbolFilter    The symbol filter. If no filter should be used, use the AcceptAll filter.
      */
-    public LStarLocalTimerMealy(Alphabet<TimedInput<I>> alphabet,
+    public LStarLocalTimerMealy(Alphabet<I> alphabet,
                                 LocalTimerMealyModelParams<O> modelParams,
                                 List<Word<TimedInput<I>>> initialSuffixes,
                                 AbstractTimedQueryOracle<I, O> timeOracle,
@@ -87,15 +90,15 @@ public LStarLocalTimerMealy(Alphabet<TimedInput<I>> alphabet,
     /**
      * Instantiates a new Rivest-Schapire learner for MMLTs.
      *
-     * @param alphabet        Input alphabet for the semantic automaton
+     * @param alphabet        Alphabet of non-delaying inputs
      * @param modelParams     LocalTimerMealyModel parameters
      * @param initialSuffixes Initial set of suffixes. May be empty.
      * @param closingStrategy Closing strategy for the observation table.
      * @param timeOracle      The output query oracle for MMLTs.
      * @param symbolFilter    The symbol filter. If no filter should be used, use the AcceptAll filter.
      * @param analyzer        The strategy for decomposing counterexamples.
      */
-    public LStarLocalTimerMealy(Alphabet<TimedInput<I>> alphabet,
+    public LStarLocalTimerMealy(Alphabet<I> alphabet,
                                 LocalTimerMealyModelParams<O> modelParams,
                                 List<Word<TimedInput<I>>> initialSuffixes,
                                 ClosingStrategy<? super TimedInput<I>, ? super Word<TimedOutput<O>>> closingStrategy,
@@ -108,9 +111,14 @@ public LStarLocalTimerMealy(Alphabet<TimedInput<I>> alphabet,
 
         // Prepare hyp data:
 
+        // Internally, the learner also stores TimeStepSequences in its alphabet:
+        GrowingAlphabet<TimedInput<I>> internalAlphabet = new GrowingMapAlphabet<>();
+        alphabet.forEach(s -> internalAlphabet.add(TimedInput.input(s)));
+
         // Init hypothesis data:
-        this.hypData = new LStarLocalTimerMealyHypDataContainer<>(alphabet, modelParams,
-                new LocalTimerMealyObservationTable<>(alphabet, modelParams.maxTimerQueryWaitingTime(), symbolFilter, modelParams.silentOutput()));
+        this.hypData = new LStarLocalTimerMealyHypDataContainer<>(internalAlphabet, modelParams,
+                new LocalTimerMealyObservationTable<>(internalAlphabet,
+                        modelParams.maxTimerQueryWaitingTime(), symbolFilter, modelParams.silentOutput()));
 
         this.cexAnalyzer = new LocalTimerMealyCounterexampleHandler<>(timeOracle, analyzer, symbolFilter);
         this.symbolFilter = symbolFilter;

algorithms/active/lstar/src/test/java/de/learnlib/algorithm/lstar/mmlt/LStarLocalTimerMealyBenchmarkTests.java

@@ -94,8 +94,6 @@ private static <S, I, T, O> void learnModel(String name, MMLT<S, I, T, O> automa
         stats.setCounter("original_inputs", "Untimed alphabet size in original", automaton.getInputAlphabet().size());
 
         // Set up a pipeline:
-        Alphabet<TimedInput<I>> alphabet = new GrowingMapAlphabet<>(automaton.getInputAlphabet().stream().map(TimedInput::input).toList());
-
         // Query oracle -> TimeoutReducer -> Cache -> Query stats -> SUL
         LocalTimerMealySimulatorSUL<?, I, ?, O> sul = new LocalTimerMealySimulatorSUL<>(automaton.getSemantics());
         LocalTimerMealyStatsSUL<I, O> statsAfterCache = new LocalTimerMealyStatsSUL<>(sul, stats);
@@ -116,7 +114,7 @@ private static <S, I, T, O> void learnModel(String name, MMLT<S, I, T, O> automa
 
         // Create learner:
         List<Word<TimedInput<I>>> suffixes = new ArrayList<>();
-        alphabet.forEach(s -> suffixes.add(Word.fromLetter(s)));
+        automaton.getInputAlphabet().forEach(s -> suffixes.add(Word.fromLetter(TimedInput.input(s))));
         suffixes.add(Word.fromLetter(new TimeoutSymbol<>()));
 
         // Configure symbol filter:
@@ -130,7 +128,7 @@ private static <S, I, T, O> void learnModel(String name, MMLT<S, I, T, O> automa
         filter = new LocalTimerMealyStatisticsSymbolFilter<>(automaton, filter, stats);
         filter = new CachedSymbolFilter<>(filter); // need to wrap to enable updates to responses
 
-        var learner = new LStarLocalTimerMealy<>(alphabet, params, suffixes, timeOracle, filter);
+        var learner = new LStarLocalTimerMealy<>(automaton.getInputAlphabet(), params, suffixes, timeOracle, filter);
         learner.setStatsContainer(stats);
 
         // Start learning:

algorithms/active/lstar/src/test/java/de/learnlib/algorithm/lstar/mmlt/LStarLocalTimerMealyCounterexampleTests.java

@@ -29,13 +29,10 @@ public class LStarLocalTimerMealyCounterexampleTests {
 
     private static <S, I, T, O> void learnModel(LocalTimerMealyModel<S, I, T, O> model, List<Word<TimedInput<I>>> counterexamples) {
 
-        Alphabet<TimedInput<I>> alphabet =
-                new GrowingMapAlphabet<>(model.automaton().getInputAlphabet().stream().map(TimedInput::input).toList());
-
         var sul = new LocalTimerMealySimulatorSUL<>(model.automaton().getSemantics());
         TimedQueryOracle<I, O> timeOracle = new TimedQueryOracle<>(sul, model.params());
 
-        var learner = new LStarLocalTimerMealy<>(alphabet, model.params(), Collections.emptyList(),
+        var learner = new LStarLocalTimerMealy<>(model.automaton().getInputAlphabet(), model.params(), Collections.emptyList(),
                 timeOracle, new AcceptAllSymbolFilter<>());
 
         learner.startLearning();

examples/src/main/java/de/learnlib/example/mmlt/Example1.java

@@ -53,9 +53,6 @@ public static void main(String[] args) {
 
         // ======================
         // Set up the pipeline:
-        Alphabet<TimedInput<String>> alphabet =
-                new GrowingMapAlphabet<>(model.automaton().getInputAlphabet().stream().map(TimedInput::input).toList());
-
         // We use a simulator SUL to simulate our automaton:
         var sul = new LocalTimerMealySimulatorSUL<>(model.automaton().getSemantics());
 
@@ -80,7 +77,7 @@ public static void main(String[] args) {
 
         // Set up our L* learner:
         List<Word<TimedInput<String>>> suffixes = new ArrayList<>();
-        alphabet.forEach(s -> suffixes.add(Word.fromLetter(s)));
+        model.automaton().getInputAlphabet().forEach(s -> suffixes.add(Word.fromLetter(TimedInput.input(s))));
         suffixes.add(Word.fromLetter(new TimeoutSymbol<>()));
 
         // A symbol filter allows us to reduce queries by exploiting prior knowledge.
@@ -92,7 +89,7 @@ public static void main(String[] args) {
         filter = new LocalTimerMealyStatisticsSymbolFilter<>(model.automaton(), filter, stats);
         filter = new CachedSymbolFilter<>(filter); // need to wrap to enable updates to responses
 
-        var learner = new LStarLocalTimerMealy<>(alphabet, model.params(), suffixes, timeOracle, filter);
+        var learner = new LStarLocalTimerMealy<>(model.automaton().getInputAlphabet(), model.params(), suffixes, timeOracle, filter);
         learner.setStatsContainer(stats);
 
         // Start learning: