Distinguish between structural and semantic interpretations of automata

CHANGELOG.md

@@ -9,6 +9,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ### Added
 
 * A new formalism for *Mealy machines with local timers* (MMLTs) including means for conformance testing and equivalence checking has been added (thanks to [Paul Kogel](https://github.com/pdev55)).
+* With the introduction of `MMLT`s which are finite-state systems structurally but infinite-state systems semantically, AutomataLib now more rigorously distinguishes between these two concepts by introducing (and at some points requiring) specific `{Finite,}Semantics` types. For automaton types that are inherently finite-state (e.g., `DFA`s, `MealyMachine`s, etc.), this should not require any refactoring.
 * Added a new `automata-serialization-mata` module for serializing (explicit) NFAs in the `.mata` format as used by the [mata library](https://github.com/VeriFIT/mata).
 * `automata-modelchecking-m3c` now supports ARM-based macOS systems.
 * `automata-modelchecking-m3c` can now be included in jlink images.
@@ -21,14 +22,17 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ### Changed
 
 * AutomataLib now requires Java 17 at runtime.
-* The following classes have been refactored to `record`s:
-  * `BricsTransitionProperty`
-  * `TransitionEdge{,.Property}`
-  * `ProbabilisticOutput`
-  * `LTSminVersion`
-* The following class hierarchies have been made `sealed`:
-  * `CommonAttrs`
-  * `CommonStyles`
+  * The following classes have been refactored to `record`s:
+    * `BricsTransitionProperty`
+    * `TransitionEdge{,.Property}`
+    * `ProbabilisticOutput`
+    * `LTSminVersion`
+  * The following class hierarchies have been made `sealed`:
+    * `CommonAttrs`
+    * `CommonStyles`
+* `SEVPA`s have been adjusted to the new structure/semantics split, by now implementing `UniversalAutomaton` and `DeterministicSemantics`.
+* The `IntAbstraction` interfaces have been moved to their respective implementations in the `net.automatalib.automaton.abstraction` package.
+* The `ShrinkableAutomaton` interface has been replaced with the `Shrinkable` concept.
 * The `compute{State,Suffix,}Output` concepts from `Det{Suffix,}OutputAutomaton` have been lifted to infinite-state transition systems. As part of this refactoring, some inconsistencies have been addressed. Previously, for `Word`-output systems, `computeSuffixOutput` threw an `UndefinedPropertyAccessException` if the prefix traversed an undefined transition but not if the suffix did (here, the output would only be cut short). Now, both methods simply early-exit output computation. Furthermore, these changes also include the following renamings:
   * `DetOutputAutomaton` -> `DeterministicOutputAutomaton`
   * `DetSuffixOutputAutomaton` -> `DeterministicSuffixOutputAutomaton`

api/pom.xml

@@ -64,6 +64,11 @@ limitations under the License.
         </dependency>
 
         <!-- test -->
+        <dependency>
+            <groupId>org.mockito</groupId>
+            <artifactId>mockito-core</artifactId>
+        </dependency>
+
         <dependency>
             <groupId>org.testng</groupId>
             <artifactId>testng</artifactId>

api/src/main/java/module-info.java

@@ -61,6 +61,7 @@
     exports net.automatalib.graph.helper;
     exports net.automatalib.graph.visualization;
     exports net.automatalib.modelchecking;
+    exports net.automatalib.semantic;
     exports net.automatalib.serialization;
     exports net.automatalib.symbol.time;
     exports net.automatalib.ts;

api/src/main/java/net/automatalib/automaton/Automaton.java

@@ -47,4 +47,22 @@ public interface Automaton<S, I, T> extends TransitionSystem<S, I, T>, SimpleAut
     default Graph<S, TransitionEdge<I, T>> transitionGraphView(Collection<? extends I> inputs) {
         return new AutomatonGraphView<>(this, inputs);
     }
+
+    /**
+     * Convenience interface that links an {@link Automaton} with {@link net.automatalib.semantic.FiniteSemantics}.
+     *
+     * @param <S>
+     *         state type
+     * @param <I>
+     *         input symbol type
+     * @param <T>
+     *         transition type
+     */
+    interface FiniteSemantics<S, I, T> extends Automaton<S, I, T>, net.automatalib.semantic.FiniteSemantics {
+
+        @Override
+        default Automaton<S, I, T> getSemantics() {
+            return this;
+        }
+    }
 }

api/src/main/java/net/automatalib/automaton/DeterministicAutomaton.java

@@ -18,10 +18,13 @@
 import java.util.function.IntFunction;
 
 import net.automatalib.alphabet.Alphabet;
-import net.automatalib.automaton.abstraction.DeterministicAbstractions;
+import net.automatalib.automaton.abstraction.DeterministicAbstractions.FullIntAbstraction;
+import net.automatalib.automaton.abstraction.DeterministicAbstractions.FullIntAbstractionImpl;
+import net.automatalib.automaton.abstraction.DeterministicAbstractions.StateIntAbstraction;
+import net.automatalib.automaton.abstraction.DeterministicAbstractions.StateIntAbstractionImpl;
 import net.automatalib.automaton.simple.SimpleDeterministicAutomaton;
+import net.automatalib.semantic.DeterministicFiniteSemantics;
 import net.automatalib.ts.DeterministicTransitionSystem;
-import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * Basic interface for a deterministic automaton. A deterministic automaton is a {@link DeterministicTransitionSystem}
@@ -44,99 +47,31 @@ default FullIntAbstraction<T> fullIntAbstraction(Alphabet<I> alphabet) {
 
     @Override
     default FullIntAbstraction<T> fullIntAbstraction(int numInputs, IntFunction<? extends I> symMapping) {
-        return new DeterministicAbstractions.FullIntAbstraction<>(stateIntAbstraction(), numInputs, symMapping);
+        return new FullIntAbstractionImpl<>(stateIntAbstraction(), numInputs, symMapping);
     }
 
     @Override
     default StateIntAbstraction<I, T> stateIntAbstraction() {
-        return new DeterministicAbstractions.StateIntAbstraction<>(this);
+        return new StateIntAbstractionImpl<>(this);
     }
 
     /**
-     * Base interface for {@link SimpleDeterministicAutomaton.IntAbstraction integer abstractions} of a {@link
-     * DeterministicAutomaton}.
-     *
-     * @param <T>
-     *         transition type
-     */
-    interface IntAbstraction<T> extends SimpleDeterministicAutomaton.IntAbstraction {
-
-        /**
-         * Retrieves the (abstracted) successor of a transition object.
-         *
-         * @param transition
-         *         the transition object
-         *
-         * @return the integer representing the successor of the given transition
-         */
-        int getIntSuccessor(T transition);
-    }
-
-    /**
-     * Interface for {@link SimpleDeterministicAutomaton.StateIntAbstraction state integer abstractions} of a {@link
-     * DeterministicAutomaton}.
+     * Convenience interface that links a {@link DeterministicAutomaton} with {@link DeterministicFiniteSemantics}.
      *
+     * @param <S>
+     *         state type
      * @param <I>
      *         input symbol type
      * @param <T>
      *         transition type
      */
-    interface StateIntAbstraction<I, T> extends IntAbstraction<T>, SimpleDeterministicAutomaton.StateIntAbstraction<I> {
+    interface FiniteSemantics<S, I, T>
+            extends DeterministicAutomaton<S, I, T>, Automaton.FiniteSemantics<S, I, T>, DeterministicFiniteSemantics {
 
         @Override
-        default int getSuccessor(int state, I input) {
-            T trans = getTransition(state, input);
-            if (trans == null) {
-                return INVALID_STATE;
-            }
-            return getIntSuccessor(trans);
+        default DeterministicAutomaton<S, I, T> getSemantics() {
+            return this;
         }
-
-        /**
-         * Retrieves the outgoing transition for an (abstracted) source state and input symbol, or returns {@code null}
-         * if the automaton has no transition for this state and input.
-         *
-         * @param state
-         *         the integer representing the source state
-         * @param input
-         *         the input symbol
-         *
-         * @return the outgoing transition, or {@code null}
-         */
-        @Nullable T getTransition(int state, I input);
-
     }
 
-    /**
-     * Interface for {@link SimpleDeterministicAutomaton.FullIntAbstraction full integer abstractions} of a {@link
-     * DeterministicAutomaton}.
-     *
-     * @param <T>
-     *         transition type
-     */
-    interface FullIntAbstraction<T> extends IntAbstraction<T>, SimpleDeterministicAutomaton.FullIntAbstraction {
-
-        @Override
-        default int getSuccessor(int state, int input) {
-            T trans = getTransition(state, input);
-            if (trans == null) {
-                return INVALID_STATE;
-            }
-            return getIntSuccessor(trans);
-        }
-
-        /**
-         * Retrieves the outgoing transition for an (abstracted) source state and (abstracted) input symbol, or returns
-         * {@code null} if the automaton has no transition for this state and input.
-         *
-         * @param state
-         *         the integer representing the source state
-         * @param input
-         *         the integer representing the input symbol
-         *
-         * @return the outgoing transition, or {@code null}
-         */
-        @Nullable T getTransition(int state, int input);
-
-    }
 }

api/src/main/java/net/automatalib/automaton/MutableAutomaton.java

@@ -20,23 +20,24 @@
 import java.util.HashSet;
 import java.util.Set;
 
+import net.automatalib.automaton.concept.Shrinkable;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * A mutable automaton. This interface adds support for non-destructive modifications, i.e., adding and modifying states
  * and transitions. If also removal of states and single transitions (from the set of outgoing transitions) should be
- * removed, then {@link ShrinkableAutomaton} is the adequate interface.
+ * removed, then {@link Shrinkable} is the adequate interface.
  *
  * @param <S>
- *         state class.
+ *         state type
  * @param <I>
- *         input symbol class.
+ *         input symbol type
  * @param <T>
- *         transition class.
+ *         transition type
  * @param <SP>
- *         state property.
+ *         state property type
  * @param <TP>
- *         transition property.
+ *         transition property type
  */
 public interface MutableAutomaton<S, I, T, SP, TP> extends UniversalAutomaton<S, I, T, SP, TP> {
 
@@ -137,4 +138,23 @@ default T copyTransition(T trans, S succ) {
         TP property = getTransitionProperty(trans);
         return createTransition(succ, property);
     }
+
+    /**
+     * Convenience interface that links a {@link MutableAutomaton} with
+     * {@link net.automatalib.semantic.FiniteSemantics}.
+     *
+     * @param <S>
+     *         state type
+     * @param <I>
+     *         input symbol type
+     * @param <T>
+     *         transition type
+     * @param <SP>
+     *         state property type
+     * @param <TP>
+     *         transition property type
+     */
+    interface FiniteSemantics<S, I, T, SP, TP>
+            extends MutableAutomaton<S, I, T, SP, TP>, UniversalAutomaton.FiniteSemantics<S, I, T, SP, TP> {}
+
 }

api/src/main/java/net/automatalib/automaton/MutableDeterministic.java

@@ -20,22 +20,26 @@
 import java.util.function.IntFunction;
 
 import net.automatalib.alphabet.Alphabet;
-import net.automatalib.automaton.abstraction.MutableDeterministicAbstraction;
+import net.automatalib.automaton.abstraction.MutableDeterministicAbstractions.FullIntAbstraction;
+import net.automatalib.automaton.abstraction.MutableDeterministicAbstractions.FullIntAbstractionImpl;
+import net.automatalib.automaton.abstraction.MutableDeterministicAbstractions.StateIntAbstraction;
+import net.automatalib.automaton.abstraction.MutableDeterministicAbstractions.StateIntAbstractionImpl;
+import net.automatalib.semantic.DeterministicFiniteSemantics;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * Interface for a <i>mutable</i> deterministic automaton.
  *
  * @param <S>
- *         state class.
+ *         state type
  * @param <I>
- *         input symbol class.
+ *         input symbol type
  * @param <T>
- *         transition class.
+ *         transition type
  * @param <SP>
- *         state property.
+ *         state property type
  * @param <TP>
- *         transition property.
+ *         transition property type
  */
 public interface MutableDeterministic<S, I, T, SP, TP>
         extends UniversalDeterministicAutomaton<S, I, T, SP, TP>, MutableAutomaton<S, I, T, SP, TP> {
@@ -148,52 +152,19 @@ default FullIntAbstraction<T, SP, TP> fullIntAbstraction(Alphabet<I> alphabet) {
 
     @Override
     default FullIntAbstraction<T, SP, TP> fullIntAbstraction(int numInputs, IntFunction<? extends I> symMapping) {
-        return new MutableDeterministicAbstraction.FullIntAbstraction<>(stateIntAbstraction(), numInputs, symMapping);
+        return new FullIntAbstractionImpl<>(stateIntAbstraction(), numInputs, symMapping);
     }
 
     @Override
     default StateIntAbstraction<I, T, SP, TP> stateIntAbstraction() {
-        return new MutableDeterministicAbstraction.StateIntAbstraction<>(this);
+        return new StateIntAbstractionImpl<>(this);
     }
 
     /**
-     * Base interface for {@link UniversalDeterministicAutomaton.IntAbstraction integer abstractions} of a {@link
-     * MutableDeterministic}.
-     *
-     * @param <T>
-     *         transition type
-     * @param <SP>
-     *         state property type
-     * @param <TP>
-     *         transition property type
-     */
-    interface IntAbstraction<T, SP, TP> extends UniversalDeterministicAutomaton.IntAbstraction<T, SP, TP> {
-
-        void setStateProperty(int state, SP property);
-
-        void setTransitionProperty(T transition, TP property);
-
-        void setInitialState(int state);
-
-        T createTransition(int successor, TP property);
-
-        default int addIntState() {
-            return addIntState(null);
-        }
-
-        int addIntState(@Nullable SP property);
-
-        default int addIntInitialState() {
-            return addIntInitialState(null);
-        }
-
-        int addIntInitialState(@Nullable SP property);
-    }
-
-    /**
-     * Interface for {@link UniversalDeterministicAutomaton.StateIntAbstraction state integer abstractions} of a {@link
-     * MutableDeterministic}.
+     * Convenience interface that links a {@link MutableDeterministic} with {@link DeterministicFiniteSemantics}.
      *
+     * @param <S>
+     *         state type
      * @param <I>
      *         input symbol type
      * @param <T>
@@ -203,32 +174,8 @@ default int addIntInitialState() {
      * @param <TP>
      *         transition property type
      */
-    interface StateIntAbstraction<I, T, SP, TP>
-            extends IntAbstraction<T, SP, TP>, UniversalDeterministicAutomaton.StateIntAbstraction<I, T, SP, TP> {
-
-        void setTransition(int state, I input, @Nullable T transition);
-
-        void setTransition(int state, I input, int successor, TP property);
-
-    }
+    interface FiniteSemantics<S, I, T, SP, TP> extends MutableDeterministic<S, I, T, SP, TP>,
+                                                       MutableAutomaton.FiniteSemantics<S, I, T, SP, TP>,
+                                                       UniversalDeterministicAutomaton.FiniteSemantics<S, I, T, SP, TP> {}
 
-    /**
-     * Interface for {@link UniversalDeterministicAutomaton.FullIntAbstraction full integer abstractions} of a {@link
-     * MutableDeterministic}.
-     *
-     * @param <T>
-     *         transition type
-     * @param <SP>
-     *         state property type
-     * @param <TP>
-     *         transition property type
-     */
-    interface FullIntAbstraction<T, SP, TP>
-            extends IntAbstraction<T, SP, TP>, UniversalDeterministicAutomaton.FullIntAbstraction<T, SP, TP> {
-
-        void setTransition(int state, int input, @Nullable T transition);
-
-        void setTransition(int state, int input, int successor, TP property);
-
-    }
 }