Integrate M3C, a model checker for context-free modal process systems

.gitignore

@@ -7,3 +7,4 @@
 test-output/
 target/
 *.versionsBackup
+.DS_STORE

CHANGELOG.md

@@ -11,6 +11,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 * Added modal transition systems (MTSs), modal contracts (MCs) and Membership-MCs (MMCs).
 * Added `SubsequentialTransducer` interface and implementations/utilities.
 * Added support for systems of procedural automata (SPAs) as well as related concepts (equivalence, etc.).
+* Added the M3C model-checker for verifying µ-calculus and CTL formulas on context-free modal process systems (thanks to [Alnis Murtovi](https://github.com/AlnisM)).
 
 ### Changed
 

README.md

@@ -21,7 +21,8 @@ Furthermore, a plethora of graph-/automata-based algorithms is implemented, cove
 
 * graph theory (traversal, shortest paths, strongly-connected components)
 * automata theory (equivalence, minimization)
-* model checking (adaptive distinguishing sequences, W(p)Method, characterizing sets, state/transition covers, LTL checking (via [LTSMin][ltsmin]))
+* model-based testing (adaptive distinguishing sequences, W(p)Method, characterizing sets, state/transition covers)
+* model verification (LTL checking (via [LTSMin][ltsmin]), CTL & µ-calculus checking (via [M3C][m3c] & [ADDlib][addlib]))
 
 While we strive to deliver code at a high quality, please note that there exist parts of the library that still need thorough testing.
 Contributions -- whether it is in the form of new features, better documentation or tests -- are welcome.
@@ -97,3 +98,5 @@ For developing the code base of AutomataLib it is suggested to use one of the ma
 [intellij]: https://www.jetbrains.com/idea/
 [eclipse]: https://www.eclipse.org/
 [ltsmin]: https://ltsmin.utwente.nl/
+[m3c]: http://dx.doi.org/10.1007/978-3-030-00244-2_15
+[addlib]: https://add-lib.scce.info/

api/src/main/java/net/automatalib/automata/spa/CFMPSView.java

@@ -0,0 +1,197 @@
+/* Copyright (C) 2013-2021 TU Dortmund
+ * This file is part of AutomataLib, http://www.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.automata.spa;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.List;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
+
+import com.google.common.collect.Maps;
+import net.automatalib.automata.fsa.DFA;
+import net.automatalib.graphs.ContextFreeModalProcessSystem;
+import net.automatalib.graphs.ProceduralModalProcessGraph;
+import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty;
+import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty.ProceduralType;
+import net.automatalib.words.SPAAlphabet;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+/**
+ * This class represent a {@link ContextFreeModalProcessSystem}-based view on the instrumented language of a given
+ * {@link SPA}, which allows to model-check language properties of an {@link SPA} with tools such as M3C.
+ *
+ * @param <I>
+ *         input symbol type
+ *
+ * @author frohme
+ */
+public class CFMPSView<I> implements ContextFreeModalProcessSystem<I, Void> {
+
+    private final SPA<?, I> spa;
+    private final Map<I, ProceduralModalProcessGraph<?, I, ?, Void, ?>> pmpgs;
+
+    public CFMPSView(SPA<?, I> spa) {
+        this.spa = spa;
+
+        final SPAAlphabet<I> spaAlphabet = spa.getInputAlphabet();
+        final Map<I, DFA<?, I>> procedures = spa.getProcedures();
+        this.pmpgs = Maps.newHashMapWithExpectedSize(procedures.size());
+        for (Entry<I, DFA<?, I>> e : procedures.entrySet()) {
+            this.pmpgs.put(e.getKey(), new MPGView<>(spaAlphabet, e.getKey(), e.getValue()));
+        }
+    }
+
+    @Override
+    public Map<I, ProceduralModalProcessGraph<?, I, ?, Void, ?>> getPMPGs() {
+        return this.pmpgs;
+    }
+
+    @Override
+    public @Nullable I getMainProcess() {
+        return this.spa.getInitialProcedure();
+    }
+
+    private static class MPGView<S, I>
+            implements ProceduralModalProcessGraph<S, I, SPAEdge<I, S>, Void, ProceduralModalEdgeProperty> {
+
+        private static final Object INIT = new Object();
+        private static final Object END = new Object();
+
+        private final SPAAlphabet<I> spaAlphabet;
+        private final I procedure;
+        private final DFA<S, I> dfa;
+        private final S dfaInit;
+
+        private final S init;
+        private final S end;
+
+        // we make sure to handle 'init' and 'end' correctly
+        @SuppressWarnings("unchecked")
+        MPGView(SPAAlphabet<I> spaAlphabet, I procedure, DFA<S, I> dfa) {
+            this.spaAlphabet = spaAlphabet;
+            this.procedure = procedure;
+            this.dfa = dfa;
+
+            final S dfaInit = this.dfa.getInitialState();
+            if (dfaInit == null) {
+                throw new IllegalArgumentException("Empty DFAs cannot be mapped to ModalProcessGraphs");
+            }
+            this.dfaInit = dfaInit;
+
+            this.init = (S) INIT;
+            this.end = (S) END;
+        }
+
+        @Override
+        public Collection<SPAEdge<I, S>> getOutgoingEdges(S node) {
+            if (node == init) {
+                return Collections.singletonList(new SPAEdge<>(this.procedure, this.dfaInit, ProceduralType.INTERNAL));
+            } else if (node == end) {
+                return Collections.emptyList();
+            } else {
+                final List<SPAEdge<I, S>> result = new ArrayList<>(this.spaAlphabet.size());
+
+                for (I i : this.spaAlphabet.getInternalAlphabet()) {
+                    final S succ = this.dfa.getSuccessor(node, i);
+                    if (succ != null) {
+                        result.add(new SPAEdge<>(i, succ, ProceduralType.INTERNAL));
+                    }
+                }
+
+                for (I i : this.spaAlphabet.getCallAlphabet()) {
+                    final S succ = this.dfa.getSuccessor(node, i);
+                    if (succ != null) {
+                        result.add(new SPAEdge<>(i, succ, ProceduralType.PROCESS));
+                    }
+                }
+
+                if (this.dfa.isAccepting(node)) {
+                    result.add(new SPAEdge<>(this.spaAlphabet.getReturnSymbol(),
+                                             this.getFinalNode(),
+                                             ProceduralType.INTERNAL));
+                }
+
+                return result;
+            }
+        }
+
+        @Override
+        public S getTarget(SPAEdge<I, S> edge) {
+            return edge.succ;
+        }
+
+        @Override
+        public Collection<S> getNodes() {
+            final List<S> nodes = new ArrayList<>(dfa.size() + 2);
+            nodes.add(this.init);
+            nodes.add(this.end);
+            nodes.addAll(dfa.getStates());
+            return nodes;
+        }
+
+        @Override
+        public Set<Void> getNodeProperty(S node) {
+            return Collections.emptySet();
+        }
+
+        @Override
+        public ProceduralModalEdgeProperty getEdgeProperty(SPAEdge<I, S> edge) {
+            return edge;
+        }
+
+        @Override
+        public I getEdgeLabel(SPAEdge<I, S> edge) {
+            return edge.input;
+        }
+
+        @Override
+        public S getFinalNode() {
+            return this.end;
+        }
+
+        @Override
+        public S getInitialNode() {
+            return this.init;
+        }
+    }
+
+    private static class SPAEdge<I, S> implements ProceduralModalEdgeProperty {
+
+        private final I input;
+        private final S succ;
+        private final ProceduralType type;
+
+        SPAEdge(I input, S succ, ProceduralType type) {
+            this.input = input;
+            this.succ = succ;
+            this.type = type;
+        }
+
+        @Override
+        public ModalType getModalType() {
+            return ModalType.MUST;
+        }
+
+        @Override
+        public ProceduralType getProceduralType() {
+            return this.type;
+        }
+    }
+
+}

api/src/main/java/net/automatalib/automata/spa/SPAGraphView.java

@@ -74,7 +74,7 @@ public Collection<Pair<I, S>> getNodes() {
     public Collection<Triple<I, I, S>> getOutgoingEdges(Pair<I, S> node) {
         final I procedure = node.getFirst();
         final S state = node.getSecond();
-        @SuppressWarnings("assignment.type.incompatible") // we only use identifier for which procedures exists
+        @SuppressWarnings("assignment.type.incompatible") // we only use identifier for which procedures exist
         final @NonNull DFA<S, I> subModel = subModels.get(procedure);
 
         final List<Triple<I, I, S>> result = new ArrayList<>(this.proceduralAlphabet.size());

api/src/main/java/net/automatalib/automata/visualization/MCVisualizationHelper.java

@@ -48,7 +48,7 @@ public boolean getEdgeProperties(S src, TransitionEdge<I, T> edge, S tgt, Map<St
             properties.put(EdgeAttrs.COLOR, "red");
         }
 
-        properties.put(MCEdgeAttrs.CONTRACT, transitionProperty.getColor().toString());
+        properties.put(MCEdgeAttrs.CONTRACT, transitionProperty.getColor().name());
 
         return true;
     }

api/src/main/java/net/automatalib/automata/visualization/MTSVisualizationHelper.java

@@ -40,7 +40,7 @@ public boolean getEdgeProperties(S src, TransitionEdge<I, T> edge, S tgt, Map<St
             properties.put(EdgeAttrs.STYLE, EdgeStyles.DASHED);
         }
 
-        properties.put(MTSEdgeAttrs.MODALITY, transitionProperty.getType().toString());
+        properties.put(MTSEdgeAttrs.MODALITY, transitionProperty.getModalType().name());
 
         return true;
     }

api/src/main/java/net/automatalib/automata/visualization/SPAVisualizationHelper.java

@@ -87,7 +87,7 @@ public boolean getEdgeProperties(Pair<I, S> src,
         properties.put(EdgeAttrs.LABEL, String.valueOf(edge.getSecond()));
 
         if (callAlphabet.containsSymbol(edge.getSecond())) {
-            properties.put(EdgeAttrs.STYLE, EdgeStyles.DASHED);
+            properties.put(EdgeAttrs.STYLE, EdgeStyles.BOLD);
         }
 
         return true;

api/src/main/java/net/automatalib/graphs/CFMPSGraphView.java

@@ -0,0 +1,98 @@
+/* Copyright (C) 2013-2021 TU Dortmund
+ * This file is part of AutomataLib, http://www.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.graphs;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.List;
+import java.util.Map;
+import java.util.Map.Entry;
+
+import net.automatalib.commons.util.Pair;
+import net.automatalib.graphs.visualization.CFMPSVisualizationHelper;
+import net.automatalib.visualization.VisualizationHelper;
+import org.checkerframework.checker.nullness.qual.NonNull;
+
+/**
+ * Graph representation of a {@link ContextFreeModalProcessSystem} that displays all nodes of its sub-procedures once,
+ * i.e., without incorporating execution semantics such as stack contents.
+ *
+ * @param <S>
+ *         common procedural state type
+ * @param <L>
+ *         label type
+ * @param <E>
+ *         edge type
+ * @param <AP>
+ *         atomic proposition type
+ *
+ * @author frohme
+ */
+public class CFMPSGraphView<S, L, E, AP> implements Graph<Pair<L, S>, Pair<L, E>> {
+
+    private final Map<L, ProceduralModalProcessGraph<S, L, E, AP, ?>> pmpgs;
+
+    // cast is fine, because we make sure to only query nodes/edges belonging to the respective procedures
+    @SuppressWarnings("unchecked")
+    public CFMPSGraphView(Map<L, ? extends ProceduralModalProcessGraph<? extends S, L, ? extends E, AP, ?>> pmpgs) {
+        this.pmpgs = (Map<L, ProceduralModalProcessGraph<S, L, E, AP, ?>>) pmpgs;
+    }
+
+    @Override
+    public Collection<Pair<L, E>> getOutgoingEdges(Pair<L, S> node) {
+        final L process = node.getFirst();
+        @SuppressWarnings("assignment.type.incompatible") // we only use identifier for which pmpgs exist
+        final @NonNull ProceduralModalProcessGraph<S, L, E, AP, ?> pmpg = pmpgs.get(process);
+        final Collection<E> outgoingEdges = pmpg.getOutgoingEdges(node.getSecond());
+
+        final Collection<Pair<L, E>> result = new ArrayList<>(outgoingEdges.size());
+
+        for (E e : outgoingEdges) {
+            result.add(Pair.of(process, e));
+        }
+
+        return result;
+    }
+
+    @Override
+    public Pair<L, S> getTarget(Pair<L, E> edge) {
+        final L process = edge.getFirst();
+        @SuppressWarnings("assignment.type.incompatible") // we only use identifier for which pmpgs exist
+        final @NonNull ProceduralModalProcessGraph<S, L, E, AP, ?> pmpg = pmpgs.get(process);
+
+        return Pair.of(process, pmpg.getTarget(edge.getSecond()));
+    }
+
+    @Override
+    public Collection<Pair<L, S>> getNodes() {
+        final int numNodes = this.pmpgs.values().stream().mapToInt(Graph::size).sum();
+        final List<Pair<L, S>> result = new ArrayList<>(numNodes);
+
+        for (Entry<L, ProceduralModalProcessGraph<S, L, E, AP, ?>> e : this.pmpgs.entrySet()) {
+            final L process = e.getKey();
+            for (S s : e.getValue()) {
+                result.add(Pair.of(process, s));
+            }
+        }
+
+        return result;
+    }
+
+    @Override
+    public VisualizationHelper<Pair<L, S>, Pair<L, E>> getVisualizationHelper() {
+        return new CFMPSVisualizationHelper<>(this.pmpgs);
+    }
+}