Code for Mealy machines with local timers.

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;

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).
+ * <p>
+ * 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.
+ * <p>
+ * 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.
+ * <p>
+ * <b>Implementation note:</b> this class resembles a "structural" view on the MMLT. For a semantic view with
+ * time-sensitive transductions, see the {@link #getSemantics()} method.
+ *
+ * @param <S>
+ *         Location type
+ * @param <I>
+ *         Input type for non-delaying inputs
+ * @param <O>
+ *         Output symbol type
+ */
+public interface MMLT<S, I, T, O> extends UniversalDeterministicAutomaton<S, I, T, Void, O>,
+                                          InputAlphabetHolder<I>,
+                                          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<O> getOutputCombiner();
+
+    /**
+     * Retrieves the non-delaying inputs for this automaton. Excludes timer timeout symbols. May be empty.
+     *
+     * @return Input alphabet
+     */
+    Alphabet<I> 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<MealyTimerInfo<S, O>> getSortedTimers(S location);
+
+    /**
+     * Returns the semantics automaton that describes the behavior of this MMLT.
+     *
+     * @return Semantics automaton
+     */
+    MMLTSemantics<S, I, ?, O> getSemantics();
+
+    @Override
+    default Graph<S, Triple<SymbolicInput<I>, O, S>> graphView() {
+        return new MMLTGraphView<>(this);
+    }
+}

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 <https://automatalib.net>.
+ *
+ * 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<A, I, O> {
+
+    default A createMMLT(Alphabet<I> alphabet, int numStatesHint, O silentOutput, SymbolCombiner<O> outputCombiner) {
+        return createMMLT(alphabet, silentOutput, outputCombiner);
+    }
+
+    A createMMLT(Alphabet<I> alphabet, O silentOutput, SymbolCombiner<O> symbolCombiner);
+
+}

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<S, I, T, O> implements Graph<S, Triple<SymbolicInput<I>, O, S>> {
+
+    private final MMLT<S, I, T, O> mmlt;
+
+    public MMLTGraphView(MMLT<S, I, T, O> mmlt) {
+        this.mmlt = mmlt;
+    }
+
+    @Override
+    public Collection<Triple<SymbolicInput<I>, O, S>> getOutgoingEdges(S node) {
+
+        Alphabet<I> alphabet = mmlt.getInputAlphabet();
+        List<MealyTimerInfo<S, O>> timers = mmlt.getSortedTimers(node);
+
+        List<Triple<SymbolicInput<I>, 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<S, O> t : timers) {
+            result.add(Triple.of(new TimerTimeoutSymbol<>(t.name()), t.output(), t.target()));
+
+        }
+
+        return result;
+    }
+
+    @Override
+    public S getTarget(Triple<SymbolicInput<I>, O, S> edge) {
+        return edge.getThird();
+    }
+
+    @Override
+    public Collection<S> getNodes() {
+        return mmlt.getStates();
+    }
+
+    @Override
+    public VisualizationHelper<S, Triple<SymbolicInput<I>, O, S>> getVisualizationHelper() {
+        return new MMLTVisualizationHelper<>(mmlt, false, false);
+    }
+}

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.
+ * <p>
+ * 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.
+ * <p>
+ * 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 <S>
+ *         Location type
+ * @param <I>
+ *         Input type for non-delaying inputs
+ * @param <O>
+ *         Output type of the MMLT
+ */
+public interface MMLTSemantics<S, I, T, O>
+        extends MealyTransitionSystem<State<S, O>, TimedInput<I>, T, TimedOutput<O>>,
+                SuffixOutput<TimedInput<I>, Word<TimedOutput<O>>>,
+                InputAlphabetHolder<TimedInput<I>> {
+
+    /**
+     * 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<TimedInput<I>> getInputAlphabet();
+
+    /**
+     * Returns the symbol used for silent outputs.
+     *
+     * @return Silent output symbol
+     */
+    TimedOutput<O> getSilentOutput();
+
+    /**
+     * Retrieves the transition in the semantics automaton that has the provided input and source configuration.
+     * <p>
+     * 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<S, O> source, TimedInput<I> input, long maxWaitingTime);
+}

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 <O> Output symbol type
+ */
+public class MealyTimerInfo<S, O> {
+    /**
+     * 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);
+    }
+
+}