From e26aa8225b37c017f1c6fa006956bfafe730b18e Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Tue, 7 Oct 2025 13:32:25 +0200 Subject: [PATCH 01/11] Bumped java version to 17 --- pom.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pom.xml b/pom.xml index 339a94462..59f1160c0 100644 --- a/pom.xml +++ b/pom.xml @@ -185,9 +185,9 @@ limitations under the License. UTF-8 UTF-8 - 11 - 11 - 11 + 17 + 17 + 17 From 3e3bc1773ef9d29459d19d766a2ccdee491ac82a Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Tue, 7 Oct 2025 13:44:52 +0200 Subject: [PATCH 02/11] Added MMLT classes --- core/src/main/java/module-info.java | 4 + .../mmlt/ILocalTimerMealyInputSymbol.java | 7 + .../ILocalTimerMealySemanticInputSymbol.java | 10 + .../mmlt/LocalTimerMealyOutputSymbol.java | 60 ++++ .../impl/time/mmlt/NonDelayingInput.java | 40 +++ .../impl/time/mmlt/TimeStepSequence.java | 48 ++++ .../impl/time/mmlt/TimeStepSymbol.java | 12 + .../impl/time/mmlt/TimeoutSymbol.java | 25 ++ .../impl/time/mmlt/TimerTimeoutSymbol.java | 41 +++ .../time/mmlt/AbstractSymbolCombiner.java | 36 +++ .../time/mmlt/CompactLocalTimerMealy.java | 229 +++++++++++++++ .../automaton/time/mmlt/LocalTimerMealy.java | 179 ++++++++++++ .../LocalTimerMealyVisualizationHelper.java | 105 +++++++ .../automaton/time/mmlt/MealyTimerInfo.java | 86 ++++++ .../time/mmlt/MutableLocalTimerMealy.java | 96 +++++++ .../time/mmlt/StringSymbolCombiner.java | 64 +++++ .../LocalTimerMealyConfiguration.java | 210 ++++++++++++++ .../semantics/LocalTimerMealySemantics.java | 272 ++++++++++++++++++ .../ReducedLocalTimerMealySemantics.java | 162 +++++++++++ .../time/mmlt/semantics/TimeoutPair.java | 22 ++ .../dot/LocalTimerMealyGraphvizParser.java | 231 +++++++++++++++ .../automaton/cover/LocalTimerMealyCover.java | 69 +++++ .../automaton/mmlt/LocalTimerMealyUtil.java | 154 ++++++++++ 23 files changed, 2162 insertions(+) create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealyInputSymbol.java create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealySemanticInputSymbol.java create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/LocalTimerMealyOutputSymbol.java create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/NonDelayingInput.java create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSequence.java create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSymbol.java create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeoutSymbol.java create mode 100644 core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimerTimeoutSymbol.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/CompactLocalTimerMealy.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/StringSymbolCombiner.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/ReducedLocalTimerMealySemantics.java create mode 100644 core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java create mode 100644 serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java create mode 100644 util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java create mode 100644 util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java diff --git a/core/src/main/java/module-info.java b/core/src/main/java/module-info.java index c482544dd..ab59cfb7a 100644 --- a/core/src/main/java/module-info.java +++ b/core/src/main/java/module-info.java @@ -35,6 +35,7 @@ // 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; @@ -51,4 +52,7 @@ exports net.automatalib.ts.modal.impl; exports net.automatalib.ts.modal.transition.impl; exports net.automatalib.ts.powerset.impl; + exports net.automatalib.alphabet.impl.time.mmlt; + exports net.automatalib.automaton.time.mmlt.semantics; + exports net.automatalib.automaton.time.mmlt; } diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealyInputSymbol.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealyInputSymbol.java new file mode 100644 index 000000000..796cf1439 --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealyInputSymbol.java @@ -0,0 +1,7 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +/** + * Base type for input symbols for the structural automaton of an MMLT. + */ +public interface ILocalTimerMealyInputSymbol { +} diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealySemanticInputSymbol.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealySemanticInputSymbol.java new file mode 100644 index 000000000..cd5618440 --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealySemanticInputSymbol.java @@ -0,0 +1,10 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +/** + * Base class for an input for the semantics automaton of some MMLT. + * + * @param + */ +public interface ILocalTimerMealySemanticInputSymbol { + +} diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/LocalTimerMealyOutputSymbol.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/LocalTimerMealyOutputSymbol.java new file mode 100644 index 000000000..8bdf590a4 --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/LocalTimerMealyOutputSymbol.java @@ -0,0 +1,60 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +import org.checkerframework.checker.nullness.qual.NonNull; + +import java.util.Objects; + +/** + * Output type for the semantics automaton: an output that occurs with some or no delay. + */ +public class LocalTimerMealyOutputSymbol { + + private final U userObject; + private final long delay; + + public LocalTimerMealyOutputSymbol(long delay, @NonNull U userObject) { + if (delay < 0) { + throw new IllegalArgumentException("Delay must not be negative."); + } + this.userObject = userObject; + this.delay = delay; + } + + public LocalTimerMealyOutputSymbol(@NonNull U userObject) { + this(0, userObject); + } + + public long getDelay() { + return delay; + } + + public boolean isDelayed() { + return this.delay > 0; + } + + public U getSymbol() { + return userObject; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + LocalTimerMealyOutputSymbol that = (LocalTimerMealyOutputSymbol) o; + return delay == that.delay && Objects.equals(userObject, that.userObject); + } + + @Override + public int hashCode() { + return Objects.hash(userObject, delay); + } + + @Override + public String toString() { + if (this.isDelayed()) { + return String.format("[%d]%s", this.getDelay(), this.userObject); + } + return this.userObject.toString(); + } + +} diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/NonDelayingInput.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/NonDelayingInput.java new file mode 100644 index 000000000..74a903b33 --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/NonDelayingInput.java @@ -0,0 +1,40 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +import org.checkerframework.checker.nullness.qual.NonNull; + +import java.util.Objects; + +/** + * An non-delaying input for the structural and semantics automaton. + * + * @param + */ +public class NonDelayingInput implements ILocalTimerMealySemanticInputSymbol, ILocalTimerMealyInputSymbol { + private final U symbol; + + public NonDelayingInput(@NonNull U input) { + this.symbol = input; + } + + public U getSymbol() { + return this.symbol; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + NonDelayingInput that = (NonDelayingInput) o; + return Objects.equals(symbol, that.symbol); + } + + @Override + public int hashCode() { + return Objects.hashCode(symbol); + } + + @Override + public String toString() { + return symbol.toString(); + } +} diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSequence.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSequence.java new file mode 100644 index 000000000..cc78c5e49 --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSequence.java @@ -0,0 +1,48 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +import java.util.Objects; + +/** + * Convenience type for aggregating multiple subsequent time steps. + */ +public class TimeStepSequence implements ILocalTimerMealySemanticInputSymbol { + + private long timeSteps; + + public TimeStepSequence(long timeSteps) { + this.timeSteps = timeSteps; + + if (timeSteps <= 0) { + throw new IllegalArgumentException("Timeout must be larger than zero."); + } + } + + public void setTimeSteps(long timeSteps) { + this.timeSteps = timeSteps; + if (timeSteps <= 0) { + throw new IllegalArgumentException("Timeout must be larger than zero."); + } + } + + public long getTimeSteps() { + return timeSteps; + } + + @Override + public String toString() { + return String.format("wait[%d]", this.timeSteps); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + TimeStepSequence that = (TimeStepSequence) o; + return timeSteps == that.timeSteps; + } + + @Override + public int hashCode() { + return Objects.hash(timeSteps); + } +} diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSymbol.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSymbol.java new file mode 100644 index 000000000..8978a7866 --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSymbol.java @@ -0,0 +1,12 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +/** + * Input for the semantics automaton: delay for a single time step. + */ +public class TimeStepSymbol extends TimeStepSequence { + + public TimeStepSymbol() { + super(1); + } + +} diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeoutSymbol.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeoutSymbol.java new file mode 100644 index 000000000..65bde2880 --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeoutSymbol.java @@ -0,0 +1,25 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +import java.util.Objects; + +/** + * Symbolic input for the semantics automaton: causes a delay until the next timeout. + */ +public class TimeoutSymbol implements ILocalTimerMealySemanticInputSymbol { + + @Override + public String toString() { + return "timeout"; + } + + @Override + public boolean equals(Object o) { + return o != null && getClass() == o.getClass(); + } + + @Override + public int hashCode() { + return Objects.hash(this.toString()); + } + +} diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimerTimeoutSymbol.java b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimerTimeoutSymbol.java new file mode 100644 index 000000000..eebd606dd --- /dev/null +++ b/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimerTimeoutSymbol.java @@ -0,0 +1,41 @@ +package net.automatalib.alphabet.impl.time.mmlt; + +import java.util.Objects; + +/** + * The timeout symbol of a timer, as used by the structural automaton. + *

