Add (de-)serializers for (explicit) NFAs in the .mata format

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)).
+* 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.
 

build-config/src/main/resources/automatalib-spotbugs-exclusions.xml

@@ -86,6 +86,14 @@ limitations under the License.
             <Class name="net.automatalib.serialization.dot.Token"/>
             <Class name="net.automatalib.serialization.dot.TokenMgrError"/>
 
+            <Class name="net.automatalib.serialization.mata.parser.ExplicitMataParser"/>
+            <Class name="net.automatalib.serialization.mata.parser.ExplicitMataParserConstants"/>
+            <Class name="net.automatalib.serialization.mata.parser.ExplicitMataParserTokenManager"/>
+            <Class name="net.automatalib.serialization.mata.parser.ParseException"/>
+            <Class name="net.automatalib.serialization.mata.parser.SimpleCharStream"/>
+            <Class name="net.automatalib.serialization.mata.parser.Token"/>
+            <Class name="net.automatalib.serialization.mata.parser.TokenMgrError"/>
+
             <Class name="net.automatalib.serialization.taf.parser.InternalTAFParser"/>
             <Class name="net.automatalib.serialization.taf.parser.InternalTAFParserConstants"/>
             <Class name="net.automatalib.serialization.taf.parser.InternalTAFParserTokenManager"/>

build-parent/pom.xml

@@ -67,6 +67,13 @@ limitations under the License.
                             <exclude>net/automatalib/serialization/dot/Token.class</exclude>
                             <exclude>net/automatalib/serialization/dot/TokenMgrError.class</exclude>
 
+                            <!-- generated parser for Mata serialization -->
+                            <exclude>net/automatalib/serialization/mata/parser/ExplicitMataParser*.class</exclude>
+                            <exclude>net/automatalib/serialization/mata/parser/ParseException.class</exclude>
+                            <exclude>net/automatalib/serialization/mata/parser/SimpleCharStream.class</exclude>
+                            <exclude>net/automatalib/serialization/mata/parser/Token.class</exclude>
+                            <exclude>net/automatalib/serialization/mata/parser/TokenMgrError.class</exclude>
+
                             <!-- generated parser for TAF serialization -->
                             <exclude>net/automatalib/serialization/taf/parser/InternalTAFParser*.class</exclude>
                             <exclude>net/automatalib/serialization/taf/parser/ParseException.class</exclude>
@@ -260,6 +267,7 @@ limitations under the License.
                                         <arg>-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED</arg>
                                         <arg>-AskipDefs=^net.automatalib.serialization.taf.parser.(Internal.*|Token.*|SimpleCharStream)|\
                                                         ^net.automatalib.serialization.dot.(Internal.*|Token.*|SimpleCharStream)|\
+                                                        ^net.automatalib.serialization.mata.parser.(Explicit.*|Token.*|SimpleCharStream)|\
                                                         ^net.automatalib.modelchecker.ltsmin.(Internal.*|Token.*|SimpleCharStream)|\
                                                         ^net.automatalib.modelchecker.m3c.formula.parser.(Internal.*|Token.*|SimpleCharStream)|\
                                         </arg>

distribution/pom.xml

@@ -128,6 +128,11 @@ limitations under the License.
             <artifactId>automata-serialization-learnlibv2</artifactId>
         </dependency>
 
+        <dependency>
+            <groupId>net.automatalib</groupId>
+            <artifactId>automata-serialization-mata</artifactId>
+        </dependency>
+
         <dependency>
             <groupId>net.automatalib</groupId>
             <artifactId>automata-serialization-saf</artifactId>
@@ -329,6 +334,13 @@ limitations under the License.
                     <classifier>sources</classifier>
                 </dependency>
 
+                <dependency>
+                    <groupId>net.automatalib</groupId>
+                    <artifactId>automata-serialization-mata</artifactId>
+                    <version>${project.version}</version>
+                    <classifier>sources</classifier>
+                </dependency>
+
                 <dependency>
                     <groupId>net.automatalib</groupId>
                     <artifactId>automata-serialization-saf</artifactId>

pom.xml

@@ -428,6 +428,11 @@ limitations under the License.
                 <artifactId>automata-serialization-learnlibv2</artifactId>
                 <version>${project.version}</version>
             </dependency>
+            <dependency>
+                <groupId>net.automatalib</groupId>
+                <artifactId>automata-serialization-mata</artifactId>
+                <version>${project.version}</version>
+            </dependency>
             <dependency>
                 <groupId>net.automatalib</groupId>
                 <artifactId>automata-serialization-saf</artifactId>

serialization/mata/pom.xml

