Implementation for learning MMLTs, new model for collecting statistics

algorithms/active/lstar/pom.xml

@@ -124,6 +124,26 @@ limitations under the License.
             <groupId>org.testng</groupId>
             <artifactId>testng</artifactId>
         </dependency>
+        <dependency>
+            <groupId>net.automatalib</groupId>
+            <artifactId>automata-serialization-dot</artifactId>
+            <scope>test</scope>
+        </dependency>
+        <dependency>
+            <groupId>de.learnlib</groupId>
+            <artifactId>learnlib-cache</artifactId>
+            <scope>test</scope>
+        </dependency>
+        <dependency>
+            <groupId>de.learnlib</groupId>
+            <artifactId>learnlib-symbol-filters</artifactId>
+            <scope>test</scope>
+        </dependency>
+        <dependency>
+            <groupId>de.learnlib</groupId>
+            <artifactId>learnlib-statistics</artifactId>
+            <scope>test</scope>
+        </dependency>
     </dependencies>
 
     <build>
@@ -134,7 +154,9 @@ limitations under the License.
                     <artifactId>maven-surefire-plugin</artifactId>
                     <configuration>
                         <!-- append to existing argLine to nicely work together with jacoco plugin -->
-                        <argLine>@{argLine} --add-reads=de.learnlib.algorithm.lstar=net.automatalib.util</argLine>
+                        <!-- allow tests access to util and statistics -->
+                        <argLine>@{argLine} --add-reads=de.learnlib.algorithm.lstar=net.automatalib.util --add-reads=de.learnlib.algorithm.lstar=de.learnlib.filter.statistic
+                        </argLine>
                     </configuration>
                 </plugin>
             </plugins>

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

@@ -0,0 +1,72 @@
+package de.learnlib.algorithm.lstar.mmlt;
+
+import de.learnlib.algorithm.LocalTimerMealyModelParams;
+import de.learnlib.datastructure.observationtable.Row;
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol;
+import net.automatalib.alphabet.time.mmlt.LocalTimerMealyOutputSymbol;
+import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+/**
+ * Stores various data used for describing the MMLT hypothesis.
+ * This includes the OT, a list of local resets, and a list of outputs.
+ *
+ * @param <I> Input type for non-delaying inputs
+ * @param <O> Output symbol type
+ */
+class LStarLocalTimerMealyHypDataContainer<I, O> {
+    private final Alphabet<LocalTimerMealySemanticInputSymbol<I>> alphabet;
+
+    private final LocalTimerMealyObservationTable<I, O> table;
+    private final Map<Word<LocalTimerMealySemanticInputSymbol<I>>, LocalTimerMealyOutputSymbol<O>> transitionOutputMap;
+    private final Set<Word<LocalTimerMealySemanticInputSymbol<I>>> transitionResetSet; // all transitions that trigger a reset
+
+    private final LocalTimerMealyModelParams<O> modelParams;
+
+    public LStarLocalTimerMealyHypDataContainer(Alphabet<LocalTimerMealySemanticInputSymbol<I>> alphabet, LocalTimerMealyModelParams<O> modelParams, LocalTimerMealyObservationTable<I, O> table) {
+        this.alphabet = alphabet;
+        this.modelParams = modelParams;
+        this.table = table;
+
+        this.transitionOutputMap = new HashMap<>();
+        this.transitionResetSet = new HashSet<>();
+    }
+
+    @Nullable
+    protected LocalTimerMealyOutputSymbol<O> getTransitionOutput(Row<LocalTimerMealySemanticInputSymbol<I>> stateRow, int inputIdx) {
+        Row<LocalTimerMealySemanticInputSymbol<I>> transRow = stateRow.getSuccessor(inputIdx);
+        if (transRow == null) {
+            return null;
+        }
+
+        return this.transitionOutputMap.getOrDefault(transRow.getLabel(), null);
+    }
+
+
+    public LocalTimerMealyModelParams<O> getModelParams() {
+        return modelParams;
+    }
+
+    public Alphabet<LocalTimerMealySemanticInputSymbol<I>> getAlphabet() {
+        return alphabet;
+    }
+
+
+    public LocalTimerMealyObservationTable<I, O> getTable() {
+        return table;
+    }
+
+    public Map<Word<LocalTimerMealySemanticInputSymbol<I>>, LocalTimerMealyOutputSymbol<O>> getTransitionOutputMap() {
+        return transitionOutputMap;
+    }
+
+    public Set<Word<LocalTimerMealySemanticInputSymbol<I>>> getTransitionResetSet() {
+        return transitionResetSet;
+    }
+}

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

