Control program exporter for LTSs refined

Author: rensink

src/main/java/nl/utwente/groove/explore/util/LTSReporter.java

@@ -96,18 +96,26 @@ static public File exportLTS(GTS lts, String filePattern, LTSLabels labels, Filt
         File outFile = new File(dir, ltsName);
         var fileType = FileType.getType(outFile);
         var exporter = Exporters.getExporter(ExportKind.GRAPH, fileType);
-        var exportable = Exportable.graph(ltsGraph);
-        if (exporter != null && exporter.exports(exportable)) {
-            try {
-                exporter.doExport(exportable, outFile, fileType);
-            } catch (PortException e1) {
-                throw new IOException(e1);
-            }
-        } else {
+        if (exporter == null) {
             if (!FileType.hasAnyExtension(outFile)) {
                 outFile = FileType.GXL.addExtension(outFile);
             }
             Groove.saveGraph(ltsGraph, outFile);
+        } else {
+            var exportable = Exportable.graph(ltsGraph);
+            if (!exporter.exports(exportable)) {
+                exportable = Exportable.graph(gtsFragment);
+            }
+            if (exporter.exports(exportable)) {
+                try {
+                    exporter.doExport(exportable, outFile, fileType);
+                } catch (PortException e1) {
+                    throw new IOException(e1);
+                }
+            } else {
+                throw new IOException("Exporter for %s refuses to process LTS graph");
+            }
+
         }
         return outFile;
     }

src/main/java/nl/utwente/groove/io/FileType.java

@@ -424,7 +424,10 @@ static public String getExtension(File file) {
      * @return the extension part of {@code filename}
      */
     static public String getExtension(String filename) {
-        return filename.substring(filename.lastIndexOf(SEPARATOR));
+        int sepIndex = filename.lastIndexOf(SEPARATOR);
+        return sepIndex < 0
+            ? ""
+            : filename.substring(sepIndex);
     }
 
     /** Tests if a given file has a pure name part,

src/main/java/nl/utwente/groove/io/external/AbstractExporter.java

@@ -43,6 +43,11 @@ public final ExportKind getExportKind() {
     /** The export kind of this exporter. */
     private final ExportKind exportKind;
 
+    @Override
+    public boolean exports(Exportable exportable) {
+        return exportable.hasExportKind(getExportKind());
+    }
+
     @Override
     public Set<FileType> getFileTypes() {
         return this.fileTypes;
@@ -64,7 +69,7 @@ protected final void register(FileType fileType) {
      */
     @Override
     public Set<FileType> getFileTypes(Exportable exportable) {
-        if (exportable.hasExportKind(getExportKind())) {
+        if (exports(exportable)) {
             return getFileTypes();
         } else {
             return Collections.emptySet();
@@ -130,9 +135,25 @@ protected abstract void initialise(Exportable exportable,
 
         /** Writes a line to the export file. */
         public void emit(String line) {
-            this.writer.println(line);
+            this.writer.println(this.indent + line);
+        }
+
+        /** Adds an step to the space indentation prefixed to every {@link #emit(String)} line. */
+        public void increaseIndent() {
+            this.indent.append(INDENT_STEP);
         }
 
+        /** Removes a step from the space indentation prefixed to every {@link #emit(String)} line. */
+        public void decreaseIndent() {
+            this.indent.delete(0, INDENT_STEP.length());
+        }
+
+        /** Indentation prefixed to every {@link #emit(String)} line. */
+        private final StringBuffer indent = new StringBuffer("");
+
+        /** Increase to the indent upon invocation of {@link #increaseIndent()}. */
+        static private final String INDENT_STEP = "  ";
+
         private PrintWriter writer;
     }
 }

src/main/java/nl/utwente/groove/io/external/Exporter.java

@@ -47,13 +47,12 @@ default public boolean hasExportKind(ExportKind exportKind) {
 
     /**
      * Indicates if this exporter is suitable for processing a given exportable.
-     * This is true if and only if {@link #getFileTypes(Exportable)} is non-empty.
      */
-    default public boolean exports(Exportable exportable) {
-        return !getFileTypes(exportable).isEmpty();
-    }
+    public boolean exports(Exportable exportable);
 
-    /** Returns the file types that can be used for a given exportable. */
+    /** Returns the file types that can be used for a given exportable.
+     * This is nonempty if and only if {@link #exports(Exportable)} holds.
+     */
     public Set<FileType> getFileTypes(Exportable exportable);
 
     /**

src/main/java/nl/utwente/groove/io/external/Exporters.java

@@ -38,6 +38,7 @@
 import nl.utwente.groove.io.external.format.EcorePorter;
 import nl.utwente.groove.io.external.format.FsmExporter;
 import nl.utwente.groove.io.external.format.GraphExportListener.DotListener;
+import nl.utwente.groove.io.external.format.LTS2ControlExporter;
 import nl.utwente.groove.io.external.format.ListenerExporter;
 import nl.utwente.groove.io.external.format.NativePorter;
 import nl.utwente.groove.io.external.format.RasterExporter;
@@ -136,6 +137,7 @@ private static List<Exporter> createExporters() {
         result.add(TikzExporter.getInstance());
         result.add(EcorePorter.instance());
         result.add(ListenerExporter.instance(DotListener.instance()));
+        result.add(LTS2ControlExporter.instance());
         return Collections.unmodifiableList(result);
     }
 

src/main/java/nl/utwente/groove/io/external/format/AbstractResourcePorter.java

@@ -33,10 +33,10 @@
 import nl.utwente.groove.grammar.model.GrammarModel;
 import nl.utwente.groove.grammar.model.ResourceKind;
 import nl.utwente.groove.grammar.model.TextBasedModel;
+import nl.utwente.groove.graph.GraphRole;
 import nl.utwente.groove.io.FileType;
 import nl.utwente.groove.io.external.AbstractExporter;
 import nl.utwente.groove.io.external.Exportable;
-import nl.utwente.groove.io.external.Exporter;
 import nl.utwente.groove.io.external.Imported;
 import nl.utwente.groove.io.external.Importer;
 import nl.utwente.groove.io.external.PortException;
@@ -52,7 +52,7 @@
 public class AbstractResourcePorter extends AbstractExporter implements Importer {
     /** Constructor for subclasses. */
     protected AbstractResourcePorter() {
-        super(Exporter.ExportKind.RESOURCE);
+        super(ExportKind.RESOURCE);
         this.fileTypeMap = new EnumMap<>(ResourceKind.class);
         this.resourceKindMap = new EnumMap<>(FileType.class);
     }
@@ -84,9 +84,21 @@ protected final void register(ResourceKind kind, FileType fileType) {
     /** Map from file type the native file type. */
     private final Map<FileType,ResourceKind> resourceKindMap;
 
+    @Override
+    public boolean exports(Exportable exportable) {
+        boolean result = super.exports(exportable);
+        if (result) {
+            var graph = exportable.graph();
+            assert graph != null;
+            var graphRole = graph.getRole();
+            result = graphRole == GraphRole.HOST || graphRole == GraphRole.TYPE;
+        }
+        return result;
+    }
+
     @Override
     public Set<FileType> getFileTypes(Exportable exportable) {
-        if (exportable.hasExportKind(getExportKind())) {
+        if (exports(exportable)) {
             return Collections.singleton(getFileType(exportable.getResourceKind()));
         } else {
             return Collections.emptySet();

src/main/java/nl/utwente/groove/io/external/format/LTS2ControlExporter.java

@@ -0,0 +1,129 @@
+/* GROOVE: GRaphs for Object Oriented VErification
+ * Copyright 2003--2023 University of Twente
+ *
+ * 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.
+ *
+ * $Id$
+ */
+package nl.utwente.groove.io.external.format;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import nl.utwente.groove.graph.EdgeRole;
+import nl.utwente.groove.io.FileType;
+import nl.utwente.groove.io.external.AbstractExporter;
+import nl.utwente.groove.io.external.Exportable;
+import nl.utwente.groove.io.external.PortException;
+import nl.utwente.groove.lts.GTS;
+import nl.utwente.groove.lts.GTSFragment;
+import nl.utwente.groove.lts.GraphState;
+
+/**
+ * Class that exports an LTS to a control program that enforces precisely the transitions in that LTS.
+ * @author Arend Rensink
+ * @version $Revision$
+ */
+public class LTS2ControlExporter extends AbstractExporter.Writer {
+    /**
+     * Constructor for the singleton instance.
+     */
+    private LTS2ControlExporter() {
+        super(ExportKind.GRAPH);
+        register(FileType.CONTROL);
+    }
+
+    @Override
+    public boolean exports(Exportable exportable) {
+        var graph = exportable.graph();
+        return super.exports(exportable) && (graph instanceof GTS || graph instanceof GTSFragment);
+    }
+
+    @Override
+    protected void initialise(Exportable exportable, FileType fileType) throws PortException {
+        var graph = exportable.graph();
+        if (graph instanceof GTS gts) {
+            this.gts = gts.toFragment(true, false);
+        } else if (graph instanceof GTSFragment fragment) {
+            this.gts = fragment;
+        } else {
+            throw new PortException("Cannot export %s to %s: not an LTS", exportable.qualName(),
+                fileType);
+        }
+    }
+
+    private GTSFragment gts;
+
+    @Override
+    protected void execute() throws PortException {
+        this.covered.clear();
+        var start = this.gts.startState();
+        this.covered.add(start);
+        emit(start);
+    }
+
+    /** Recursively emits the properties that hold in this states, followed by the choice of outgoing transitions. */
+    private void emit(GraphState state) {
+        assert this.covered.contains(state);
+        emit("// state " + state);
+        state
+            .getTransitions()
+            .stream()
+            .filter(t -> t.getRole() == EdgeRole.FLAG)
+            .filter(t -> !t.label().getAction().getRole().isConstraint())
+            .forEach(t -> emit(t.label() + ";"));
+        var outs = state
+            .getTransitions()
+            .stream()
+            .filter(t -> this.gts.edgeSet().contains(t))
+            .filter(t -> this.covered.add(t.target()))
+            .toList();
+        if (outs.isEmpty()) {
+            emit(state.isFinal()
+                ? "// final state"
+                : "halt");
+        } else if (outs.size() == 1 && !state.isFinal()) {
+            var out = outs.get(0);
+            emit(out.label() + ";");
+            emit(out.target());
+        } else {
+            boolean first = true;
+            for (var out : outs) {
+                if (first) {
+                    emit("choice {");
+                    first = false;
+                } else {
+                    emit("} or {");
+                }
+                increaseIndent();
+                emit(out.label() + ";");
+                emit(out.target());
+                decreaseIndent();
+            }
+            if (state.isFinal()) {
+                emit("} or { // final state");
+            }
+            emit("}");
+        }
+    }
+
+    /** The set of currently covered states. */
+    private final Set<GraphState> covered = new HashSet<>();
+
+    /** Returns the singleton instance of this class. */
+    static public LTS2ControlExporter instance() {
+        return INSTANCE;
+    }
+
+    /** The singleton instance of this class. */
+    static private LTS2ControlExporter INSTANCE = new LTS2ControlExporter();
+}

src/main/java/nl/utwente/groove/lts/GTSFragment.java

@@ -92,6 +92,11 @@ public Set<GraphTransition> edgeSet() {
 
     private final Set<GraphTransition> transitions = new LinkedHashSet<>();
 
+    /** Returns the start state of the GTS. */
+    public GraphState startState() {
+        return this.gts.startState();
+    }
+
     @Override
     public @NonNull GGraph<GraphState,GraphTransition> newGraph(String name) {
         return new GTSFragment(gts(), name);