diff --git a/api/src/main/java/module-info.java b/api/src/main/java/module-info.java
index dadb03ec7..60bd01305 100644
--- a/api/src/main/java/module-info.java
+++ b/api/src/main/java/module-info.java
@@ -47,6 +47,7 @@
exports net.automatalib.automaton.fsa;
exports net.automatalib.automaton.graph;
exports net.automatalib.automaton.helper;
+ exports net.automatalib.automaton.mmlt;
exports net.automatalib.automaton.procedural;
exports net.automatalib.automaton.simple;
exports net.automatalib.automaton.transducer;
@@ -61,6 +62,7 @@
exports net.automatalib.graph.visualization;
exports net.automatalib.modelchecking;
exports net.automatalib.serialization;
+ exports net.automatalib.symbol.time;
exports net.automatalib.ts;
exports net.automatalib.ts.acceptor;
exports net.automatalib.ts.modal;
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/MMLT.java b/api/src/main/java/net/automatalib/automaton/mmlt/MMLT.java
new file mode 100644
index 000000000..6ce422131
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/MMLT.java
@@ -0,0 +1,101 @@
+package net.automatalib.automaton.mmlt;
+
+import java.util.List;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.automaton.UniversalDeterministicAutomaton;
+import net.automatalib.automaton.concept.InputAlphabetHolder;
+import net.automatalib.common.util.Triple;
+import net.automatalib.graph.Graph;
+import net.automatalib.graph.concept.GraphViewable;
+import net.automatalib.symbol.time.InputSymbol;
+import net.automatalib.symbol.time.SymbolicInput;
+import net.automatalib.symbol.time.TimerTimeoutSymbol;
+
+/**
+ * Base type for a Mealy Machine with Local Timers (MMLT).
+ *
+ * An MMLT extends Mealy machines with local timers. Each location can have multiple timers. A timer can only be active
+ * in its assigned location. All timers of a location reset when this location is entered from a different location or,
+ * in case of the initial location, if the location is entered for the first time. There are periodic and one-shot
+ * timers. Periodic timers reset themselves on timeout. They cannot cause a location change. One-shot timers can cause a
+ * location change. They reset all timers of the target location at timeout. A location can have arbitrarily many
+ * periodic timers and up to one one-shot timers. Timers are always reset to their initial value. The initial values
+ * must be chosen so that a periodic timer never times out at the same time as a one-shot timer (to preserve
+ * determinism). Multiple periodic timers may time out simultaneously. In this case, their outputs are combined using an
+ * AbstractSymbolCombiner.
+ *
+ * The timeout of a timer is modeled with a transition that has a {@link TimerTimeoutSymbol} as input. Other inputs are
+ * {@link InputSymbol non-delaying}. A non-delaying input that causes a self-loop can cause a local reset. Then, all
+ * timers of that location reset.
+ *
+ * Implementation note: this class resembles a "structural" view on the MMLT. For a semantic view with
+ * time-sensitive transductions, see the {@link #getSemantics()} method.
+ *
+ * @param
+ * Location type
+ * @param
+ * Input type for non-delaying inputs
+ * @param
+ * Output symbol type
+ */
+public interface MMLT extends UniversalDeterministicAutomaton,
+ InputAlphabetHolder,
+ GraphViewable {
+
+ /**
+ * Returns the symbol used for silent outputs.
+ *
+ * @return Silent output symbol
+ */
+ O getSilentOutput();
+
+ /**
+ * Multiple periodic timers may out simultaneously. Then, their outputs are combined using an SymbolCombiner. This
+ * method returns the combiner used for this model.
+ *
+ * @return symbol combiner used for this model.
+ */
+ SymbolCombiner getOutputCombiner();
+
+ /**
+ * Retrieves the non-delaying inputs for this automaton. Excludes timer timeout symbols. May be empty.
+ *
+ * @return Input alphabet
+ */
+ Alphabet getInputAlphabet();
+
+ /**
+ * Indicates if the provided input performs a local reset in the given location.
+ *
+ * @param location
+ * Location
+ * @param input
+ * Non-delaying input
+ *
+ * @return True if performing a local reset
+ */
+ boolean isLocalReset(S location, I input);
+
+ /**
+ * Returns the timers of the specified location sorted ascendingly by their initial time.
+ *
+ * @param location
+ * Location
+ *
+ * @return Sorted list of local timers. Empty if location has no timers.
+ */
+ List> getSortedTimers(S location);
+
+ /**
+ * Returns the semantics automaton that describes the behavior of this MMLT.
+ *
+ * @return Semantics automaton
+ */
+ MMLTSemantics getSemantics();
+
+ @Override
+ default Graph, O, S>> graphView() {
+ return new MMLTGraphView<>(this);
+ }
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/MMLTCreator.java b/api/src/main/java/net/automatalib/automaton/mmlt/MMLTCreator.java
new file mode 100644
index 000000000..053ada709
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/MMLTCreator.java
@@ -0,0 +1,30 @@
+/* Copyright (C) 2013-2025 TU Dortmund University
+ * This file is part of AutomataLib .
+ *
+ * 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 net.automatalib.automaton.mmlt;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.symbol.time.InputSymbol;
+
+@FunctionalInterface
+public interface MMLTCreator {
+
+ default A createMMLT(Alphabet alphabet, int numStatesHint, O silentOutput, SymbolCombiner outputCombiner) {
+ return createMMLT(alphabet, silentOutput, outputCombiner);
+ }
+
+ A createMMLT(Alphabet alphabet, O silentOutput, SymbolCombiner symbolCombiner);
+
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/MMLTGraphView.java b/api/src/main/java/net/automatalib/automaton/mmlt/MMLTGraphView.java
new file mode 100644
index 000000000..82551bfef
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/MMLTGraphView.java
@@ -0,0 +1,62 @@
+package net.automatalib.automaton.mmlt;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.List;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.automaton.visualization.MMLTVisualizationHelper;
+import net.automatalib.common.util.Triple;
+import net.automatalib.graph.Graph;
+import net.automatalib.symbol.time.InputSymbol;
+import net.automatalib.symbol.time.SymbolicInput;
+import net.automatalib.symbol.time.TimedInput;
+import net.automatalib.symbol.time.TimerTimeoutSymbol;
+import net.automatalib.visualization.VisualizationHelper;
+
+public class MMLTGraphView implements Graph, O, S>> {
+
+ private final MMLT mmlt;
+
+ public MMLTGraphView(MMLT mmlt) {
+ this.mmlt = mmlt;
+ }
+
+ @Override
+ public Collection, O, S>> getOutgoingEdges(S node) {
+
+ Alphabet alphabet = mmlt.getInputAlphabet();
+ List> timers = mmlt.getSortedTimers(node);
+
+ List, O, S>> result = new ArrayList<>(alphabet.size() + timers.size());
+
+ for (I i : alphabet) {
+ var t = mmlt.getTransition(node, i);
+ if (t != null) {
+ result.add(Triple.of(TimedInput.input(i), mmlt.getTransitionProperty(t), mmlt.getSuccessor(t)));
+ }
+ }
+
+ for (MealyTimerInfo t : timers) {
+ result.add(Triple.of(new TimerTimeoutSymbol<>(t.name()), t.output(), t.target()));
+
+ }
+
+ return result;
+ }
+
+ @Override
+ public S getTarget(Triple, O, S> edge) {
+ return edge.getThird();
+ }
+
+ @Override
+ public Collection getNodes() {
+ return mmlt.getStates();
+ }
+
+ @Override
+ public VisualizationHelper, O, S>> getVisualizationHelper() {
+ return new MMLTVisualizationHelper<>(mmlt, false, false);
+ }
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/MMLTSemantics.java b/api/src/main/java/net/automatalib/automaton/mmlt/MMLTSemantics.java
new file mode 100644
index 000000000..e214997c2
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/MMLTSemantics.java
@@ -0,0 +1,68 @@
+package net.automatalib.automaton.mmlt;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.symbol.time.TimedOutput;
+import net.automatalib.symbol.time.TimedInput;
+import net.automatalib.automaton.concept.InputAlphabetHolder;
+import net.automatalib.automaton.concept.SuffixOutput;
+import net.automatalib.symbol.time.TimeoutSymbol;
+import net.automatalib.ts.output.MealyTransitionSystem;
+import net.automatalib.word.Word;
+
+/**
+ * Defines the semantics of an MMLT.
+ *
+ * The semantics of an MMLT are defined with an associated Mealy machine. The states of this machine are
+ * LocalTimerMealyConfiguration objects. These represent tuples of an active location and the current timer values of
+ * this location. The inputs of the machine are non-delaying inputs, discrete time steps, and the symbolic input
+ * timeout, which causes a delay until the next timeout.
+ *
+ * The outputs of this machine are the outputs of the MMLT, extended with a delay. This delay is zero for all
+ * transitions, except for those with the input {@link TimeoutSymbol}.
+ *
+ * @param
+ * Location type
+ * @param
+ * Input type for non-delaying inputs
+ * @param
+ * Output type of the MMLT
+ */
+public interface MMLTSemantics
+ extends MealyTransitionSystem, TimedInput, T, TimedOutput>,
+ SuffixOutput, Word>>,
+ InputAlphabetHolder> {
+
+ /**
+ * Returns the input alphabet of the semantics automaton. This consists of all non-delaying inputs of the associated
+ * MMLT, as well as the time step symbol and the symbolic timeout symbol.
+ *
+ * @return Input alphabet
+ */
+ Alphabet> getInputAlphabet();
+
+ /**
+ * Returns the symbol used for silent outputs.
+ *
+ * @return Silent output symbol
+ */
+ TimedOutput getSilentOutput();
+
+ /**
+ * Retrieves the transition in the semantics automaton that has the provided input and source configuration.
+ *
+ * If the input is a sequence of time steps, the target of the transition is the configuration reached after
+ * executing all time steps. If the sequence counts more than one step, the sequence might trigger multiple
+ * timeouts. To avoid ambiguity, the transition output is set to null in this case. If the sequence comprises a
+ * single time step only, the output is either that of a timeout or silence.
+ *
+ * @param source
+ * Source configuration
+ * @param input
+ * Input symbol
+ * @param maxWaitingTime
+ * Maximum time steps to wait for a timeout
+ *
+ * @return Transition in semantics automaton
+ */
+ T getTransition(State source, TimedInput input, long maxWaitingTime);
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/MealyTimerInfo.java b/api/src/main/java/net/automatalib/automaton/mmlt/MealyTimerInfo.java
new file mode 100644
index 000000000..02edb7951
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/MealyTimerInfo.java
@@ -0,0 +1,94 @@
+package net.automatalib.automaton.mmlt;
+
+import java.util.Objects;
+
+/**
+ * Provides information about a timer that is stored in an MMLT.
+ *
+ * @param Output symbol type
+ */
+public class MealyTimerInfo {
+ /**
+ * Name of the timer
+ */
+ private final String name;
+
+ /**
+ * Initial value of the timer
+ */
+ private final long initial;
+
+ /**
+ * Symbol that the timer produces at timeout. Must not be silent.
+ */
+ private final O output;
+
+ /**
+ * True if the timer is periodic.
+ */
+ private boolean periodic;
+
+ private final S target;
+
+ public MealyTimerInfo(String name, long initial, O output, boolean periodic, S target) {
+ this.target = target;
+ if (initial <= 0) {
+ throw new IllegalArgumentException("Timer values must be greater than zero.");
+ }
+
+ this.name = name;
+ this.initial = initial;
+ this.output = output;
+ this.periodic = periodic;
+ }
+
+ public MealyTimerInfo(String name, long initial, O output, S target) {
+ this(name, initial, output, true, target);
+ }
+
+ public void setOneShot() {
+ this.periodic = false;
+ }
+
+ public String name() {
+ return name;
+ }
+
+ public long initial() {
+ return initial;
+ }
+
+ public boolean periodic() {
+ return this.periodic;
+ }
+
+ public O output() {
+ return output;
+ }
+
+ public S target() {
+ return target;
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (obj == this) return true;
+ if (obj == null || obj.getClass() != this.getClass()) return false;
+ var that = (MealyTimerInfo) obj;
+ return Objects.equals(this.name, that.name) &&
+ this.initial == that.initial &&
+ Objects.equals(this.output, that.output) &&
+ Objects.equals(this.target, that.target);
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(name, initial, output, target);
+ }
+
+ @Override
+ public String toString() {
+ return String.format("%s=%d/%s", name, initial, output);
+ }
+
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/MutableMMLT.java b/api/src/main/java/net/automatalib/automaton/mmlt/MutableMMLT.java
new file mode 100644
index 000000000..7b16a1f3c
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/MutableMMLT.java
@@ -0,0 +1,62 @@
+package net.automatalib.automaton.mmlt;
+
+import net.automatalib.automaton.MutableDeterministic;
+
+public interface MutableMMLT extends MMLT, MutableDeterministic {
+
+ /**
+ * Adds a new periodic timer to the provided location.
+ *
+ * Throws an error if a) the output is silent b) the initial value is less zero or less
+ * c) the initial value exceeds that of a one-shot timer (-> timer never expires)
+ * d) the timer will time out at the same time as a one-shot timer.
+ *
+ * @param location Location of the timer
+ * @param name Timer name
+ * @param initial Initial value
+ * @param output Output at timeout
+ */
+ void addPeriodicTimer(S location, String name, long initial, O output);
+
+ /**
+ * Adds a new one-shot timer to the provided location.
+ * Removes all timers of that location with higher initial value, as these can no longer time out.
+ *
+ * Throws an error if a) the output is silent b) the initial value is less zero or less
+ * c) the initial value exceeds that of a one-shot timer (-> timer never expires)
+ * d) the timer will time out at the same time as a periodic timer.
+ *
+ * @param location Location of the timer
+ * @param name Timer name
+ * @param initial Initial value
+ * @param output Output at timeout
+ */
+ void addOneShotTimer(S location, String name, long initial, O output, S target);
+
+ /**
+ * Removes the timer with the provided name.
+ * No effect if the location has no such timer.
+ *
+ * @param location Location of the timer
+ * @param timerName Name of the timer
+ */
+ void removeTimer(S location, String timerName);
+
+ /**
+ * Adds a local reset at the provided input in the provided location.
+ * Throws an error if the transition does not self-loop.
+ *
+ * @param location Source location
+ * @param input Input of the transition that should perform a local reset
+ */
+ void addLocalReset(S location, I input);
+
+ /**
+ * Removes a local reset at the provided input in the provided location.
+ * No effect if the input does not trigger a local reset.
+ *
+ * @param location Source location
+ * @param input Input of the transition that performs a local reset.
+ */
+ void removeLocalReset(S location, I input);
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/State.java b/api/src/main/java/net/automatalib/automaton/mmlt/State.java
new file mode 100644
index 000000000..2d7a8c33a
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/State.java
@@ -0,0 +1,214 @@
+package net.automatalib.automaton.mmlt;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+import java.util.*;
+
+/**
+ * A configuration, a.k.a., state of an MMLT. A configuration is a tuple of an active location and the values of its
+ * timers.
+ *
+ * @param
+ * Location type
+ * @param
+ * Output symbol type
+ */
+public final class State {
+
+ private final S location;
+
+ private final List> sortedTimers;
+ private final long[] timerValues;
+ private final long[] initialValues;
+ private final long minimumTimerValue;
+
+ private long entryDistance;
+
+ /**
+ * Initializes the entry configuration for the provided location, where all timers have their initial value.
+ *
+ * @param location
+ * Location
+ * @param sortedTimers
+ * Timers of the location, sorted by initial value.
+ */
+ public State(S location, List> sortedTimers) {
+ this.location = location;
+
+ this.sortedTimers = sortedTimers;
+
+ this.initialValues = new long[sortedTimers.size()];
+ this.timerValues = new long[sortedTimers.size()];
+ this.minimumTimerValue = (sortedTimers.isEmpty()) ? 0 : sortedTimers.get(0).initial();
+
+ for (int i = 0; i < sortedTimers.size(); i++) {
+ initialValues[i] = sortedTimers.get(i).initial();
+ timerValues[i] = initialValues[i]; // reset
+ }
+
+ this.entryDistance = 0;
+ }
+
+ private State(S location,
+ List> sortedTimers,
+ long[] timerValues,
+ long[] initialValues,
+ long entryDistance,
+ long minimumTimerValue) {
+ this.location = location;
+ this.sortedTimers = sortedTimers;
+
+ this.initialValues = initialValues;
+ this.minimumTimerValue = minimumTimerValue;
+ this.timerValues = Arrays.copyOf(timerValues, timerValues.length);
+ this.entryDistance = entryDistance;
+ }
+
+ /**
+ * Creates a copy of this configuration. The location, timers, prefix, and initialValue still point to the original
+ * instances. The current timer values are copied. Modifying these in the resulting object does not affect the
+ * original configuration.
+ */
+ public State copy() {
+ return new State<>(location, sortedTimers, timerValues, initialValues, entryDistance, minimumTimerValue);
+ }
+
+ public S getLocation() {
+ return location;
+ }
+
+ /**
+ * Returns the entry distance. This is the minimal number of time steps required to reach this configuration from
+ * the entry configuration.
+ *
+ * @return Entry distance
+ */
+ public long getEntryDistance() {
+ return entryDistance;
+ }
+
+ /**
+ * Indicates if this is the entry configuration of the location. A configuration is the entry configuration if all
+ * timers have their initial value.
+ *
+ * @return True if entry configuration.
+ */
+ public boolean isEntryConfig() {
+ return this.entryDistance == 0;
+ }
+
+ /**
+ * Indicates if this configuration is stable. A configuration is stable if its entry distance is less than the
+ * initial value of the timer with the lowest initial value of the location. If the location has no timers, its only
+ * configuration is its entry configuration, which is always stable.
+ *
+ * @return True if stable
+ */
+ public boolean isStableConfig() {
+ return this.entryDistance == 0 || this.entryDistance < minimumTimerValue;
+ }
+
+ /**
+ * Resets all timers to their initial values.
+ */
+ public void resetTimers() {
+ System.arraycopy(this.initialValues, 0, this.timerValues, 0, sortedTimers.size());
+ this.entryDistance = 0;
+ }
+
+ /**
+ * Returns all timers that time out in the least number of time steps.
+ */
+ @Nullable
+ public TimeoutPair getNextExpiringTimers() {
+ if (sortedTimers.isEmpty()) {
+ return null;
+ } else if (this.sortedTimers.size() == 1) {
+ // No need to collect timeouts - there is only one timer that can expire.
+ // The time to its timeout is its remaining value:
+ return new TimeoutPair<>(this.timerValues[0], Collections.singletonList(this.sortedTimers.get(0)));
+
+ } else {
+ // Multiple timers may time out at the same time.
+ // Get minimum distance to next timeout:
+ long minValue = Long.MAX_VALUE;
+ for (int i = 0; i < sortedTimers.size(); i++) {
+ if (timerValues[i] < minValue) {
+ minValue = timerValues[i];
+ }
+ }
+
+ assert minValue != Long.MAX_VALUE;
+
+ // Collect info of all timers that time out then:
+ List> expiringTimers = new ArrayList<>();
+ for (int i = 0; i < sortedTimers.size(); i++) {
+ if (timerValues[i] == minValue) {
+ expiringTimers.add(this.sortedTimers.get(i));
+ }
+ }
+
+ // Return timed-out timers:
+ return new TimeoutPair<>(minValue, expiringTimers);
+ }
+ }
+
+ /**
+ * Decreases all timer values by the specified amount. This amount must be at most the time to the next timeout. If
+ * this sets a timer to zero, this timer is immediately reset. to its initial value.
+ *
+ * @param delay
+ * Decrement
+ */
+ public void decrement(long delay) {
+ int timerResets = 0;
+ int oneShotResets = 0;
+ for (int i = 0; i < this.sortedTimers.size(); i++) {
+ long newValue = this.timerValues[i] - delay;
+
+ if (newValue < 0) {
+ throw new IllegalArgumentException("Can only advance to next timeout.");
+ } else if (newValue == 0) {
+ if (!sortedTimers.get(i).periodic()) {
+ oneShotResets += 1;
+ }
+
+ newValue = this.initialValues[i];
+ timerResets += 1;
+ }
+ this.timerValues[i] = newValue;
+ }
+
+ if (oneShotResets > 1) {throw new AssertionError();}
+ if (timerResets == this.sortedTimers.size() || oneShotResets == 1) {
+ // reset all timers -> back at entry config:
+ this.entryDistance = 0;
+ } else {
+ this.entryDistance += delay;
+ }
+ }
+
+ @Override
+ public boolean equals(Object o) {
+ if (o == null || getClass() != o.getClass()) {return false;}
+ State that = (State) o;
+ return minimumTimerValue == that.minimumTimerValue && entryDistance == that.entryDistance &&
+ Objects.equals(location, that.location) && Objects.equals(sortedTimers, that.sortedTimers) &&
+ Arrays.equals(timerValues, that.timerValues) && Arrays.equals(initialValues, that.initialValues);
+ }
+
+ @Override
+ public int hashCode() {
+ return Objects.hash(location,
+ sortedTimers,
+ Arrays.hashCode(timerValues),
+ Arrays.hashCode(initialValues),
+ minimumTimerValue,
+ entryDistance);
+ }
+
+ @Override
+ public String toString() {
+ return String.format("[%s,%d]", this.location, this.entryDistance);
+ }
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/SymbolCombiner.java b/api/src/main/java/net/automatalib/automaton/mmlt/SymbolCombiner.java
new file mode 100644
index 000000000..23ea44ac0
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/SymbolCombiner.java
@@ -0,0 +1,43 @@
+package net.automatalib.automaton.mmlt;
+
+import java.util.List;
+
+/**
+ * In an MMLT, multiple timeouts may occur simultaneously. We use these symbol combiners to combine their outputs
+ * deterministically.
+ *
+ * @param
+ * Symbol type
+ */
+public interface SymbolCombiner {
+
+ /**
+ * Indicates if the provided suffix is a combined suffix.
+ *
+ * @param symbol
+ * Symbol for testing
+ *
+ * @return True if combined suffix, false if not.
+ */
+ boolean isCombinedSymbol(U symbol);
+
+ /**
+ * Combines the provided symbols to a single suffix of same data type. Must be deterministic.
+ *
+ * @param symbols
+ * Provided symbols.
+ *
+ * @return Combined suffix
+ */
+ U combineSymbols(List symbols);
+
+ /**
+ * Attempts to separate the provided combined suffix into individual symbols.
+ *
+ * @param symbol
+ * Combined symbols
+ *
+ * @return Individual symbols
+ */
+ List separateSymbols(U symbol);
+}
diff --git a/api/src/main/java/net/automatalib/automaton/mmlt/TimeoutPair.java b/api/src/main/java/net/automatalib/automaton/mmlt/TimeoutPair.java
new file mode 100644
index 000000000..be967d5d9
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/mmlt/TimeoutPair.java
@@ -0,0 +1,23 @@
+package net.automatalib.automaton.mmlt;
+
+import java.util.List;
+
+/**
+ * Stores information about timers that expire after a given time from now.
+ *
+ * @param delay
+ * Offset to the next timeout
+ * @param timers
+ * Timers expiring simultaneously at next timeout
+ * @param
+ * Output suffix type
+ */
+public record TimeoutPair(long delay, List> timers) {
+
+ public boolean allPeriodic() {
+ if (timers.size() == 1) {
+ return timers.get(0).periodic();
+ }
+ return timers.stream().allMatch(MealyTimerInfo::periodic);
+ }
+}
diff --git a/api/src/main/java/net/automatalib/automaton/visualization/MMLTVisualizationHelper.java b/api/src/main/java/net/automatalib/automaton/visualization/MMLTVisualizationHelper.java
new file mode 100644
index 000000000..c5125dd8d
--- /dev/null
+++ b/api/src/main/java/net/automatalib/automaton/visualization/MMLTVisualizationHelper.java
@@ -0,0 +1,136 @@
+package net.automatalib.automaton.visualization;
+
+import java.util.Map;
+import java.util.Objects;
+import java.util.stream.Collectors;
+
+import net.automatalib.automaton.mmlt.MMLT;
+import net.automatalib.automaton.mmlt.MealyTimerInfo;
+import net.automatalib.common.util.Triple;
+import net.automatalib.symbol.time.InputSymbol;
+import net.automatalib.symbol.time.SymbolicInput;
+import net.automatalib.symbol.time.TimerTimeoutSymbol;
+import net.automatalib.visualization.DefaultVisualizationHelper;
+
+public class MMLTVisualizationHelper
+ extends DefaultVisualizationHelper, O, S>> {
+
+ private final MMLT automaton;
+ private final boolean colorEdges;
+ private final boolean includeResets;
+
+ /**
+ * Creates a new visualization helper for an MMLT. Allows edge coloring and explicit resets in transition labels for
+ * easier inspection.
+ *
+ * If you want to serialize the resulting file to graphviz, disable explicit resets. The parse does not know how to
+ * treat the reset information.
+ *
+ * @param automaton
+ * Automaton
+ * @param colorEdges
+ * If set, the transitions for local resets, periodic timers, and one-shot timers are colored differently.
+ * @param includeResets
+ * If set, each transition includes a list of timers that it resets.
+ */
+ public MMLTVisualizationHelper(MMLT automaton,
+ boolean colorEdges,
+ boolean includeResets) {
+ this.automaton = automaton;
+ this.colorEdges = colorEdges;
+ this.includeResets = includeResets;
+ }
+
+ @Override
+ public boolean getNodeProperties(S node, Map properties) {
+ super.getNodeProperties(node, properties);
+
+ if (Objects.equals(node, automaton.getInitialState())) {
+ properties.put(NodeAttrs.INITIAL, Boolean.TRUE.toString());
+ }
+
+ // Include timer assignments:
+ var localTimers = automaton.getSortedTimers(node);
+ if (!localTimers.isEmpty()) {
+ // Add local timer info:
+ String timers = localTimers.stream()
+ .map(t -> String.format("%s=%d", t.name(), t.initial()))
+ .sorted()
+ .collect(Collectors.joining(","));
+ properties.put(MMLTNodeAttrs.TIMERS, timers);
+ }
+
+ return true;
+ }
+
+ @Override
+ public boolean getEdgeProperties(S src, Triple, O, S> edge, S tgt, Map properties) {
+ super.getEdgeProperties(src, edge, tgt, properties);
+
+ final SymbolicInput input = edge.getFirst();
+
+ String label = String.format("%s / %s", input, edge.getSecond());
+
+ // Infer the label color + reset information for the transition:
+ String resetExtraInfo = "";
+ String resetInfo = "";
+ String edgeColor = "";
+ if (input instanceof TimerTimeoutSymbol ts) {
+ // Get info for corresponding timer:
+ var optTimer = automaton.getSortedTimers(src).stream()
+ .filter(t -> t.name().equals(ts.timer()))
+ .findFirst();
+ assert optTimer.isPresent();
+
+ if (optTimer.get().periodic()) {
+ // Periodic -> resets itself:
+ resetExtraInfo = String.format("%s↦%d", optTimer.get().name(), optTimer.get().initial());
+ edgeColor = "cornflowerblue";
+ } else {
+ // One-shot -> resets all in target:
+ resetExtraInfo = automaton.getSortedTimers(tgt)
+ .stream()
+ .map(t -> String.format("%s↦%d", t.name(), t.initial()))
+ .sorted()
+ .collect(Collectors.joining(","));
+ if (tgt.equals(src)) {
+ // If the target is another location, reset info can always be inferred from context.
+ // --> Only include if self-loop:
+ resetInfo = automaton.getSortedTimers(tgt).stream()
+ .map(MealyTimerInfo::name)
+ .sorted()
+ .collect(Collectors.joining(","));
+ }
+ edgeColor = "chartreuse3";
+ }
+ } else if (input instanceof InputSymbol ndi) {
+ if (src.equals(tgt) && automaton.isLocalReset(src, ndi.symbol())) {
+ // Self-loop + local reset -> resets all in target:
+ resetExtraInfo = automaton.getSortedTimers(tgt)
+ .stream()
+ .map(t -> String.format("%s↦%d", t.name(), t.initial()))
+ .sorted()
+ .collect(Collectors.joining(","));
+ resetInfo = automaton.getSortedTimers(tgt).stream()
+ .map(MealyTimerInfo::name)
+ .sorted()
+ .collect(Collectors.joining(","));
+ edgeColor = "orange";
+ }
+ }
+
+ if (this.colorEdges && !edgeColor.isBlank()) {
+ properties.put(EdgeAttrs.COLOR, edgeColor);
+ properties.put("fontcolor", edgeColor);
+ }
+ if (this.includeResets) {
+ label += " {" + resetExtraInfo + "}";
+ }
+ if (!resetInfo.isEmpty()) {
+ properties.put(MMLTEdgeAttrs.RESETS, resetInfo);
+ }
+ properties.put(EdgeAttrs.LABEL, label);
+
+ return true;
+ }
+}
diff --git a/api/src/main/java/net/automatalib/symbol/time/InputSymbol.java b/api/src/main/java/net/automatalib/symbol/time/InputSymbol.java
new file mode 100644
index 000000000..449e62974
--- /dev/null
+++ b/api/src/main/java/net/automatalib/symbol/time/InputSymbol.java
@@ -0,0 +1,19 @@
+package net.automatalib.symbol.time;
+
+import java.util.Objects;
+
+/**
+ * An input symbol that represents a direct action without any delay.
+ *
+ * @param symbol
+ * the symbolic action
+ * @param
+ * input symbol type
+ */
+public record InputSymbol(I symbol) implements TimedInput, SymbolicInput {
+
+ @Override
+ public String toString() {
+ return Objects.toString(symbol);
+ }
+}
diff --git a/api/src/main/java/net/automatalib/symbol/time/SymbolicInput.java b/api/src/main/java/net/automatalib/symbol/time/SymbolicInput.java
new file mode 100644
index 000000000..1f542d8b0
--- /dev/null
+++ b/api/src/main/java/net/automatalib/symbol/time/SymbolicInput.java
@@ -0,0 +1,11 @@
+package net.automatalib.symbol.time;
+
+import net.automatalib.automaton.mmlt.MMLT;
+
+/**
+ * Markup-interface for structural inputs currently used in {@link MMLT}s.
+ *
+ * @param
+ * input symbol type
+ */
+public sealed interface SymbolicInput permits InputSymbol, TimerTimeoutSymbol {}
diff --git a/api/src/main/java/net/automatalib/symbol/time/TimeStepSequence.java b/api/src/main/java/net/automatalib/symbol/time/TimeStepSequence.java
new file mode 100644
index 000000000..d2ed6ff5f
--- /dev/null
+++ b/api/src/main/java/net/automatalib/symbol/time/TimeStepSequence.java
@@ -0,0 +1,24 @@
+package net.automatalib.symbol.time;
+
+/**
+ * An input that represents multiple subsequent time steps.
+ *
+ * @param timeSteps
+ * the number of time steps this symbol should elapse
+ * @param
+ * input symbol type (of other timed symbols)
+ */
+public record TimeStepSequence(long timeSteps) implements TimedInput {
+
+ public TimeStepSequence {
+ if (timeSteps <= 0) {
+ throw new IllegalArgumentException("Timeout must be larger than zero.");
+ }
+ }
+
+ @Override
+ public String toString() {
+ return String.format("wait[%d]", this.timeSteps);
+ }
+
+}
diff --git a/api/src/main/java/net/automatalib/symbol/time/TimedInput.java b/api/src/main/java/net/automatalib/symbol/time/TimedInput.java
new file mode 100644
index 000000000..90cbebf7a
--- /dev/null
+++ b/api/src/main/java/net/automatalib/symbol/time/TimedInput.java
@@ -0,0 +1,59 @@
+package net.automatalib.symbol.time;
+
+import java.util.function.Supplier;
+
+import net.automatalib.automaton.mmlt.MMLTSemantics;
+import net.automatalib.word.Word;
+import net.automatalib.word.WordBuilder;
+
+/**
+ * Markup-interface for timing-sensitive inputs currently used in {@link MMLTSemantics}s. Contains utility methods for
+ * conveniently constructing instances of timed symbols.
+ *
+ * @param
+ * input symbol type
+ */
+public sealed interface TimedInput permits InputSymbol, TimeoutSymbol, TimeStepSequence {
+
+ static InputSymbol input(I symbol) {
+ return new InputSymbol<>(symbol);
+ }
+
+ @SafeVarargs
+ static Word> inputs(I... symbols) {
+ var wb = new WordBuilder>(symbols.length);
+ for (I symbol : symbols) {
+ wb.add(new InputSymbol<>(symbol));
+ }
+ return wb.toWord();
+ }
+
+ static TimeoutSymbol timeout() {
+ return new TimeoutSymbol<>();
+ }
+
+ static Word> timeouts(int i) {
+ return generate(i, TimeoutSymbol::new);
+ }
+
+ static TimeStepSequence step() {
+ return new TimeStepSequence<>(1);
+ }
+
+ static TimeStepSequence step(int i) {
+ return new TimeStepSequence<>(i);
+ }
+
+ static Word> steps(int i) {
+ return generate(i, () -> new TimeStepSequence<>(1));
+ }
+
+ private static Word generate(int i, Supplier supplier) {
+ var wb = new WordBuilder(i);
+ for (int j = 0; j < i; j++) {
+ wb.append(supplier.get());
+ }
+
+ return wb.toWord();
+ }
+}
diff --git a/api/src/main/java/net/automatalib/symbol/time/TimedOutput.java b/api/src/main/java/net/automatalib/symbol/time/TimedOutput.java
new file mode 100644
index 000000000..d5b17f331
--- /dev/null
+++ b/api/src/main/java/net/automatalib/symbol/time/TimedOutput.java
@@ -0,0 +1,39 @@
+package net.automatalib.symbol.time;
+
+import java.util.Objects;
+
+/**
+ * Output that may occur with some or no delay.
+ *
+ * @param symbol
+ * the output symbol
+ * @param delay
+ * the delay
+ * @param
+ * output symbol type
+ */
+public record TimedOutput(O symbol, long delay) {
+
+ public TimedOutput {
+ if (delay < 0) {
+ throw new IllegalArgumentException("Delay must not be negative.");
+ }
+ }
+
+ public TimedOutput(O symbol) {
+ this(symbol, 0);
+ }
+
+ public boolean isDelayed() {
+ return this.delay > 0;
+ }
+
+ @Override
+ public String toString() {
+ if (this.isDelayed()) {
+ return String.format("[%d]%s", this.delay, this.symbol);
+ }
+ return Objects.toString(this.symbol);
+ }
+
+}
diff --git a/api/src/main/java/net/automatalib/symbol/time/TimeoutSymbol.java b/api/src/main/java/net/automatalib/symbol/time/TimeoutSymbol.java
new file mode 100644
index 000000000..5f4c02b00
--- /dev/null
+++ b/api/src/main/java/net/automatalib/symbol/time/TimeoutSymbol.java
@@ -0,0 +1,16 @@
+package net.automatalib.symbol.time;
+
+/**
+ * An input that causes a delay until the next timeout.
+ *
+ * @param
+ * input symbol type (of other timed symbols)
+ */
+public record TimeoutSymbol() implements TimedInput {
+
+ @Override
+ public String toString() {
+ return "timeout";
+ }
+
+}
diff --git a/api/src/main/java/net/automatalib/symbol/time/TimerTimeoutSymbol.java b/api/src/main/java/net/automatalib/symbol/time/TimerTimeoutSymbol.java
new file mode 100644
index 000000000..a516a6eae
--- /dev/null
+++ b/api/src/main/java/net/automatalib/symbol/time/TimerTimeoutSymbol.java
@@ -0,0 +1,20 @@
+package net.automatalib.symbol.time;
+
+import net.automatalib.automaton.mmlt.MMLT;
+
+/**
+ * The timeout symbol of a timer currently used by {@link MMLT}s.
+ *
+ * @param timer
+ * the name of the timer
+ * @param
+ * input symbol type (of other timed symbols)
+ */
+public record TimerTimeoutSymbol(String timer) implements SymbolicInput {
+
+ @Override
+ public String toString() {
+ return String.format("to[%s]", this.timer);
+ }
+
+}
diff --git a/api/src/main/java/net/automatalib/visualization/VisualizationHelper.java b/api/src/main/java/net/automatalib/visualization/VisualizationHelper.java
index 0e779f200..9177e4fab 100644
--- a/api/src/main/java/net/automatalib/visualization/VisualizationHelper.java
+++ b/api/src/main/java/net/automatalib/visualization/VisualizationHelper.java
@@ -83,7 +83,7 @@ private CommonAttrs() {
}
}
- final class NodeAttrs extends CommonAttrs {
+ class NodeAttrs extends CommonAttrs {
public static final String SHAPE = "shape";
public static final String WIDTH = "width";
@@ -97,6 +97,15 @@ private NodeAttrs() {
}
}
+ final class MMLTNodeAttrs extends NodeAttrs {
+
+ public static final String TIMERS = "timers";
+
+ private MMLTNodeAttrs() {
+ // prevent instantiation
+ }
+ }
+
class EdgeAttrs extends CommonAttrs {
public static final String PENWIDTH = "penwidth";
@@ -166,4 +175,13 @@ private MTSEdgeAttrs() {
// prevent instantiation
}
}
+
+ final class MMLTEdgeAttrs extends NodeAttrs {
+
+ public static final String RESETS = "resets";
+
+ private MMLTEdgeAttrs() {
+ // prevent instantiation
+ }
+ }
}
diff --git a/core/src/main/java/module-info.java b/core/src/main/java/module-info.java
index c482544dd..cb0dc0b71 100644
--- a/core/src/main/java/module-info.java
+++ b/core/src/main/java/module-info.java
@@ -35,11 +35,13 @@
// annotations are 'provided'-scoped and do not need to be loaded at runtime
requires static org.checkerframework.checker.qual;
+ requires org.slf4j;
exports net.automatalib.alphabet.impl;
exports net.automatalib.automaton.base;
exports net.automatalib.automaton.fsa.impl;
exports net.automatalib.automaton.impl;
+ exports net.automatalib.automaton.mmlt.impl;
exports net.automatalib.automaton.procedural.impl;
exports net.automatalib.automaton.transducer.impl;
exports net.automatalib.automaton.transducer.probabilistic.impl;
diff --git a/core/src/main/java/net/automatalib/automaton/mmlt/impl/CompactMMLT.java b/core/src/main/java/net/automatalib/automaton/mmlt/impl/CompactMMLT.java
new file mode 100644
index 000000000..8ada1a3a3
--- /dev/null
+++ b/core/src/main/java/net/automatalib/automaton/mmlt/impl/CompactMMLT.java
@@ -0,0 +1,215 @@
+package net.automatalib.automaton.mmlt.impl;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.alphabet.impl.Alphabets;
+import net.automatalib.automaton.impl.CompactTransition;
+import net.automatalib.automaton.mmlt.MMLTGraphView;
+import net.automatalib.automaton.mmlt.MMLTSemantics;
+import net.automatalib.automaton.mmlt.MealyTimerInfo;
+import net.automatalib.automaton.mmlt.MutableMMLT;
+import net.automatalib.automaton.mmlt.SymbolCombiner;
+import net.automatalib.automaton.transducer.impl.CompactMealy;
+import net.automatalib.common.util.Triple;
+import net.automatalib.graph.Graph;
+import net.automatalib.symbol.time.InputSymbol;
+import net.automatalib.symbol.time.SymbolicInput;
+
+/**
+ * Implements a LocalTimerMealy that is mutable. The structure automaton is backed by a CompactMealy automaton.
+ *
+ * @param
+ * Input type for non-delaying inputs
+ * @param
+ * Output symbol type
+ */
+public class CompactMMLT extends CompactMealy implements MutableMMLT, O> {
+
+ private final Map>> sortedTimers; // location -> (sorted timers)
+ private final Map> resets; // location -> inputs (that reset all timers)
+
+ private final O silentOutput;
+ private final SymbolCombiner outputCombiner;
+
+ /**
+ * Initializes a new CompactLocalTimerMealy.
+ *
+ * @param nonDelayingInputs
+ * Non-delaying inputs used by this MMLT.
+ * @param silentOutput
+ * The silent output used by this MMLT.
+ * @param outputCombiner
+ * The combiner function for simultaneous timeouts of periodic timers.
+ */
+ public CompactMMLT(Alphabet nonDelayingInputs, O silentOutput, SymbolCombiner outputCombiner) {
+ this(nonDelayingInputs, DEFAULT_INIT_CAPACITY, silentOutput, outputCombiner);
+ }
+
+ public CompactMMLT(Alphabet nonDelayingInputs, int sizeHint, O silentOutput, SymbolCombiner outputCombiner) {
+ super(nonDelayingInputs, sizeHint);
+
+ this.sortedTimers = new HashMap<>();
+ this.resets = new HashMap<>();
+
+ this.silentOutput = silentOutput;
+ this.outputCombiner = outputCombiner;
+ }
+
+ @Override
+ public O getSilentOutput() {
+ return this.silentOutput;
+ }
+
+ @Override
+ public SymbolCombiner getOutputCombiner() {
+ return this.outputCombiner;
+ }
+
+ @Override
+ public boolean isLocalReset(Integer location, I input) {
+ return this.resets.getOrDefault(location, Collections.emptySet()).contains(input);
+ }
+
+ @Override
+ public List> getSortedTimers(Integer location) {
+ return Collections.unmodifiableList(this.sortedTimers.getOrDefault(location, Collections.emptyList()));
+ }
+
+ @Override
+ public MMLTSemantics getSemantics() {
+ return new CompactMMLTSemantics<>(this);
+ }
+
+ private void ensureThatCanAddTimer(List> timers,
+ String name,
+ long initial,
+ O output,
+ boolean periodic) {
+ if (output.equals(this.silentOutput)) {
+ throw new IllegalArgumentException(String.format("Provided silent output for timer '%s'.", name));
+ }
+
+ // Verify that the timer name is unique:
+ if (timers.stream().anyMatch(t -> t.name().equals(name))) {
+ throw new IllegalArgumentException(String.format("Location already has a timer of the name '%s'.", name));
+ }
+
+ // Ensure that our new timer can time out AND that its timeouts do not coincide with that of an existing one-shot timer:
+ var oldOneShot = timers.stream().filter(t -> !t.periodic()).findFirst();
+ if (oldOneShot.isPresent()) {
+ if (initial > oldOneShot.get().initial()) {
+ throw new IllegalArgumentException(String.format(
+ "The initial value %d of '%s' exceeds that of a one-shot timer; will never time out.",
+ initial,
+ name));
+ }
+ if (periodic && (oldOneShot.get().initial() % initial == 0)) {
+ // Our new periodic timer will time out at the same time as the existing one-shot timer.
+ // This makes the model non-deterministic and is not allowed:
+ throw new IllegalArgumentException(String.format(
+ "The timer '%s' times out at the same time as a one-shot timer (%d).",
+ name,
+ initial));
+ }
+ }
+ if (!periodic) {
+ // Our new one-shot timer is the one-shot timer with the highest initial value (or the only one).
+ // Check that no timer with a lower initial value will time out at the same time:
+ for (var timer : timers) {
+ if (timer.initial() <= initial && initial % timer.initial() == 0) {
+ throw new IllegalArgumentException(String.format(
+ "The existing timer '%s' times out at the same time as the new one-shot timer (%d).",
+ timer.name(),
+ initial));
+ }
+ }
+ }
+ }
+
+ @Override
+ public void addPeriodicTimer(Integer location, String name, long initial, O output) {
+ this.sortedTimers.putIfAbsent(location, new ArrayList<>());
+ var localTimers = this.sortedTimers.get(location);
+
+ ensureThatCanAddTimer(localTimers, name, initial, output, true);
+ localTimers.add(new MealyTimerInfo<>(name, initial, output, true, location));
+ localTimers.sort(Comparator.comparingLong(MealyTimerInfo::initial));
+
+ // Add self-looping transition:
+// TimerTimeoutSymbol newTimerSymbol = new TimerTimeoutSymbol<>(name);
+// this.automaton.addAlphabetSymbol(newTimerSymbol);
+// automaton.addTransition(location, newTimerSymbol, location, output);
+ }
+
+ @Override
+ public void addOneShotTimer(Integer location, String name, long initial, O output, Integer target) {
+ this.sortedTimers.putIfAbsent(location, new ArrayList<>());
+ var localTimers = this.sortedTimers.get(location);
+
+ ensureThatCanAddTimer(localTimers, name, initial, output, false);
+ localTimers.add(new MealyTimerInfo<>(name, initial, output, false, target));
+ localTimers.sort(Comparator.comparingLong(MealyTimerInfo::initial));
+
+ // Add transition with location change:
+// TimerTimeoutSymbol newTimerSymbol = new TimerTimeoutSymbol<>(name);
+// this.automaton.addAlphabetSymbol(newTimerSymbol);
+// automaton.addTransition(location, newTimerSymbol, target, output);
+
+ // Remove all timers with higher initial value, as these can no longer time out:
+ localTimers.removeIf(t -> t.initial() > initial);
+ }
+
+ @Override
+ public void removeTimer(Integer location, String timerName) {
+ var localTimers = this.sortedTimers.get(location);
+ if (localTimers == null) {
+ return;
+ }
+
+ localTimers.removeIf(t -> t.name().equals(timerName));
+// automaton.removeAllTransitions(location, new TimerTimeoutSymbol<>(timerName));
+ }
+
+ @Override
+ public void addLocalReset(Integer location, I input) {
+ // Ensure that input causes self-loop:
+ var target = this.getSuccessor(location, input);
+ if (target == null || !target.equals(location)) {
+ throw new IllegalArgumentException("Provided input is not defined or does not trigger a self-loop.");
+ }
+
+ resets.putIfAbsent(location, new HashSet<>());
+ resets.get(location).add(input);
+ }
+
+ @Override
+ public void removeLocalReset(Integer location, I input) {
+ var localResets = resets.get(location);
+ if (localResets == null) {
+ return;
+ }
+
+ localResets.remove(input);
+ }
+
+ @Override
+ public void clear() {
+ super.clear();
+ this.sortedTimers.clear();
+ this.resets.clear();
+ }
+
+ @Override
+ public Graph, O, Integer>> graphView() {
+ return new MMLTGraphView<>(this);
+ }
+}
diff --git a/core/src/main/java/net/automatalib/automaton/mmlt/impl/CompactMMLTSemantics.java b/core/src/main/java/net/automatalib/automaton/mmlt/impl/CompactMMLTSemantics.java
new file mode 100644
index 000000000..b8e337b73
--- /dev/null
+++ b/core/src/main/java/net/automatalib/automaton/mmlt/impl/CompactMMLTSemantics.java
@@ -0,0 +1,220 @@
+package net.automatalib.automaton.mmlt.impl;
+
+import java.util.List;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.alphabet.impl.GrowingMapAlphabet;
+import net.automatalib.automaton.concept.Output;
+import net.automatalib.automaton.mmlt.MMLT;
+import net.automatalib.automaton.mmlt.MMLTSemantics;
+import net.automatalib.automaton.mmlt.MealyTimerInfo;
+import net.automatalib.automaton.mmlt.State;
+import net.automatalib.automaton.transducer.impl.MealyTransition;
+import net.automatalib.symbol.time.InputSymbol;
+import net.automatalib.symbol.time.TimeStepSequence;
+import net.automatalib.symbol.time.TimedInput;
+import net.automatalib.symbol.time.TimedOutput;
+import net.automatalib.symbol.time.TimeoutSymbol;
+import net.automatalib.word.Word;
+import net.automatalib.word.WordBuilder;
+import org.checkerframework.checker.nullness.qual.NonNull;
+
+/**
+ * Defines the semantics of an MMLT.
+ *
+ * The semantics of an MMLT are defined with an associated Mealy machine. The states of this machine are
+ * LocalTimerMealyConfiguration objects. These represent tuples of an active location and the current timer values of
+ * this location. The inputs of the machine are non-delaying inputs, discrete time steps, and the symbolic input
+ * timeout, which causes a delay until the next timeout.
+ *
+ * The outputs of this machine are the outputs of the MMLT, extended with a delay. This delay is zero for all
+ * transitions, except for those with the input timeout.
+ *
+ * @param
+ * Location type
+ * @param
+ * Input type for non-delaying inputs
+ * @param
+ * Output type of the MMLT
+ */
+public class CompactMMLTSemantics
+ implements MMLTSemantics, TimedOutput>, O> {
+
+ private final State initialConfiguration;
+ private final MMLT model;
+
+ private final Alphabet> alphabet;
+ private final TimedOutput silentOutput;
+
+ public CompactMMLTSemantics(MMLT model) {
+ this.model = model;
+
+ var initialLocation = model.getInitialState();
+ this.initialConfiguration = new State<>(initialLocation, model.getSortedTimers(initialLocation));
+
+ this.alphabet = new GrowingMapAlphabet<>(model.getInputAlphabet().stream().map(TimedInput::input).toList());
+ this.alphabet.add(TimedInput.timeout());
+ this.alphabet.add(TimedInput.step());
+
+ this.silentOutput = new TimedOutput<>(model.getSilentOutput());
+ }
+
+ @Override
+ public Alphabet> getInputAlphabet() {
+ return alphabet;
+ }
+
+ @Override
+ public TimedOutput getSilentOutput() {
+ return this.silentOutput;
+ }
+
+ @Override
+ public State getInitialState() {
+ return this.initialConfiguration;
+ }
+
+ @Override
+ public Word> computeSuffixOutput(Iterable> prefix,
+ Iterable> suffix) {
+ WordBuilder> wbOutput = Output.getBuilderFor(suffix);
+ var currentConfiguration = getState(prefix);
+ for (var sym : suffix) {
+ var trans = getTransition(currentConfiguration, sym);
+ currentConfiguration = trans.getSuccessor();
+
+ if (trans.getOutput() == null) {
+ throw new IllegalArgumentException(
+ "Cannot use time step sequences in suffix that have more than one symbol.");
+ }
+ wbOutput.append(trans.getOutput());
+ }
+
+ return wbOutput.toWord();
+ }
+
+ @Override
+ public @NonNull MealyTransition, TimedOutput> getTransition(State source, TimedInput input) {
+ return getTransition(source, input, Long.MAX_VALUE);
+ }
+
+ @Override
+ public @NonNull MealyTransition, TimedOutput> getTransition(State source,
+ TimedInput input,
+ long maxWaitingTime) {
+ var sourceCopy = source.copy(); // we do not want to modify values of the source configuration
+
+ if (input instanceof InputSymbol ndi) {
+ return getTransition(sourceCopy, ndi);
+ } else if (input instanceof TimeoutSymbol) {
+ return getTimeoutTransition(sourceCopy, maxWaitingTime);
+ } else if (input instanceof TimeStepSequence ts) {
+ // Per step, we can advance at most by the time to the next timeout:
+ var currentConfig = sourceCopy;
+ TimedOutput lastOutput = null;
+ long remainingTime = ts.timeSteps();
+ while (remainingTime > 0) {
+ var nextTimeoutTrans = getTimeoutTransition(currentConfig, remainingTime);
+ lastOutput = nextTimeoutTrans.getOutput();
+ if (nextTimeoutTrans.getOutput().equals(this.getSilentOutput())) {
+ // No timer will expire during remaining waiting time:
+ break;
+ } else {
+ remainingTime -= nextTimeoutTrans.getOutput().delay();
+ currentConfig = nextTimeoutTrans.getSuccessor();
+ }
+ }
+
+ if (ts.timeSteps() > 1) {
+ lastOutput = null; // ignore multiple outputs
+ } else {
+ // Output for single time step includes no delay by definition:
+ lastOutput = new TimedOutput<>(lastOutput.symbol());
+ }
+
+ // Return final target + output:
+ return new MealyTransition<>(currentConfig, lastOutput);
+ } else {
+ throw new IllegalArgumentException("Unknown input symbol type");
+ }
+ }
+
+ @Override
+ public TimedOutput getTransitionOutput(MealyTransition, TimedOutput> transition) {
+ return transition.getOutput();
+ }
+
+ @Override
+ public State getSuccessor(MealyTransition, TimedOutput> transition) {
+ return transition.getSuccessor();
+ }
+
+ private MealyTransition, TimedOutput> getTimeoutTransition(State source, long maxWaitingTime) {
+ State target;
+ TimedOutput output;
+
+ var nextTimeouts = source.getNextExpiringTimers();
+ if (nextTimeouts == null) {
+ // no timers:
+ output = this.getSilentOutput();
+ target = source;
+ } else if (nextTimeouts.delay() > maxWaitingTime) {
+ // timers, but too far away:
+ target = source;
+ target.decrement(maxWaitingTime);
+ output = this.getSilentOutput();
+ } else {
+ if (nextTimeouts.allPeriodic()) {
+ target = source;
+ target.decrement(nextTimeouts.delay());
+ } else {
+ // query target + update configuration:
+ assert nextTimeouts.timers().size() == 1;
+ var timer = nextTimeouts.timers().get(0);
+ var successor = timer.target();
+
+ target = new State<>(successor, model.getSortedTimers(successor));
+ target.resetTimers();
+ }
+
+ // Create combined output:
+ if (nextTimeouts.timers().size() == 1) {
+ output = new TimedOutput<>(nextTimeouts.timers().get(0).output(), nextTimeouts.delay());
+ } else {
+ List outputs = nextTimeouts.timers().stream().map(MealyTimerInfo::output).toList();
+ O combinedOutput = model.getOutputCombiner().combineSymbols(outputs);
+ output = new TimedOutput<>(combinedOutput, nextTimeouts.delay());
+ }
+ }
+
+ return new MealyTransition<>(target, output);
+ }
+
+ private MealyTransition, TimedOutput> getTransition(State source, InputSymbol input) {
+ State target;
+ TimedOutput output;
+
+ var trans = model.getTransition(source.getLocation(), input.symbol());
+ if (trans == null) { // silent self-loop
+ target = source;
+ output = this.getSilentOutput();
+ } else {
+ // Identify successor configuration:
+ S succ = model.getSuccessor(trans);
+ if (!succ.equals(source.getLocation())) {
+ // Change to a different location resets all timers in target:
+ target = new State<>(succ, model.getSortedTimers(succ));
+ target.resetTimers();
+ } else if (model.isLocalReset(source.getLocation(), input.symbol())) {
+ target = source;
+ target.resetTimers();
+ } else {
+ target = source;
+ }
+ output = new TimedOutput<>(model.getTransitionProperty(trans));
+ }
+
+ // Return output:
+ return new MealyTransition<>(target, output);
+ }
+}
diff --git a/core/src/main/java/net/automatalib/automaton/mmlt/impl/ReducedMMLTSemantics.java b/core/src/main/java/net/automatalib/automaton/mmlt/impl/ReducedMMLTSemantics.java
new file mode 100644
index 000000000..bd3b52a7d
--- /dev/null
+++ b/core/src/main/java/net/automatalib/automaton/mmlt/impl/ReducedMMLTSemantics.java
@@ -0,0 +1,186 @@
+package net.automatalib.automaton.mmlt.impl;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.symbol.time.TimedInput;
+import net.automatalib.symbol.time.TimedOutput;
+import net.automatalib.symbol.time.TimeoutSymbol;
+import net.automatalib.automaton.mmlt.MMLT;
+import net.automatalib.automaton.mmlt.State;
+import net.automatalib.automaton.mmlt.MMLTSemantics;
+import net.automatalib.automaton.transducer.impl.CompactMealy;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+/**
+ * Provides a reduced version of the semantics automaton of an MMLT.
+ * This reduced version retains all configurations that can be reached by timeouts and non-delaying inputs.
+ * It omits configurations that can only be reached by at least two subsequent time steps.
+ *
+ * The resulting automaton suffices to check the equivalence of two MMLTs.
+ * However, as the timeStep-transition is undefined in some configurations,
+ * the automaton cannot execute any sequence of inputs that can be executed on an MMLT.
+ *
+ * @param Location type
+ * @param Input type for non-delaying inputs
+ * @param Output symbol type
+ */
+public class ReducedMMLTSemantics extends CompactMealy, TimedOutput> {
+
+ private final static Logger logger = LoggerFactory.getLogger(ReducedMMLTSemantics.class);
+
+ private final Map, Integer> stateMap;
+
+ private ReducedMMLTSemantics(Alphabet> alphabet) {
+ super(alphabet);
+ this.stateMap = new HashMap<>();
+ }
+
+ public static ReducedMMLTSemantics forLocalTimerMealy(MMLT automaton) {
+ return forLocalTimerMealy(automaton, automaton.getSemantics());
+ }
+
+ private static ReducedMMLTSemantics forLocalTimerMealy(MMLT automaton, MMLTSemantics semantics) {
+ // Create alphabet for expanded form:
+ var alphabet = semantics.getInputAlphabet();
+
+ ReducedMMLTSemantics mealy = new ReducedMMLTSemantics<>(alphabet);
+
+ // 1a: Add all configurations that can be reached via timeouts/non-delaying inputs, or are at least one time
+ // step away from these configurations:
+ for (var loc : automaton.getStates()) {
+ getRelevantConfigurations(loc, automaton, semantics)
+ .forEach(c -> mealy.stateMap.put(c, mealy.addState()));
+ }
+
+ // 1b: Mark initial state:
+ var initialConfig = semantics.getInitialState();
+ mealy.setInitialState(mealy.stateMap.get(initialConfig));
+
+ // 2. Add transitions:
+ for (var config : mealy.stateMap.keySet()) {
+ var sourceState = mealy.stateMap.get(config);
+
+ for (var sym : alphabet) {
+ var trans = semantics.getTransition(config, sym);
+ var output = semantics.getTransitionOutput(trans);
+
+ // Try to find matching state. If not found, leave undefined:
+ int targetId = mealy.stateMap.getOrDefault(semantics.getSuccessor(trans), -1);
+ if (targetId != -1) {
+ mealy.addTransition(sourceState, sym, targetId, output);
+ }
+ }
+ }
+
+ logger.debug("Expanded from {} locations to {} states.",
+ automaton.getStates().size(), mealy.size());
+
+ return mealy;
+ }
+
+ /**
+ * Retrieves a list of configurations of the provided location
+ * that can be reached via timeouts, and those that are at most one time step away from these.
+ *
+ * @param Location type
+ * @param location Considered location
+ * @param automaton MMLT
+ * @return List of the relevant configurations of the location
+ */
+ private static List> getRelevantConfigurations(S location,
+ MMLT automaton,
+ MMLTSemantics semantics) {
+
+ List> configurations = new ArrayList<>();
+
+ State currentConfiguration = new State<>(location, automaton.getSortedTimers(location));
+ configurations.add(currentConfiguration);
+
+ // Enumerate all timeouts, until we change to a different location or re-enter the entry configuration
+ // of this location:
+ while (true) {
+ // Wait for next timeout:
+ var trans = semantics.getTransition(currentConfiguration, new TimeoutSymbol<>());
+ var output = semantics.getTransitionOutput(trans);
+ var target = semantics.getSuccessor(trans);
+ if (output.equals(semantics.getSilentOutput())) {
+ break; // no timeout
+ }
+
+ if (output.delay() > 1) {
+ // More than one time unit away -> add 1-step successor config.
+ // If one time unit away, the successor is already in our list.
+ var newGapConfig = currentConfiguration.copy();
+ newGapConfig.decrement(1);
+ configurations.add(newGapConfig);
+ }
+
+ if (target.isEntryConfig()) {
+ break; // location change OR repeating behavior
+ }
+ configurations.add(target);
+ currentConfiguration = target;
+ }
+ return configurations;
+ }
+
+
+ /**
+ * Returns the state that represents the provided configuration.
+ *
+ * If the configuration is not included and allowApproximate is set,
+ * the closest configuration of the same location (with a smaller entry distance)
+ * will be returned. If allowApproximate is not set, an error is thrown.
+ *
+ * @param configuration Provided configuration
+ * @param allowApproximate If set, the closest matching state is returned if the configuration is not part of the reduced automaton
+ * @return Corresponding state in the reduced automaton
+ */
+ public Integer getStateForConfiguration(State configuration, boolean allowApproximate) {
+
+ State closestMatch = null;
+
+ for (var cfg : stateMap.keySet()) {
+ if (!cfg.getLocation().equals(configuration.getLocation()) ||
+ cfg.getEntryDistance() > configuration.getEntryDistance()) {
+ continue;
+ }
+
+ if (cfg.getEntryDistance() == configuration.getEntryDistance()) {
+ // Perfect match:
+ return stateMap.get(cfg);
+ }
+
+ if (closestMatch == null || cfg.getEntryDistance() > closestMatch.getEntryDistance()) {
+ // Closer than previous candidate:
+ closestMatch = cfg;
+ }
+ }
+
+ if (closestMatch == null || !allowApproximate) {
+ throw new IllegalStateException("Could not find corresponding configuration in expanded form.");
+ }
+
+ return stateMap.get(closestMatch);
+ }
+
+ /**
+ * Returns the configuration that represents the provided state.
+ * Throws an error if the state is not part of the reduced automaton.
+ *
+ * @param state Considered state
+ * @return Corresponding configuration
+ */
+ public State getConfigurationForState(int state) {
+ return this.stateMap.entrySet().stream()
+ .filter(e -> e.getValue() == state)
+ .map(Map.Entry::getKey)
+ .findFirst()
+ .orElseThrow(() -> new IllegalStateException("Could not find corresponding configuration in expanded form."));
+ }
+}
diff --git a/core/src/main/java/net/automatalib/automaton/mmlt/impl/StringSymbolCombiner.java b/core/src/main/java/net/automatalib/automaton/mmlt/impl/StringSymbolCombiner.java
new file mode 100644
index 000000000..aa5472517
--- /dev/null
+++ b/core/src/main/java/net/automatalib/automaton/mmlt/impl/StringSymbolCombiner.java
@@ -0,0 +1,58 @@
+package net.automatalib.automaton.mmlt.impl;
+
+import net.automatalib.automaton.mmlt.SymbolCombiner;
+
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+/**
+ * Combines multiple String outputs by concatenating them and using a pipe as separator.
+ */
+public class StringSymbolCombiner implements SymbolCombiner {
+
+ private static final StringSymbolCombiner combiner = new StringSymbolCombiner();
+
+ public static StringSymbolCombiner getInstance() {
+ return combiner;
+ }
+
+ private StringSymbolCombiner() {}
+
+ @Override
+ public boolean isCombinedSymbol(String symbol) {
+ return symbol.contains("|") && symbol.length() > 1;
+ }
+
+ @Override
+ public String combineSymbols(List symbols) {
+
+ // Break all inputs (if needed) + put the results in a set:
+ Set expandedSymbols = new HashSet<>();
+ for (var sym : symbols) {
+ if (sym.equals("|")) {
+ throw new IllegalArgumentException("The output | is reserved as delimiter.");
+ }
+
+ if (this.isCombinedSymbol(sym)) {
+ expandedSymbols.addAll(this.separateSymbols(sym));
+ } else {
+ expandedSymbols.add(sym);
+ }
+ }
+
+ // Sort the symbols + separate with pipe:
+ return expandedSymbols.stream().sorted().collect(Collectors.joining("|"));
+ }
+
+ @Override
+ public List separateSymbols(String symbol) {
+ if (!this.isCombinedSymbol(symbol)) {
+ return List.of(symbol);
+ }
+
+ return Arrays.stream(symbol.split("\\|")).distinct().sorted().toList();
+ }
+}
diff --git a/core/src/test/java/net/automatalib/automaton/mmlt/impl/MMLTTests.java b/core/src/test/java/net/automatalib/automaton/mmlt/impl/MMLTTests.java
new file mode 100644
index 000000000..ddad3494b
--- /dev/null
+++ b/core/src/test/java/net/automatalib/automaton/mmlt/impl/MMLTTests.java
@@ -0,0 +1,198 @@
+package net.automatalib.automaton.mmlt.impl;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Random;
+
+import net.automatalib.alphabet.impl.Alphabets;
+import net.automatalib.symbol.time.InputSymbol;
+import net.automatalib.symbol.time.TimeStepSequence;
+import net.automatalib.symbol.time.TimedInput;
+import net.automatalib.symbol.time.TimeoutSymbol;
+import net.automatalib.word.Word;
+import org.testng.Assert;
+import org.testng.annotations.Test;
+
+public class MMLTTests {
+
+ public CompactMMLT buildBaseModel() {
+ var alphabet = Alphabets.fromArray("p1", "p2", "abort", "collect");
+ var model = new CompactMMLT<>(alphabet, "void", StringSymbolCombiner.getInstance());
+
+ var s0 = model.addState();
+ var s1 = model.addState();
+ var s2 = model.addState();
+ var s3 = model.addState();
+
+ model.setInitialState(s0);
+
+ model.addTransition(s0, "p1", s1, "go");
+ model.addTransition(s1, "abort", s1, "ok");
+ model.addLocalReset(s1, "abort");
+
+ model.addPeriodicTimer(s1, "a", 3, "part");
+ model.addPeriodicTimer(s1, "b", 6, "noise");
+ model.addOneShotTimer(s1, "c", 40, "done", s3);
+
+ model.addTransition(s0, "p2", s2, "go");
+ model.addTransition(s2, "abort", s3, "void");
+ model.addOneShotTimer(s2, "d", 4, "done", s3);
+
+ model.addTransition(s3, "collect", s0, "void");
+
+ return model;
+ }
+
+ private static List generateRandomWords(int count, int wordLength) {
+ Random r = new Random(100);
+ List words = new ArrayList<>();
+ for (int j = 0; j < count; j++) {
+ StringBuilder sb = new StringBuilder(wordLength);
+ for (int i = 0; i < wordLength; i++) {
+ char tmp = (char) ('a' + r.nextInt('z' - 'a'));
+ sb.append(tmp);
+ }
+ words.add(sb.toString());
+ }
+ return words;
+ }
+
+ @Test
+ public void testStringCombiner() {
+ var combiner = StringSymbolCombiner.getInstance();
+ var words = generateRandomWords(100, 10);
+
+ var combined = combiner.combineSymbols(words);
+ Assert.assertTrue(combiner.isCombinedSymbol(combined));
+ var separated = combiner.separateSymbols(combined);
+
+ Assert.assertEquals(words.stream().sorted().toList(), separated.stream().sorted().toList());
+
+ // Tests words with an absent output:
+ Assert.assertThrows(IllegalArgumentException.class, () -> combiner.combineSymbols(List.of("|", "d|c")));
+
+ var combinedAbsent = combiner.combineSymbols(List.of("a|", "d|c"));
+ Assert.assertEquals(combinedAbsent, "a|c|d");
+
+ // Now test words that contain a pipe:
+ var combinedPipe = combiner.combineSymbols(List.of("b|a", "d|c"));
+ Assert.assertEquals(combinedPipe, "a|b|c|d");
+
+ // Test words with duplicate characters:
+ var combinedDupes = combiner.combineSymbols(List.of("b|a", "c|a"));
+ var separateDupes = combiner.separateSymbols(combinedDupes);
+ Assert.assertEquals(combinedDupes, "a|b|c");
+ Assert.assertEquals(List.of("a", "b", "c"), separateDupes);
+ }
+
+ @Test
+ public void testConfigurationProperties() {
+ var model = buildBaseModel();
+
+ var nonStableConfig = model.getSemantics()
+ .getState(Word.fromSymbols(new InputSymbol<>("p1"),
+ new TimeStepSequence<>(12)));
+ Assert.assertNotNull(nonStableConfig);
+ Assert.assertFalse(nonStableConfig.isStableConfig());
+ Assert.assertFalse(nonStableConfig.isEntryConfig());
+ Assert.assertEquals(nonStableConfig.getEntryDistance(), 12);
+ Assert.assertEquals(nonStableConfig.getLocation().intValue(), 1);
+
+ var stableConfig = model.getSemantics()
+ .getState(Word.fromSymbols(new InputSymbol<>("p1"), new TimeStepSequence<>(2)));
+ Assert.assertNotNull(stableConfig);
+ Assert.assertTrue(stableConfig.isStableConfig());
+ Assert.assertFalse(stableConfig.isEntryConfig());
+ Assert.assertEquals(stableConfig.getEntryDistance(), 2);
+ Assert.assertEquals(stableConfig.getLocation().intValue(), 1);
+ }
+
+ @Test
+ public void testReducedSemanticsIncludedConfiguration() {
+ var automaton = buildBaseModel();
+ var reducedSemanticsModel = ReducedMMLTSemantics.forLocalTimerMealy(automaton);
+ Assert.assertEquals(reducedSemanticsModel.size(), 31);
+
+ // Reachable in both automata:
+ Word> includedConfigPrefix =
+ Word.fromSymbols(new InputSymbol<>("p1"),
+ new TimeoutSymbol<>(),
+ new TimeoutSymbol<>(),
+ new TimeoutSymbol<>(),
+ new TimeoutSymbol<>(),
+ new TimeoutSymbol<>(),
+ new TimeoutSymbol<>(),
+ TimedInput.step());
+ var includedConfig = automaton.getSemantics().getState(includedConfigPrefix);
+
+ // Verify that the reached states are identical:
+ var expectedState = reducedSemanticsModel.getStateForConfiguration(includedConfig, false);
+ var reachedState = reducedSemanticsModel.getState(includedConfigPrefix);
+
+ // Verify that the output is identical:
+ var fullOutput = automaton.getSemantics().computeSuffixOutput(Word.epsilon(), includedConfigPrefix);
+ var reducedOutput = reducedSemanticsModel.computeOutput(includedConfigPrefix);
+ Assert.assertEquals(fullOutput, reducedOutput);
+
+ Assert.assertEquals(expectedState, reachedState);
+ }
+
+ @Test
+ public void testReducedSemanticsOmittedConfiguration() {
+ var automaton = buildBaseModel();
+ var reducedSemanticsModel = ReducedMMLTSemantics.forLocalTimerMealy(automaton);
+ Assert.assertEquals(reducedSemanticsModel.size(), 31);
+
+ // Only reachable via at least two following time steps:
+ Word> omittedConfigPrefix =
+ Word.fromSymbols(new InputSymbol<>("p1"),
+ new TimeoutSymbol<>(),
+ new TimeoutSymbol<>(),
+ TimedInput.step(),
+ TimedInput.step());
+ var omittedConfig = automaton.getSemantics().getState(omittedConfigPrefix);
+
+ // Verify that we cannot reach this state in the reduced semantics:
+ Assert.assertNull(reducedSemanticsModel.getState(omittedConfigPrefix));
+ Assert.assertThrows(IllegalStateException.class,
+ () -> reducedSemanticsModel.getStateForConfiguration(omittedConfig, false));
+
+ // Verify that the output is incomplete:
+ var fullOutput = automaton.getSemantics().computeSuffixOutput(Word.epsilon(), omittedConfigPrefix);
+ var reducedOutput = reducedSemanticsModel.computeOutput(omittedConfigPrefix);
+ Assert.assertNotEquals(fullOutput, reducedOutput);
+
+ // Check the approximated state:
+ Assert.assertNotNull(omittedConfig);
+ var approxStateId = reducedSemanticsModel.getStateForConfiguration(omittedConfig, true);
+ var approxConfig = reducedSemanticsModel.getConfigurationForState(approxStateId);
+
+ Assert.assertEquals(approxConfig.getLocation(), omittedConfig.getLocation());
+ Assert.assertEquals(approxConfig.getEntryDistance(), 7);
+ }
+
+ @Test
+ public void testInvalidTimerChecks() {
+ var automaton = buildBaseModel();
+
+ int s1 = 1;
+
+ // Duplicate timer name:
+ Assert.assertThrows(IllegalArgumentException.class, () -> automaton.addPeriodicTimer(s1, "a", 3, "test"));
+
+ // Timer with silent output:
+ Assert.assertThrows(IllegalArgumentException.class, () -> automaton.addPeriodicTimer(s1, "e", 3, "void"));
+
+ // Timer never expires:
+ Assert.assertThrows(IllegalArgumentException.class, () -> automaton.addPeriodicTimer(s1, "e", 41, "test"));
+
+ // One-shot timer that times out at same time as periodic:
+ Assert.assertThrows(IllegalArgumentException.class, () -> automaton.addOneShotTimer(s1, "e", 12, "test", 3));
+
+ // Periodic timer that times out at same time as one-shot:
+ Assert.assertThrows(IllegalArgumentException.class, () -> automaton.addPeriodicTimer(s1, "e", 20, "test"));
+
+ // Duplicate one-shot timer:
+ Assert.assertThrows(IllegalArgumentException.class, () -> automaton.addOneShotTimer(s1, "e", 12, "test", 3));
+ }
+}
diff --git a/pom.xml b/pom.xml
index 339a94462..bf48e1acd 100644
--- a/pom.xml
+++ b/pom.xml
@@ -84,6 +84,14 @@ limitations under the License.
Developer
+
+ Paul Kogel
+ TU Berlin, Software and Embedded Systems Engineering
+ https://www.tu.berlin/sese
+
+ Developer
+
+
Jeroen Meijer
j.j.g.meijer@utwente.nl
@@ -185,9 +193,9 @@ limitations under the License.
UTF-8
UTF-8
- 11
- 11
- 11
+ 17
+ 17
+ 17
diff --git a/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTMMLTParser.java b/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTMMLTParser.java
new file mode 100644
index 000000000..76a61ecfa
--- /dev/null
+++ b/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTMMLTParser.java
@@ -0,0 +1,314 @@
+package net.automatalib.serialization.dot;
+
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.Reader;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+import net.automatalib.alphabet.Alphabet;
+import net.automatalib.alphabet.impl.Alphabets;
+import net.automatalib.automaton.mmlt.MMLTCreator;
+import net.automatalib.automaton.mmlt.MealyTimerInfo;
+import net.automatalib.automaton.mmlt.MutableMMLT;
+import net.automatalib.automaton.mmlt.SymbolCombiner;
+import net.automatalib.common.util.IOUtil;
+import net.automatalib.common.util.mapping.Mapping;
+import net.automatalib.common.util.mapping.MutableMapping;
+import net.automatalib.exception.FormatException;
+import net.automatalib.visualization.VisualizationHelper.EdgeAttrs;
+import net.automatalib.visualization.VisualizationHelper.MMLTEdgeAttrs;
+import net.automatalib.visualization.VisualizationHelper.MMLTNodeAttrs;
+
+/**
+ * Parses a DOT file that defines an MMLT automaton.
+ * Expected syntax:
+ *
+ * - Mealy labels:
input/output
+ * - Initial node marker:
__start0
+ * - Timeout input:
to[x] where x is the name of a local timer
+ * - Local timers: node attribute
timers with comma-separated assignments x=t with t > 0.
+ * Timer names must be unique per location. For one-shot timers choose values such that they never expire at the
+ * same time as another local timer.
+ * - Reset behavior: edge attribute
resets as specified below.
+ *
+ * Resets:
+ *
+ * - If the input is a timeout symbol:
+ *
+ * - Attribute omitted: periodic if self-loop, one-shot otherwise.
+ * - Self-loop and value is list of all local timers: one-shot timer.
+ * - Self-loop and value is the name of the timed-out timer: periodic.
+ * - Any other value: invalid.
+ *
+ *
+ * - If the input is a normal input and the edge is a self-loop:
+ *
+ * - Attribute omitted: regular edge.
+ * - Value is list of all local timers: local reset.
+ * - Any other value: invalid.
+ *
+ * If the edge is not a self-loop, reset values are ignored.
+ *
+ *
+ * Notes:
+ *
+ * - It is currently not possible to define a location with a single timer that is one-shot and whose timeout
+ * causes a self-loop. Such a timer is always considered periodic. This is semantically equivalent for learning,
+ * but hypotheses may still use the former variant; those timers may be highlighted specially for debugging.
+ * - Edges with a timeout input must not be silent.
+ *
+ * Example DOT:
+ * {@code
+ * digraph g {
+ * s0 [label="L0" timers="a=2"]
+ * s1 [label="L1" timers="b=4,c=6"]
+ * s2 [label="L2" timers="d=2,e=3"]
+ *
+ * s0 -> s1 [label="to[a] / A"] // one-shot with location change
+ * s1 -> s1 [label="to[b] / B"] // periodic
+ * s1 -> s1 [label="to[c] / C" resets="b,c"] // one-shot with loop
+ *
+ * s2 -> s2 [label="to[d] / D" resets="d"] // periodic with explicit resets
+ * s2 -> s2 [label="to[e] / E"] // periodic
+ *
+ * s1 -> s2 [label="x / void"]
+ * s1 -> s1 [label="y / Y" resets="b,c"] // loop with reset
+ * s2 -> s2 [label="y / D"] // loop without reset
+ *
+ * __start0 [label="" shape="none" width="0" height="0"];
+ * __start0 -> s0;
+ * }
+ * }
+ */
+
+public class DOTMMLTParser>
+ implements DOTInputModelDeserializer {
+
+ private static final Pattern assignPattern = Pattern.compile("(\\S+)=(\\d+)");
+
+ private final MMLTCreator creator;
+ private final Function inputParser;
+ private final Function outputParser;
+ private final O silentSymbol;
+ private final SymbolCombiner outputCombiner;
+ private final Collection initialNodeIds;
+ private final boolean fakeInitialNodeIds;
+
+ public DOTMMLTParser(MMLTCreator creator,
+ Function inputParser,
+ Function outputParser,
+ O silentOutput,
+ SymbolCombiner outputCombiner,
+ Collection initialNodeIds,
+ boolean fakeInitialNodeIds) {
+ this.creator = creator;
+ this.inputParser = inputParser;
+ this.outputParser = outputParser;
+ this.silentSymbol = silentOutput;
+ this.outputCombiner = outputCombiner;
+ this.initialNodeIds = initialNodeIds;
+ this.fakeInitialNodeIds = fakeInitialNodeIds;
+ }
+
+ @Override
+ public DOTInputModelData readModel(InputStream is) throws IOException, FormatException {
+
+ try (Reader r = IOUtil.asNonClosingUTF8Reader(is)) {
+ InternalDOTParser parser = new InternalDOTParser(r);
+ parser.parse();
+
+ assert parser.isDirected();
+
+ final Set inputs = new HashSet<>();
+
+ for (Edge edge : parser.getEdges()) {
+ if (!fakeInitialNodeIds || !initialNodeIds.contains(edge.src)) {
+ final String input = tokenizeLabel(edge)[0].trim();
+ if (!input.startsWith("to[")) {
+ inputs.add(inputParser.apply(input));
+ }
+ }
+ }
+
+ final Alphabet alphabet = Alphabets.fromCollection(inputs);
+ final A automaton = creator.createMMLT(alphabet, parser.getNodes().size(), silentSymbol, outputCombiner);
+
+ final Mapping labels = parseNodesAndEdges(parser, automaton);
+
+ return new DOTInputModelData<>(automaton, alphabet, labels);
+ }
+ }
+
+ private Mapping parseNodesAndEdges(InternalDOTParser parser, MutableMMLT result) {
+
+ final Collection nodes = parser.getNodes();
+ final Collection edges = parser.getEdges();
+
+ final Map>> timers =
+ new HashMap<>(nodes.size() - 1); // id in dot -> local timers
+ final Map stateMap = new HashMap<>(nodes.size() - 1); // name in dot -> new id
+ final MutableMapping mapping = result.createDynamicStateMapping();
+
+ // Parse nodes:
+ for (var node : nodes) {
+ final S n;
+
+ if (fakeInitialNodeIds && initialNodeIds.contains(node.id)) {
+ continue;
+ } else if (!fakeInitialNodeIds && initialNodeIds.contains(node.id)) {
+ n = result.addInitialState();
+ } else {
+ n = result.addState();
+ }
+
+ stateMap.put(node.id, n);
+ mapping.put(n, node.id);
+
+ // Parse timers:
+ final String timersAttr = node.attributes.get(MMLTNodeAttrs.TIMERS);
+ if (timersAttr != null) {
+ String[] settings = timersAttr.split(",");
+ for (String setting : settings) {
+ Matcher m = assignPattern.matcher(setting.trim()); // remove whitespace
+ if (!m.matches()) {
+ continue;
+ }
+ String timerName = m.group(1).trim();
+ int value = Integer.parseInt(m.group(2));
+ if (value <= 0) {
+ throw new IllegalArgumentException(String.format(
+ "Reset for timer %s in location %s must be greater zero.",
+ timerName,
+ node.id));
+ }
+
+ Map> timeInfo = timers.computeIfAbsent(node.id, k -> new HashMap<>());
+ if (timeInfo.containsKey(timerName)) {
+ throw new IllegalArgumentException(String.format(
+ "Timer %s in location %s must only be set once.",
+ timerName,
+ node.id));
+ }
+
+ // Add timer:
+ timeInfo.put(timerName, new MealyTimerInfo<>(timerName, value, null, null));
+ }
+ } else {
+ timers.put(node.id, Collections.emptyMap()); // no timers in this location
+ }
+ }
+
+ // Parse edges:
+ for (var edge : edges) {
+
+ if (fakeInitialNodeIds && initialNodeIds.contains(edge.src)) {
+ result.setInitial(stateMap.get(edge.tgt), true);
+ continue;
+ }
+
+ // Check for resets:
+ Set edgeResets = new HashSet<>();
+ String resetAttr = edge.attributes.get(MMLTEdgeAttrs.RESETS);
+ if (resetAttr != null) {
+ // Parse resets:
+ for (String timer : resetAttr.split(",")) {
+ edgeResets.add(timer.strip());
+ }
+ }
+
+ final String[] tokens = tokenizeLabel(edge);
+ final String input = tokens[0].trim();
+ final String output = tokens[1].trim();
+
+ if (input.startsWith("to[")) {
+ // Ensure that we defined the corresponding timer:
+ String timerName = input.substring(3, input.length() - 1);
+ if (!timers.get(edge.src).containsKey(timerName)) {
+ throw new IllegalArgumentException(String.format(
+ "Defined %s in state %s, but timer value is not set.",
+ input,
+ edge.src));
+ }
+
+ // Add output to timer info:
+ final MealyTimerInfo oldInfo = timers.get(edge.src).get(timerName);
+
+ // Infer timer type:
+ final long initial = oldInfo.initial();
+ boolean periodic = true;
+ if (edge.src.equals(edge.tgt)) {
+ if (edgeResets.size() == 1) {
+ if (!edgeResets.contains(timerName)) {
+ // Invalid periodic timer:
+ throw new IllegalArgumentException(String.format("Invalid reset at to[%s]", timerName));
+ }
+ } else if (edgeResets.size() > 1) {
+ // Need to contain all local timers to be one-shot with loop:
+ for (var locTimer : timers.get(edge.tgt).keySet()) {
+ if (!edgeResets.contains(locTimer)) {
+ throw new IllegalArgumentException(String.format("Invalid reset at to[%s]", timerName));
+ }
+ }
+ periodic = false;
+ }
+ } else {
+ // No need to check resets on location-change: always resetting all in target
+ periodic = false;
+ }
+
+ final O o = outputParser.apply(output);
+
+ // Add timer to location:
+ if (periodic) {
+ result.addPeriodicTimer(stateMap.get(edge.src), timerName, initial, o);
+ } else {
+ result.addOneShotTimer(stateMap.get(edge.src), timerName, initial, o, stateMap.get(edge.tgt));
+ }
+ } else {
+ // Non-delaying input:
+ final I i = inputParser.apply(input);
+ final O o = outputParser.apply(output);
+
+ result.addTransition(stateMap.get(edge.src), i, stateMap.get(edge.tgt), o);
+
+ // Parse resets of self-loops with untimed input:
+ if (edge.src.equals(edge.tgt) && !edgeResets.isEmpty()) {
+ // Reset list needs to contain all local timers:
+ for (var locTimer : timers.get(edge.tgt).keySet()) {
+ if (!edgeResets.contains(locTimer)) {
+ throw new IllegalArgumentException(String.format("Invalid local reset at %s", i));
+ }
+ }
+ result.addLocalReset(stateMap.get(edge.src), i);
+ }
+ }
+ }
+
+ return mapping;
+ }
+
+ private static String[] tokenizeLabel(Edge edge) {
+ final String label = edge.attributes.get(EdgeAttrs.LABEL);
+
+ if (label == null) {
+ throw new IllegalArgumentException("All edges must have an input and an output.");
+ }
+
+ final String[] tokens = label.split("/");
+
+ if (tokens.length != 2) {
+ throw new IllegalArgumentException("All edges must have an input and an output.");
+ }
+
+ return tokens;
+ }
+
+}
diff --git a/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTParsers.java b/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTParsers.java
index 2380e3b54..90184a029 100644
--- a/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTParsers.java
+++ b/serialization/dot/src/main/java/net/automatalib/serialization/dot/DOTParsers.java
@@ -30,6 +30,10 @@
import net.automatalib.automaton.fsa.NFA;
import net.automatalib.automaton.fsa.impl.CompactDFA;
import net.automatalib.automaton.fsa.impl.CompactNFA;
+import net.automatalib.automaton.mmlt.MMLTCreator;
+import net.automatalib.automaton.mmlt.MutableMMLT;
+import net.automatalib.automaton.mmlt.SymbolCombiner;
+import net.automatalib.automaton.mmlt.impl.CompactMMLT;
import net.automatalib.automaton.transducer.MealyMachine;
import net.automatalib.automaton.transducer.MooreMachine;
import net.automatalib.automaton.transducer.MutableMealyMachine;
@@ -695,6 +699,48 @@ public static ModelDeserializer> graph(Fu
true);
}
+ public static DOTInputModelDeserializer> mmlt(String silentOutput,
+ SymbolCombiner outputCombiner) {
+ return mmlt(Function.identity(), Function.identity(), silentOutput, outputCombiner);
+ }
+
+ public static DOTInputModelDeserializer