Merge CounterExample (#54)

* initial commit to include solver * renaming and cleanup (I) * cleanup (II) * cleanup(III) * deleted graphgeneratortest * initial refactoring * cleanup and doc * cleanup * add test case for loops Co-authored-by: Markus Frohme <[email protected]>
LearnLib · Nov 2, 2022 · 905df31 · 905df31
1 parent e1e198b
commit 905df31
Show file tree

Hide file tree

Showing 17 changed files with 1,229 additions and 16 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -12,6 +12,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 * 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)).
+* Added the ability to M3C to generate witnesses for negated safety properties (thanks to [Maximilian Freese](https://github.com/Viperish-byte)).
 
 ### Changed
 

diff --git a/modelchecking/m3c/pom.xml b/modelchecking/m3c/pom.xml
@@ -43,6 +43,10 @@ limitations under the License.
             <groupId>net.automatalib</groupId>
             <artifactId>automata-commons-util</artifactId>
         </dependency>
+        <dependency>
+            <groupId>net.automatalib</groupId>
+            <artifactId>automata-core</artifactId>
+        </dependency>
 
         <!-- external -->
         <dependency>
@@ -71,7 +75,7 @@ limitations under the License.
         </dependency>
         <dependency>
             <groupId>net.automatalib</groupId>
-            <artifactId>automata-core</artifactId>
+            <artifactId>automata-serialization-dot</artifactId>
             <scope>test</scope>
         </dependency>
         <dependency>

diff --git a/...checking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/formula/DependencyGraph.java b/...checking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/formula/DependencyGraph.java
@@ -20,6 +20,7 @@
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
 
 import net.automatalib.modelcheckers.m3c.formula.modalmu.AbstractFixedPointFormulaNode;
 import net.automatalib.modelcheckers.m3c.formula.modalmu.GfpNode;
@@ -188,4 +189,22 @@ public List<EquationalBlock<L, AP>> getBlocks() {
     public FormulaNode<L, AP> getAST() {
         return ast;
     }
+
+    /**
+     * Returns a boolean array that is sized according to {@link #getNumVariables()} such that every index provided in
+     * {@code satisfiedVars} is set to {@code true}.
+     *
+     * @param satisfiedVars
+     *         the set of indices that should be set to {@code true}
+     *
+     * @return a boolean array that is sized according to {@link #getNumVariables()} such that every index provided in
+     * {@code satisfiedVars} is set to {@code true}.
+     */
+    public boolean[] toBoolArray(Set<Integer> satisfiedVars) {
+        final boolean[] arr = new boolean[getNumVariables()];
+        for (Integer satisfiedVar : satisfiedVars) {
+            arr[satisfiedVar] = true;
+        }
+        return arr;
+    }
 }
diff --git a/...checking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/AbstractDDSolver.java b/...checking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/AbstractDDSolver.java
@@ -16,6 +16,7 @@
 package net.automatalib.modelcheckers.m3c.solver;
 
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.Collections;
 import java.util.HashMap;
 import java.util.HashSet;
@@ -44,6 +45,7 @@
 import net.automatalib.modelcheckers.m3c.formula.visitor.CTLToMuCalc;
 import net.automatalib.modelcheckers.m3c.transformer.AbstractPropertyTransformer;
 import net.automatalib.modelcheckers.m3c.transformer.TransformerSerializer;
+import net.automatalib.modelchecking.ModelChecker;
 import net.automatalib.ts.modal.transition.ModalEdgeProperty;
 import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty;
 import org.checkerframework.checker.initialization.qual.UnderInitialization;
@@ -52,7 +54,9 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
- * Base implementation of the model checker which supports different types of property transformers.
+ * Base implementation of the model checker which supports different types of property transformers. The
+ * {@link ModelChecker} is (currently) implemented on the basis of the {@link WitnessTreeExtractor} including all its
+ * restrictions.
  *
  * @param <T>
  *         property transformer type
@@ -63,7 +67,8 @@
  *
  * @author murtovi
  */
-abstract class AbstractDDSolver<T extends AbstractPropertyTransformer<T, L, AP>, L, AP> {
+abstract class AbstractDDSolver<T extends AbstractPropertyTransformer<T, L, AP>, L, AP>
+        implements ModelChecker<L, ContextFreeModalProcessSystem<L, AP>, FormulaNode<L, AP>, WitnessTree<L, AP>> {
 
     // Attributes that are constant for a given CFMPS
     private final @KeyFor("workUnits") L mainProcess;
@@ -149,6 +154,34 @@ private <N, E> boolean isGuarded(@UnderInitialization AbstractDDSolver<T, L, AP>
         return nodeToPredecessors;
     }
 
+    @Override
+    public @Nullable WitnessTree<L, AP> findCounterExample(ContextFreeModalProcessSystem<L, AP> cfmps,
+                                                           Collection<? extends L> inputs,
+                                                           FormulaNode<L, AP> formulaNode) {
+        final NotNode<L, AP> negatedFormula = new NotNode<>(formulaNode);
+        final FormulaNode<L, AP> ast = ctlToMuCalc(negatedFormula).toNNF();
+
+        initialize(ast);
+        this.solveInternal(false, Collections.emptyList());
+
+        final boolean sat = isSat();
+
+        if (sat) {
+            try {
+                final Map<L, AbstractDDSolver<?, L, AP>.WorkUnit<?, ?>> units = Collections.unmodifiableMap(workUnits);
+                return WitnessTreeExtractor.computeWitness(cfmps,
+                                                           units,
+                                                           dependencyGraph,
+                                                           ast,
+                                                           getAllAPDeadlockedNode());
+            } finally {
+                shutdownDDManager();
+            }
+        }
+
+        return null;
+    }
+
     public boolean solve(FormulaNode<L, AP> formula) {
         final FormulaNode<L, AP> ast = ctlToMuCalc(formula).toNNF();
 
@@ -266,7 +299,8 @@ private <N> Mapping<N, List<FormulaNode<L, AP>>> computeSatisfiedSubformulas(Wor
     }
 
     private <N> List<FormulaNode<L, AP>> getSatisfiedSubformulas(WorkUnit<N, ?> unit, N node) {
-        final Set<Integer> output = unit.propTransformers.get(node).evaluate(toBoolArray(getAllAPDeadlockedNode()));
+        final Set<Integer> output =
+                unit.propTransformers.get(node).evaluate(dependencyGraph.toBoolArray(getAllAPDeadlockedNode()));
         final List<FormulaNode<L, AP>> satisfiedSubFormulas = new ArrayList<>();
         for (FormulaNode<L, AP> n : dependencyGraph.getFormulaNodes()) {
             if (output.contains(n.getVarNumber())) {
@@ -276,14 +310,6 @@ private <N> List<FormulaNode<L, AP>> getSatisfiedSubformulas(WorkUnit<N, ?> unit
         return satisfiedSubFormulas;
     }
 
-    private boolean[] toBoolArray(Set<Integer> satisfiedVars) {
-        final boolean[] arr = new boolean[dependencyGraph.getNumVariables()];
-        for (Integer satisfiedVar : satisfiedVars) {
-            arr[satisfiedVar] = true;
-        }
-        return arr;
-    }
-
     private Set<Integer> getAllAPDeadlockedNode() {
         return getAllAPDeadlockedNode(workUnits.get(mainProcess).pmpg);
     }
@@ -557,12 +583,12 @@ protected abstract <TP extends ModalEdgeProperty> T createInitTransformerEdge(De
 
     protected abstract TransformerSerializer<T, L, AP> getSerializer();
 
-    private class WorkUnit<N, E> {
+    class WorkUnit<N, E> {
 
-        private final L label;
-        private final ProceduralModalProcessGraph<N, L, E, AP, ?> pmpg;
+        final L label;
+        final ProceduralModalProcessGraph<N, L, E, AP, ?> pmpg;
         private final Mapping<N, @Nullable Set<N>> predecessors;
-        private MutableMapping<N, T> propTransformers;
+        MutableMapping<N, T> propTransformers;
         private Set<N> workSet; // Keeps track of which node's property transformers have to be updated.
 
         WorkUnit(L label, ProceduralModalProcessGraph<N, L, E, AP, ?> pmpg, Mapping<N, @Nullable Set<N>> predecessors) {

diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTree.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTree.java
@@ -0,0 +1,72 @@
+/* Copyright (C) 2013-2022 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.modelcheckers.m3c.solver;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+
+import net.automatalib.graphs.Graph;
+import net.automatalib.graphs.base.compact.CompactGraph;
+import net.automatalib.words.Word;
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
+/**
+ * A tree-like {@link Graph} that represents the BFS-style exploration of the tableau generated by the
+ * {@link WitnessTreeExtractor}. Edges may represent the extraction of inner subformulae, procedural calls/returns
+ * to/from other procedures, or actual steps in the transition system (modal nodes).
+ *
+ * @param <L>
+ *         label type
+ * @param <AP>
+ *         atomic proposition type
+ *
+ * @author freese
+ * @author frohme
+ */
+@SuppressWarnings("type.argument.type.incompatible") // we only add non-null properties
+public class WitnessTree<L, AP> extends CompactGraph<WitnessTreeState<?, L, ?, AP>, String> {
+
+    private @MonotonicNonNull Word<L> result;
+
+    public Word<L> getWitness() {
+        assert result != null;
+        return result;
+    }
+
+    void computePath(int finishingNode) {
+        int currentNode = finishingNode;
+
+        final List<L> tmpPath = new ArrayList<>();
+
+        while (currentNode >= 0) {
+            final WitnessTreeState<?, L, ?, AP> prop = super.getNodeProperty(currentNode);
+            assert prop != null;
+
+            final L label = prop.edgeLabel;
+            prop.isPartOfResult = true;
+
+            if (label != null) {
+                tmpPath.add(label);
+            }
+
+            currentNode = prop.parentId;
+        }
+
+        Collections.reverse(tmpPath);
+        this.result = Word.fromList(tmpPath);
+    }
+}