+ * This input is used for the transition and output function of some MMLT. + * These symbols are not inputs for the expanded form of an MMLT. + * + * @param + */ +public class TimerTimeoutSymbol implements ILocalTimerMealyInputSymbol { + private final String timer; + + public TimerTimeoutSymbol(String timer) { + this.timer = timer; + } + + public String getTimer() { + return timer; + } + + @Override + public String toString() { + return String.format("to[%s]", this.timer); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + TimerTimeoutSymbol that = (TimerTimeoutSymbol) o; + return Objects.equals(timer, that.timer); + } + + @Override + public int hashCode() { + return Objects.hashCode(timer); + } +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java new file mode 100644 index 000000000..b3ab1a3d0 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java @@ -0,0 +1,36 @@ +package net.automatalib.automaton.time.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 abstract class AbstractSymbolCombiner { + + /** + * Indicates if the provided suffix is a combined suffix. + * + * @param symbol Symbol for testing + * @return True if combined suffix, false if not. + */ + public abstract 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 + */ + public abstract U combineSymbols(List symbols); + + /** + * Attempts to separate the provided combined suffix into individual symbols. + * + * @param symbol Combined symbols + * @return Individual symbols + */ + public abstract List separateSymbols(U symbol); +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/CompactLocalTimerMealy.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/CompactLocalTimerMealy.java new file mode 100644 index 000000000..6cf601ce1 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/CompactLocalTimerMealy.java @@ -0,0 +1,229 @@ +package net.automatalib.automaton.time.mmlt; + +import net.automatalib.alphabet.Alphabet; +import net.automatalib.alphabet.GrowingAlphabet; +import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.impl.time.mmlt.TimerTimeoutSymbol; +import net.automatalib.automaton.transducer.impl.CompactMealy; +import org.checkerframework.checker.nullness.qual.Nullable; + +import java.util.*; + +/** + * 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 CompactLocalTimerMealy implements LocalTimerMealy, MutableLocalTimerMealy { + private final CompactMealy, O> automaton; + private final Map>> sortedTimers; // location -> (sorted timers) + private final Map>> resets; // location -> inputs (that reset all timers) + + private final GrowingAlphabet> untimedAlphabet; + + private final O silentOutput; + private final AbstractSymbolCombiner 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 CompactLocalTimerMealy(Collection> nonDelayingInputs, + O silentOutput, + AbstractSymbolCombiner outputCombiner + ) { + this.untimedAlphabet = new GrowingMapAlphabet<>(); + this.untimedAlphabet.addAll(nonDelayingInputs); + + this.sortedTimers = new HashMap<>(); + this.resets = new HashMap<>(); + + this.silentOutput = silentOutput; + this.outputCombiner = outputCombiner; + + // Prepare compact Mealy: + GrowingMapAlphabet> inputAlphabet = new GrowingMapAlphabet<>(); + inputAlphabet.addAll(nonDelayingInputs); + this.automaton = new CompactMealy<>(inputAlphabet); + } + + + @Override + public O getSilentOutput() { + return this.silentOutput; + } + + @Override + public AbstractSymbolCombiner getOutputCombiner() { + return this.outputCombiner; + } + + @Override + public Alphabet> getInputAlphabet() { + return this.automaton.getInputAlphabet(); + } + + @Override + public Alphabet> getUntimedAlphabet() { + return this.untimedAlphabet; + } + + @Override + public boolean isLocalReset(Integer location, NonDelayingInput 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 Collection getStates() { + return automaton.getStates(); + } + + @Override + public @Nullable LocalTimerMealyTransition getTransition(Integer location, ILocalTimerMealyInputSymbol input) { + var trans = this.automaton.getTransition(location, input); + if (trans == null) { + return null; + } + return new LocalTimerMealyTransition<>(trans.getSuccId(), trans.getProperty()); + } + + @Override + public @Nullable Integer getInitialState() { + return automaton.getInitialState(); + } + + @Override + public Integer addState() { + return automaton.addState(); + } + + @Override + public void setInitialState(Integer location) { + automaton.setInitialState(location); + } + + @Override + public void addTransition(Integer source, NonDelayingInput input, O output, Integer target) { + automaton.addAlphabetSymbol(input); + this.untimedAlphabet.addSymbol(input); + + automaton.removeAllTransitions(source, input); // remove transition if already defined + automaton.addTransition(source, input, target, output); + } + + @Override + public void removeTransition(Integer source, NonDelayingInput input) { + automaton.removeAllTransitions(source, input); + } + + 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)); + 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)); + 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, NonDelayingInput 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, NonDelayingInput input) { + var localResets = resets.get(location); + if (localResets == null) { + return; + } + + localResets.remove(input); + } +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java new file mode 100644 index 000000000..783d8b74c --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java @@ -0,0 +1,179 @@ +package net.automatalib.automaton.time.mmlt; + +import net.automatalib.alphabet.Alphabet; +import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.automaton.UniversalDeterministicAutomaton; +import net.automatalib.automaton.graph.TransitionEdge; +import net.automatalib.automaton.graph.UniversalAutomatonGraphView; +import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealySemantics; +import net.automatalib.graph.UniversalGraph; +import net.automatalib.visualization.VisualizationHelper; +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +import java.util.Collection; +import java.util.List; +import java.util.Set; + +/** + * 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 TimerTimeoutSymbol as input. Other inputs are called + * non-delaying. A non-delaying input that causes a self-loop can cause a local reset. Then, all timers of that + * location reset. + *

+ * To be able to subclass existing automata, some methods refer to locations as "state". + * + * @param Location type + * @param Input type for non-delaying inputs + * @param Output symbol type + */ +public interface LocalTimerMealy extends UniversalDeterministicAutomaton, LocalTimerMealy.LocalTimerMealyTransition, Void, O> { + + record LocalTimerMealyTransition(@NonNull S successor, @NonNull O output) { + + } + + /** + * 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 AbstractSymbolCombiner. This method returns the combiner used for + * this model. + * + * @return Symbol combiner used for this model. + */ + AbstractSymbolCombiner getOutputCombiner(); + + /** + * Returns the input alphabet of this MMLT, consisting of non-delaying inputs + * and timeout-symbols for its timers. + * + * @return Input alphabet + */ + Alphabet> getInputAlphabet(); + + /** + * Retrieves the non-delaying inputs for this automaton. + * Excludes timer timeout symbols. May be empty. + * + * @return Untimed alphabet. + */ + Alphabet> getUntimedAlphabet(); + + @Override + default O getTransitionProperty(LocalTimerMealyTransition transition) { + return transition.output(); + } + + @Override + default S getSuccessor(LocalTimerMealyTransition transition) { + return transition.successor(); + } + + /** + * 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, NonDelayingInput 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 + */ + default LocalTimerMealySemantics getSemantics() { + return new LocalTimerMealySemantics<>(this); + } + + // ======================================= + + @Override + default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView(Collection> inputs) { + return new LocalTimerMealyGraphView<>(this, inputs, false, false); + } + + default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView() { + return this.transitionGraphView(getInputAlphabet()); + } + + default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView(boolean colorEdges, boolean includeResets) { + return new LocalTimerMealyGraphView<>(this, getInputAlphabet(), colorEdges, includeResets); + } + + // ======================================= + + @Override + default Void getStateProperty(S state) { + return null; + } + + // We do not want to provide tracing abilities for inputs of the structure automaton: + @Override + default Set getStates(Iterable> input) { + throw new IllegalStateException("Not supported. Use the semantics automaton to trace inputs."); + } + + @Override + @Nullable + default S getSuccessor(S state, Iterable> input) { + throw new IllegalStateException("Not supported. Use the semantics automaton to trace inputs."); + } + + @Override + @Nullable + default S getState(Iterable> input) { + throw new IllegalStateException("Not supported. Use the semantics automaton to trace inputs."); + } + + // ======================================= + + class LocalTimerMealyGraphView extends + UniversalAutomatonGraphView, LocalTimerMealy.LocalTimerMealyTransition, Void, OX, LocalTimerMealy> { + + private final boolean colorEdges; + private final boolean includeResets; + + public LocalTimerMealyGraphView(LocalTimerMealy automaton, + Collection> inputs, + boolean colorEdges, boolean includeResets) { + super(automaton, inputs); + this.colorEdges = colorEdges; + this.includeResets = includeResets; + } + + @Override + public VisualizationHelper, LocalTimerMealyTransition>> getVisualizationHelper() { + return new LocalTimerMealyVisualizationHelper<>(automaton, colorEdges, includeResets); + } + } + +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java new file mode 100644 index 000000000..d793ed2a4 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java @@ -0,0 +1,105 @@ +package net.automatalib.automaton.time.mmlt; + +import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.impl.time.mmlt.TimerTimeoutSymbol; +import net.automatalib.automaton.graph.TransitionEdge; +import net.automatalib.automaton.visualization.AutomatonVisualizationHelper; + +import java.util.Map; +import java.util.stream.Collectors; + +class LocalTimerMealyVisualizationHelper extends + AutomatonVisualizationHelper, LocalTimerMealy.LocalTimerMealyTransition, LocalTimerMealy> { + + 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 LocalTimerMealyVisualizationHelper(LocalTimerMealy automaton, boolean colorEdges, boolean includeResets) { + super(automaton); + this.colorEdges = colorEdges; + this.includeResets = includeResets; + } + + @Override + public boolean getNodeProperties(S node, Map properties) { + super.getNodeProperties(node, properties); + + // 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("timers", timers); + } + + return true; + } + + @Override + public boolean getEdgeProperties(S src, + TransitionEdge, LocalTimerMealy.LocalTimerMealyTransition> edge, + S tgt, Map properties) { + super.getEdgeProperties(src, edge, tgt, properties); + + String label = String.format("%s / %s", edge.getInput(), edge.getTransition().output()); + + // Infer the label color + reset information for the transition: + String resetInfo = ""; + String edgeColor = ""; + if (edge.getInput() instanceof TimerTimeoutSymbol ts) { + // Get info for corresponding timer: + var optTimer = automaton.getSortedTimers(src).stream() + .filter(t -> t.name().equals(ts.getTimer())) + .findFirst(); + assert optTimer.isPresent(); + + if (optTimer.get().periodic()) { + // Periodic -> resets itself: + resetInfo = String.format("%s↦%d", optTimer.get().name(), optTimer.get().initial()); + edgeColor = "cornflowerblue"; + } else { + // One-shot -> resets all in target: + resetInfo = automaton.getSortedTimers(tgt).stream() + .map(t -> String.format("%s↦%d", t.name(), t.initial())) + .sorted() + .collect(Collectors.joining(",")); + edgeColor = "chartreuse3"; + } + } else if (edge.getInput() instanceof NonDelayingInput ndi) { + if (src.equals(tgt) && automaton.isLocalReset(src, ndi)) { + // Self-loop + local reset -> resets all in target: + resetInfo = automaton.getSortedTimers(tgt).stream() + .map(t -> String.format("%s↦%d", t.name(), t.initial())) + .sorted() + .collect(Collectors.joining(",")); + edgeColor = "orange"; + } + } + + if (this.colorEdges && !edgeColor.isBlank()) { + properties.put(EdgeAttrs.COLOR, edgeColor); + properties.put("fontcolor", edgeColor); + } + if (this.includeResets) { + label += " {" + resetInfo + "}"; + } + properties.put(EdgeAttrs.LABEL, label); + + return true; + } +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java new file mode 100644 index 000000000..a7870e9e9 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java @@ -0,0 +1,86 @@ +package net.automatalib.automaton.time.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; + + public MealyTimerInfo(String name, long initial, O output, boolean periodic) { + 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) { + this(name, initial, output, true); + } + + @Override + public String toString() { + return String.format("%s=%d/%s", name, initial, output); + } + + 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; + } + + @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); + } + + @Override + public int hashCode() { + return Objects.hash(name, initial, output); + } + +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java new file mode 100644 index 000000000..e684e55e8 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java @@ -0,0 +1,96 @@ +package net.automatalib.automaton.time.mmlt; + +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; + +public interface MutableLocalTimerMealy { + + /** + * Adds a new location to the MMLT. + * + * @return The newly-added location. + */ + S addState(); + + /** + * Sets the initial location to the provided location. + * + * @param location New initial location + */ + void setInitialState(S location); + + /** + * Adds a transition for a non-delaying input, adding the input + * to the automaton's alphabet if necessary. + * + * @param source Source location + * @param input Non-delaying input symbol + * @param output Output + * @param target Target location + */ + void addTransition(S source, NonDelayingInput input, O output, S target); + + /** + * Removes the transition at the provided non-delaying input. + * No effect if the location has no such transition. + * + * @param source Transition source location + * @param input Transition input + */ + void removeTransition(S source, NonDelayingInput input); + + /** + * 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, NonDelayingInput 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, NonDelayingInput input); +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/StringSymbolCombiner.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/StringSymbolCombiner.java new file mode 100644 index 000000000..7d1991468 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/StringSymbolCombiner.java @@ -0,0 +1,64 @@ +package net.automatalib.automaton.time.mmlt; + +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 extends AbstractSymbolCombiner { + + 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/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java new file mode 100644 index 000000000..e7f1c025e --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java @@ -0,0 +1,210 @@ +package net.automatalib.automaton.time.mmlt.semantics; + +import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.automaton.time.mmlt.MealyTimerInfo; +import net.automatalib.word.Word; +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 LocalTimerMealyConfiguration { + 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 LocalTimerMealyConfiguration(S location, List> sortedTimers) { + this(location, sortedTimers, null); + } + + public LocalTimerMealyConfiguration(S location, List> sortedTimers, Word> locationPrefix) { + 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 LocalTimerMealyConfiguration(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 LocalTimerMealyConfiguration copy() { + return new LocalTimerMealyConfiguration<>(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; + LocalTimerMealyConfiguration that = (LocalTimerMealyConfiguration) o; + return minimumTimerValue == that.minimumTimerValue && entryDistance == that.entryDistance && Objects.equals(location, that.location) && Objects.equals(sortedTimers, that.sortedTimers) && Objects.deepEquals(timerValues, that.timerValues) && Objects.deepEquals(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/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java new file mode 100644 index 000000000..20de8b9e4 --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java @@ -0,0 +1,272 @@ +package net.automatalib.automaton.time.mmlt.semantics; + +import net.automatalib.alphabet.Alphabet; +import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.impl.time.mmlt.*; +import net.automatalib.automaton.time.mmlt.LocalTimerMealy; +import net.automatalib.automaton.time.mmlt.MealyTimerInfo; +import net.automatalib.word.Word; +import net.automatalib.word.WordBuilder; +import org.checkerframework.checker.nullness.qual.NonNull; + +import java.util.List; + +/** + * 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 LocalTimerMealySemantics { + private final LocalTimerMealyConfiguration initialConfiguration; + private final LocalTimerMealy model; + + private final Alphabet> alphabet; + private final LocalTimerMealyOutputSymbol silentOutput; + + /** + * Represents a transition in the semantics automaton ("expanded form") of an MMLT. + * + * @param output Transition output + * @param target Transition target + * @param Location type + * @param Input type + * @param Output type + */ + public record LocalTimerMealySemanticTransition(LocalTimerMealyOutputSymbol output, + LocalTimerMealyConfiguration target) { + + } + + public LocalTimerMealySemantics(LocalTimerMealy model) { + this.model = model; + + var initialLocation = model.getInitialState(); + this.initialConfiguration = new LocalTimerMealyConfiguration<>(initialLocation, model.getSortedTimers(initialLocation)); + + this.alphabet = new GrowingMapAlphabet<>(model.getUntimedAlphabet()); + this.alphabet.add(new TimeoutSymbol<>()); + this.alphabet.add(new TimeStepSymbol<>()); + + this.silentOutput = new LocalTimerMealyOutputSymbol<>(model.getSilentOutput()); + } + + /** + * 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 + */ + public Alphabet> getInputAlphabet() { + return alphabet; + } + + /** + * Returns the symbol used for silent outputs. + * + * @return Silent output symbol + */ + public LocalTimerMealyOutputSymbol getSilentOutput() { + return this.silentOutput; + } + + /** + * Returns the initial configuration of this MMLT. This is a tuple of the + * initial location and its initial timer values. + * + * @return Initial configuration + */ + public LocalTimerMealyConfiguration getInitialConfiguration() { + return this.initialConfiguration; + } + + /** + * Enters the suffix into the provided configuration and returns corresponding outputs. + *

+ * Cannot provide TimeSequences with more than 1 symbol for the suffix, as this might trigger multiple timeouts + * and thus lead to output sequences that are longer than the suffix. + * + * @param configuration Configuration + * @param suffix Suffix inputs + * @return Outputs for the suffix + */ + public Word> computeSuffixOutput(LocalTimerMealyConfiguration configuration, Word> suffix) { + WordBuilder> wbOutput = new WordBuilder<>(); + + var currentConfiguration = configuration; + for (var sym : suffix) { + var trans = getTransition(currentConfiguration, sym); + currentConfiguration = trans.target(); + + if (trans.output() == null) { + throw new IllegalArgumentException("Cannot use time step sequences in suffix that have more than one symbol."); + } + wbOutput.append(trans.output()); + } + + return wbOutput.toWord(); + } + + /** + * Enters the prefix and suffix sequences into the automaton and returns the outputs that occur for the suffixes. + * + * @param prefix Configuration prefix + * @param suffix Suffix inputs + * @return Outputs for the suffix + */ + public Word> computeSuffixOutput(Word> prefix, Word> suffix) { + var prefixConfig = this.traceInputs(prefix); + return computeSuffixOutput(prefixConfig, suffix); + } + + /** + * Traces the provided prefix and returns the reached configuration. + * + * @param prefix Configuration prefix + * @return Reached configuration + */ + public LocalTimerMealyConfiguration traceInputs(Word> prefix) { + var currentConfiguration = getInitialConfiguration().copy(); + for (var sym : prefix) { + currentConfiguration = getTransition(currentConfiguration, sym).target(); + } + return currentConfiguration; + } + + + @NonNull + public LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, ILocalTimerMealySemanticInputSymbol input) { + return getTransition(source, input, Long.MAX_VALUE); + } + + /** + * 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 + */ + @NonNull + public LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, + ILocalTimerMealySemanticInputSymbol input, + long maxWaitingTime) { + var sourceCopy = source.copy(); // we do not want to modify values of the source configuration + + if (input instanceof NonDelayingInput 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; + LocalTimerMealyOutputSymbol lastOutput = null; + long remainingTime = ts.getTimeSteps(); + while (remainingTime > 0) { + var nextTimeoutTrans = getTimeoutTransition(currentConfig, remainingTime); + lastOutput = nextTimeoutTrans.output(); + if (nextTimeoutTrans.output().equals(this.getSilentOutput())) { + // No timer will expire during remaining waiting time: + break; + } else { + remainingTime -= nextTimeoutTrans.output().getDelay(); + currentConfig = nextTimeoutTrans.target(); + } + } + + if (ts.getTimeSteps() > 1) { + lastOutput = null; // ignore multiple outputs + } else { + // Output for single time step includes no delay by definition: + lastOutput = new LocalTimerMealyOutputSymbol<>(lastOutput.getSymbol()); + } + + // Return final target + output: + return new LocalTimerMealySemanticTransition<>(lastOutput, currentConfig); + } else { + throw new IllegalArgumentException("Unknown input symbol type"); + } + } + + private LocalTimerMealySemanticTransition getTimeoutTransition(LocalTimerMealyConfiguration source, long maxWaitingTime) { + LocalTimerMealyConfiguration target; + LocalTimerMealyOutputSymbol 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; + TimerTimeoutSymbol expiringTimerSym = new TimerTimeoutSymbol<>(nextTimeouts.timers().get(0).name()); + + var successor = model.getSuccessor(source.getLocation(), expiringTimerSym); + target = new LocalTimerMealyConfiguration<>(successor, model.getSortedTimers(successor)); + target.resetTimers(); + } + + // Create combined output: + if (nextTimeouts.timers().size() == 1) { + output = new LocalTimerMealyOutputSymbol<>(nextTimeouts.delay(), nextTimeouts.timers().get(0).output()); + } else { + List outputs = nextTimeouts.timers().stream().map(MealyTimerInfo::output).toList(); + O combinedOutput = model.getOutputCombiner().combineSymbols(outputs); + output = new LocalTimerMealyOutputSymbol<>(nextTimeouts.delay(), combinedOutput); + } + } + + return new LocalTimerMealySemanticTransition<>(output, target); + } + + private LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, NonDelayingInput input) { + LocalTimerMealyConfiguration target; + LocalTimerMealyOutputSymbol output; + + var trans = model.getTransition(source.getLocation(), input); + if (trans == null) { // silent self-loop + target = source; + output = this.getSilentOutput(); + } else { + // Identify successor configuration: + if (!trans.successor().equals(source.getLocation())) { + // Change to a different location resets all timers in target: + target = new LocalTimerMealyConfiguration<>(trans.successor(), model.getSortedTimers(trans.successor())); + target.resetTimers(); + } else if (model.isLocalReset(source.getLocation(), input)) { + target = source; + target.resetTimers(); + } else { + target = source; + } + output = new LocalTimerMealyOutputSymbol<>(trans.output()); + } + + // Return output: + return new LocalTimerMealySemanticTransition<>(output, target); + } +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/ReducedLocalTimerMealySemantics.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/ReducedLocalTimerMealySemantics.java new file mode 100644 index 000000000..dbf99f5da --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/ReducedLocalTimerMealySemantics.java @@ -0,0 +1,162 @@ +package net.automatalib.automaton.time.mmlt.semantics; + +import net.automatalib.alphabet.Alphabet; +import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.impl.time.mmlt.LocalTimerMealyOutputSymbol; +import net.automatalib.alphabet.impl.time.mmlt.TimeoutSymbol; +import net.automatalib.automaton.time.mmlt.LocalTimerMealy; +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 ReducedLocalTimerMealySemantics extends CompactMealy, LocalTimerMealyOutputSymbol> { + + private final static Logger logger = LoggerFactory.getLogger(ReducedLocalTimerMealySemantics.class); + + private final Map, Integer> stateMap; + + private ReducedLocalTimerMealySemantics(Alphabet> alphabet) { + super(alphabet); + this.stateMap = new HashMap<>(); + } + + public static ReducedLocalTimerMealySemantics forLocalTimerMealy(LocalTimerMealy automaton) { + // Create alphabet for expanded form: + var alphabet = automaton.getSemantics().getInputAlphabet(); + + ReducedLocalTimerMealySemantics mealy = new ReducedLocalTimerMealySemantics<>(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) + .forEach(c -> mealy.stateMap.put(c, mealy.addState())); + } + + // 1b: Mark initial state: + var initialConfig = automaton.getSemantics().getInitialConfiguration(); + 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 = automaton.getSemantics().getTransition(config, sym); + var output = trans.output(); + + // Try to find matching state. If not found, leave undefined: + int targetId = mealy.stateMap.getOrDefault(trans.target(), -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, + LocalTimerMealy automaton) { + + List> configurations = new ArrayList<>(); + + LocalTimerMealyConfiguration currentConfiguration = new LocalTimerMealyConfiguration<>(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 = automaton.getSemantics().getTransition(currentConfiguration, new TimeoutSymbol<>()); + if (trans.output().equals(automaton.getSemantics().getSilentOutput())) { + break; // no timeout + } + + if (trans.output().getDelay() > 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 (trans.target().isEntryConfig()) { + break; // location change OR repeating behavior + } + configurations.add(trans.target()); + currentConfiguration = trans.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(LocalTimerMealyConfiguration configuration, boolean allowApproximate) { + + LocalTimerMealyConfiguration 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); + } +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java new file mode 100644 index 000000000..53536d31d --- /dev/null +++ b/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java @@ -0,0 +1,22 @@ +package net.automatalib.automaton.time.mmlt.semantics; + +import net.automatalib.automaton.time.mmlt.MealyTimerInfo; + +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/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java b/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java new file mode 100644 index 000000000..acd28675a --- /dev/null +++ b/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java @@ -0,0 +1,231 @@ +package net.automatalib.serialization.dot; + +import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.automaton.time.mmlt.*; +import net.automatalib.common.util.IOUtil; +import net.automatalib.common.util.Pair; +import org.checkerframework.checker.nullness.qual.Nullable; + +import java.io.File; +import java.io.FileInputStream; +import java.io.InputStream; +import java.util.*; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +/** + * 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 LocalTimerMealyGraphvizParser { + + private static final Pattern assignPattern = Pattern.compile("(\\S+)=(\\d+)"); + + public static LocalTimerMealy parseLocalTimerMealy(File path, String silentOutput, AbstractSymbolCombiner outputCombiner) { + InternalDOTParser parser; + try (InputStream r = IOUtil.asUncompressedBufferedInputStream(new FileInputStream(path))) { + parser = new InternalDOTParser(r); + parser.parse(); + } catch (Exception e) { + throw new RuntimeException(String.format("Parsing \"%s\" failed: %n %s", path, e)); + } + return parseLocalTimerMealy(parser, silentOutput, outputCombiner); + } + + private static LocalTimerMealy parseLocalTimerMealy(InternalDOTParser parser, String silentOutput, AbstractSymbolCombiner outputCombiner) { + 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 CompactLocalTimerMealy result = new CompactLocalTimerMealy<>(new GrowingMapAlphabet<>(), silentOutput, outputCombiner); + + // Parse nodes: + for (var node : nodes) { + if (node.id.equals(GraphDOT.initialLabel(0))) { + continue; // initial node marker + } + final int n = result.addState(); + stateMap.put(node.id, n); + + // Parse timers: + if (node.attributes.containsKey("timers")) { + String[] settings = node.attributes.get("timers").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)); + } + + timers.putIfAbsent(node.id, new HashMap<>()); + if (timers.get(node.id).containsKey(timerName)) { + throw new IllegalArgumentException(String.format("Timer %s in location %s must only be set once.", + timerName, node.id)); + } + + // Add timer: + timers.get(node.id).put(timerName, new MealyTimerInfo<>(timerName, value, null)); + } + } else { + timers.put(node.id, Collections.emptyMap()); // no timers in this location + } + } + + // Parse edges: + for (var edge : edges) { + // Parse input/output: + Pair<@Nullable String, @Nullable String> props = DOTParsers.DEFAULT_MEALY_EDGE_PARSER.apply(edge.attributes); + if (props.getFirst() == null || props.getSecond() == null) { + if (edge.src.equals(GraphDOT.initialLabel(0))) { + result.setInitialState(stateMap.get(edge.tgt)); + continue; + } + throw new IllegalArgumentException("All edges must have an input and an output."); + } + + // Check for resets: + HashSet edgeResets = new HashSet<>(); + if (edge.attributes.containsKey("resets")) { + // Parse resets: + for (String timer : edge.attributes.get("resets").split(",")) { + edgeResets.add(timer.strip()); + } + } + + + if (props.getFirst().startsWith("to[")) { + // Ensure that we defined the corresponding timer: + String timerName = props.getFirst().substring(3, props.getFirst().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.", + props.getFirst(), edge.src)); + } + + // Add output to timer info: + MealyTimerInfo oldInfo = timers.get(edge.src).get(timerName); + + // Infer timer type: + var updatedInfo = new MealyTimerInfo<>(timerName, oldInfo.initial(), props.getSecond()); + 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)); + } + } + updatedInfo.setOneShot(); + } + } else { + // No need to check resets on location-change: always resetting all in target + updatedInfo.setOneShot(); + } + + // Add timer to location: + if (updatedInfo.periodic()) { + result.addPeriodicTimer(stateMap.get(edge.src), updatedInfo.name(), updatedInfo.initial(), updatedInfo.output()); + } else { + result.addOneShotTimer(stateMap.get(edge.src), + updatedInfo.name(), updatedInfo.initial(), updatedInfo.output(), + stateMap.get(edge.tgt)); + } + } else { + // Non-delaying input: + var nonDelInput = new NonDelayingInput<>(props.getFirst()); + + result.addTransition(stateMap.get(edge.src), nonDelInput, props.getSecond(), + stateMap.get(edge.tgt)); + + // 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", nonDelInput)); + } + } + result.addLocalReset(stateMap.get(edge.src), nonDelInput); + } + } + } + + // Ensure initial location: + if (result.getInitialState() == null) { + throw new IllegalArgumentException("Automaton must have an initial location."); + } + + return result; + } + +} diff --git a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java new file mode 100644 index 000000000..052d8beae --- /dev/null +++ b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java @@ -0,0 +1,69 @@ +package net.automatalib.util.automaton.cover; + +import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.impl.time.mmlt.TimeoutSymbol; +import net.automatalib.automaton.time.mmlt.LocalTimerMealy; +import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealyConfiguration; +import net.automatalib.word.Word; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +public class LocalTimerMealyCover { + + public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton) { + return getLocalTimerMealyLocationCover(automaton, true); + } + + /** + * Calculates a location cover for an MMLT. + *

+ * The cover provides one prefix for each location of the MMLT. + * The returned prefixes use inputs for the extended semantics. + * If some locations are isolated, they are excluded from the cover. + * + * @param automaton MMLT + * @param allowIncomplete If set, no error is thrown if some locations are unreachable. + * @return Location cover in format location -> prefix. + */ + public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, boolean allowIncomplete) { + Map>> locPrefixes = new HashMap<>(); + Map, Word>> cfgPrefixes = new HashMap<>(); + List> queue = new ArrayList<>(); + + queue.add(automaton.getSemantics().getInitialConfiguration()); + cfgPrefixes.put(automaton.getSemantics().getInitialConfiguration(), Word.epsilon()); + locPrefixes.put(automaton.getInitialState(), Word.epsilon()); + + GrowingMapAlphabet> exploreAlphabet = new GrowingMapAlphabet<>(automaton.getUntimedAlphabet()); + exploreAlphabet.add(new TimeoutSymbol<>()); + + while (!queue.isEmpty()) { + var current = queue.remove(0); + for (var symbol : exploreAlphabet) { + var trans = automaton.getSemantics().getTransition(current, symbol); + if (trans.target().equals(current)) { + continue; // self-loop + } + if (!cfgPrefixes.containsKey(trans.target())) { + var newPrefix = cfgPrefixes.get(current).append(symbol); + cfgPrefixes.put(trans.target(), newPrefix); + queue.add(trans.target()); + + if (trans.target().isEntryConfig()) { + locPrefixes.put(trans.target().getLocation(), newPrefix); + } + } + } + } + + if (!allowIncomplete && locPrefixes.size() != automaton.getStates().size()) { + throw new AssertionError("Incomplete state cover."); + } + + return locPrefixes; + } +} diff --git a/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java new file mode 100644 index 000000000..8b6ce0e4f --- /dev/null +++ b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java @@ -0,0 +1,154 @@ +package net.automatalib.util.automaton.mmlt; + +import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.automaton.time.mmlt.LocalTimerMealy; +import net.automatalib.automaton.time.mmlt.MealyTimerInfo; +import net.automatalib.automaton.time.mmlt.semantics.ReducedLocalTimerMealySemantics; +import net.automatalib.util.automaton.Automata; +import net.automatalib.word.Word; +import org.checkerframework.checker.nullness.qual.Nullable; + +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Collections; +import java.util.List; + +/** + * Provides various functions that are related MMLTs. + */ +public class LocalTimerMealyUtil { + + public static @Nullable Word> findSeparatingWord(LocalTimerMealy modelA, LocalTimerMealy modelB) { + var expandedA = ReducedLocalTimerMealySemantics.forLocalTimerMealy(modelA); + var expandedB = ReducedLocalTimerMealySemantics.forLocalTimerMealy(modelB); + + var separatingWord = Automata.findSeparatingWord(expandedA, expandedB, expandedA.getInputAlphabet()); + + if (separatingWord != null) { + var outputA = modelA.getSemantics().computeSuffixOutput(Word.epsilon(), separatingWord); + var outputB = modelB.getSemantics().computeSuffixOutput(Word.epsilon(), separatingWord); + if (outputA.equals(outputB)) { + throw new AssertionError("Invalid separating word."); + } + } + + return separatingWord; + } + + /** + * Returns the number of configurations for the given location. This is defined as follows: + * - When l has no timers: one + * - When l has a one-shot timer: initial value of this timer + * - When l only has periodic timers: least-common multiple of their initial values + * + * @param automaton Considered automaton + * @param location Considered location + * @param Location type + * @param Input type + * @param Output type + * @return Maximum configuration time. Long.MAX_VALUE, if exceeding integer maximum. + */ + public static long getConfigurationCount(LocalTimerMealy automaton, L location) { + Collection> timers = automaton.getSortedTimers(location); + if (timers.isEmpty()) { + return 1; + } + + // Single timer: take that timer's value: + if (timers.size() == 1) { + return timers.stream().findFirst().get().initial(); + } + + var optOneShot = timers.stream().filter(t -> !t.periodic()).findFirst(); + if (optOneShot.isPresent()) { + return optOneShot.get().initial(); // leave location at latest when one-shot expires + } + + // The lcm of multiple numbers is equal to the product of their multiple with their gcd. + // Therefore: calculate gcd and multiple. Then, divide multiple by gcd. + List bigTimeouts = timers.stream().map(t -> new BigInteger(String.valueOf(t.initial()))).toList(); + + // Calculate gcd of all timeouts: + BigInteger gcd = bigTimeouts.get(0); + BigInteger multiple = bigTimeouts.get(0); + for (int i = 1; i < bigTimeouts.size(); i++) { + gcd = gcd.gcd(bigTimeouts.get(i)); + multiple = multiple.multiply(bigTimeouts.get(i)); + } + BigInteger lcm = multiple.divide(gcd); + + try { + return lcm.longValueExact(); + } catch (ArithmeticException ignored) { + return Long.MAX_VALUE; + } + } + + + /** + * Returns the maximum initial value of all timers. + * + * @return Maximum initial timer value. Zero, if no timers are used. + */ + public static long getMaximumInitialTimerValue(LocalTimerMealy automaton) { + long maxValue = 0; + for (S loc : automaton.getStates()) { + var optMaxInitial = automaton.getSortedTimers(loc).stream().mapToLong(MealyTimerInfo::initial).max(); + if (optMaxInitial.isPresent()) { + maxValue = Math.max(maxValue, optMaxInitial.getAsLong()); + } + } + return maxValue; + } + + /** + * Retrieves the maximum delay to the next timeout in this model. + * + * @return Maximum timeout delay. Is at least one. + */ + public static long getMaximumTimeoutDelay(LocalTimerMealy automaton) { + long maxValue = 1; + + for (S loc : automaton.getStates()) { + var timers = automaton.getSortedTimers(loc); + if (timers.isEmpty()) { + continue; + } + + if (timers.size() == 1) { + maxValue = Math.max(maxValue, timers.stream().findFirst().get().initial()); + continue; + } + + // Get the least common multiple of the initial times: + long lcm = LocalTimerMealyUtil.getConfigurationCount(automaton, loc); + + // Calculate expiration times of all timers: + List timeouts = new ArrayList<>(); + for (var timer : automaton.getSortedTimers(loc)) { + long currentValue = timer.initial(); + while (currentValue < lcm) { + timeouts.add(currentValue); + currentValue += timer.initial(); + } + } + + // Find the largest distance between two successive expirations: + timeouts.add(0L); // need to consider time to first expiration + Collections.sort(timeouts); + long maxDiff = 0; + for (int i = 0; i < timeouts.size() - 1; i++) { + long diff = timeouts.get(i + 1) - timeouts.get(i); + if (diff > maxDiff) { + maxDiff = diff; + } + } + + maxValue = Math.max(maxValue, maxDiff); + } + + return maxValue; + } + +} From 633ff0309ef04b77825d0b92f1f17f87dd8640f1 Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Tue, 7 Oct 2025 14:44:06 +0200 Subject: [PATCH 03/11] Added basic tests for MMLTs; included sample MMLT model file. --- .../automaton/impl/LocalTimerMealyTests.java | 153 +++++++++++++++++ .../LocalTimerMealyDeserializationTest.java | 96 +++++++++++ .../dot/src/test/resources/sensor_mmlt.dot | 26 +++ .../automaton/mmlt/LocalTimerMealyTests.java | 156 ++++++++++++++++++ 4 files changed, 431 insertions(+) create mode 100644 core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java create mode 100644 serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyDeserializationTest.java create mode 100644 serialization/dot/src/test/resources/sensor_mmlt.dot create mode 100644 util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java diff --git a/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java b/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java new file mode 100644 index 000000000..71c8f4f23 --- /dev/null +++ b/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java @@ -0,0 +1,153 @@ +package net.automatalib.automaton.impl; + +import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.impl.time.mmlt.TimeStepSequence; +import net.automatalib.automaton.time.mmlt.CompactLocalTimerMealy; +import net.automatalib.automaton.time.mmlt.StringSymbolCombiner; +import net.automatalib.word.Word; +import org.testng.Assert; +import org.testng.annotations.Test; + + +import java.util.ArrayList; +import java.util.List; +import java.util.Random; + +public class LocalTimerMealyTests { + + public CompactLocalTimerMealy buildBaseModel() { + var symbols = List.of("p1", "p2", "abort", "collect"); + GrowingMapAlphabet> alphabet = new GrowingMapAlphabet<>(); + symbols.forEach(s -> alphabet.add(new NonDelayingInput<>(s))); + + var model = new CompactLocalTimerMealy<>(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, new NonDelayingInput<>("p1"), "go", s1); + model.addTransition(s1, new NonDelayingInput<>("abort"), "ok", s1); + model.addLocalReset(s1, new NonDelayingInput<>("abort")); + + model.addPeriodicTimer(s1, "a", 3, "part"); + model.addPeriodicTimer(s1, "b", 6, "noise"); + model.addOneShotTimer(s1, "c", 40, "done", s3); + + model.addTransition(s0, new NonDelayingInput<>("p2"), "go", s2); + model.addTransition(s2, new NonDelayingInput<>("abort"), "void", s3); + model.addOneShotTimer(s2, "d", 4, "done", s3); + + model.addTransition(s3, new NonDelayingInput<>("collect"), "void", s0); + + 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().traceInputs(Word.fromSymbols( + new NonDelayingInput<>("p1"), new TimeStepSequence<>(12) + )); + Assert.assertFalse(nonStableConfig.isStableConfig()); + Assert.assertFalse(nonStableConfig.isEntryConfig()); + Assert.assertEquals(nonStableConfig.getEntryDistance(), 12); + Assert.assertEquals(nonStableConfig.getLocation().intValue(), 1); + + + var stableConfig = model.getSemantics().traceInputs(Word.fromSymbols( + new NonDelayingInput<>("p1"), new TimeStepSequence<>(2) + )); + Assert.assertTrue(stableConfig.isStableConfig()); + Assert.assertFalse(stableConfig.isEntryConfig()); + Assert.assertEquals(stableConfig.getEntryDistance(), 2); + Assert.assertEquals(stableConfig.getLocation().intValue(), 1); + } + + + @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/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyDeserializationTest.java b/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyDeserializationTest.java new file mode 100644 index 000000000..525518722 --- /dev/null +++ b/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyDeserializationTest.java @@ -0,0 +1,96 @@ +package net.automatalib.serialization.dot; + +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.automaton.time.mmlt.LocalTimerMealy; +import net.automatalib.automaton.time.mmlt.StringSymbolCombiner; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.io.File; + +public class LocalTimerMealyDeserializationTest { + + @Test + public void parseSensorModel() { + // Load a model from file: + var resource = LocalTimerMealyDeserializationTest.class.getResource("/sensor_mmlt.dot"); + + var dotAutomaton = LocalTimerMealyGraphvizParser.parseLocalTimerMealy(new File(resource.getFile()), "void", StringSymbolCombiner.getInstance()); + + // Compare to reference: + var ndiP1 = new NonDelayingInput<>("p1"); + var ndiP2 = new NonDelayingInput<>("p2"); + var ndiAbort = new NonDelayingInput<>("abort"); + var ndiCollect = new NonDelayingInput<>("collect"); + + int s0 = 0; + int s1 = 1; + int s2 = 2; + int s3 = 3; + + // Check non-delaying transitions: + assertSilentLoop(dotAutomaton, s0, ndiAbort); + assertSilentLoop(dotAutomaton, s0, ndiCollect); + assertTransition(dotAutomaton, s0, s1, ndiP1, "go"); + assertTransition(dotAutomaton, s0, s2, ndiP2, "go"); + + assertTransition(dotAutomaton, s1, s1, ndiAbort, "ok"); + Assert.assertTrue(dotAutomaton.isLocalReset(s1, ndiAbort)); + assertSilentLoop(dotAutomaton, s1, ndiP1); + assertSilentLoop(dotAutomaton, s1, ndiP2); + assertSilentLoop(dotAutomaton, s1, ndiCollect); + + assertTransition(dotAutomaton, s2, s3, ndiAbort, "void"); + assertSilentLoop(dotAutomaton, s2, ndiP1); + assertSilentLoop(dotAutomaton, s2, ndiP2); + assertSilentLoop(dotAutomaton, s2, ndiCollect); + + assertSilentLoop(dotAutomaton, s3, ndiAbort); + assertSilentLoop(dotAutomaton, s3, ndiP1); + assertSilentLoop(dotAutomaton, s3, ndiP2); + assertTransition(dotAutomaton, s3, s0, ndiCollect, "void"); + + // Check timers: + Assert.assertTrue(dotAutomaton.getSortedTimers(s0).isEmpty()); + Assert.assertTrue(dotAutomaton.getSortedTimers(s3).isEmpty()); + Assert.assertEquals(dotAutomaton.getSortedTimers(s1).size(), 3); + Assert.assertEquals(dotAutomaton.getSortedTimers(s2).size(), 1); + + var firstTimerS1 = dotAutomaton.getSortedTimers(s1).get(0); + Assert.assertEquals(firstTimerS1.initial(), 3); + Assert.assertEquals(firstTimerS1.output(), "part"); + Assert.assertTrue(firstTimerS1.periodic()); + + var secondTimerS1 = dotAutomaton.getSortedTimers(s1).get(1); + Assert.assertEquals(secondTimerS1.initial(), 6); + Assert.assertEquals(secondTimerS1.output(), "noise"); + Assert.assertTrue(secondTimerS1.periodic()); + + var thirdTimerS1 = dotAutomaton.getSortedTimers(s1).get(2); + Assert.assertEquals(thirdTimerS1.initial(), 40); + Assert.assertEquals(thirdTimerS1.output(), "done"); + Assert.assertFalse(thirdTimerS1.periodic()); + + var firstTimerS2 = dotAutomaton.getSortedTimers(s2).get(0); + Assert.assertEquals(firstTimerS2.initial(), 4); + Assert.assertEquals(firstTimerS2.output(), "done"); + Assert.assertFalse(firstTimerS2.periodic()); + } + + private void assertTransition(LocalTimerMealy model, int state, int target, NonDelayingInput input, String output) { + var trans = model.getTransition(state, input); + if (trans == null || (trans.successor() != target) || !trans.output().equals(output)) { + throw new AssertionError(); + } + } + + private void assertSilentLoop(LocalTimerMealy model, int state, NonDelayingInput input) { + var trans = model.getTransition(state, input); + if (trans != null && (trans.successor() != state || !trans.output().equals("void"))) { + throw new AssertionError(); + } + Assert.assertFalse(model.isLocalReset(state, input)); + } + + +} diff --git a/serialization/dot/src/test/resources/sensor_mmlt.dot b/serialization/dot/src/test/resources/sensor_mmlt.dot new file mode 100644 index 000000000..a6a57caf8 --- /dev/null +++ b/serialization/dot/src/test/resources/sensor_mmlt.dot @@ -0,0 +1,26 @@ +// This is an example for a sensor node. +// p1 starts a normal measurement. part triggers a sensor for particulate matter, noise a sensor for ambient noise. +// p2 performs a self-check. +// Set maximum waiting time = 40 to reproduce bad hypothesis from diss. +digraph g { + s0 [label="L0" timers=""] + s1 [label="L1" timers="a=3,b=6,c=40"] + s2 [label="L2" timers="d=4"] + s3 [label="L3" timers=""] + + s0 -> s1 [label="p1/go"] + + s1 -> s1 [label="abort / ok" resets="a,b,c"] + s1 -> s1 [label="to[a] / part"] + s1 -> s1 [label="to[b] / noise"] + s1 -> s3 [label="to[c] / done"] + + s0 -> s2 [label="p2 / go"] + s2 -> s3 [label="abort / void"] + s2 -> s3 [label="to[d] / done"] + + s3 -> s0 [label="collect / void"] + + __start0 [label="" shape="none" width="0" height="0"]; + __start0 -> s0; +} \ No newline at end of file diff --git a/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java b/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java new file mode 100644 index 000000000..0567f60ad --- /dev/null +++ b/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java @@ -0,0 +1,156 @@ +package net.automatalib.util.automaton.mmlt; + +import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.automaton.time.mmlt.CompactLocalTimerMealy; +import net.automatalib.automaton.time.mmlt.StringSymbolCombiner; +import org.testng.Assert; +import org.testng.annotations.Test; + + +import java.util.List; + +public class LocalTimerMealyTests { + + public CompactLocalTimerMealy buildBaseModel() { + var symbols = List.of("p1", "p2", "abort", "collect"); + GrowingMapAlphabet> alphabet = new GrowingMapAlphabet<>(); + symbols.forEach(s -> alphabet.add(new NonDelayingInput<>(s))); + + var model = new CompactLocalTimerMealy<>(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, new NonDelayingInput<>("p1"), "go", s1); + model.addTransition(s1, new NonDelayingInput<>("abort"), "ok", s1); + model.addLocalReset(s1, new NonDelayingInput<>("abort")); + + model.addPeriodicTimer(s1, "a", 3, "part"); + model.addPeriodicTimer(s1, "b", 6, "noise"); + model.addOneShotTimer(s1, "c", 40, "done", s3); + + model.addTransition(s0, new NonDelayingInput<>("p2"), "go", s2); + model.addTransition(s2, new NonDelayingInput<>("abort"), "void", s3); + model.addOneShotTimer(s2, "d", 4, "done", s3); + + model.addTransition(s3, new NonDelayingInput<>("collect"), "void", s0); + + return model; + } + + @Test + public void testTimerAndResetRemovals() { + var model = buildBaseModel(); + + int s1 = 1; + int s3 = 3; + + // Remove and add some timers: + model.addPeriodicTimer(s1, "e", 12, "test"); + model.removeTimer(s1, "b"); + model.removeTimer(s1, "a"); + model.addPeriodicTimer(s1, "a", 3, "part"); + model.addPeriodicTimer(s1, "b", 6, "noise"); + model.removeTimer(s1, "c"); + model.addOneShotTimer(s1, "c", 40, "done", s3); + model.removeTimer(s1, "e"); + + model.removeLocalReset(s1, new NonDelayingInput<>("abort")); + model.addLocalReset(s1, new NonDelayingInput<>("abort")); + + // Still needs to be equivalent to original: + var originalModel = buildBaseModel(); + Assert.assertNull(LocalTimerMealyUtil.findSeparatingWord(model, originalModel)); + } + + @Test + public void testSeparatedByResetsSimple() { + GrowingMapAlphabet> alphabet = new GrowingMapAlphabet<>(); + alphabet.addSymbol(new NonDelayingInput<>("x")); + + // Same model, but with reset in A and no reset in B: + var modelA = new CompactLocalTimerMealy<>(alphabet, "void", StringSymbolCombiner.getInstance()); + var s0 = modelA.addState(); + modelA.setInitialState(s0); + modelA.addPeriodicTimer(s0, "a", 3, "test"); + modelA.addTransition(s0, new NonDelayingInput<>("x"), "ok", s0); + modelA.addLocalReset(s0, new NonDelayingInput<>("x")); + + var modelB = new CompactLocalTimerMealy<>(alphabet, "void", StringSymbolCombiner.getInstance()); + var s0B = modelB.addState(); + modelB.setInitialState(s0B); + modelB.addPeriodicTimer(s0B, "a", 3, "test"); + modelB.addTransition(s0B, new NonDelayingInput<>("x"), "ok", s0B); + + Assert.assertNotNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB)); + } + + @Test + public void testSeparatedByResetsComplex() { + GrowingMapAlphabet> alphabet = new GrowingMapAlphabet<>(); + alphabet.addSymbol(new NonDelayingInput<>("x")); + + // Same model, but with reset in A and no reset in B: + var modelA = new CompactLocalTimerMealy<>(alphabet, "void", StringSymbolCombiner.getInstance()); + var s0 = modelA.addState(); + var s1 = modelA.addState(); + modelA.setInitialState(s0); + modelA.addPeriodicTimer(s0, "a", 3, "test"); + modelA.addOneShotTimer(s0, "b", 5, "test2", s1); + + var modelB = new CompactLocalTimerMealy<>(alphabet, "void", StringSymbolCombiner.getInstance()); + var s0B = modelB.addState(); + var s1B = modelB.addState(); + var s2B = modelB.addState(); + modelB.setInitialState(s0B); + modelB.addOneShotTimer(s0B, "a", 3, "test", s1B); + modelB.addOneShotTimer(s1B, "b", 2, "test2", s2B); + modelB.addTransition(s1B, new NonDelayingInput<>("x"), "void", s1B); + modelB.addLocalReset(s1B, new NonDelayingInput<>("x")); + + Assert.assertNotNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB)); + } + + + @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) + ); + } +} From 6f51d593f310eea7e0760cb444915d5e113b5bce Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Wed, 8 Oct 2025 08:55:36 +0200 Subject: [PATCH 04/11] Added serialization test for MMLTs. --- ...ionTest.java => LocalTimerMealyTests.java} | 36 +++++++++++++++++-- .../resources/demo_expected_serialized.dot | 20 +++++++++++ .../dot/src/test/resources/demo_mmlt.dot | 20 +++++++++++ 3 files changed, 74 insertions(+), 2 deletions(-) rename serialization/dot/src/test/java/net/automatalib/serialization/dot/{LocalTimerMealyDeserializationTest.java => LocalTimerMealyTests.java} (73%) create mode 100644 serialization/dot/src/test/resources/demo_expected_serialized.dot create mode 100644 serialization/dot/src/test/resources/demo_mmlt.dot diff --git a/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyDeserializationTest.java b/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyTests.java similarity index 73% rename from serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyDeserializationTest.java rename to serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyTests.java index 525518722..8479380c9 100644 --- a/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyDeserializationTest.java +++ b/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyTests.java @@ -7,13 +7,45 @@ import org.testng.annotations.Test; import java.io.File; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.Arrays; +import java.util.List; -public class LocalTimerMealyDeserializationTest { +public class LocalTimerMealyTests { + + @Test + public void parseAndWriteDemoModel() { + var demoResource = LocalTimerMealyTests.class.getResource("/demo_mmlt.dot"); + var expResultPath = Paths.get(LocalTimerMealyTests.class.getResource("/demo_expected_serialized.dot").getPath()); + var demoModel = LocalTimerMealyGraphvizParser.parseLocalTimerMealy(new File(demoResource.getFile()), "void", StringSymbolCombiner.getInstance()); + + + StringBuilder sbOutput = new StringBuilder(); + try { + List expected = Files.readAllLines(expResultPath).stream() + .filter(l -> !l.isBlank() && !l.startsWith("//")) + .map(String::trim) + .toList(); + + GraphDOT.write(demoModel.transitionGraphView(true, true), sbOutput); + var actualData = sbOutput.toString(); + System.out.println(actualData); + List actual = Arrays.stream(actualData.split("\\n")) + .filter(l -> !l.isBlank()) + .map(String::trim) + .toList(); + + Assert.assertEquals(expected, actual); + } catch (Exception ex) { + throw new AssertionError(); + } + } @Test public void parseSensorModel() { // Load a model from file: - var resource = LocalTimerMealyDeserializationTest.class.getResource("/sensor_mmlt.dot"); + var resource = LocalTimerMealyTests.class.getResource("/sensor_mmlt.dot"); var dotAutomaton = LocalTimerMealyGraphvizParser.parseLocalTimerMealy(new File(resource.getFile()), "void", StringSymbolCombiner.getInstance()); diff --git a/serialization/dot/src/test/resources/demo_expected_serialized.dot b/serialization/dot/src/test/resources/demo_expected_serialized.dot new file mode 100644 index 000000000..b7cbf2684 --- /dev/null +++ b/serialization/dot/src/test/resources/demo_expected_serialized.dot @@ -0,0 +1,20 @@ +// Resulting model that is expected when deserializing demo_mmlt.gv first, and then +// serializing the result with edge coloring and reset information enabled. +digraph g { + + s0 [timers="a=2" shape="circle" label="0"]; + s1 [timers="b=4,c=6" shape="circle" label="1"]; + s2 [timers="d=2,e=3" shape="circle" label="2"]; + s0 -> s1 [color="chartreuse3" fontcolor="chartreuse3" label="to[a] / A {b↦4,c↦6}"]; + s1 -> s1 [color="cornflowerblue" fontcolor="cornflowerblue" label="to[b] / B {b↦4}"]; + s1 -> s1 [color="chartreuse3" fontcolor="chartreuse3" label="to[c] / C {b↦4,c↦6}"]; + s1 -> s2 [label="x / void {}"]; + s1 -> s1 [color="orange" fontcolor="orange" label="y / Y {b↦4,c↦6}"]; + s2 -> s2 [color="cornflowerblue" fontcolor="cornflowerblue" label="to[d] / D {d↦2}"]; + s2 -> s2 [color="cornflowerblue" fontcolor="cornflowerblue" label="to[e] / E {e↦3}"]; + s2 -> s2 [label="y / D {}"]; + +__start0 [label="" shape="none" width="0" height="0"]; +__start0 -> s0; + +} \ No newline at end of file diff --git a/serialization/dot/src/test/resources/demo_mmlt.dot b/serialization/dot/src/test/resources/demo_mmlt.dot new file mode 100644 index 000000000..d657df7bf --- /dev/null +++ b/serialization/dot/src/test/resources/demo_mmlt.dot @@ -0,0 +1,20 @@ +// This file demonstrates several MMLT features +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 local reset + s2 -> s2 [label="y / D"] // loop without reset + + __start0 [label="" shape="none" width="0" height="0"]; + __start0 -> s0; +} \ No newline at end of file From 4c7657e991b2db52963828fc60f3dc837e7cf2fa Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Wed, 8 Oct 2025 16:34:28 +0200 Subject: [PATCH 05/11] Separated more files into API and implementation to enable use from LearnLib. --- api/src/main/java/module-info.java | 3 + .../mmlt/ILocalTimerMealyInputSymbol.java | 2 +- .../ILocalTimerMealySemanticInputSymbol.java | 2 +- .../mmlt/LocalTimerMealyOutputSymbol.java | 2 +- .../alphabet}/time/mmlt/NonDelayingInput.java | 2 +- .../alphabet}/time/mmlt/TimeStepSequence.java | 2 +- .../alphabet}/time/mmlt/TimeStepSymbol.java | 2 +- .../alphabet}/time/mmlt/TimeoutSymbol.java | 2 +- .../time/mmlt/TimerTimeoutSymbol.java | 2 +- .../time/mmlt/AbstractSymbolCombiner.java | 0 .../automaton/time/mmlt/LocalTimerMealy.java | 8 +- .../LocalTimerMealyVisualizationHelper.java | 6 +- .../automaton/time/mmlt/MealyTimerInfo.java | 0 .../time/mmlt/MutableLocalTimerMealy.java | 2 +- .../LocalTimerMealyConfiguration.java | 2 +- .../LocalTimerMealySemanticTransition.java | 17 +++ .../semantics/LocalTimerMealySemantics.java | 97 +++++++++++++++++ .../time/mmlt/semantics/TimeoutPair.java | 0 core/src/main/java/module-info.java | 4 +- .../mmlt/CompactLocalTimerMealy.java | 18 +++- .../mmlt}/LocalTimerMealySemantics.java | 100 +++++------------- .../ReducedLocalTimerMealySemantics.java | 9 +- .../{ => impl}/mmlt/StringSymbolCombiner.java | 4 +- .../automaton/impl/LocalTimerMealyTests.java | 8 +- .../dot/LocalTimerMealyGraphvizParser.java | 3 +- .../dot/LocalTimerMealyTests.java | 4 +- .../automaton/cover/LocalTimerMealyCover.java | 4 +- .../automaton/mmlt/LocalTimerMealyUtil.java | 4 +- .../automaton/mmlt/LocalTimerMealyTests.java | 6 +- 29 files changed, 195 insertions(+), 120 deletions(-) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/ILocalTimerMealyInputSymbol.java (73%) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/ILocalTimerMealySemanticInputSymbol.java (76%) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/LocalTimerMealyOutputSymbol.java (96%) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/NonDelayingInput.java (94%) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/TimeStepSequence.java (96%) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/TimeStepSymbol.java (80%) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/TimeoutSymbol.java (90%) rename {core/src/main/java/net/automatalib/alphabet/impl => api/src/main/java/net/automatalib/alphabet}/time/mmlt/TimerTimeoutSymbol.java (95%) rename {core => api}/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java (100%) rename {core => api}/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java (96%) rename {core => api}/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java (95%) rename {core => api}/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java (100%) rename {core => api}/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java (98%) rename {core => api}/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java (98%) create mode 100644 api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemanticTransition.java create mode 100644 api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java rename {core => api}/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java (100%) rename core/src/main/java/net/automatalib/automaton/time/{ => impl}/mmlt/CompactLocalTimerMealy.java (92%) rename core/src/main/java/net/automatalib/automaton/time/{mmlt/semantics => impl/mmlt}/LocalTimerMealySemantics.java (73%) rename core/src/main/java/net/automatalib/automaton/time/{mmlt/semantics => impl/mmlt}/ReducedLocalTimerMealySemantics.java (95%) rename core/src/main/java/net/automatalib/automaton/time/{ => impl}/mmlt/StringSymbolCombiner.java (93%) diff --git a/api/src/main/java/module-info.java b/api/src/main/java/module-info.java index dadb03ec7..4d5caf8c4 100644 --- a/api/src/main/java/module-info.java +++ b/api/src/main/java/module-info.java @@ -70,6 +70,9 @@ exports net.automatalib.ts.simple; exports net.automatalib.visualization; exports net.automatalib.word; + exports net.automatalib.alphabet.time.mmlt; + exports net.automatalib.automaton.time.mmlt.semantics; + exports net.automatalib.automaton.time.mmlt; uses VisualizationProvider; } diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealyInputSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealyInputSymbol.java similarity index 73% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealyInputSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealyInputSymbol.java index 796cf1439..71cd30f07 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealyInputSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealyInputSymbol.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; /** * Base type for input symbols for the structural automaton of an MMLT. diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealySemanticInputSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealySemanticInputSymbol.java similarity index 76% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealySemanticInputSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealySemanticInputSymbol.java index cd5618440..add92a233 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/ILocalTimerMealySemanticInputSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealySemanticInputSymbol.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; /** * Base class for an input for the semantics automaton of some MMLT. diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/LocalTimerMealyOutputSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealyOutputSymbol.java similarity index 96% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/LocalTimerMealyOutputSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealyOutputSymbol.java index 8bdf590a4..a73aadb25 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/LocalTimerMealyOutputSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealyOutputSymbol.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; import org.checkerframework.checker.nullness.qual.NonNull; diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/NonDelayingInput.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/NonDelayingInput.java similarity index 94% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/NonDelayingInput.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/NonDelayingInput.java index 74a903b33..a16ae1189 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/NonDelayingInput.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/NonDelayingInput.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; import org.checkerframework.checker.nullness.qual.NonNull; diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSequence.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSequence.java similarity index 96% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSequence.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSequence.java index cc78c5e49..ff7f18268 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSequence.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSequence.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; import java.util.Objects; diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSymbol.java similarity index 80% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSymbol.java index 8978a7866..c5a78e8d8 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeStepSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSymbol.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; /** * Input for the semantics automaton: delay for a single time step. diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeoutSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeoutSymbol.java similarity index 90% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeoutSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeoutSymbol.java index 65bde2880..46307ed45 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimeoutSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeoutSymbol.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; import java.util.Objects; diff --git a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimerTimeoutSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimerTimeoutSymbol.java similarity index 95% rename from core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimerTimeoutSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/TimerTimeoutSymbol.java index eebd606dd..1caec3a57 100644 --- a/core/src/main/java/net/automatalib/alphabet/impl/time/mmlt/TimerTimeoutSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimerTimeoutSymbol.java @@ -1,4 +1,4 @@ -package net.automatalib.alphabet.impl.time.mmlt; +package net.automatalib.alphabet.time.mmlt; import java.util.Objects; diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java similarity index 100% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java rename to api/src/main/java/net/automatalib/automaton/time/mmlt/AbstractSymbolCombiner.java diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java similarity index 96% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java rename to api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java index 783d8b74c..9401c3310 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java @@ -1,8 +1,8 @@ package net.automatalib.automaton.time.mmlt; import net.automatalib.alphabet.Alphabet; -import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealyInputSymbol; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; import net.automatalib.automaton.UniversalDeterministicAutomaton; import net.automatalib.automaton.graph.TransitionEdge; import net.automatalib.automaton.graph.UniversalAutomatonGraphView; @@ -110,9 +110,7 @@ default S getSuccessor(LocalTimerMealyTransition transition) { * * @return Semantics automaton */ - default LocalTimerMealySemantics getSemantics() { - return new LocalTimerMealySemantics<>(this); - } + LocalTimerMealySemantics getSemantics(); // ======================================= diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java similarity index 95% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java rename to api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java index d793ed2a4..57db24f54 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java @@ -1,8 +1,8 @@ package net.automatalib.automaton.time.mmlt; -import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealyInputSymbol; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; -import net.automatalib.alphabet.impl.time.mmlt.TimerTimeoutSymbol; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.TimerTimeoutSymbol; import net.automatalib.automaton.graph.TransitionEdge; import net.automatalib.automaton.visualization.AutomatonVisualizationHelper; diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java similarity index 100% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java rename to api/src/main/java/net/automatalib/automaton/time/mmlt/MealyTimerInfo.java diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java similarity index 98% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java rename to api/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java index e684e55e8..445566288 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/MutableLocalTimerMealy.java @@ -1,6 +1,6 @@ package net.automatalib.automaton.time.mmlt; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; public interface MutableLocalTimerMealy { diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java similarity index 98% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java rename to api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java index e7f1c025e..a1a712876 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java @@ -1,6 +1,6 @@ package net.automatalib.automaton.time.mmlt.semantics; -import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; import net.automatalib.automaton.time.mmlt.MealyTimerInfo; import net.automatalib.word.Word; import org.checkerframework.checker.nullness.qual.Nullable; diff --git a/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemanticTransition.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemanticTransition.java new file mode 100644 index 000000000..58e8235b2 --- /dev/null +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemanticTransition.java @@ -0,0 +1,17 @@ +package net.automatalib.automaton.time.mmlt.semantics; + +import net.automatalib.alphabet.time.mmlt.LocalTimerMealyOutputSymbol; + +/** + * Represents a transition in the semantics automaton ("expanded form") of an MMLT. + * + * @param output Transition output + * @param target Transition target + * @param Location type + * @param Input type for non-delaying inputs + * @param Output symbol type + */ +public record LocalTimerMealySemanticTransition(LocalTimerMealyOutputSymbol output, + LocalTimerMealyConfiguration target) { + +} diff --git a/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java new file mode 100644 index 000000000..2a7b7ffb0 --- /dev/null +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java @@ -0,0 +1,97 @@ +package net.automatalib.automaton.time.mmlt.semantics; + +import net.automatalib.alphabet.Alphabet; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealyOutputSymbol; +import net.automatalib.word.Word; +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 interface LocalTimerMealySemantics { + /** + * 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 + */ + LocalTimerMealyOutputSymbol getSilentOutput(); + + /** + * Returns the initial configuration of this MMLT. This is a tuple of the + * initial location and its initial timer values. + * + * @return Initial configuration + */ + LocalTimerMealyConfiguration getInitialConfiguration(); + + /** + * Enters the suffix into the provided configuration and returns corresponding outputs. + *

+ * Cannot provide TimeSequences with more than 1 symbol for the suffix, as this might trigger multiple timeouts + * and thus lead to output sequences that are longer than the suffix. + * + * @param configuration Configuration + * @param suffix Suffix inputs + * @return Outputs for the suffix + */ + Word> computeSuffixOutput(LocalTimerMealyConfiguration configuration, Word> suffix); + + /** + * Enters the prefix and suffix sequences into the automaton and returns the outputs that occur for the suffixes. + * + * @param prefix Configuration prefix + * @param suffix Suffix inputs + * @return Outputs for the suffix + */ + Word> computeSuffixOutput(Word> prefix, Word> suffix); + + /** + * Traces the provided prefix and returns the reached configuration. + * + * @param prefix Configuration prefix + * @return Reached configuration + */ + LocalTimerMealyConfiguration traceInputs(Word> prefix); + + @NonNull + LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, ILocalTimerMealySemanticInputSymbol input); + + /** + * 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 + */ + @NonNull + LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, + ILocalTimerMealySemanticInputSymbol input, + long maxWaitingTime); +} diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java similarity index 100% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java rename to api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/TimeoutPair.java diff --git a/core/src/main/java/module-info.java b/core/src/main/java/module-info.java index ab59cfb7a..07e6b9bab 100644 --- a/core/src/main/java/module-info.java +++ b/core/src/main/java/module-info.java @@ -52,7 +52,5 @@ exports net.automatalib.ts.modal.impl; exports net.automatalib.ts.modal.transition.impl; exports net.automatalib.ts.powerset.impl; - exports net.automatalib.alphabet.impl.time.mmlt; - exports net.automatalib.automaton.time.mmlt.semantics; - exports net.automatalib.automaton.time.mmlt; + exports net.automatalib.automaton.time.impl.mmlt; } diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/CompactLocalTimerMealy.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/CompactLocalTimerMealy.java similarity index 92% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/CompactLocalTimerMealy.java rename to core/src/main/java/net/automatalib/automaton/time/impl/mmlt/CompactLocalTimerMealy.java index 6cf601ce1..ffdaf11da 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/CompactLocalTimerMealy.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/CompactLocalTimerMealy.java @@ -1,11 +1,16 @@ -package net.automatalib.automaton.time.mmlt; +package net.automatalib.automaton.time.impl.mmlt; import net.automatalib.alphabet.Alphabet; import net.automatalib.alphabet.GrowingAlphabet; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealyInputSymbol; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; -import net.automatalib.alphabet.impl.time.mmlt.TimerTimeoutSymbol; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.TimerTimeoutSymbol; +import net.automatalib.automaton.time.mmlt.AbstractSymbolCombiner; +import net.automatalib.automaton.time.mmlt.LocalTimerMealy; +import net.automatalib.automaton.time.mmlt.MealyTimerInfo; +import net.automatalib.automaton.time.mmlt.MutableLocalTimerMealy; +import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealySemantics; import net.automatalib.automaton.transducer.impl.CompactMealy; import org.checkerframework.checker.nullness.qual.Nullable; @@ -85,6 +90,11 @@ public List> getSortedTimers(Integer location) { return Collections.unmodifiableList(this.sortedTimers.getOrDefault(location, Collections.emptyList())); } + @Override + public LocalTimerMealySemantics getSemantics() { + return new net.automatalib.automaton.time.impl.mmlt.LocalTimerMealySemantics<>(this); + } + @Override public Collection getStates() { return automaton.getStates(); diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/LocalTimerMealySemantics.java similarity index 73% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java rename to core/src/main/java/net/automatalib/automaton/time/impl/mmlt/LocalTimerMealySemantics.java index 20de8b9e4..4dc52b622 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/LocalTimerMealySemantics.java @@ -1,10 +1,12 @@ -package net.automatalib.automaton.time.mmlt.semantics; +package net.automatalib.automaton.time.impl.mmlt; import net.automatalib.alphabet.Alphabet; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.impl.time.mmlt.*; +import net.automatalib.alphabet.time.mmlt.*; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; import net.automatalib.automaton.time.mmlt.MealyTimerInfo; +import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealyConfiguration; +import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealySemanticTransition; import net.automatalib.word.Word; import net.automatalib.word.WordBuilder; import org.checkerframework.checker.nullness.qual.NonNull; @@ -26,27 +28,13 @@ * @param Input type for non-delaying inputs * @param Output type of the MMLT */ -public class LocalTimerMealySemantics { +public class LocalTimerMealySemantics implements net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealySemantics { private final LocalTimerMealyConfiguration initialConfiguration; private final LocalTimerMealy model; private final Alphabet> alphabet; private final LocalTimerMealyOutputSymbol silentOutput; - /** - * Represents a transition in the semantics automaton ("expanded form") of an MMLT. - * - * @param output Transition output - * @param target Transition target - * @param Location type - * @param Input type - * @param Output type - */ - public record LocalTimerMealySemanticTransition(LocalTimerMealyOutputSymbol output, - LocalTimerMealyConfiguration target) { - - } - public LocalTimerMealySemantics(LocalTimerMealy model) { this.model = model; @@ -60,45 +48,26 @@ public LocalTimerMealySemantics(LocalTimerMealy model) { this.silentOutput = new LocalTimerMealyOutputSymbol<>(model.getSilentOutput()); } - /** - * 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 - */ + + @Override public Alphabet> getInputAlphabet() { return alphabet; } - /** - * Returns the symbol used for silent outputs. - * - * @return Silent output symbol - */ + + @Override public LocalTimerMealyOutputSymbol getSilentOutput() { return this.silentOutput; } - /** - * Returns the initial configuration of this MMLT. This is a tuple of the - * initial location and its initial timer values. - * - * @return Initial configuration - */ + + @Override public LocalTimerMealyConfiguration getInitialConfiguration() { return this.initialConfiguration; } - /** - * Enters the suffix into the provided configuration and returns corresponding outputs. - *

- * Cannot provide TimeSequences with more than 1 symbol for the suffix, as this might trigger multiple timeouts - * and thus lead to output sequences that are longer than the suffix. - * - * @param configuration Configuration - * @param suffix Suffix inputs - * @return Outputs for the suffix - */ + + @Override public Word> computeSuffixOutput(LocalTimerMealyConfiguration configuration, Word> suffix) { WordBuilder> wbOutput = new WordBuilder<>(); @@ -116,24 +85,15 @@ public Word> computeSuffixOutput(LocalTimerMealyC return wbOutput.toWord(); } - /** - * Enters the prefix and suffix sequences into the automaton and returns the outputs that occur for the suffixes. - * - * @param prefix Configuration prefix - * @param suffix Suffix inputs - * @return Outputs for the suffix - */ + + @Override public Word> computeSuffixOutput(Word> prefix, Word> suffix) { var prefixConfig = this.traceInputs(prefix); return computeSuffixOutput(prefixConfig, suffix); } - /** - * Traces the provided prefix and returns the reached configuration. - * - * @param prefix Configuration prefix - * @return Reached configuration - */ + + @Override public LocalTimerMealyConfiguration traceInputs(Word> prefix) { var currentConfiguration = getInitialConfiguration().copy(); for (var sym : prefix) { @@ -143,28 +103,16 @@ public LocalTimerMealyConfiguration traceInputs(Word getTransition(LocalTimerMealyConfiguration source, ILocalTimerMealySemanticInputSymbol input) { + @Override + public @NonNull LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, ILocalTimerMealySemanticInputSymbol input) { return getTransition(source, input, Long.MAX_VALUE); } - /** - * 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 - */ - @NonNull - public LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, - ILocalTimerMealySemanticInputSymbol input, - long maxWaitingTime) { + + @Override + public @NonNull LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, + ILocalTimerMealySemanticInputSymbol input, + long maxWaitingTime) { var sourceCopy = source.copy(); // we do not want to modify values of the source configuration if (input instanceof NonDelayingInput ndi) { diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/ReducedLocalTimerMealySemantics.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java similarity index 95% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/ReducedLocalTimerMealySemantics.java rename to core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java index dbf99f5da..7508eb520 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/semantics/ReducedLocalTimerMealySemantics.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java @@ -1,10 +1,11 @@ -package net.automatalib.automaton.time.mmlt.semantics; +package net.automatalib.automaton.time.impl.mmlt; import net.automatalib.alphabet.Alphabet; -import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; -import net.automatalib.alphabet.impl.time.mmlt.LocalTimerMealyOutputSymbol; -import net.automatalib.alphabet.impl.time.mmlt.TimeoutSymbol; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealyOutputSymbol; +import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; +import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealyConfiguration; import net.automatalib.automaton.transducer.impl.CompactMealy; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/core/src/main/java/net/automatalib/automaton/time/mmlt/StringSymbolCombiner.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/StringSymbolCombiner.java similarity index 93% rename from core/src/main/java/net/automatalib/automaton/time/mmlt/StringSymbolCombiner.java rename to core/src/main/java/net/automatalib/automaton/time/impl/mmlt/StringSymbolCombiner.java index 7d1991468..1157e118a 100644 --- a/core/src/main/java/net/automatalib/automaton/time/mmlt/StringSymbolCombiner.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/StringSymbolCombiner.java @@ -1,4 +1,6 @@ -package net.automatalib.automaton.time.mmlt; +package net.automatalib.automaton.time.impl.mmlt; + +import net.automatalib.automaton.time.mmlt.AbstractSymbolCombiner; import java.util.Arrays; import java.util.HashSet; diff --git a/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java b/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java index 71c8f4f23..c3f167fa5 100644 --- a/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java +++ b/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java @@ -1,10 +1,10 @@ package net.automatalib.automaton.impl; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; -import net.automatalib.alphabet.impl.time.mmlt.TimeStepSequence; -import net.automatalib.automaton.time.mmlt.CompactLocalTimerMealy; -import net.automatalib.automaton.time.mmlt.StringSymbolCombiner; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.TimeStepSequence; +import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy; +import net.automatalib.automaton.time.impl.mmlt.StringSymbolCombiner; import net.automatalib.word.Word; import org.testng.Assert; import org.testng.annotations.Test; diff --git a/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java b/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java index acd28675a..f3478cb25 100644 --- a/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java +++ b/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java @@ -1,7 +1,8 @@ package net.automatalib.serialization.dot; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; +import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy; import net.automatalib.automaton.time.mmlt.*; import net.automatalib.common.util.IOUtil; import net.automatalib.common.util.Pair; diff --git a/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyTests.java b/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyTests.java index 8479380c9..0a443814b 100644 --- a/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyTests.java +++ b/serialization/dot/src/test/java/net/automatalib/serialization/dot/LocalTimerMealyTests.java @@ -1,8 +1,8 @@ package net.automatalib.serialization.dot; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; -import net.automatalib.automaton.time.mmlt.StringSymbolCombiner; +import net.automatalib.automaton.time.impl.mmlt.StringSymbolCombiner; import org.testng.Assert; import org.testng.annotations.Test; diff --git a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java index 052d8beae..697ffdf14 100644 --- a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java +++ b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java @@ -1,8 +1,8 @@ package net.automatalib.util.automaton.cover; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; -import net.automatalib.alphabet.impl.time.mmlt.TimeoutSymbol; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealyConfiguration; import net.automatalib.word.Word; diff --git a/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java index 8b6ce0e4f..9eed88701 100644 --- a/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java +++ b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java @@ -1,9 +1,9 @@ package net.automatalib.util.automaton.mmlt; -import net.automatalib.alphabet.impl.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; import net.automatalib.automaton.time.mmlt.MealyTimerInfo; -import net.automatalib.automaton.time.mmlt.semantics.ReducedLocalTimerMealySemantics; +import net.automatalib.automaton.time.impl.mmlt.ReducedLocalTimerMealySemantics; import net.automatalib.util.automaton.Automata; import net.automatalib.word.Word; import org.checkerframework.checker.nullness.qual.Nullable; diff --git a/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java b/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java index 0567f60ad..3289db674 100644 --- a/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java +++ b/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java @@ -1,9 +1,9 @@ package net.automatalib.util.automaton.mmlt; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.impl.time.mmlt.NonDelayingInput; -import net.automatalib.automaton.time.mmlt.CompactLocalTimerMealy; -import net.automatalib.automaton.time.mmlt.StringSymbolCombiner; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; +import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy; +import net.automatalib.automaton.time.impl.mmlt.StringSymbolCombiner; import org.testng.Assert; import org.testng.annotations.Test; From d9311cc2f8a18ee024ae58a70e8bd842c0fb1b60 Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Thu, 9 Oct 2025 11:28:38 +0200 Subject: [PATCH 06/11] Removed I prefix for some interfaces for the MMLT automaton. --- ...l.java => LocalTimerMealyInputSymbol.java} | 2 +- ...> LocalTimerMealySemanticInputSymbol.java} | 4 ++-- .../alphabet/time/mmlt/NonDelayingInput.java | 2 +- .../alphabet/time/mmlt/TimeStepSequence.java | 2 +- .../alphabet/time/mmlt/TimeoutSymbol.java | 2 +- .../time/mmlt/TimerTimeoutSymbol.java | 2 +- .../automaton/time/mmlt/LocalTimerMealy.java | 24 +++++++++---------- .../LocalTimerMealyVisualizationHelper.java | 6 ++--- .../LocalTimerMealyConfiguration.java | 4 ++-- .../semantics/LocalTimerMealySemantics.java | 14 +++++------ .../impl/mmlt/CompactLocalTimerMealy.java | 10 ++++---- .../impl/mmlt/LocalTimerMealySemantics.java | 14 +++++------ .../mmlt/ReducedLocalTimerMealySemantics.java | 6 ++--- util/src/main/java/module-info.java | 1 + .../automaton/cover/LocalTimerMealyCover.java | 12 +++++----- .../automaton/mmlt/LocalTimerMealyUtil.java | 4 ++-- 16 files changed, 55 insertions(+), 54 deletions(-) rename api/src/main/java/net/automatalib/alphabet/time/mmlt/{ILocalTimerMealyInputSymbol.java => LocalTimerMealyInputSymbol.java} (71%) rename api/src/main/java/net/automatalib/alphabet/time/mmlt/{ILocalTimerMealySemanticInputSymbol.java => LocalTimerMealySemanticInputSymbol.java} (64%) diff --git a/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealyInputSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealyInputSymbol.java similarity index 71% rename from api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealyInputSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealyInputSymbol.java index 71cd30f07..4843139f0 100644 --- a/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealyInputSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealyInputSymbol.java @@ -3,5 +3,5 @@ /** * Base type for input symbols for the structural automaton of an MMLT. */ -public interface ILocalTimerMealyInputSymbol { +public interface LocalTimerMealyInputSymbol { } diff --git a/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealySemanticInputSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealySemanticInputSymbol.java similarity index 64% rename from api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealySemanticInputSymbol.java rename to api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealySemanticInputSymbol.java index add92a233..294583de0 100644 --- a/api/src/main/java/net/automatalib/alphabet/time/mmlt/ILocalTimerMealySemanticInputSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/LocalTimerMealySemanticInputSymbol.java @@ -3,8 +3,8 @@ /** * Base class for an input for the semantics automaton of some MMLT. * - * @param + * @param */ -public interface ILocalTimerMealySemanticInputSymbol { +public interface LocalTimerMealySemanticInputSymbol { } diff --git a/api/src/main/java/net/automatalib/alphabet/time/mmlt/NonDelayingInput.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/NonDelayingInput.java index a16ae1189..594fed52e 100644 --- a/api/src/main/java/net/automatalib/alphabet/time/mmlt/NonDelayingInput.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/NonDelayingInput.java @@ -9,7 +9,7 @@ * * @param */ -public class NonDelayingInput implements ILocalTimerMealySemanticInputSymbol, ILocalTimerMealyInputSymbol { +public class NonDelayingInput implements LocalTimerMealySemanticInputSymbol, LocalTimerMealyInputSymbol { private final U symbol; public NonDelayingInput(@NonNull U input) { diff --git a/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSequence.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSequence.java index ff7f18268..ad4f50b72 100644 --- a/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSequence.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeStepSequence.java @@ -5,7 +5,7 @@ /** * Convenience type for aggregating multiple subsequent time steps. */ -public class TimeStepSequence implements ILocalTimerMealySemanticInputSymbol { +public class TimeStepSequence implements LocalTimerMealySemanticInputSymbol { private long timeSteps; diff --git a/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeoutSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeoutSymbol.java index 46307ed45..a7a789d94 100644 --- a/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeoutSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimeoutSymbol.java @@ -5,7 +5,7 @@ /** * Symbolic input for the semantics automaton: causes a delay until the next timeout. */ -public class TimeoutSymbol implements ILocalTimerMealySemanticInputSymbol { +public class TimeoutSymbol implements LocalTimerMealySemanticInputSymbol { @Override public String toString() { diff --git a/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimerTimeoutSymbol.java b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimerTimeoutSymbol.java index 1caec3a57..22f90d57b 100644 --- a/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimerTimeoutSymbol.java +++ b/api/src/main/java/net/automatalib/alphabet/time/mmlt/TimerTimeoutSymbol.java @@ -10,7 +10,7 @@ * * @param */ -public class TimerTimeoutSymbol implements ILocalTimerMealyInputSymbol { +public class TimerTimeoutSymbol implements LocalTimerMealyInputSymbol { private final String timer; public TimerTimeoutSymbol(String timer) { diff --git a/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java index 9401c3310..1ebd06503 100644 --- a/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealy.java @@ -1,7 +1,7 @@ package net.automatalib.automaton.time.mmlt; import net.automatalib.alphabet.Alphabet; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealyInputSymbol; import net.automatalib.alphabet.time.mmlt.NonDelayingInput; import net.automatalib.automaton.UniversalDeterministicAutomaton; import net.automatalib.automaton.graph.TransitionEdge; @@ -40,7 +40,7 @@ * @param Input type for non-delaying inputs * @param Output symbol type */ -public interface LocalTimerMealy extends UniversalDeterministicAutomaton, LocalTimerMealy.LocalTimerMealyTransition, Void, O> { +public interface LocalTimerMealy extends UniversalDeterministicAutomaton, LocalTimerMealy.LocalTimerMealyTransition, Void, O> { record LocalTimerMealyTransition(@NonNull S successor, @NonNull O output) { @@ -68,7 +68,7 @@ record LocalTimerMealyTransition(@NonNull S successor, @NonNull O output) * * @return Input alphabet */ - Alphabet> getInputAlphabet(); + Alphabet> getInputAlphabet(); /** * Retrieves the non-delaying inputs for this automaton. @@ -115,15 +115,15 @@ default S getSuccessor(LocalTimerMealyTransition transition) { // ======================================= @Override - default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView(Collection> inputs) { + default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView(Collection> inputs) { return new LocalTimerMealyGraphView<>(this, inputs, false, false); } - default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView() { + default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView() { return this.transitionGraphView(getInputAlphabet()); } - default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView(boolean colorEdges, boolean includeResets) { + default UniversalGraph, LocalTimerMealyTransition>, Void, TransitionEdge.Property, O>> transitionGraphView(boolean colorEdges, boolean includeResets) { return new LocalTimerMealyGraphView<>(this, getInputAlphabet(), colorEdges, includeResets); } @@ -136,32 +136,32 @@ default Void getStateProperty(S state) { // We do not want to provide tracing abilities for inputs of the structure automaton: @Override - default Set getStates(Iterable> input) { + default Set getStates(Iterable> input) { throw new IllegalStateException("Not supported. Use the semantics automaton to trace inputs."); } @Override @Nullable - default S getSuccessor(S state, Iterable> input) { + default S getSuccessor(S state, Iterable> input) { throw new IllegalStateException("Not supported. Use the semantics automaton to trace inputs."); } @Override @Nullable - default S getState(Iterable> input) { + default S getState(Iterable> input) { throw new IllegalStateException("Not supported. Use the semantics automaton to trace inputs."); } // ======================================= class LocalTimerMealyGraphView extends - UniversalAutomatonGraphView, LocalTimerMealy.LocalTimerMealyTransition, Void, OX, LocalTimerMealy> { + UniversalAutomatonGraphView, LocalTimerMealy.LocalTimerMealyTransition, Void, OX, LocalTimerMealy> { private final boolean colorEdges; private final boolean includeResets; public LocalTimerMealyGraphView(LocalTimerMealy automaton, - Collection> inputs, + Collection> inputs, boolean colorEdges, boolean includeResets) { super(automaton, inputs); this.colorEdges = colorEdges; @@ -169,7 +169,7 @@ public LocalTimerMealyGraphView(LocalTimerMealy automaton, } @Override - public VisualizationHelper, LocalTimerMealyTransition>> getVisualizationHelper() { + public VisualizationHelper, LocalTimerMealyTransition>> getVisualizationHelper() { return new LocalTimerMealyVisualizationHelper<>(automaton, colorEdges, includeResets); } } diff --git a/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java index 57db24f54..9ece20559 100644 --- a/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/LocalTimerMealyVisualizationHelper.java @@ -1,6 +1,6 @@ package net.automatalib.automaton.time.mmlt; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealyInputSymbol; import net.automatalib.alphabet.time.mmlt.NonDelayingInput; import net.automatalib.alphabet.time.mmlt.TimerTimeoutSymbol; import net.automatalib.automaton.graph.TransitionEdge; @@ -10,7 +10,7 @@ import java.util.stream.Collectors; class LocalTimerMealyVisualizationHelper extends - AutomatonVisualizationHelper, LocalTimerMealy.LocalTimerMealyTransition, LocalTimerMealy> { + AutomatonVisualizationHelper, LocalTimerMealy.LocalTimerMealyTransition, LocalTimerMealy> { private final boolean colorEdges; private final boolean includeResets; @@ -52,7 +52,7 @@ public boolean getNodeProperties(S node, Map properties) { @Override public boolean getEdgeProperties(S src, - TransitionEdge, LocalTimerMealy.LocalTimerMealyTransition> edge, + TransitionEdge, LocalTimerMealy.LocalTimerMealyTransition> edge, S tgt, Map properties) { super.getEdgeProperties(src, edge, tgt, properties); diff --git a/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java index a1a712876..93867cdcc 100644 --- a/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealyConfiguration.java @@ -1,6 +1,6 @@ package net.automatalib.automaton.time.mmlt.semantics; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; import net.automatalib.automaton.time.mmlt.MealyTimerInfo; import net.automatalib.word.Word; import org.checkerframework.checker.nullness.qual.Nullable; @@ -34,7 +34,7 @@ public LocalTimerMealyConfiguration(S location, List> sortedTi this(location, sortedTimers, null); } - public LocalTimerMealyConfiguration(S location, List> sortedTimers, Word> locationPrefix) { + public LocalTimerMealyConfiguration(S location, List> sortedTimers, Word> locationPrefix) { this.location = location; this.sortedTimers = sortedTimers; diff --git a/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java index 2a7b7ffb0..94fc66985 100644 --- a/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java +++ b/api/src/main/java/net/automatalib/automaton/time/mmlt/semantics/LocalTimerMealySemantics.java @@ -1,7 +1,7 @@ package net.automatalib.automaton.time.mmlt.semantics; import net.automatalib.alphabet.Alphabet; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; import net.automatalib.alphabet.time.mmlt.LocalTimerMealyOutputSymbol; import net.automatalib.word.Word; import org.checkerframework.checker.nullness.qual.NonNull; @@ -28,7 +28,7 @@ public interface LocalTimerMealySemantics { * * @return Input alphabet */ - Alphabet> getInputAlphabet(); + Alphabet> getInputAlphabet(); /** * Returns the symbol used for silent outputs. @@ -55,7 +55,7 @@ public interface LocalTimerMealySemantics { * @param suffix Suffix inputs * @return Outputs for the suffix */ - Word> computeSuffixOutput(LocalTimerMealyConfiguration configuration, Word> suffix); + Word> computeSuffixOutput(LocalTimerMealyConfiguration configuration, Word> suffix); /** * Enters the prefix and suffix sequences into the automaton and returns the outputs that occur for the suffixes. @@ -64,7 +64,7 @@ public interface LocalTimerMealySemantics { * @param suffix Suffix inputs * @return Outputs for the suffix */ - Word> computeSuffixOutput(Word> prefix, Word> suffix); + Word> computeSuffixOutput(Word> prefix, Word> suffix); /** * Traces the provided prefix and returns the reached configuration. @@ -72,10 +72,10 @@ public interface LocalTimerMealySemantics { * @param prefix Configuration prefix * @return Reached configuration */ - LocalTimerMealyConfiguration traceInputs(Word> prefix); + LocalTimerMealyConfiguration traceInputs(Word> prefix); @NonNull - LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, ILocalTimerMealySemanticInputSymbol input); + LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, LocalTimerMealySemanticInputSymbol input); /** * Retrieves the transition in the semantics automaton that has the provided input and source configuration. @@ -92,6 +92,6 @@ public interface LocalTimerMealySemantics { */ @NonNull LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, - ILocalTimerMealySemanticInputSymbol input, + LocalTimerMealySemanticInputSymbol input, long maxWaitingTime); } diff --git a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/CompactLocalTimerMealy.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/CompactLocalTimerMealy.java index ffdaf11da..049015026 100644 --- a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/CompactLocalTimerMealy.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/CompactLocalTimerMealy.java @@ -3,7 +3,7 @@ import net.automatalib.alphabet.Alphabet; import net.automatalib.alphabet.GrowingAlphabet; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealyInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealyInputSymbol; import net.automatalib.alphabet.time.mmlt.NonDelayingInput; import net.automatalib.alphabet.time.mmlt.TimerTimeoutSymbol; import net.automatalib.automaton.time.mmlt.AbstractSymbolCombiner; @@ -24,7 +24,7 @@ * @param Output symbol type */ public class CompactLocalTimerMealy implements LocalTimerMealy, MutableLocalTimerMealy { - private final CompactMealy, O> automaton; + private final CompactMealy, O> automaton; private final Map>> sortedTimers; // location -> (sorted timers) private final Map>> resets; // location -> inputs (that reset all timers) @@ -54,7 +54,7 @@ public CompactLocalTimerMealy(Collection> nonDelayingInputs, this.outputCombiner = outputCombiner; // Prepare compact Mealy: - GrowingMapAlphabet> inputAlphabet = new GrowingMapAlphabet<>(); + GrowingMapAlphabet> inputAlphabet = new GrowingMapAlphabet<>(); inputAlphabet.addAll(nonDelayingInputs); this.automaton = new CompactMealy<>(inputAlphabet); } @@ -71,7 +71,7 @@ public AbstractSymbolCombiner getOutputCombiner() { } @Override - public Alphabet> getInputAlphabet() { + public Alphabet> getInputAlphabet() { return this.automaton.getInputAlphabet(); } @@ -101,7 +101,7 @@ public Collection getStates() { } @Override - public @Nullable LocalTimerMealyTransition getTransition(Integer location, ILocalTimerMealyInputSymbol input) { + public @Nullable LocalTimerMealyTransition getTransition(Integer location, LocalTimerMealyInputSymbol input) { var trans = this.automaton.getTransition(location, input); if (trans == null) { return null; diff --git a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/LocalTimerMealySemantics.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/LocalTimerMealySemantics.java index 4dc52b622..e7411b296 100644 --- a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/LocalTimerMealySemantics.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/LocalTimerMealySemantics.java @@ -32,7 +32,7 @@ public class LocalTimerMealySemantics implements net.automatalib.automa private final LocalTimerMealyConfiguration initialConfiguration; private final LocalTimerMealy model; - private final Alphabet> alphabet; + private final Alphabet> alphabet; private final LocalTimerMealyOutputSymbol silentOutput; public LocalTimerMealySemantics(LocalTimerMealy model) { @@ -50,7 +50,7 @@ public LocalTimerMealySemantics(LocalTimerMealy model) { @Override - public Alphabet> getInputAlphabet() { + public Alphabet> getInputAlphabet() { return alphabet; } @@ -68,7 +68,7 @@ public LocalTimerMealyConfiguration getInitialConfiguration() { @Override - public Word> computeSuffixOutput(LocalTimerMealyConfiguration configuration, Word> suffix) { + public Word> computeSuffixOutput(LocalTimerMealyConfiguration configuration, Word> suffix) { WordBuilder> wbOutput = new WordBuilder<>(); var currentConfiguration = configuration; @@ -87,14 +87,14 @@ public Word> computeSuffixOutput(LocalTimerMealyC @Override - public Word> computeSuffixOutput(Word> prefix, Word> suffix) { + public Word> computeSuffixOutput(Word> prefix, Word> suffix) { var prefixConfig = this.traceInputs(prefix); return computeSuffixOutput(prefixConfig, suffix); } @Override - public LocalTimerMealyConfiguration traceInputs(Word> prefix) { + public LocalTimerMealyConfiguration traceInputs(Word> prefix) { var currentConfiguration = getInitialConfiguration().copy(); for (var sym : prefix) { currentConfiguration = getTransition(currentConfiguration, sym).target(); @@ -104,14 +104,14 @@ public LocalTimerMealyConfiguration traceInputs(Word getTransition(LocalTimerMealyConfiguration source, ILocalTimerMealySemanticInputSymbol input) { + public @NonNull LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, LocalTimerMealySemanticInputSymbol input) { return getTransition(source, input, Long.MAX_VALUE); } @Override public @NonNull LocalTimerMealySemanticTransition getTransition(LocalTimerMealyConfiguration source, - ILocalTimerMealySemanticInputSymbol input, + LocalTimerMealySemanticInputSymbol input, long maxWaitingTime) { var sourceCopy = source.copy(); // we do not want to modify values of the source configuration diff --git a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java index 7508eb520..096dd9ab8 100644 --- a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java @@ -1,7 +1,7 @@ package net.automatalib.automaton.time.impl.mmlt; import net.automatalib.alphabet.Alphabet; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; import net.automatalib.alphabet.time.mmlt.LocalTimerMealyOutputSymbol; import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; @@ -28,13 +28,13 @@ * @param Input type for non-delaying inputs * @param Output symbol type */ -public class ReducedLocalTimerMealySemantics extends CompactMealy, LocalTimerMealyOutputSymbol> { +public class ReducedLocalTimerMealySemantics extends CompactMealy, LocalTimerMealyOutputSymbol> { private final static Logger logger = LoggerFactory.getLogger(ReducedLocalTimerMealySemantics.class); private final Map, Integer> stateMap; - private ReducedLocalTimerMealySemantics(Alphabet> alphabet) { + private ReducedLocalTimerMealySemantics(Alphabet> alphabet) { super(alphabet); this.stateMap = new HashMap<>(); } diff --git a/util/src/main/java/module-info.java b/util/src/main/java/module-info.java index 61e6fba30..7139d86e4 100644 --- a/util/src/main/java/module-info.java +++ b/util/src/main/java/module-info.java @@ -70,4 +70,5 @@ exports net.automatalib.util.ts.modal; exports net.automatalib.util.ts.transducer; exports net.automatalib.util.ts.traversal; + exports net.automatalib.util.automaton.mmlt; } diff --git a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java index 697ffdf14..4ab017300 100644 --- a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java +++ b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java @@ -1,7 +1,7 @@ package net.automatalib.util.automaton.cover; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealyConfiguration; @@ -14,7 +14,7 @@ public class LocalTimerMealyCover { - public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton) { + public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton) { return getLocalTimerMealyLocationCover(automaton, true); } @@ -29,16 +29,16 @@ public static Map>> get * @param allowIncomplete If set, no error is thrown if some locations are unreachable. * @return Location cover in format location -> prefix. */ - public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, boolean allowIncomplete) { - Map>> locPrefixes = new HashMap<>(); - Map, Word>> cfgPrefixes = new HashMap<>(); + public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, boolean allowIncomplete) { + Map>> locPrefixes = new HashMap<>(); + Map, Word>> cfgPrefixes = new HashMap<>(); List> queue = new ArrayList<>(); queue.add(automaton.getSemantics().getInitialConfiguration()); cfgPrefixes.put(automaton.getSemantics().getInitialConfiguration(), Word.epsilon()); locPrefixes.put(automaton.getInitialState(), Word.epsilon()); - GrowingMapAlphabet> exploreAlphabet = new GrowingMapAlphabet<>(automaton.getUntimedAlphabet()); + GrowingMapAlphabet> exploreAlphabet = new GrowingMapAlphabet<>(automaton.getUntimedAlphabet()); exploreAlphabet.add(new TimeoutSymbol<>()); while (!queue.isEmpty()) { diff --git a/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java index 9eed88701..a71d7fa74 100644 --- a/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java +++ b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java @@ -1,6 +1,6 @@ package net.automatalib.util.automaton.mmlt; -import net.automatalib.alphabet.time.mmlt.ILocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; import net.automatalib.automaton.time.mmlt.MealyTimerInfo; import net.automatalib.automaton.time.impl.mmlt.ReducedLocalTimerMealySemantics; @@ -19,7 +19,7 @@ */ public class LocalTimerMealyUtil { - public static @Nullable Word> findSeparatingWord(LocalTimerMealy modelA, LocalTimerMealy modelB) { + public static @Nullable Word> findSeparatingWord(LocalTimerMealy modelA, LocalTimerMealy modelB) { var expandedA = ReducedLocalTimerMealySemantics.forLocalTimerMealy(modelA); var expandedB = ReducedLocalTimerMealySemantics.forLocalTimerMealy(modelB); From e33c012b65b17cb7912e07b0e3afaadabff367b1 Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Fri, 10 Oct 2025 08:52:37 +0200 Subject: [PATCH 07/11] Updated calculation of MMLT location cover to accept a list of inputs to be considered. --- .../automaton/cover/LocalTimerMealyCover.java | 23 ++--- .../cover/LocalTimerMealyCoverTest.java | 91 +++++++++++++++++++ 2 files changed, 100 insertions(+), 14 deletions(-) create mode 100644 util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java diff --git a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java index 4ab017300..ff4a0780a 100644 --- a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java +++ b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java @@ -1,35 +1,33 @@ package net.automatalib.util.automaton.cover; -import net.automatalib.alphabet.impl.GrowingMapAlphabet; import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; -import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealyConfiguration; import net.automatalib.word.Word; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; +import java.util.*; public class LocalTimerMealyCover { - public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton) { - return getLocalTimerMealyLocationCover(automaton, true); + public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, Collection> inputs) { + return getLocalTimerMealyLocationCover(automaton, inputs, true); } /** * Calculates a location cover for an MMLT. *

* The cover provides one prefix for each location of the MMLT. - * The returned prefixes use inputs for the extended semantics. + * The returned prefixes use only the provided inputs. + *

* If some locations are isolated, they are excluded from the cover. + * If some locations cannot be reached with the provided inputs, they are also excluded. * * @param automaton MMLT + * @param inputs The inputs to use when calculating the cover. Must be an ordered collection. * @param allowIncomplete If set, no error is thrown if some locations are unreachable. * @return Location cover in format location -> prefix. */ - public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, boolean allowIncomplete) { + public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, Collection> inputs, boolean allowIncomplete) { Map>> locPrefixes = new HashMap<>(); Map, Word>> cfgPrefixes = new HashMap<>(); List> queue = new ArrayList<>(); @@ -38,12 +36,9 @@ public static Map>> getL cfgPrefixes.put(automaton.getSemantics().getInitialConfiguration(), Word.epsilon()); locPrefixes.put(automaton.getInitialState(), Word.epsilon()); - GrowingMapAlphabet> exploreAlphabet = new GrowingMapAlphabet<>(automaton.getUntimedAlphabet()); - exploreAlphabet.add(new TimeoutSymbol<>()); - while (!queue.isEmpty()) { var current = queue.remove(0); - for (var symbol : exploreAlphabet) { + for (var symbol : inputs) { var trans = automaton.getSemantics().getTransition(current, symbol); if (trans.target().equals(current)) { continue; // self-loop diff --git a/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java b/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java new file mode 100644 index 000000000..75f35a0b6 --- /dev/null +++ b/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java @@ -0,0 +1,91 @@ +package net.automatalib.util.automaton.cover; + +import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; +import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy; +import net.automatalib.automaton.time.impl.mmlt.StringSymbolCombiner; +import org.testng.Assert; +import org.testng.annotations.Test; + +import java.util.List; + +@Test +public class LocalTimerMealyCoverTest { + private CompactLocalTimerMealy buildBaseModel() { + var symbols = List.of("p1", "p2", "abort", "collect"); + GrowingMapAlphabet> alphabet = new GrowingMapAlphabet<>(); + symbols.forEach(s -> alphabet.add(new NonDelayingInput<>(s))); + + var model = new CompactLocalTimerMealy<>(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, new NonDelayingInput<>("p1"), "go", s1); + model.addTransition(s1, new NonDelayingInput<>("abort"), "ok", s1); + model.addLocalReset(s1, new NonDelayingInput<>("abort")); + + model.addPeriodicTimer(s1, "a", 3, "part"); + model.addPeriodicTimer(s1, "b", 6, "noise"); + model.addOneShotTimer(s1, "c", 40, "done", s3); + + model.addTransition(s0, new NonDelayingInput<>("p2"), "go", s2); + model.addTransition(s2, new NonDelayingInput<>("abort"), "void", s3); + model.addOneShotTimer(s2, "d", 4, "done", s3); + + model.addTransition(s3, new NonDelayingInput<>("collect"), "void", s0); + + return model; + } + + @Test + public void computeFullCover() { + var automaton = buildBaseModel(); + var cover = LocalTimerMealyCover.getLocalTimerMealyLocationCover(automaton, automaton.getSemantics().getInputAlphabet()); + + // Verify that all states are covered: + Assert.assertEquals(cover.size(), automaton.size()); + for (var state : automaton.getStates()) { + Assert.assertTrue(cover.containsKey(state)); + } + + // Verify that the assigned prefixes are correct: + for (var entry : cover.entrySet()) { + var targetConfig = automaton.getSemantics().traceInputs(entry.getValue()); + Assert.assertTrue(targetConfig.isEntryConfig()); + Assert.assertEquals(targetConfig.getLocation(), entry.getKey()); + } + } + + @Test + public void computeIncompleteCover() { + var automaton = buildBaseModel(); + + // Create alphabet where state 3 is unreachable: + var symbols = List.of("p1", "p2", "collect"); + GrowingMapAlphabet> partialAlphabet = new GrowingMapAlphabet<>(); + symbols.forEach(s -> partialAlphabet.add(new NonDelayingInput<>(s))); + + // Test if detecting incomplete cover: + Assert.assertThrows(AssertionError.class, () -> LocalTimerMealyCover.getLocalTimerMealyLocationCover(automaton, partialAlphabet, false)); + + // Verify that state 3 is not covered: + var cover = LocalTimerMealyCover.getLocalTimerMealyLocationCover(automaton, partialAlphabet); + Assert.assertTrue(cover.size() < automaton.size()); + for (var state : automaton.getStates()) { + if (state != 3) { + Assert.assertTrue(cover.containsKey(state)); + } else { + Assert.assertFalse(cover.containsKey(state)); + } + } + + } + +} From a0e713c316578437cedff47c87c09cb1c1075d04 Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Fri, 10 Oct 2025 08:58:10 +0200 Subject: [PATCH 08/11] Method for finding a separating word in an MMLT now considers a provided collection of inputs. --- .../automaton/mmlt/LocalTimerMealyUtil.java | 5 +++-- .../automaton/mmlt/LocalTimerMealyTests.java | 19 ++++++++++++++++--- 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java index a71d7fa74..1679ae4b1 100644 --- a/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java +++ b/util/src/main/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyUtil.java @@ -19,11 +19,12 @@ */ public class LocalTimerMealyUtil { - public static @Nullable Word> findSeparatingWord(LocalTimerMealy modelA, LocalTimerMealy modelB) { + public static @Nullable Word> findSeparatingWord(LocalTimerMealy modelA, LocalTimerMealy modelB, + Collection> inputs) { var expandedA = ReducedLocalTimerMealySemantics.forLocalTimerMealy(modelA); var expandedB = ReducedLocalTimerMealySemantics.forLocalTimerMealy(modelB); - var separatingWord = Automata.findSeparatingWord(expandedA, expandedB, expandedA.getInputAlphabet()); + var separatingWord = Automata.findSeparatingWord(expandedA, expandedB, inputs); if (separatingWord != null) { var outputA = modelA.getSemantics().computeSuffixOutput(Word.epsilon(), separatingWord); diff --git a/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java b/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java index 3289db674..15c1ddc67 100644 --- a/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java +++ b/util/src/test/java/net/automatalib/util/automaton/mmlt/LocalTimerMealyTests.java @@ -1,13 +1,16 @@ package net.automatalib.util.automaton.mmlt; import net.automatalib.alphabet.impl.GrowingMapAlphabet; +import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; import net.automatalib.alphabet.time.mmlt.NonDelayingInput; +import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy; import net.automatalib.automaton.time.impl.mmlt.StringSymbolCombiner; import org.testng.Assert; import org.testng.annotations.Test; +import java.util.ArrayList; import java.util.List; public class LocalTimerMealyTests { @@ -65,7 +68,7 @@ public void testTimerAndResetRemovals() { // Still needs to be equivalent to original: var originalModel = buildBaseModel(); - Assert.assertNull(LocalTimerMealyUtil.findSeparatingWord(model, originalModel)); + Assert.assertNull(LocalTimerMealyUtil.findSeparatingWord(model, originalModel, originalModel.getSemantics().getInputAlphabet())); } @Test @@ -87,7 +90,12 @@ public void testSeparatedByResetsSimple() { modelB.addPeriodicTimer(s0B, "a", 3, "test"); modelB.addTransition(s0B, new NonDelayingInput<>("x"), "ok", s0B); - Assert.assertNotNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB)); + Assert.assertNotNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB, modelA.getSemantics().getInputAlphabet())); + + // If we remove the timestep, should not find a counterexample: + List> reducedInputs = new ArrayList<>(modelA.getUntimedAlphabet()); + reducedInputs.add(new TimeoutSymbol<>()); + Assert.assertNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB, reducedInputs)); } @Test @@ -113,7 +121,12 @@ public void testSeparatedByResetsComplex() { modelB.addTransition(s1B, new NonDelayingInput<>("x"), "void", s1B); modelB.addLocalReset(s1B, new NonDelayingInput<>("x")); - Assert.assertNotNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB)); + Assert.assertNotNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB, modelA.getSemantics().getInputAlphabet())); + + // If we remove the timestep, should not find a counterexample: + List> reducedInputs = new ArrayList<>(modelA.getUntimedAlphabet()); + reducedInputs.add(new TimeoutSymbol<>()); + Assert.assertNull(LocalTimerMealyUtil.findSeparatingWord(modelA, modelB, reducedInputs)); } From c14653dd3adbf32e6d5d4df028771a862a40b62b Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Fri, 10 Oct 2025 09:20:27 +0200 Subject: [PATCH 09/11] Convenience flag for faster location cover calculation. --- .../automaton/cover/LocalTimerMealyCover.java | 15 +++++++++++++-- .../automaton/cover/LocalTimerMealyCoverTest.java | 2 +- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java index ff4a0780a..b0e6deacd 100644 --- a/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java +++ b/util/src/main/java/net/automatalib/util/automaton/cover/LocalTimerMealyCover.java @@ -1,6 +1,8 @@ package net.automatalib.util.automaton.cover; import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; +import net.automatalib.alphabet.time.mmlt.TimeStepSequence; +import net.automatalib.alphabet.time.mmlt.TimeStepSymbol; import net.automatalib.automaton.time.mmlt.LocalTimerMealy; import net.automatalib.automaton.time.mmlt.semantics.LocalTimerMealyConfiguration; import net.automatalib.word.Word; @@ -10,7 +12,7 @@ public class LocalTimerMealyCover { public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, Collection> inputs) { - return getLocalTimerMealyLocationCover(automaton, inputs, true); + return getLocalTimerMealyLocationCover(automaton, inputs, true, true); } /** @@ -18,16 +20,21 @@ public static Map>> getL *

* The cover provides one prefix for each location of the MMLT. * The returned prefixes use only the provided inputs. + * Time steps are not needed to calculate a full cover. If set, they are ignored when calculating the cover, + * even if they are part of the provided inputs. *

* If some locations are isolated, they are excluded from the cover. * If some locations cannot be reached with the provided inputs, they are also excluded. * * @param automaton MMLT * @param inputs The inputs to use when calculating the cover. Must be an ordered collection. + * @param ignoreTimeStep If this option is set, time steps are ignored when calculating the cover, + * even if they are part of the provided inputs. This is a convenience option for not having to + * create a separate alphabet when calculating location covers. * @param allowIncomplete If set, no error is thrown if some locations are unreachable. * @return Location cover in format location -> prefix. */ - public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, Collection> inputs, boolean allowIncomplete) { + public static Map>> getLocalTimerMealyLocationCover(LocalTimerMealy automaton, Collection> inputs, boolean ignoreTimeStep, boolean allowIncomplete) { Map>> locPrefixes = new HashMap<>(); Map, Word>> cfgPrefixes = new HashMap<>(); List> queue = new ArrayList<>(); @@ -39,6 +46,10 @@ public static Map>> getL while (!queue.isEmpty()) { var current = queue.remove(0); for (var symbol : inputs) { + if (symbol instanceof TimeStepSequence) { + continue; + } + var trans = automaton.getSemantics().getTransition(current, symbol); if (trans.target().equals(current)) { continue; // self-loop diff --git a/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java b/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java index 75f35a0b6..f3d5f567e 100644 --- a/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java +++ b/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java @@ -73,7 +73,7 @@ public void computeIncompleteCover() { symbols.forEach(s -> partialAlphabet.add(new NonDelayingInput<>(s))); // Test if detecting incomplete cover: - Assert.assertThrows(AssertionError.class, () -> LocalTimerMealyCover.getLocalTimerMealyLocationCover(automaton, partialAlphabet, false)); + Assert.assertThrows(AssertionError.class, () -> LocalTimerMealyCover.getLocalTimerMealyLocationCover(automaton, partialAlphabet, true, false)); // Verify that state 3 is not covered: var cover = LocalTimerMealyCover.getLocalTimerMealyLocationCover(automaton, partialAlphabet); From 985aee6d5009683fdbeeb5f5c744918be03b3a78 Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Fri, 10 Oct 2025 09:58:23 +0200 Subject: [PATCH 10/11] Added more tests for the reduced semantics. --- .../mmlt/ReducedLocalTimerMealySemantics.java | 15 +++++ .../automaton/impl/LocalTimerMealyTests.java | 59 ++++++++++++++++++- .../cover/LocalTimerMealyCoverTest.java | 1 - 3 files changed, 72 insertions(+), 3 deletions(-) diff --git a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java index 096dd9ab8..28ed120f9 100644 --- a/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java +++ b/core/src/main/java/net/automatalib/automaton/time/impl/mmlt/ReducedLocalTimerMealySemantics.java @@ -160,4 +160,19 @@ public Integer getStateForConfiguration(LocalTimerMealyConfiguration co 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 LocalTimerMealyConfiguration 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/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java b/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java index c3f167fa5..43f6cab24 100644 --- a/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java +++ b/core/src/test/java/net/automatalib/automaton/impl/LocalTimerMealyTests.java @@ -1,9 +1,9 @@ package net.automatalib.automaton.impl; import net.automatalib.alphabet.impl.GrowingMapAlphabet; -import net.automatalib.alphabet.time.mmlt.NonDelayingInput; -import net.automatalib.alphabet.time.mmlt.TimeStepSequence; +import net.automatalib.alphabet.time.mmlt.*; import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy; +import net.automatalib.automaton.time.impl.mmlt.ReducedLocalTimerMealySemantics; import net.automatalib.automaton.time.impl.mmlt.StringSymbolCombiner; import net.automatalib.word.Word; import org.testng.Assert; @@ -113,6 +113,61 @@ public void testConfigurationProperties() { Assert.assertEquals(stableConfig.getLocation().intValue(), 1); } + @Test + public void testReducedSemanticsIncludedConfiguration() { + var automaton = buildBaseModel(); + var reducedSemanticsModel = ReducedLocalTimerMealySemantics.forLocalTimerMealy(automaton); + Assert.assertEquals(reducedSemanticsModel.size(), 31); + + // Reachable in both automata: + Word> includedConfigPrefix = Word.fromSymbols( + new NonDelayingInput<>("p1"), new TimeoutSymbol<>(), new TimeoutSymbol<>(), new TimeoutSymbol<>(), + new TimeoutSymbol<>(), new TimeoutSymbol<>(), new TimeoutSymbol<>(), new TimeStepSymbol<>() + ); + var includedConfig = automaton.getSemantics().traceInputs(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 = ReducedLocalTimerMealySemantics.forLocalTimerMealy(automaton); + Assert.assertEquals(reducedSemanticsModel.size(), 31); + + // Only reachable via at least two following time steps: + Word> omittedConfigPrefix = Word.fromSymbols( + new NonDelayingInput<>("p1"), new TimeoutSymbol<>(), new TimeoutSymbol<>(), + new TimeStepSymbol<>(), new TimeStepSymbol<>() + ); + var omittedConfig = automaton.getSemantics().traceInputs(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: + 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() { diff --git a/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java b/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java index f3d5f567e..51cca14ee 100644 --- a/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java +++ b/util/src/test/java/net/automatalib/util/automaton/cover/LocalTimerMealyCoverTest.java @@ -3,7 +3,6 @@ import net.automatalib.alphabet.impl.GrowingMapAlphabet; import net.automatalib.alphabet.time.mmlt.LocalTimerMealySemanticInputSymbol; import net.automatalib.alphabet.time.mmlt.NonDelayingInput; -import net.automatalib.alphabet.time.mmlt.TimeoutSymbol; import net.automatalib.automaton.time.impl.mmlt.CompactLocalTimerMealy; import net.automatalib.automaton.time.impl.mmlt.StringSymbolCombiner; import org.testng.Assert; From 9afd4fac89002a95fc7562dc5332d15666807970 Mon Sep 17 00:00:00 2001 From: Paul Kogel Date: Mon, 13 Oct 2025 13:32:59 +0200 Subject: [PATCH 11/11] Parser for MMLTs now accepts an input stream, in addition to a file. --- .../dot/LocalTimerMealyGraphvizParser.java | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java b/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java index f3478cb25..5fe9c6398 100644 --- a/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java +++ b/serialization/dot/src/main/java/net/automatalib/serialization/dot/LocalTimerMealyGraphvizParser.java @@ -6,6 +6,7 @@ import net.automatalib.automaton.time.mmlt.*; import net.automatalib.common.util.IOUtil; import net.automatalib.common.util.Pair; +import net.automatalib.exception.FormatException; import org.checkerframework.checker.nullness.qual.Nullable; import java.io.File; @@ -81,6 +82,17 @@ public class LocalTimerMealyGraphvizParser { private static final Pattern assignPattern = Pattern.compile("(\\S+)=(\\d+)"); + public static LocalTimerMealy parseLocalTimerMealy(InputStream stream, String silentOutput, AbstractSymbolCombiner outputCombiner) { + InternalDOTParser parser; + try { + parser = new InternalDOTParser(stream); + parser.parse(); + } catch (FormatException fe) { + throw new RuntimeException(String.format("Parsing failed: %s", fe)); + } + return parseLocalTimerMealy(parser, silentOutput, outputCombiner); + } + public static LocalTimerMealy parseLocalTimerMealy(File path, String silentOutput, AbstractSymbolCombiner outputCombiner) { InternalDOTParser parser; try (InputStream r = IOUtil.asUncompressedBufferedInputStream(new FileInputStream(path))) {