Code for Mealy machines with local timers. (#96)

* Added MMLT classes

* Added basic tests for MMLTs; included sample MMLT model file.

* Added serialization test for MMLTs.

* Separated more files into API and implementation to enable use from LearnLib.

* Removed I prefix for some interfaces for the MMLT automaton.

* Updated calculation of MMLT location cover to accept a list of inputs to be considered.

* Method for finding a separating word in an MMLT now considers a provided collection of inputs.

* Convenience flag for faster location cover calculation.

* Added more tests for the reduced semantics.

* Parser for MMLTs now accepts an input stream, in addition to a file.

* Updated Serialization for MMLTs: resets-attribute for edges is now included when resets cannot be inferred from context.

* initial refactorings / cleanups

* use InputSymbols directly

* use input type I directly

* Removed getUntimedAlphabet, as it has the same function as getInputAlphabet.

* CompactMMLT: allow for sizeHints

* MMLTs: add direct equivalence check

* make code-analysis pass

* mention MMLTs in README

* adjust to LearnLib refactorings

* add documentation

* add some more test cases

* Using LinkedHashMap instead of HashMap in MMLT-Cover for deterministic ordering.

* MMLT transition output can no longer be null.

* Added more validation tests for the MMLT-parser.

* TimerInfo now supports multiple outputs per timer. StringSymbolCombiner expects atomic outputs for its input list when combining symbols.

* MMLT parser now parses multiple outputs for one timer. Updated corresponding tests.

* fix analysis and adjust to LearnLib refactorings

* cleanups

* documentation

* last de-stream-ifications

---------

Co-authored-by: Paul Kogel <[email protected]>
Co-authored-by: Markus Frohme <[email protected]>

Author: 3 people

CHANGELOG.md

@@ -8,6 +8,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
+* A new formalism for *Mealy machines with local timers* (MMLTs) including means for conformance testing and equivalence checking has been added (thanks to [Paul Kogel](https://github.com/pdev55)).
 * `automata-modelchecking-m3c` now supports ARM-based macOS systems.
 * `automata-modelchecking-m3c` can now be included in jlink images.
 

README.md

@@ -14,7 +14,7 @@ Its original purpose is to serve as the automaton framework for the [LearnLib][3
 However, it is completely independent of LearnLib and can be used for other projects as well.
 
 AutomataLib supports modeling a variety of graph-based structures.
-Currently, it covers generic transition systems, Deterministic Finite Automata (DFAs) and Mealy machines as well as more advanced structures such as Modal Transition Systems (MTSs), Subsequential Transducers (SSTs), Visibly Pushdown Automata (VPAs) and Procedural Systems (SPAs, SBAs, SPMMs).
+Currently, it covers generic transition systems like Deterministic Finite Automata (DFAs) and Mealy machines as well as more advanced structures such as Modal Transition Systems (MTSs), Mealy machines with local timers (MMLTs), Visibly Pushdown Automata (VPAs) and Procedural Systems (SPAs, SBAs, SPMMs).
 
 Models of AutomataLib can be (de-)serialized (from) to one of the various supported serialization formats and may be visualized using either the GraphViz or JUNG library.
 Furthermore, a plethora of graph-/automata-based algorithms is implemented, covering the following topics:

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,103 @@
+/* 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 java.util.List;
+
+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.SymbolicInput;
+
+/**
+ * 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 timer. 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 the provided
+ * {@link #getOutputCombiner()}.
+ * <p>
+ * <b>Implementation note:</b> This class resembles a "structural" view on the MMLT. Timeouts can also be interpreted
+ * as explicit transitions between locations. For this representation, use the {@link #graphView()} method. For a
+ * semantic view that supports time-sensitive transductions, see the {@link #getSemantics()} method.
+ *
+ * @param <S>
+ *         location type
+ * @param <I>
+ *         input symbol type (of non-delaying inputs)
+ * @param <T>
+ *         transition type
+ * @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 the silent output symbol
+     */
+    O getSilentOutput();
+
+    /**
+     * Returns the output combiner used when multiple periodic timers time out simultaneously.
+     *
+     * @return the output combiner
+     */
+    SymbolCombiner<O> getOutputCombiner();
+
+    /**
+     * Indicates if the provided input performs a local reset in the given location.
+     *
+     * @param location
+     *         the location
+     * @param input
+     *         the input
+     *
+     * @return {@code true} if performing a local reset, {@code false} otherwise
+     */
+    boolean isLocalReset(S location, I input);
+
+    /**
+     * Returns the timers of the specified location sorted ascendingly by their initial time.
+     *
+     * @param location
+     *         the location
+     *
+     * @return sorted list of local timers (may be empty if the location has no timers)
+     */
+    List<TimerInfo<S, O>> getSortedTimers(S location);
+
+    /**
+     * Returns the semantics automaton that describes the behavior of this MMLT.
+     *
+     * @return a semantic view of this MMLT
+     */
+    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/MMLTGraphView.java

@@ -0,0 +1,93 @@
+/* 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 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;
+
+/**
+ * A graphview for {@link MMLT}s that explicitly represents timeouts as transitions between locations if possible. For
+ * this purpose, edges use {@link SymbolicInput}s which include {@link InputSymbol}s and {@link TimerTimeoutSymbol}s.
+ *
+ * @param <S>
+ *         location type
+ * @param <I>
+ *         input symbol type (of non-delaying inputs)
+ * @param <T>
+ *         transition type
+ * @param <O>
+ *         output symbol type
+ */
+public class MMLTGraphView<S, I, T, O> implements Graph<S, Triple<SymbolicInput<I>, O, S>> {
+
+    private final MMLT<S, I, T, O> mmlt;
+    private final SymbolCombiner<O> outputCombiner;
+
+    public MMLTGraphView(MMLT<S, I, T, O> mmlt) {
+        this.mmlt = mmlt;
+        this.outputCombiner = mmlt.getOutputCombiner();
+    }
+
+    @Override
+    public Collection<Triple<SymbolicInput<I>, O, S>> getOutgoingEdges(S node) {
+
+        Alphabet<I> alphabet = mmlt.getInputAlphabet();
+        List<TimerInfo<S, O>> timers = mmlt.getSortedTimers(node);
+
+        List<Triple<SymbolicInput<I>, O, S>> result = new ArrayList<>(alphabet.size() + timers.size());
+
+        for (I i : alphabet) {
+            T t = mmlt.getTransition(node, i);
+            if (t != null) {
+                result.add(Triple.of(TimedInput.input(i), mmlt.getTransitionProperty(t), mmlt.getSuccessor(t)));
+            }
+        }
+
+        for (TimerInfo<S, O> t : timers) {
+            result.add(Triple.of(new TimerTimeoutSymbol<>(t.name()),
+                                 outputCombiner.combineSymbols(t.outputs()),
+                                 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,82 @@
+/* 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.automaton.concept.InputAlphabetHolder;
+import net.automatalib.automaton.concept.SuffixOutput;
+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.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 {@link State states} of this machine
+ * represent tuples of an active location and the current valuation of timers of this location. The inputs of the
+ * machine are {@link InputSymbol non-delaying inputs}, {@link TimeStepSequence discrete time steps}, and the
+ * {@link TimeoutSymbol symbolic input timeout}, which causes a delay until the next timeout.
+ * <p>
+ * The input alphabet of this machine consists of all non-delaying inputs of the associated MMLT, as well as a
+ * {@link TimeStepSequence time step symbol} and the {@link TimeoutSymbol symbolic input 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 {@link TimeoutSymbol} input.
+ *
+ * @param <S>
+ *         location type
+ * @param <I>
+ *         input symbol type (of non-delaying inputs)
+ * @param <T>
+ *         transition type
+ * @param <O>
+ *         output symbol type
+ */
+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 symbol used for silent outputs.
+     *
+     * @return the 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. The output of the transition is the output of the time step that was executed last.
+     * This output might belong to a timeout or be silence. The delay of this output is set to zero.
+     * <p>
+     * Please note that a sequence with more than one time step may trigger multiple timeouts. Regardless of that, only
+     * the output at the last time step is returned.
+     *
+     * @param source
+     *         the source configuration
+     * @param input
+     *         the input symbol
+     * @param maxWaitingTime
+     *         the maximum time steps to wait for a timeout
+     *
+     * @return the transition in semantics automaton
+     */
+    T getTransition(State<S, O> source, TimedInput<I> input, long maxWaitingTime);
+}