cexAnalyzer;
+
+ /**
+ * Instantiates a new Rivest-Schapire learner for MMLTs.
+ *
+ * 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 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> alphabet,
+ LocalTimerMealyModelParams modelParams,
+ @NonNull
+ List>> initialSuffixes,
+ AbstractTimedQueryOracle timeOracle,
+ @NonNull SymbolFilter, NonDelayingInput> symbolFilter) {
+ this(alphabet, modelParams, initialSuffixes, ClosingStrategies.CLOSE_SHORTEST, timeOracle, symbolFilter, AcexAnalyzers.BINARY_SEARCH_BWD);
+ }
+
+ /**
+ * Instantiates a new Rivest-Schapire learner for MMLTs.
+ *
+ * @param alphabet Input alphabet for the semantic automaton
+ * @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> alphabet,
+ LocalTimerMealyModelParams modelParams,
+ @NonNull
+ List>> initialSuffixes,
+ ClosingStrategy, ? super Word>> closingStrategy,
+ AbstractTimedQueryOracle timeOracle,
+ @NonNull SymbolFilter, NonDelayingInput> symbolFilter,
+ AcexAnalyzer analyzer) {
+ this.closingStrategy = closingStrategy;
+ this.timeOracle = timeOracle;
+ this.initialSuffixes = initialSuffixes;
+
+ // Prepare hyp data:
+
+ // Init hypothesis data:
+ this.hypData = new LStarLocalTimerMealyHypDataContainer<>(alphabet, modelParams,
+ new LocalTimerMealyObservationTable<>(alphabet, modelParams.maxTimerQueryWaitingTime(), symbolFilter, modelParams.silentOutput()));
+
+ this.cexAnalyzer = new LocalTimerMealyCounterexampleHandler<>(timeOracle, analyzer, symbolFilter);
+ this.symbolFilter = symbolFilter;
+ }
+
+ /**
+ * Heuristically chooses a new one-shot timer from the provided timers:
+ * takes the timer with the highest initial value that a) does not exceed maxInitialValue and b) has not timer
+ * with a lower initial value that times out at the same time.
+ *
+ * @param sortedTimers Timers, sorted ascendingly by their initial value
+ * @param maxInitialValue Max. initial value to consider
+ * @param Output type
+ * @return New one-shot timer
+ */
+ public static MealyTimerInfo selectOneShotTimer(List> sortedTimers, long maxInitialValue) {
+
+ // Filter relevant timers:
+ // Start at timer with the highest initial value.
+ // Ignore all timers whose initial value exceeds the maximum value.
+ // Also ignore timers whose timeout is the multiple of another timer's initial value.
+ List> relevantTimers = new ArrayList<>();
+ for (int i = sortedTimers.size() - 1; i >= 0; i--) {
+ MealyTimerInfo timer = sortedTimers.get(i);
+
+ if (timer.initial() > maxInitialValue) {
+ continue; // could not have expired
+ }
+
+ // Ignore timers whose initial value is a multiple of another one.
+ // When set to one-shot, these would expire at same time as periodic timer -> non-deterministic behavior!
+ boolean multiple = false;
+ for (int j = 0; j < i; j++) {
+ MealyTimerInfo otherTimer = sortedTimers.get(j);
+ if (timer.initial() % otherTimer.initial() == 0) {
+ multiple = true;
+ break;
+ }
+ }
+ if (multiple) {
+ continue;
+ }
+
+ relevantTimers.add(timer); // not a multiple and within time
+ }
+
+ if (relevantTimers.isEmpty()) {
+ throw new IllegalStateException("Max. initial value is too low; must include at least one timer.");
+ }
+
+ // Return the candidate with the highest initial value one-shot:
+ return relevantTimers.get(0); // order is reversed -> first is last
+ }
+
+
+ /**
+ * Constructs an MMLT hypothesis.
+ * This updates all transition outputs, if required.
+ *
+ * @return MMLT hypothesis
+ */
+ public LocalTimerMealy getHypothesisModel() {
+ return getInternalLocalTimerMealyHypothesis();
+ }
+
+ /**
+ * Like the construction above, but returns an LocalTimerMealyHypothesis object instead.
+ * This objects provides additional functions that are just intended for the learner but not the teacher.
+ *
+ * @return MMLT hypothesis
+ */
+ private LocalTimerMealyHypothesis getInternalLocalTimerMealyHypothesis() {
+ this.updateOutputs();
+ var hyp = LocalTimerMealyHypothesisBuilder.constructHypothesis(this.hypData);
+
+ return new LocalTimerMealyHypothesis<>(hyp.automaton(), hyp.prefixMap());
+ }
+
+ protected List>> selectClosingRows(List>>> unclosed) {
+ return closingStrategy.selectClosingRows(unclosed, hypData.getTable(), timeOracle);
+ }
+
+
+ protected void updateOutputs() {
+ // Query output of newly-added transitions:
+ Stream.concat(this.hypData.getTable().getShortPrefixRows().stream(), this.hypData.getTable().getLongPrefixRows().stream())
+ .forEach(row -> {
+ if (row.getLabel().isEmpty()) {
+ return; // initial state
+ }
+
+ if (this.hypData.getTransitionOutputMap().containsKey(row.getLabel())) {
+ return; // already queried
+ }
+
+ Word> prefix = row.getLabel().prefix(-1);
+ LocalTimerMealySemanticInputSymbol inputSym = row.getLabel().suffix(1).lastSymbol();
+
+ LocalTimerMealyOutputSymbol output = null;
+ if (inputSym instanceof TimeStepSequence ws) {
+ // Query timer output from table:
+ MealyTimerInfo timerInfo = this.hypData.getTable().getTimerInfo(prefix, ws.getTimeSteps());
+ if (timerInfo == null) {
+ throw new AssertionError();
+ }
+ output = new LocalTimerMealyOutputSymbol<>(timerInfo.output());
+ } else {
+ output = this.timeOracle.querySuffixOutput(prefix, Word.fromLetter(inputSym)).lastSymbol();
+ }
+
+ if (output != null) {
+ this.hypData.getTransitionOutputMap().put(row.getLabel(), output);
+ }
+ });
+ }
+
+ // ==========================
+
+ @Override
+ public void startLearning() {
+ List>>> initialUnclosed = this.hypData.getTable().initialize(Collections.emptyList(), this.initialSuffixes, timeOracle);
+
+ // Ensure that closed:
+ this.completeConsistentTable(initialUnclosed);
+ }
+
+ @Override
+ public boolean refineHypothesis(DefaultQuery, Word>> ceQuery) {
+ if (!refineHypothesisSingle(ceQuery)) {
+ return false; // no valid CEX
+ }
+ while (refineHypothesisSingle(ceQuery)) {
+ }
+ return true;
+ }
+
+
+ /**
+ * Transforms the provided counterexample to an inconsistency object:
+ * First, checks if still a counterexample. If so, cuts the cex after the first output deviation.
+ *
+ * @param ceQuery Counterexample
+ * @param hypothesis Current hypothesis
+ * @return The resulting inconsistency, or null, if the counterexample is not a counterexample.
+ */
+ @Nullable
+ private LocalTimerMealyOutputInconsistency toOutputInconsistency(DefaultQuery, Word>> ceQuery, LocalTimerMealyHypothesis hypothesis) {
+ // 1. Cut example after first deviation:
+ Word> hypOutput = hypothesis.getSemantics().computeSuffixOutput(ceQuery.getPrefix(), ceQuery.getSuffix());
+ DefaultQuery, Word>> shortQuery = CexPreprocessor.truncateCEX(ceQuery, hypOutput);
+ if (shortQuery == null) {
+ return null;
+ }
+
+ // 2. Calculate shortened hypothesis output:
+ var shortHypOutput = hypothesis.getSemantics().computeSuffixOutput(shortQuery.getPrefix(), shortQuery.getSuffix());
+ if (shortHypOutput.equals(shortQuery.getOutput())) {
+ throw new AssertionError("Deviation lost after shortening.");
+ }
+
+ return new LocalTimerMealyOutputInconsistency<>(shortQuery.getPrefix(),
+ shortQuery.getSuffix(),
+ shortQuery.getOutput(), shortHypOutput);
+ }
+
+ private boolean refineHypothesisSingle(DefaultQuery, Word>> ceQuery) {
+ // 1. Update hypothesis (may have changed since last refinement):
+ var hypothesis = this.getInternalLocalTimerMealyHypothesis();
+
+ // 2. Transform to output inconsistency:
+ var outputIncons = this.toOutputInconsistency(ceQuery, hypothesis);
+ if (outputIncons == null) {
+ return false;
+ }
+
+ logger.debug(String.format("Refining with inconsistency %s", outputIncons));
+
+ // 3. Identify source of deviation:
+ stats.startOrResumeClock("clk_cex_analysis", "Total cex analysis time");
+ stats.increaseCounter("cnt_cex_analysis", "Cex analyses");
+ var analysisResult = this.cexAnalyzer.analyzeInconsistency(outputIncons, hypothesis);
+ stats.pauseClock("clk_cex_analysis");
+
+ // 4. Refine:
+ if (analysisResult instanceof MissingDiscriminatorResult locSplit) {
+ stats.increaseCounter("INACC_MISSING_DISC",
+ "Inaccuracies: missing discriminators");
+
+ // Add new discriminator as suffix:
+ if (hypData.getTable().getSuffixes().contains(locSplit.getDiscriminator())) throw new AssertionError();
+ List>> suffixes = Collections.singletonList(locSplit.getDiscriminator());
+ var unclosed = hypData.getTable().addSuffixes(suffixes, timeOracle);
+
+ // Close transitions:
+ this.completeConsistentTable(unclosed); // no consistency check for RS
+ } else if (analysisResult instanceof MissingResetResult noReset) {
+ stats.increaseCounter("INACC_MISSING_RESETS",
+ "Inaccuracies: missing resets");
+
+ // Add missing reset:
+ var resetTrans = hypothesis.getPrefix(noReset.getLocation()).append(noReset.getInput());
+ this.hypData.getTransitionResetSet().add(resetTrans);
+ } else if (analysisResult instanceof MissingOneShotResult noAperiodic) {
+ stats.increaseCounter("INACC_MISSING_OS",
+ "Inaccuracies: missing one-shot timers");
+
+ // Identify corresponding sp row:
+ Word> locPrefix = hypothesis.getPrefix(noAperiodic.getLocation());
+ Row> spRow = hypData.getTable().getRow(locPrefix);
+ if (spRow == null || !spRow.isShortPrefixRow()) {
+ throw new AssertionError();
+ }
+
+ this.handleMissingTimeoutChange(spRow, noAperiodic.getTimeout());
+ } else if (analysisResult instanceof FalseIgnoreResult falseIgnore) {
+ stats.increaseCounter("INACC_MISSING_FI",
+ "Inaccuracies: false ignores");
+
+ if (this.symbolFilter == null) {
+ throw new AssertionError("Cannot detect false ignores without symbol filter.");
+ }
+
+ // Identify corresponding sp row:
+ Word> locPrefix = hypothesis.getPrefix(falseIgnore.getLocation());
+ Row> spRow = hypData.getTable().getRow(locPrefix);
+ if (spRow == null || !spRow.isShortPrefixRow()) {
+ throw new AssertionError();
+ }
+
+ // Update filter:
+ this.symbolFilter.update(locPrefix, falseIgnore.getSymbol(), SymbolFilterResponse.ACCEPT);
+
+ // Legalize symbol + close table:
+ var unclosed = hypData.getTable().addOutgoingTransition(spRow, falseIgnore.getSymbol(), this.timeOracle);
+ stats.increaseCounter("Count_legalized", "Legalized symbols");
+
+ this.completeConsistentTable(unclosed);
+ } else {
+ throw new IllegalStateException("Unknown inconsistency type.");
+ }
+
+ return true;
+ }
+
+ private void handleMissingTimeoutChange(Row> spRow, MealyTimerInfo timeout) {
+ var locationTimerInfo = hypData.getTable().getLocationTimerInfo(spRow);
+ if (locationTimerInfo == null) {
+ throw new AssertionError("Location with missing one-shot timer must have timers.");
+ }
+
+ // Only timer with highest initial value can be one-shot.
+ // If location already has a one-shot timer, prefix of its timeout-transition might be core or fringe prefix.
+ // If it is a fringe prefix, we need to remove it:
+ var lastTimerTransPrefix = spRow.getLabel().append(new TimeStepSequence<>(locationTimerInfo.getLastTimer().initial()));
+ if (!locationTimerInfo.getLastTimer().periodic()) {
+ if (!hypData.getTable().getRow(lastTimerTransPrefix).isShortPrefixRow()) {
+ // Last timer is one-shot + has fringe prefix:
+ this.hypData.getTable().removeLpRow(lastTimerTransPrefix);
+ }
+ }
+
+ // Prefix for timeout-transition of new one-shot timer:
+ Word> timerTransPrefix = spRow.getLabel().append(new TimeStepSequence<>(timeout.initial()));
+ if (this.hypData.getTable().getRow(timerTransPrefix) != null) {
+ throw new AssertionError("Timer already appears to be one-shot.");
+ }
+
+ // Remove all timers with greater timeout (are now redundant):
+ var subsequentTimers = locationTimerInfo.getSortedTimers().stream()
+ .filter(t -> t.initial() > timeout.initial())
+ .map(MealyTimerInfo::name).toList();
+ subsequentTimers.forEach(locationTimerInfo::removeTimer);
+
+ // Change from periodic to one-shot:
+ locationTimerInfo.setOneShotTimer(timeout.name());
+
+ // Update fringe prefixes + close table:
+ List>>> unclosed = this.hypData.getTable().addTimerTransition(spRow, timeout, this.timeOracle);
+ this.completeConsistentTable(unclosed);
+ }
+
+
+ @Override
+ public ObservationTable, Word>> getObservationTable() {
+ return this.hypData.getTable();
+ }
+
+ /**
+ * Iteratively checks for unclosedness and inconsistencies in the table, and fixes any occurrences thereof. This
+ * process is repeated until the observation table is both closed and consistent.
+ *
+ * Simplified version for RS learner: assumes that OT is always consistent.
+ *
+ * @param unclosed the unclosed rows (equivalence classes) to start with.
+ */
+ protected void completeConsistentTable(List>>> unclosed) {
+ List>>> unclosedIter = unclosed;
+ while (!unclosedIter.isEmpty()) {
+ List>> closingRows = this.selectClosingRows(unclosedIter);
+
+ // Add new states:
+ unclosedIter = hypData.getTable().toShortPrefixes(closingRows, timeOracle);
+ }
+
+ }
+
+ @Override
+ public void setStatsContainer(StatsContainer container) {
+ this.stats = container;
+ this.cexAnalyzer.setStatsContainer(container);
+ }
+
+
+}
diff --git a/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LStarLocalTimerMealyHypDataContainer.java b/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LStarLocalTimerMealyHypDataContainer.java
new file mode 100644
index 0000000000..14954492ac
--- /dev/null
+++ b/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 Input type for non-delaying inputs
+ * @param Output symbol type
+ */
+class LStarLocalTimerMealyHypDataContainer {
+ private final Alphabet> alphabet;
+
+ private final LocalTimerMealyObservationTable table;
+ private final Map>, LocalTimerMealyOutputSymbol> transitionOutputMap;
+ private final Set>> transitionResetSet; // all transitions that trigger a reset
+
+ private final LocalTimerMealyModelParams modelParams;
+
+ public LStarLocalTimerMealyHypDataContainer(Alphabet> alphabet, LocalTimerMealyModelParams modelParams, LocalTimerMealyObservationTable table) {
+ this.alphabet = alphabet;
+ this.modelParams = modelParams;
+ this.table = table;
+
+ this.transitionOutputMap = new HashMap<>();
+ this.transitionResetSet = new HashSet<>();
+ }
+
+ @Nullable
+ protected LocalTimerMealyOutputSymbol getTransitionOutput(Row> stateRow, int inputIdx) {
+ Row> transRow = stateRow.getSuccessor(inputIdx);
+ if (transRow == null) {
+ return null;
+ }
+
+ return this.transitionOutputMap.getOrDefault(transRow.getLabel(), null);
+ }
+
+
+ public LocalTimerMealyModelParams getModelParams() {
+ return modelParams;
+ }
+
+ public Alphabet> getAlphabet() {
+ return alphabet;
+ }
+
+
+ public LocalTimerMealyObservationTable getTable() {
+ return table;
+ }
+
+ public Map>, LocalTimerMealyOutputSymbol> getTransitionOutputMap() {
+ return transitionOutputMap;
+ }
+
+ public Set>> getTransitionResetSet() {
+ return transitionResetSet;
+ }
+}
diff --git a/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocalTimerMealyHypothesisBuilder.java b/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocalTimerMealyHypothesisBuilder.java
new file mode 100644
index 0000000000..d23788ebaa
--- /dev/null
+++ b/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(LocalTimerMealy automaton,
+ Map>> prefixMap) {
+
+ }
+
+ /**
+ * Constructs a hypothesis MMLT from an observation table, inferred local resets, and inferred local timers.
+ */
+ static LocalTimerMealyHypothesisBuildResult constructHypothesis(LStarLocalTimerMealyHypDataContainer hypData) {
+
+ // 1. Create map that stores link between contentID and short-prefix row:
+ final Map>> 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> alphabet = new GrowingMapAlphabet<>();
+ for (var symbol : hypData.getAlphabet()) {
+ if (symbol instanceof NonDelayingInput 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 stateMap = new HashMap<>(numLocations); // row content id -> state id
+
+ final Map>> 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> 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> 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 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);
+ }
+
+}
diff --git a/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocalTimerMealyObservationTable.java b/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocalTimerMealyObservationTable.java
new file mode 100644
index 0000000000..163961d834
--- /dev/null
+++ b/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocalTimerMealyObservationTable.java
@@ -0,0 +1,583 @@
+package de.learnlib.algorithm.lstar.mmlt;
+
+import de.learnlib.datastructure.observationtable.MutableObservationTable;
+import de.learnlib.datastructure.observationtable.Row;
+import de.learnlib.datastructure.observationtable.RowImpl;
+import de.learnlib.oracle.AbstractTimedQueryOracle;
+import de.learnlib.oracle.MembershipOracle;
+import de.learnlib.symbol_filter.SymbolFilter;
+import de.learnlib.symbol_filter.SymbolFilterResponse;
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.alphabet.time.mmlt.*;
+import net.automatalib.automaton.time.mmlt.MealyTimerInfo;
+import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.util.*;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
+/**
+ * The observation table used by the MMLT learner.
+ *
+ * Unlike an OT for standard Mealy learning, includes prefixes for the timeout transitions of one-shot timers.
+ * Intended to be used with a symbol filter. The filter is queried before adding a new transition for a non-delaying input.
+ * If the filter considers the transition to be a silent self-loop, the output of the transition is first verified.
+ * If it is actually silent the learner considers the transition to be a silent self-loop. Consequently,
+ * it does not add a transition for it. Transitions may be added later if an input was falsely ignored.
+ *
+ * Assumes that all short prefixes lead to different locations (-> no need to make canonical)
+ *
+ * @param Input type for non-delaying inputs
+ * @param Output symbol type
+ */
+public class LocalTimerMealyObservationTable implements MutableObservationTable, Word>> {
+
+ private static final Logger logger = LoggerFactory.getLogger(LocalTimerMealyObservationTable.class);
+
+ private final SymbolFilter, NonDelayingInput> symbolFilter;
+
+ private final Map>, LocationTimerInfo> timerInfoMap; // prefix -> timer info
+
+ private final Map>, RowImpl>> shortPrefixRowMap; // label -> row info
+ private final Map>, RowImpl>> longPrefixRowMap; // label -> row info
+
+ private final List>> sortedShortPrefixes; // values of shortPrefixRowMap sorted by label, for faster access.
+ private final List>> longPrefixList; // values of longPrefixRowMap as list, for faster access.
+
+ private final Map> rowContentMap; // contentID -> row content
+ private static final int NO_CONTENT = -1;
+
+ private final List>> suffixes = new ArrayList<>();
+ private final Set>> suffixSet = new HashSet<>();
+
+ private final Alphabet> alphabet;
+ private final long minTimerQueryWaitTime;
+ private final LocalTimerMealyOutputSymbol silentOutput; // used for symbol filtering
+
+ public LocalTimerMealyObservationTable(Alphabet> alphabet, long minTimerQueryWaitTime,
+ @NonNull SymbolFilter, NonDelayingInput> symbolFilter, O silentOutput) {
+ this.alphabet = alphabet;
+
+ this.symbolFilter = symbolFilter;
+ this.silentOutput = new LocalTimerMealyOutputSymbol<>(silentOutput);
+ this.minTimerQueryWaitTime = minTimerQueryWaitTime;
+
+ this.timerInfoMap = new HashMap<>();
+
+ this.shortPrefixRowMap = new HashMap<>();
+ this.sortedShortPrefixes = new ArrayList<>();
+
+ this.longPrefixRowMap = new HashMap<>();
+ this.longPrefixList = new ArrayList<>();
+
+ this.rowContentMap = new HashMap<>();
+ }
+
+ /**
+ * Infers local timers for the provided location.
+ *
+ * @param location Source location.
+ */
+ private void identifyLocalTimers(LocationTimerInfo location, AbstractTimedQueryOracle timeOracle) {
+ var timerQueryResponse = timeOracle.queryTimers(location.getPrefix(), this.minTimerQueryWaitTime);
+
+ if (timerQueryResponse.aborted()) {
+ var newOneShot = LStarLocalTimerMealy.selectOneShotTimer(timerQueryResponse.timers(), Long.MAX_VALUE);
+ newOneShot.setOneShot();
+ }
+
+ // Add timers up to one-shot:
+ for (var timer : timerQueryResponse.timers()) {
+ location.addTimer(timer);
+ this.extendAlphabet(new TimeStepSequence<>(timer.initial()));
+ if (!timer.periodic()) {
+ break;
+ }
+ }
+ }
+
+ /**
+ * Extends the global alphabet without adding new transitions.
+ *
+ * @param symbol New alphabet symbol
+ */
+ private void extendAlphabet(TimeStepSequence symbol) {
+ if (!alphabet.containsSymbol(symbol)) {
+ alphabet.asGrowingAlphabetOrThrowException().addSymbol(symbol);
+ }
+
+ for (RowImpl> prefix : this.shortPrefixRowMap.values()) {
+ prefix.ensureInputCapacity(alphabet.size());
+ }
+ }
+
+ /**
+ * Adds the initial location.
+ *
+ * @return Corresponding row in the OT
+ */
+ private RowImpl> addInitialLocation() {
+ RowImpl> newRow = new RowImpl<>(Word.epsilon(), 0, alphabet.size());
+ newRow.makeShort(alphabet.size());
+ this.shortPrefixRowMap.put(Word.epsilon(), newRow);
+ this.sortedShortPrefixes.add(newRow);
+ this.sortedShortPrefixes.sort(Comparator.comparing(r -> r.getLabel().toString()));
+
+ return newRow;
+ }
+
+
+ /**
+ * Adds a new location that belongs to the provided short-prefix row.
+ * Infers timers for this location and creates outgoing transitions.
+ *
+ * @param newRow Newly-added short prefix row
+ * @param timeOracle Time oracle
+ */
+ private void initLocation(RowImpl> newRow, AbstractTimedQueryOracle timeOracle) {
+ LocationTimerInfo timerInfo = new LocationTimerInfo<>(newRow.getLabel());
+ this.identifyLocalTimers(timerInfo, timeOracle);
+
+ if (timerInfo.getLastTimer() != null) { // location has timer
+ this.timerInfoMap.put(newRow.getLabel(), timerInfo);
+ }
+
+ // Add outgoing transitions:
+ List>> transitions = this.createOutgoingTransitions(newRow, timeOracle);
+ transitions.forEach(t -> this.queryAllSuffixes(t, timeOracle));
+ }
+
+ /**
+ * Creates transitions for the provided short-prefix row. Adds transitions for non-delaying inputs
+ * and a transition for the one-shot timer of the location, if present.
+ *
+ * If a symbol filter is provided, the filter is queried before adding a transition for a non-delaying input.
+ * If the filter considers the input a silent self-loop, no transition is explicitly created for the input.
+ *
+ * @param spRow Short prefix row
+ * @param timeOracle Time query oracle
+ * @return New transitions
+ */
+ private List>> createOutgoingTransitions(RowImpl> spRow, AbstractTimedQueryOracle timeOracle) {
+ List>> transitions = new ArrayList<>();
+
+ Word> sp = spRow.getLabel();
+
+ // First, add transitions for non-delaying symbols:
+ for (int i = 0; i < alphabet.size(); i++) {
+ LocalTimerMealySemanticInputSymbol sym = alphabet.getSymbol(i);
+ if (sym instanceof TimeStepSequence || sym instanceof TimeoutSymbol) {
+ continue;
+ }
+
+ Word> lp = sp.append(sym);
+ assert !this.shortPrefixRowMap.containsKey(lp);
+
+ RowImpl> succRow = this.longPrefixRowMap.get(lp);
+ if (succRow == null) {
+ // Query symbol filter before adding transition:
+ var filterResponse = this.symbolFilter.query(sp, (NonDelayingInput) sym);
+ if (filterResponse == SymbolFilterResponse.IGNORE) {
+ // Verify that output is silent:
+ var response = timeOracle.querySuffixOutput(sp, Word.fromLetter(sym));
+ assert response.size() == 1;
+ if (!response.firstSymbol().equals(silentOutput)) {
+ // Not silent -> cannot be silent self-loop:
+ filterResponse = SymbolFilterResponse.ACCEPT;
+
+ // Update filter:
+ this.symbolFilter.update(sp, (NonDelayingInput) sym, SymbolFilterResponse.ACCEPT);
+ }
+ }
+
+ if (filterResponse == SymbolFilterResponse.ACCEPT) {
+ // Treat as usual:
+ succRow = this.createLpRow(lp);
+ }
+ }
+
+ spRow.setSuccessor(i, succRow);
+ if (succRow != null) {
+ transitions.add(succRow);
+ }
+ }
+
+ // Second, add one-shot timer transition (if any):
+ var locTimers = timerInfoMap.getOrDefault(spRow.getLabel(), null);
+ if (locTimers != null && !locTimers.getLastTimer().periodic()) {
+ LocalTimerMealySemanticInputSymbol waitSym = new TimeStepSequence<>(locTimers.getLastTimer().initial());
+ Word> lp = sp.append(waitSym);
+ assert !this.shortPrefixRowMap.containsKey(lp);
+
+ RowImpl> succRow = this.longPrefixRowMap.get(lp);
+ if (succRow == null) {
+ succRow = this.createLpRow(lp);
+ }
+ spRow.setSuccessor(this.alphabet.getSymbolIndex(waitSym), succRow);
+ transitions.add(succRow);
+ }
+
+ return transitions;
+ }
+
+ private RowImpl> createLpRow(Word> prefix) {
+ RowImpl> newRow = new RowImpl<>(prefix, 0);
+ this.longPrefixRowMap.put(prefix, newRow);
+ this.longPrefixList.add(newRow);
+ if (this.longPrefixList.size() != this.longPrefixRowMap.size()) throw new AssertionError();
+
+ newRow.setLpIndex(0); // unused
+
+ return newRow;
+ }
+
+ /**
+ * Identify transitions that have not been closed.
+ * I.e., there is no state with the same suffix behavior.
+ * Also removes unused content ids.
+ *
+ * Guarantees that returned transition list order is deterministic.
+ */
+ public List>>> findUnclosedTransitions() {
+ // Identify contentIds for locations:
+ Set spContentIds = this.shortPrefixRowMap.values().stream()
+ .map(RowImpl::getRowContentId)
+ .collect(Collectors.toSet());
+
+ // Group lp rows by their content id:
+ Map>>> lpContentMap = new HashMap<>();
+ for (var lpRow : this.longPrefixRowMap.values()) {
+ lpContentMap.putIfAbsent(lpRow.getRowContentId(), new ArrayList<>());
+ lpContentMap.get(lpRow.getRowContentId()).add(lpRow);
+ }
+
+ // Identify ids that are not used by any SP:
+ List>>> unclosedRows = new ArrayList<>();
+ List sortedLpIds = lpContentMap.keySet().stream().sorted().toList();
+ for (var lpId : sortedLpIds) {
+ if (spContentIds.contains(lpId)) {
+ continue;
+ }
+
+ // Sort row s.t. list order deterministic:
+ List>> unclosedWithId = lpContentMap.get(lpId);
+ unclosedWithId.sort(Comparator.comparing(r -> r.getLabel().toString()));
+ unclosedRows.add(unclosedWithId);
+ }
+
+ // Remove unused content ids:
+ Set usedContentIds = Stream.concat(this.shortPrefixRowMap.values().stream(), this.longPrefixRowMap.values().stream())
+ .map(RowImpl::getRowContentId).collect(Collectors.toSet());
+
+ List oldContentIds = this.rowContentMap.keySet().stream().toList();
+ for (int oldId : oldContentIds) {
+ if (!usedContentIds.contains(oldId)) {
+ this.rowContentMap.remove(oldId);
+ }
+ }
+
+
+ return unclosedRows;
+ }
+
+ @Override
+ public List>>> initialize(List>> initialShortPrefixes,
+ List>> initialSuffixes,
+ MembershipOracle, Word>> oracle) {
+
+ if (isInitialized()) {
+ throw new IllegalStateException("Called initialize, but there are already rows present");
+ }
+ if (!initialShortPrefixes.isEmpty()) {
+ throw new IllegalArgumentException("Init with short prefixes is not supported.");
+ }
+ if (!(oracle instanceof AbstractTimedQueryOracle timedOracle)) {
+ throw new IllegalArgumentException("Must use timed oracle!");
+ }
+
+ // Add initial suffixes:
+ for (Word> suffix : initialSuffixes) {
+ if (suffixSet.add(suffix)) {
+ suffixes.add(suffix);
+ }
+ }
+
+ // 1. Create initial location:
+ var newLoc = this.addInitialLocation();
+ this.initLocation(newLoc, timedOracle);
+ this.queryAllSuffixes(newLoc, timedOracle);
+
+ // 2. Identify unclosed transitions:
+ return this.findUnclosedTransitions();
+ }
+
+ private void queryAllSuffixes(RowImpl> row, AbstractTimedQueryOracle timedOracle) {
+ Word> prefix = row.getLabel();
+
+ List>> suffixOutputs = new ArrayList<>(this.suffixes.size());
+ for (Word> suffix : this.suffixes) {
+ Word> output = timedOracle.querySuffixOutput(prefix, suffix);
+ suffixOutputs.add(output);
+ }
+
+ this.processSuffixOutputs(row, suffixOutputs);
+ }
+
+ private void processSuffixOutputs(RowImpl> row, List>> rowContents) {
+ if (rowContents.isEmpty()) {
+ row.setRowContentId(NO_CONTENT);
+ return;
+ }
+
+ RowContent content = new RowContent<>(rowContents);
+ int contentId = content.hashCode();
+ this.rowContentMap.putIfAbsent(contentId, content);
+ row.setRowContentId(contentId);
+ }
+
+ @Override
+ public boolean isInitialized() {
+ return !(shortPrefixRowMap.isEmpty() && longPrefixRowMap.isEmpty());
+ }
+
+ @Override
+ public boolean isInitialConsistencyCheckRequired() {
+ return false;
+ }
+
+ @Override
+ public List>>> addSuffixes(Collection>> newSuffixes, MembershipOracle, Word>> oracle) {
+ if (!(oracle instanceof AbstractTimedQueryOracle timedOracle)) {
+ throw new IllegalArgumentException();
+ }
+
+ // 1. Extend current suffixes + identify new suffixes:
+ List>> newSuffixList = new ArrayList<>();
+ for (Word> suffix : newSuffixes) {
+ if (this.suffixSet.add(suffix)) {
+ logger.debug(String.format("Adding new suffix '%s'", suffix));
+
+ newSuffixList.add(suffix);
+ this.suffixes.add(suffix);
+ }
+ }
+ if (newSuffixList.isEmpty()) {
+ return Collections.emptyList();
+ }
+
+ // 2. Update row content:
+ Stream.concat(shortPrefixRowMap.values().stream(), longPrefixRowMap.values().stream()).forEach(row -> {
+ List>> updatedOutputs = new ArrayList<>();
+ if (row.getRowContentId() != NO_CONTENT) {
+ // Add existing suffix outputs:
+ updatedOutputs.addAll(this.rowContentMap.get(row.getRowContentId()).outputs());
+ }
+
+ for (Word> suffix : newSuffixList) {
+ Word> output = timedOracle.querySuffixOutput(row.getLabel(), suffix);
+ updatedOutputs.add(output);
+ }
+
+ this.processSuffixOutputs(row, updatedOutputs);
+ });
+
+ return this.findUnclosedTransitions();
+ }
+
+ @Override
+ public List>>> addShortPrefixes(List>> shortPrefixes, MembershipOracle, Word>> oracle) {
+ throw new IllegalStateException("Not supported.");
+ }
+
+ @Override
+ public List>>> toShortPrefixes(List>> lpRows, MembershipOracle, Word>> oracle) {
+ if (!(oracle instanceof AbstractTimedQueryOracle timedOracle)) {
+ throw new IllegalArgumentException();
+ }
+
+ for (Row> row : lpRows) {
+ logger.debug(String.format("Adding new location with prefix '%s'", row.getLabel()));
+
+ final RowImpl> lpRow = (RowImpl>) row;
+
+ // Delete from LP rows:
+ var removed = this.longPrefixRowMap.remove(row.getLabel());
+ this.longPrefixList.remove(removed);
+ if (this.longPrefixList.size() != this.longPrefixRowMap.size()) throw new AssertionError();
+
+ // Add to SP rows:
+ this.shortPrefixRowMap.put(row.getLabel(), lpRow);
+ this.sortedShortPrefixes.add(lpRow);
+ this.sortedShortPrefixes.sort(Comparator.comparing(r -> r.getLabel().toString()));
+
+ lpRow.makeShort(alphabet.size());
+
+ this.initLocation(lpRow, timedOracle);
+ }
+ return this.findUnclosedTransitions();
+ }
+
+ @Override
+ public List>>> addAlphabetSymbol(LocalTimerMealySemanticInputSymbol symbol, MembershipOracle, Word>> oracle) {
+ throw new IllegalStateException("Not supported.");
+ }
+
+ @Override
+ public Alphabet> getInputAlphabet() {
+ return this.alphabet;
+ }
+
+ @Override
+ public Collection>> getShortPrefixRows() {
+ if (this.sortedShortPrefixes.size() != this.shortPrefixRowMap.size()) throw new AssertionError();
+ return Collections.unmodifiableList(this.sortedShortPrefixes);
+ }
+
+ @Override
+ public Collection>> getLongPrefixRows() {
+ return Collections.unmodifiableList(this.longPrefixList);
+ }
+
+ @Override
+ public Row> getRow(int idx) {
+ throw new IllegalStateException("Not supported. Use prefix to access rows instead.");
+ }
+
+ @Override
+ public @Nullable Row> getRow(Word> prefix) {
+ if (this.shortPrefixRowMap.containsKey(prefix)) {
+ return this.shortPrefixRowMap.get(prefix);
+ }
+ if (this.longPrefixRowMap.containsKey(prefix)) {
+ return this.longPrefixRowMap.get(prefix);
+ }
+ return null;
+ }
+
+ @Override
+ public int numberOfDistinctRows() {
+ return this.rowContentMap.size();
+ }
+
+ @Override
+ public List>> getSuffixes() {
+ return this.suffixes;
+ }
+
+ @Override
+ @Nullable
+ public List>> rowContents(Row> row) {
+ if (this.rowContentMap.isEmpty()) {
+ // OT may be empty if only single location with timers:
+ if (!this.suffixes.isEmpty()) {
+ throw new AssertionError();
+ }
+ return Collections.emptyList();
+ }
+
+ return this.rowContentMap.get(row.getRowContentId()).outputs();
+ }
+
+ @Override
+ public Word> transformAccessSequence(Word> word) {
+ throw new IllegalStateException("Not implemented.");
+ }
+
+
+ @Override
+ public boolean isAccessSequence(Word> word) {
+ throw new IllegalStateException("Not implemented.");
+ }
+
+ public @Nullable MealyTimerInfo getTimerInfo(Word> prefix, long initial) {
+ var info = this.timerInfoMap.get(prefix);
+ if (info != null) {
+ return info.getTimerInfo(initial);
+ }
+ return null;
+ }
+
+ @Nullable
+ public LocationTimerInfo getLocationTimerInfo(Row> sp) {
+ return this.timerInfoMap.getOrDefault(sp.getLabel(), null);
+ }
+
+ /**
+ * Adds an outgoing transition for the given symbol to the given location
+ * and subsequently tests for unclosed transitions.
+ *
+ * Raises an error if this transition already exists.
+ *
+ * @param spRow Source location
+ * @param symbol Input symbol
+ * @param timeOracle Oracle
+ * @return List of unclosed rows. Empty, if none.
+ */
+ public List>>> addOutgoingTransition(Row> spRow, LocalTimerMealySemanticInputSymbol symbol, AbstractTimedQueryOracle timeOracle) {
+ if (!this.alphabet.containsSymbol(symbol)) {
+ throw new IllegalArgumentException("Unknown symbol.");
+ }
+
+ Word> transitionPrefix = spRow.getLabel().append(symbol);
+
+ // Add long-prefix row:
+ if (this.getRow(transitionPrefix) != null) {
+ throw new AssertionError("Location already has an outgoing transition for the provided symbol");
+ }
+
+ RowImpl> succRow = this.createLpRow(transitionPrefix);
+
+ // Set as successor:
+ int symIdx = this.alphabet.getSymbolIndex(symbol);
+ ((RowImpl>) spRow).setSuccessor(symIdx, succRow);
+
+ // Update suffixes:
+ this.queryAllSuffixes(succRow, timeOracle);
+
+ return this.findUnclosedTransitions();
+ }
+
+ public List>>> addTimerTransition(Row> spRow, MealyTimerInfo timeout, AbstractTimedQueryOracle timeOracle) {
+ return this.addOutgoingTransition(spRow, new TimeStepSequence<>(timeout.initial()), timeOracle);
+ }
+
+ /**
+ * Removes a long prefix row. Should only be used when removing a transition of a former one-shot timer.
+ * When turning a long into a short prefix, use toShortPrefix instead,
+ *
+ * @param prefix Row prefix
+ */
+ public void removeLpRow(Word> prefix) {
+ if (!this.longPrefixRowMap.containsKey(prefix)) {
+ throw new IllegalArgumentException("Attempting to remove lp row that does not exist.");
+ }
+
+ // Remove lp row:
+ var removed = this.longPrefixRowMap.remove(prefix);
+ this.longPrefixList.remove(removed);
+ if (this.longPrefixList.size() != this.longPrefixRowMap.size()) throw new AssertionError();
+
+ // Unset as successor:
+ int symIdx = this.alphabet.getSymbolIndex(prefix.lastSymbol());
+ RowImpl> spRow = this.shortPrefixRowMap.get(prefix.prefix(-1));
+ assert spRow != null;
+
+ spRow.setSuccessor(symIdx, null);
+ }
+
+ // =============================
+
+ private record RowContent(List>> outputs) {
+
+ @Override
+ public int hashCode() {
+ return outputs.toString().hashCode();
+ }
+ }
+
+
+}
diff --git a/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocationTimerInfo.java b/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocationTimerInfo.java
new file mode 100644
index 0000000000..f0ab4616dc
--- /dev/null
+++ b/algorithms/active/lstar/src/main/java/de/learnlib/algorithm/lstar/mmlt/LocationTimerInfo.java
@@ -0,0 +1,119 @@
+package de.learnlib.algorithm.lstar.mmlt;
+
+import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol;
+import net.automatalib.automaton.time.mmlt.MealyTimerInfo;
+import net.automatalib.word.Word;
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.io.Serializable;
+import java.util.*;
+
+/**
+ * Stores information about local timers of a location.
+ *
+ * @param Input type for non-delaying inputs
+ * @param Output symbol type
+ */
+public class LocationTimerInfo implements Serializable {
+
+ private static final Logger logger = LoggerFactory.getLogger(LocationTimerInfo.class);
+
+ private final Map> timers; // name -> info
+
+ // Keep a list of timers sorted by their initial value. This lets us avoid redundant sort operations.
+ private final List> sortedTimers;
+
+ private final Word> prefix;
+
+ public LocationTimerInfo(Word> prefix) {
+ this.prefix = prefix;
+ this.timers = new HashMap<>();
+ this.sortedTimers = new ArrayList<>();
+ }
+
+ public Word> getPrefix() {
+ return prefix;
+ }
+
+ // ====================
+
+ /**
+ * Adds a local timer to this location.
+ *
+ */
+ public void addTimer(MealyTimerInfo timer) {
+ this.timers.put(timer.name(), timer);
+ this.sortedTimers.add(timer);
+ this.sortedTimers.sort(Comparator.comparingLong(MealyTimerInfo::initial));
+ }
+
+ public void removeTimer(String timerName) {
+ if (!this.timers.containsKey(timerName)) {
+ logger.warn("Attempted to remove an unknown timer.");
+ return;
+ }
+ MealyTimerInfo removedTimer = this.timers.remove(timerName);
+ this.sortedTimers.remove(removedTimer);
+ }
+
+ @Nullable
+ public MealyTimerInfo getTimerInfo(long initial) {
+ Optional