@@ -0,0 +1,75 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!--
+Copyright (C) 2013-2025 TU Dortmund University
+This file is part of AutomataLib <https://automatalib.net>.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-->
+<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 https://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+
+    <parent>
+        <groupId>net.automatalib</groupId>
+        <artifactId>automata-serialization-parent</artifactId>
+        <version>0.13.0-SNAPSHOT</version>
+        <relativePath>../pom.xml</relativePath>
+    </parent>
+
+    <artifactId>automata-serialization-mata</artifactId>
+    <packaging>jar</packaging>
+
+    <name>AutomataLib :: Serialization :: Mata</name>
+    <description>(De-)Serializers for the Mata automaton format</description>
+
+    <dependencies>
+        <!-- internal -->
+        <dependency>
+            <groupId>net.automatalib</groupId>
+            <artifactId>automata-api</artifactId>
+        </dependency>
+        <dependency>
+            <groupId>net.automatalib</groupId>
+            <artifactId>automata-commons-util</artifactId>
+        </dependency>
+        <dependency>
+            <groupId>net.automatalib</groupId>
+            <artifactId>automata-core</artifactId>
+        </dependency>
+
+        <!-- build -->
+        <dependency>
+            <groupId>org.checkerframework</groupId>
+            <artifactId>checker-qual</artifactId>
+        </dependency>
+
+        <!-- test -->
+        <dependency>
+            <groupId>net.automatalib</groupId>
+            <artifactId>automata-util</artifactId>
+            <scope>test</scope>
+        </dependency>
+        <dependency>
+            <groupId>org.testng</groupId>
+            <artifactId>testng</artifactId>
+        </dependency>
+    </dependencies>
+
+    <build>
+        <plugins>
+            <plugin>
+                <groupId>org.codehaus.mojo</groupId>
+                <artifactId>javacc-maven-plugin</artifactId>
+            </plugin>
+        </plugins>
+    </build>
+</project>

serialization/mata/src/main/java/module-info.java

@@ -0,0 +1,41 @@
+/* Copyright (C) 2013-2025 TU Dortmund University
+ * This file is part of AutomataLib <https://automatalib.net>.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/**
+ * This module contains (de-) serializers for the Mata automaton format. This format is used by the <a
+ * href="https://doi.org/10.1007/978-3-031-57249-4_7">Mata Automata Library</a>.
+ * <p>
+ * This module is provided by the following Maven dependency:
+ * <pre>
+ * &lt;dependency&gt;
+ *   &lt;groupId&gt;net.automatalib&lt;/groupId&gt;
+ *   &lt;artifactId&gt;automata-serialization-mata&lt;/artifactId&gt;
+ *   &lt;version&gt;${version}&lt;/version&gt;
+ * &lt;/dependency&gt;
+ * </pre>
+ */
+open module net.automatalib.serialization.mata {
+
+    requires net.automatalib.api;
+    requires net.automatalib.common.util;
+    requires net.automatalib.core;
+
+    // annotations are 'provided'-scoped and do not need to be loaded at runtime
+    requires static org.checkerframework.checker.qual;
+
+    exports net.automatalib.serialization.mata.parser;
+    exports net.automatalib.serialization.mata.writer;
+}

serialization/mata/src/main/java/net/automatalib/serialization/mata/parser/MataNFAParser.java

@@ -0,0 +1,103 @@
+/* Copyright (C) 2013-2025 TU Dortmund University
+ * This file is part of AutomataLib <https://automatalib.net>.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package net.automatalib.serialization.mata.parser;
+
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.Reader;
+import java.util.function.Function;
+
+import net.automatalib.automaton.AutomatonCreator;
+import net.automatalib.automaton.fsa.MutableNFA;
+import net.automatalib.automaton.fsa.NFA;
+import net.automatalib.common.util.IOUtil;
+import net.automatalib.exception.FormatException;
+import net.automatalib.serialization.InputModelData;
+import net.automatalib.serialization.InputModelDeserializer;
+
+/**
+ * Parser for reading {@link NFA}s from the <a
+ * href="https://github.com/VeriFIT/mata/blob/devel/AUTOMATAFORMAT.md">NFA-explicit</a> format.
+ *
+ * @param <S>
+ *         state type
+ * @param <I>
+ *         input symbol type
+ * @param <A>
+ *         concrete automaton type
+ */
+public class MataNFAParser<S, I, A extends MutableNFA<S, I>> implements InputModelDeserializer<I, A> {
+
+    private final AutomatonCreator<A, I> creator;
+    private final Function<String, I> symbolParser;
+
+    /**
+     * Constructor.
+     *
+     * @param creator
+     *         the creator of the concrete NFA instance
+     * @param symbolParser
+     *         the parser for transforming (string-based) labels to concrete input symbols
+     */
+    public MataNFAParser(AutomatonCreator<A, I> creator, Function<String, I> symbolParser) {
+        this.creator = creator;
+        this.symbolParser = symbolParser;
+    }
+
+    @Override
+    public InputModelData<I, A> readModel(InputStream is) throws IOException, FormatException {
+        try (Reader r = IOUtil.asNonClosingUTF8Reader(is)) {
+            return parse(r, creator, symbolParser);
+        }
+    }
+
+    /**
+     * Reads the contents from the given input stream and de-serializes it into a model instance.
+     *
+     * @param reader
+     *         the reader to read the contents from
+     * @param creator
+     *         the creator of the concrete NFA instance
+     * @param symbolParser
+     *         the parser for transforming (string-based) labels to concrete input symbols
+     * @param <S>
+     *         state type
+     * @param <I>
+     *         input symbol type
+     * @param <A>
+     *         concrete automaton type
+     *
+     * @return the de-serialized model data
+     *
+     * @throws FormatException
+     *         if the content of the stream was not in the expected format
+     */
+    public static <S, I, A extends MutableNFA<S, I>> InputModelData<I, A> parse(Reader reader,
+                                                                                AutomatonCreator<A, I> creator,
+                                                                                Function<String, I> symbolParser)
+            throws FormatException {
+
+        final ExplicitMataParser parser = new ExplicitMataParser(reader);
+
+        try {
+            parser.parse();
+        } catch (ParseException ex) {
+            throw new FormatException(ex);
+        }
+
+        return parser.extract(creator, symbolParser);
+    }
+}