@@ -0,0 +1,127 @@
+package de.learnlib.algorithm.lstar.mmlt;
+
+import de.learnlib.datastructure.observationtable.Row;
+import net.automatalib.alphabet.impl.GrowingMapAlphabet;
+import net.automatalib.alphabet.time.mmlt.*;
+import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy;
+import net.automatalib.automaton.time.mmlt.LocalTimerMealy;
+import net.automatalib.word.Word;
+
+import java.util.HashMap;
+import java.util.Map;
+
+class LocalTimerMealyHypothesisBuilder {
+
+    record LocalTimerMealyHypothesisBuildResult<S, I, O>(LocalTimerMealy<S, I, O> automaton,
+                                                         Map<Integer, Word<LocalTimerMealySemanticInputSymbol<I>>> prefixMap) {
+
+    }
+
+    /**
+     * Constructs a hypothesis MMLT from an observation table, inferred local resets, and inferred local timers.
+     */
+    static <I, O> LocalTimerMealyHypothesisBuildResult<Integer, I, O> constructHypothesis(LStarLocalTimerMealyHypDataContainer<I, O> hypData) {
+
+        // 1. Create map that stores link between contentID and short-prefix row:
+        final Map<Integer, Row<LocalTimerMealySemanticInputSymbol<I>>> locationContentIdMap = new HashMap<>(); // contentId -> sp location
+        for (var spRow : hypData.getTable().getShortPrefixRows()) {
+            if (locationContentIdMap.containsKey(spRow.getRowContentId())) {
+                // Multiple sp rows may have same contentID. Thus, assign each id one location:
+                continue;
+            }
+            locationContentIdMap.put(spRow.getRowContentId(), spRow);
+        }
+
+        // 2. Create untimed alphabet:
+        GrowingMapAlphabet<NonDelayingInput<I>> alphabet = new GrowingMapAlphabet<>();
+        for (var symbol : hypData.getAlphabet()) {
+            if (symbol instanceof NonDelayingInput<I> ndi) {
+                alphabet.add(ndi);
+            }
+        }
+
+        // 3. Prepare objects for automaton, timers and resets:
+        int numLocations = hypData.getTable().numberOfShortPrefixRows();
+        var hypothesis = new CompactLocalTimerMealy<>(alphabet, hypData.getModelParams().silentOutput(), hypData.getModelParams().outputCombiner());
+
+        final Map<Integer, Integer> stateMap = new HashMap<>(numLocations); // row content id -> state id
+
+        final Map<Integer, Word<LocalTimerMealySemanticInputSymbol<I>>> prefixMap = new HashMap<>(numLocations); // state id -> location prefix
+
+        // 4. Create one state per location:
+        for (var row : hypData.getTable().getShortPrefixRows()) {
+            int newStateId = hypothesis.addState();
+            stateMap.putIfAbsent(row.getRowContentId(), newStateId);
+            prefixMap.put(newStateId, row.getLabel());
+
+            if (row.getLabel().equals(Word.epsilon())) {
+                hypothesis.setInitialState(newStateId);
+            }
+        }
+        // Ensure initial location:
+        if (hypothesis.getInitialState() == null) {
+            throw new IllegalArgumentException("Automaton must have an initial location.");
+        }
+
+        // 5. Create outgoing transitions for non-delaying inputs:
+        for (var rowContentId : stateMap.keySet()) {
+            Row<LocalTimerMealySemanticInputSymbol<I>> spLocation = locationContentIdMap.get(rowContentId);
+
+            for (var symbol : alphabet) {
+                int symIdx = hypData.getAlphabet().getSymbolIndex(symbol);
+
+                var transOutput = hypData.getTransitionOutput(spLocation, symIdx);
+                O output = hypData.getModelParams().silentOutput(); // silent by default
+                if (transOutput != null) {
+                    output = transOutput.getSymbol();
+                }
+
+                int successorId;
+                if (spLocation.getSuccessor(symIdx) == null) {
+                    successorId = spLocation.getRowContentId(); // not in local alphabet -> self-loop
+                } else {
+                    successorId = spLocation.getSuccessor(symIdx).getRowContentId();
+                }
+
+                // Add transition to automaton:
+                int sourceLocId = stateMap.get(rowContentId);
+                int successorLocId = stateMap.get(successorId);
+                hypothesis.addTransition(sourceLocId, symbol, output, successorLocId);
+
+                // Check for local reset:
+                var targetTransition = spLocation.getLabel().append(symbol);
+                if (hypData.getTransitionResetSet().contains(targetTransition) && sourceLocId == successorLocId) {
+                    hypothesis.addLocalReset(sourceLocId, symbol);
+                }
+            }
+
+        }
+
+        // 6. Add timeout transitions:
+        for (var rowContentId : stateMap.keySet()) {
+            Row<LocalTimerMealySemanticInputSymbol<I>> spLocation = locationContentIdMap.get(rowContentId);
+
+            var timerInfo = hypData.getTable().getLocationTimerInfo(spLocation);
+            if (timerInfo == null) {
+                continue; // no timers
+            }
+
+            for (var timer : timerInfo.getLocalTimers().values()) {
+                if (timer.periodic()) {
+                    hypothesis.addPeriodicTimer(stateMap.get(rowContentId), timer.name(), timer.initial(), timer.output());
+                } else {
+                    // One-shot: use successor from table
+                    LocalTimerMealySemanticInputSymbol<I> symbol = new TimeStepSequence<>(timer.initial());
+
+                    int symIdx = hypData.getAlphabet().getSymbolIndex(symbol);
+                    int successorId = spLocation.getSuccessor(symIdx).getRowContentId();
+
+                    hypothesis.addOneShotTimer(stateMap.get(rowContentId), timer.name(), timer.initial(), timer.output(), stateMap.get(successorId));
+                }
+            }
+        }
+
+        return new LocalTimerMealyHypothesisBuildResult<>(hypothesis, prefixMap);
+    }
+
+}