From 905df31fe35be178ba826dd8a45feca0917fcac7 Mon Sep 17 00:00:00 2001 From: Viperish-byte <76216576+Viperish-byte@users.noreply.github.com> Date: Wed, 2 Nov 2022 14:01:39 +0100 Subject: [PATCH] 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 --- CHANGELOG.md | 1 + modelchecking/m3c/pom.xml | 6 +- .../m3c/formula/DependencyGraph.java | 19 ++ .../m3c/solver/AbstractDDSolver.java | 56 +++- .../modelcheckers/m3c/solver/WitnessTree.java | 72 ++++ .../m3c/solver/WitnessTreeExtractor.java | 317 ++++++++++++++++++ .../m3c/solver/WitnessTreeState.java | 89 +++++ .../AbstractVisualizationHelper.java | 64 ++++ .../ColorVisualizationHelper.java | 68 ++++ .../EdgeVisualizationHelper.java | 52 +++ .../HTMLVisualizationHelper.java | 79 +++++ .../NodeVisualizationHelper.java | 50 +++ .../m3c/solver/WitnessExtractorTest.java | 157 +++++++++ .../test/resources/cfmps/witness/an_c_bn.xml | 57 ++++ .../src/test/resources/cfmps/witness/loop.xml | 111 ++++++ .../test/resources/dot/witness/palindrome.dot | 39 +++ pom.xml | 8 + 17 files changed, 1229 insertions(+), 16 deletions(-) create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTree.java create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeExtractor.java create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeState.java create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/AbstractVisualizationHelper.java create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/ColorVisualizationHelper.java create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/EdgeVisualizationHelper.java create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/HTMLVisualizationHelper.java create mode 100644 modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/NodeVisualizationHelper.java create mode 100644 modelchecking/m3c/src/test/java/net/automatalib/modelcheckers/m3c/solver/WitnessExtractorTest.java create mode 100644 modelchecking/m3c/src/test/resources/cfmps/witness/an_c_bn.xml create mode 100755 modelchecking/m3c/src/test/resources/cfmps/witness/loop.xml create mode 100644 modelchecking/m3c/src/test/resources/dot/witness/palindrome.dot diff --git a/CHANGELOG.md b/CHANGELOG.md index 4cf120a1cd..26a008321e 100644 --- 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 index 5dccbb61be..a2ecae9103 100644 --- a/modelchecking/m3c/pom.xml +++ b/modelchecking/m3c/pom.xml @@ -43,6 +43,10 @@ limitations under the License. net.automatalib automata-commons-util + + net.automatalib + automata-core + @@ -71,7 +75,7 @@ limitations under the License. net.automatalib - automata-core + automata-serialization-dot test diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/formula/DependencyGraph.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/formula/DependencyGraph.java index b224a831fd..cfa65a5c98 100644 --- a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/formula/DependencyGraph.java +++ b/modelchecking/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> getBlocks() { public FormulaNode 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 satisfiedVars) { + final boolean[] arr = new boolean[getNumVariables()]; + for (Integer satisfiedVar : satisfiedVars) { + arr[satisfiedVar] = true; + } + return arr; + } } diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/AbstractDDSolver.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/AbstractDDSolver.java index 79d775e772..239f5db82e 100644 --- a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/AbstractDDSolver.java +++ b/modelchecking/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 * property transformer type @@ -63,7 +67,8 @@ * * @author murtovi */ -abstract class AbstractDDSolver, L, AP> { +abstract class AbstractDDSolver, L, AP> + implements ModelChecker, FormulaNode, WitnessTree> { // Attributes that are constant for a given CFMPS private final @KeyFor("workUnits") L mainProcess; @@ -149,6 +154,34 @@ private boolean isGuarded(@UnderInitialization AbstractDDSolver return nodeToPredecessors; } + @Override + public @Nullable WitnessTree findCounterExample(ContextFreeModalProcessSystem cfmps, + Collection inputs, + FormulaNode formulaNode) { + final NotNode negatedFormula = new NotNode<>(formulaNode); + final FormulaNode ast = ctlToMuCalc(negatedFormula).toNNF(); + + initialize(ast); + this.solveInternal(false, Collections.emptyList()); + + final boolean sat = isSat(); + + if (sat) { + try { + final Map.WorkUnit> units = Collections.unmodifiableMap(workUnits); + return WitnessTreeExtractor.computeWitness(cfmps, + units, + dependencyGraph, + ast, + getAllAPDeadlockedNode()); + } finally { + shutdownDDManager(); + } + } + + return null; + } + public boolean solve(FormulaNode formula) { final FormulaNode ast = ctlToMuCalc(formula).toNNF(); @@ -266,7 +299,8 @@ private Mapping>> computeSatisfiedSubformulas(Wor } private List> getSatisfiedSubformulas(WorkUnit unit, N node) { - final Set output = unit.propTransformers.get(node).evaluate(toBoolArray(getAllAPDeadlockedNode())); + final Set output = + unit.propTransformers.get(node).evaluate(dependencyGraph.toBoolArray(getAllAPDeadlockedNode())); final List> satisfiedSubFormulas = new ArrayList<>(); for (FormulaNode n : dependencyGraph.getFormulaNodes()) { if (output.contains(n.getVarNumber())) { @@ -276,14 +310,6 @@ private List> getSatisfiedSubformulas(WorkUnit unit return satisfiedSubFormulas; } - private boolean[] toBoolArray(Set satisfiedVars) { - final boolean[] arr = new boolean[dependencyGraph.getNumVariables()]; - for (Integer satisfiedVar : satisfiedVars) { - arr[satisfiedVar] = true; - } - return arr; - } - private Set getAllAPDeadlockedNode() { return getAllAPDeadlockedNode(workUnits.get(mainProcess).pmpg); } @@ -557,12 +583,12 @@ protected abstract T createInitTransformerEdge(De protected abstract TransformerSerializer getSerializer(); - private class WorkUnit { + class WorkUnit { - private final L label; - private final ProceduralModalProcessGraph pmpg; + final L label; + final ProceduralModalProcessGraph pmpg; private final Mapping> predecessors; - private MutableMapping propTransformers; + MutableMapping propTransformers; private Set workSet; // Keeps track of which node's property transformers have to be updated. WorkUnit(L label, ProceduralModalProcessGraph pmpg, Mapping> 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 new file mode 100644 index 0000000000..72808e1670 --- /dev/null +++ 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 + * label type + * @param + * atomic proposition type + * + * @author freese + * @author frohme + */ +@SuppressWarnings("type.argument.type.incompatible") // we only add non-null properties +public class WitnessTree extends CompactGraph, String> { + + private @MonotonicNonNull Word result; + + public Word getWitness() { + assert result != null; + return result; + } + + void computePath(int finishingNode) { + int currentNode = finishingNode; + + final List tmpPath = new ArrayList<>(); + + while (currentNode >= 0) { + final WitnessTreeState 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); + } +} diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeExtractor.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeExtractor.java new file mode 100644 index 0000000000..3d3d48a3bd --- /dev/null +++ b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeExtractor.java @@ -0,0 +1,317 @@ +/* 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.ArrayDeque; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Deque; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Set; + +import net.automatalib.graphs.ContextFreeModalProcessSystem; +import net.automatalib.graphs.ProceduralModalProcessGraph; +import net.automatalib.modelcheckers.m3c.formula.AtomicNode; +import net.automatalib.modelcheckers.m3c.formula.DependencyGraph; +import net.automatalib.modelcheckers.m3c.formula.DiamondNode; +import net.automatalib.modelcheckers.m3c.formula.FormulaNode; +import net.automatalib.modelcheckers.m3c.formula.OrNode; +import net.automatalib.modelcheckers.m3c.formula.TrueNode; +import net.automatalib.modelcheckers.m3c.formula.modalmu.LfpNode; +import net.automatalib.modelcheckers.m3c.formula.modalmu.VariableNode; +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * An implementation for generating witnesses of satisfied µ-calculus formulae based on the tableau algorithm of Colin Stirling & David Walker. This + * implementation is (currently) restricted to witnesses of negated safety-properties, as for these properties a single + * witnesses is sufficient and the witnesses are guaranteed to be finite. + * + * @param + * label type + * @param + * atomic proposition type + * + * @author freese + * @author frohme + */ +final class WitnessTreeExtractor { + + private final WitnessTree wTree = new WitnessTree<>(); + private final Map.WorkUnit> units; + private final DependencyGraph dg; + private final Set initialContext; + + private WitnessTreeExtractor(Map.WorkUnit> units, + DependencyGraph dg, + Set initialContext) { + this.units = units; + this.dg = dg; + this.initialContext = initialContext; + } + + static WitnessTree computeWitness(ContextFreeModalProcessSystem cfmps, + Map.WorkUnit> workUnits, + DependencyGraph dependencyGraph, + FormulaNode formula, + Set initialContext) { + + // assert that the formula equals the AST (in NNF) so that we can continue to use the AST for its set varNumbers + assert Objects.equals(dependencyGraph.getAST().toString(), formula.toString()); + + final WitnessTreeExtractor extractor = + new WitnessTreeExtractor<>(workUnits, dependencyGraph, initialContext); + return extractor.computeWitnessStep(cfmps, dependencyGraph.getAST()); + } + + private WitnessTree computeWitnessStep(ContextFreeModalProcessSystem cfmps, + FormulaNode formula) { + + final Deque> queue = new ArrayDeque<>(); + final AbstractDDSolver.WorkUnit mainUnit = units.get(cfmps.getMainProcess()); + assert mainUnit != null; + final WitnessTreeState init = getInitialTreeState(mainUnit, formula); + + queue.add(init); + + while (!queue.isEmpty()) { + final WitnessTreeState queueElement = queue.pop(); + final int currentNode = wTree.addNode(queueElement); + + if (currentNode > 0) { + wTree.connect(queueElement.parentId, currentNode, queueElement.displayLabel); + } + + final List> nextTreeStates = getNextTreeStates(queueElement); + + if (nextTreeStates.isEmpty()) { + wTree.computePath(currentNode); + break; + } else { + queue.addAll(nextTreeStates); + } + } + + return wTree; + } + + private List> getNextTreeStates(WitnessTreeState queueElement) { + + FormulaNode visitedFormula = queueElement.subformula; + + if (visitedFormula instanceof LfpNode) { + visitedFormula = ((LfpNode) visitedFormula).getChild(); + } + if (visitedFormula instanceof VariableNode) { + // fetch fresh child formula because in case of a VariableNode we want the whole formula again + visitedFormula = dg.getFormulaNodes().get(visitedFormula.getVarNumber()); + } + + if (visitedFormula instanceof OrNode) { + return exploreOR((OrNode) visitedFormula, queueElement); + } else if (visitedFormula instanceof DiamondNode) { + return exploreDia((DiamondNode) visitedFormula, queueElement); + } else if (visitedFormula instanceof TrueNode) { + return Collections.emptyList(); + } else if (visitedFormula instanceof AtomicNode) { + return Collections.emptyList(); + } else { + throw new IllegalArgumentException("Cannot handle node" + visitedFormula); + } + } + + private List> exploreOR(OrNode formula, + WitnessTreeState queueElement) { + final FormulaNode leftFormula = formula.getLeftChild(); + final FormulaNode rightFormula = formula.getRightChild(); + + final List> result = new ArrayList<>(); + + if (queueElement.getSatisfiedSubformulae(dg, queueElement.state).contains(leftFormula.getVarNumber())) { + result.add(new WitnessTreeState<>(queueElement.stack, + queueElement.unit, + queueElement.state, + leftFormula, + queueElement.context, + leftFormula.toString(), + null, + wTree.size() - 1)); + } + if (queueElement.getSatisfiedSubformulae(dg, queueElement.state).contains(rightFormula.getVarNumber())) { + result.add(new WitnessTreeState<>(queueElement.stack, + queueElement.unit, + queueElement.state, + rightFormula, + queueElement.context, + rightFormula.toString(), + null, + wTree.size() - 1)); + } + + return result; + } + + private List> exploreDia(DiamondNode formula, + WitnessTreeState queueElement) { + if (Objects.equals(queueElement.state, queueElement.pmpg.getFinalNode())) { + assert queueElement.stack != null; + return findDiaMoveEndNodeReturn(queueElement); + } else if (formula.getAction() == null) { + return findDiaMoveWithEmpty(queueElement, formula); + } else { + return findDiaMoveRegularStep(queueElement, formula); + } + } + + private List> findDiaMoveWithEmpty(WitnessTreeState queueElement, + DiamondNode formula) { + + final List> result = new ArrayList<>(); + final ProceduralModalProcessGraph pmpg = queueElement.pmpg; + + for (E edge : pmpg.getOutgoingEdges(queueElement.state)) { + final N target = pmpg.getTarget(edge); + final L label = pmpg.getEdgeLabel(edge); + + if (pmpg.getEdgeProperty(edge).isInternal()) { + if (queueElement.getSatisfiedSubformulae(dg, target).contains(formula.getChild().getVarNumber())) { + final WitnessTreeState toAdd = new WitnessTreeState<>(queueElement.stack, + queueElement.unit, + target, + formula.getChild(), + queueElement.context, + Objects.toString(label), + label, + wTree.size() - 1); + result.add(toAdd); + } + } else { + final AbstractDDSolver.WorkUnit unit = units.get(label); + assert unit != null; + final WitnessTreeState toAdd = + buildProcessNode(queueElement, unit, label, target, formula); + + if (toAdd != null) { + result.add(toAdd); + } + } + } + + return result; + } + + private List> findDiaMoveEndNodeReturn(WitnessTreeState queueElement) { + + assert queueElement.stack != null; + final WitnessTreeState toAdd = buildReturnNode(queueElement, queueElement.stack); + + return Collections.singletonList(toAdd); + } + + private List> findDiaMoveRegularStep(WitnessTreeState queueElement, + DiamondNode formula) { + final List> result = new ArrayList<>(); + final L moveLabel = formula.getAction(); + final ProceduralModalProcessGraph pmpg = queueElement.pmpg; + + for (E edge : pmpg.getOutgoingEdges(queueElement.state)) { + final N target = pmpg.getTarget(edge); + final L label = pmpg.getEdgeLabel(edge); + + if (pmpg.getEdgeProperty(edge).isInternal()) { + if (Objects.equals(label, moveLabel) && + queueElement.getSatisfiedSubformulae(dg, target).contains(formula.getChild().getVarNumber())) { + final WitnessTreeState toAdd = new WitnessTreeState<>(queueElement.stack, + queueElement.unit, + target, + formula.getChild(), + queueElement.context, + Objects.toString(label), + label, + wTree.size() - 1); + result.add(toAdd); + } + } else { + final AbstractDDSolver.WorkUnit unit = units.get(label); + assert unit != null; + final WitnessTreeState toAdd = + buildProcessNode(queueElement, unit, label, target, formula); + + if (toAdd != null) { + result.add(toAdd); + } + } + } + + return result; + } + + private @Nullable WitnessTreeState buildProcessNode(WitnessTreeState queueElement, + AbstractDDSolver.WorkUnit unit, + L label, + N1 target, + DiamondNode formula) { + final WitnessTreeState succ = new WitnessTreeState<>(queueElement.stack, + queueElement.unit, + target, + queueElement.subformula, + queueElement.context, + Objects.toString(label), + null, + queueElement.parentId); + + @SuppressWarnings("nullness") // we have checked non-nullness of initial nodes in the model checker + final @NonNull N2 initialNode = unit.pmpg.getInitialNode(); + final Set finalFormulae = queueElement.getSatisfiedSubformulae(dg, target); + + WitnessTreeState result = new WitnessTreeState<>(succ, + unit, + initialNode, + formula, + finalFormulae, + Objects.toString(label), + null, + wTree.size() - 1); + + if (result.getSatisfiedSubformulae(dg, result.state).contains(formula.getVarNumber())) { + return result; + } else { + return null; + } + } + + private WitnessTreeState buildReturnNode(WitnessTreeState queueElement, + WitnessTreeState prev) { + return new WitnessTreeState<>(prev.stack, + prev.unit, + prev.state, + queueElement.subformula, + prev.context, + "return", + null, + wTree.size() - 1); + } + + private WitnessTreeState getInitialTreeState(AbstractDDSolver.WorkUnit unit, + FormulaNode formula) { + @SuppressWarnings("nullness") // we have checked non-nullness of initial nodes in the model checker + final @NonNull N initialNode = unit.pmpg.getInitialNode(); + return new WitnessTreeState<>(null, unit, initialNode, formula, initialContext, "", null, -1); + } +} diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeState.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeState.java new file mode 100644 index 0000000000..1ed7b0c398 --- /dev/null +++ b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/solver/WitnessTreeState.java @@ -0,0 +1,89 @@ +/* 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.HashSet; +import java.util.Set; + +import net.automatalib.graphs.ProceduralModalProcessGraph; +import net.automatalib.modelcheckers.m3c.formula.DependencyGraph; +import net.automatalib.modelcheckers.m3c.formula.FormulaNode; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * A utility class that represents a current configuration (node property) in the {@link WitnessTree}. + * + * @param + * node type of the referenced {@link ProceduralModalProcessGraph} + * @param + * label type + * @param + * edge type of the referenced {@link ProceduralModalProcessGraph} + * @param + * atomic proposition type + * + * @author freese + * @author frohme + */ +public class WitnessTreeState { + + public final @Nullable WitnessTreeState stack; + public final AbstractDDSolver.WorkUnit unit; + public final L procedure; + public final ProceduralModalProcessGraph pmpg; + public final N state; + public final FormulaNode subformula; + public final Set context; + public final String displayLabel; + public final @Nullable L edgeLabel; + public final int parentId; + public boolean isPartOfResult; + + WitnessTreeState(@Nullable WitnessTreeState stack, + AbstractDDSolver.WorkUnit unit, + N state, + FormulaNode subformula, + Set context, + String displayLabel, + @Nullable L edgeLabel, + int parentId) { + this.stack = stack; + this.unit = unit; + this.procedure = unit.label; + this.pmpg = unit.pmpg; + this.state = state; + this.subformula = subformula; + this.context = context; + + this.edgeLabel = edgeLabel; + this.parentId = parentId; + this.displayLabel = displayLabel; + this.isPartOfResult = false; + } + + Set getSatisfiedSubformulae(DependencyGraph dependencyGraph, N node) { + + final Set output = unit.propTransformers.get(node).evaluate(dependencyGraph.toBoolArray(context)); + final Set satisfiedSubFormulas = new HashSet<>(); + for (FormulaNode n : dependencyGraph.getFormulaNodes()) { + if (output.contains(n.getVarNumber())) { + satisfiedSubFormulas.add(n.getVarNumber()); + } + } + + return satisfiedSubFormulas; + } +} diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/AbstractVisualizationHelper.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/AbstractVisualizationHelper.java new file mode 100644 index 0000000000..ba18a43f4e --- /dev/null +++ b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/AbstractVisualizationHelper.java @@ -0,0 +1,64 @@ +/* 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.visualization; + +import java.util.Map; +import java.util.Objects; + +import net.automatalib.graphs.base.compact.CompactEdge; +import net.automatalib.modelcheckers.m3c.solver.WitnessTree; +import net.automatalib.visualization.DefaultVisualizationHelper; +import net.automatalib.visualization.VisualizationHelper; + +/** + * A base {@link VisualizationHelper} for {@link WitnessTree}s. + * + * @author freese + * @author frohme + */ +abstract class AbstractVisualizationHelper extends DefaultVisualizationHelper> { + + protected final WitnessTree resultTree; + + AbstractVisualizationHelper(WitnessTree resultTree) { + this.resultTree = resultTree; + } + + @Override + public boolean getNodeProperties(Integer node, Map properties) { + if (super.getNodeProperties(node, properties)) { + properties.put(NodeAttrs.SHAPE, NodeShapes.BOX); + properties.put(NodeAttrs.LABEL, Objects.toString(resultTree.getNodeProperty(node))); + return true; + } + + return false; + } + + @Override + public boolean getEdgeProperties(Integer src, + CompactEdge edge, + Integer tgt, + Map properties) { + if (super.getEdgeProperties(src, edge, tgt, properties)) { + properties.put(EdgeAttrs.ARROWHEAD, "none"); + properties.put(EdgeAttrs.LABEL, Objects.toString(edge.getProperty())); + return true; + } + + return false; + } +} diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/ColorVisualizationHelper.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/ColorVisualizationHelper.java new file mode 100644 index 0000000000..52a444693a --- /dev/null +++ b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/ColorVisualizationHelper.java @@ -0,0 +1,68 @@ +/* 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.visualization; + +import java.util.Map; + +import net.automatalib.graphs.base.compact.CompactEdge; +import net.automatalib.modelcheckers.m3c.solver.WitnessTree; +import net.automatalib.visualization.VisualizationHelper; + +/** + * A {@link VisualizationHelper} for {@link WitnessTree}s that emphasizes nodes and edges of the witness and + * de-emphasizes the remaining ones. + * + * @author freese + * @author frohme + */ +public class ColorVisualizationHelper extends AbstractVisualizationHelper { + + public ColorVisualizationHelper(WitnessTree resultTree) { + super(resultTree); + } + + @Override + public boolean getNodeProperties(Integer node, Map properties) { + if (super.getNodeProperties(node, properties)) { + if (resultTree.getNodeProperty(node).isPartOfResult) { + properties.put(NodeAttrs.COLOR, "green"); + } else { + properties.put(NodeAttrs.COLOR, "red"); + } + return true; + } + + return false; + } + + @Override + public boolean getEdgeProperties(Integer src, + CompactEdge edge, + Integer tgt, + Map properties) { + if (super.getEdgeProperties(src, edge, tgt, properties)) { + if (resultTree.getNodeProperty(src).isPartOfResult && resultTree.getNodeProperty(tgt).isPartOfResult) { + properties.put(EdgeAttrs.COLOR, "green"); + } else { + properties.put(EdgeAttrs.COLOR, "red"); + } + return true; + } + + return false; + } + +} diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/EdgeVisualizationHelper.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/EdgeVisualizationHelper.java new file mode 100644 index 0000000000..883e122871 --- /dev/null +++ b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/EdgeVisualizationHelper.java @@ -0,0 +1,52 @@ +/* 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.visualization; + +import java.util.Map; + +import net.automatalib.graphs.base.compact.CompactEdge; +import net.automatalib.modelcheckers.m3c.solver.WitnessTree; +import net.automatalib.visualization.VisualizationHelper; + +/** + * A {@link VisualizationHelper} for {@link WitnessTree}s that emphasizes edges of the witness and de-emphasizes the + * remaining ones. + * + * @author freese + * @author frohme + */ +public class EdgeVisualizationHelper extends AbstractVisualizationHelper { + + public EdgeVisualizationHelper(WitnessTree resultTree) { + super(resultTree); + } + + @Override + public boolean getEdgeProperties(Integer src, + CompactEdge edge, + Integer tgt, + Map properties) { + if (super.getEdgeProperties(src, edge, tgt, properties)) { + if (resultTree.getNodeProperty(src).isPartOfResult && resultTree.getNodeProperty(tgt).isPartOfResult) { + properties.put(EdgeAttrs.STYLE, EdgeStyles.BOLD); + } else { + properties.put(EdgeAttrs.STYLE, EdgeStyles.DASHED); + } + return true; + } + return false; + } +} diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/HTMLVisualizationHelper.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/HTMLVisualizationHelper.java new file mode 100644 index 0000000000..f6e7316295 --- /dev/null +++ b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/HTMLVisualizationHelper.java @@ -0,0 +1,79 @@ +/* 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.visualization; + +import java.util.Map; + +import net.automatalib.modelcheckers.m3c.solver.WitnessTree; +import net.automatalib.modelcheckers.m3c.solver.WitnessTreeState; +import net.automatalib.visualization.VisualizationHelper; + +/** + * A {@link VisualizationHelper} for {@link WitnessTree}s that renders the node labels as an HTML-based table. Note that + * the syntax is specific to a DOT-based visualization. + * + * @author freese + * @author frohme + */ +public class HTMLVisualizationHelper extends AbstractVisualizationHelper { + + private final boolean shortDisplay; + + public HTMLVisualizationHelper(WitnessTree resultTree) { + this(resultTree, false); + } + + public HTMLVisualizationHelper(WitnessTree resultTree, boolean shortDisplay) { + super(resultTree); + this.shortDisplay = shortDisplay; + } + + @Override + public boolean getNodeProperties(Integer node, Map properties) { + + if (super.getNodeProperties(node, properties)) { + + final WitnessTreeState prop = resultTree.getNodeProperty(node); + + final String label = + "" + + "" + + "" + + "" + + "" + + "" + + "
State:" + prop.state + "
Context:" + prop.context + "
Procedure:" + prop.procedure + "
ReturnAddress:" + (prop.stack != null ? prop.stack.state : null) + "
Formula:" + renderFormula(node) + "
"; + + properties.put(NodeAttrs.LABEL, label); + return true; + } + + return false; + + } + + private String renderFormula(Integer node) { + final WitnessTreeState prop = resultTree.getNodeProperty(node); + + if (shortDisplay) { + return Integer.toString(prop.subformula.getVarNumber()); + } else { + final String formula = prop.subformula.toString(); + return formula.replace("&", "&").replace("<", "<").replace(">", ">"); + } + } + +} diff --git a/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/NodeVisualizationHelper.java b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/NodeVisualizationHelper.java new file mode 100644 index 0000000000..9e36df3f9d --- /dev/null +++ b/modelchecking/m3c/src/main/java/net/automatalib/modelcheckers/m3c/visualization/NodeVisualizationHelper.java @@ -0,0 +1,50 @@ +/* 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.visualization; + +import java.util.Map; + +import net.automatalib.modelcheckers.m3c.solver.WitnessTree; +import net.automatalib.visualization.VisualizationHelper; + +/** + * A {@link VisualizationHelper} for {@link WitnessTree}s that emphasizes nodes of the witness and de-emphasizes the + * remaining ones. + * + * @author freese + * @author frohme + */ +public class NodeVisualizationHelper extends AbstractVisualizationHelper { + + public NodeVisualizationHelper(WitnessTree resultTree) { + super(resultTree); + } + + @Override + public boolean getNodeProperties(Integer node, Map properties) { + if (super.getNodeProperties(node, properties)) { + if (resultTree.getNodeProperty(node).isPartOfResult) { + properties.put(NodeAttrs.STYLE, NodeStyles.BOLD); + } else { + properties.put(NodeAttrs.STYLE, NodeStyles.DASHED); + } + return true; + } + + return false; + } + +} diff --git a/modelchecking/m3c/src/test/java/net/automatalib/modelcheckers/m3c/solver/WitnessExtractorTest.java b/modelchecking/m3c/src/test/java/net/automatalib/modelcheckers/m3c/solver/WitnessExtractorTest.java new file mode 100644 index 0000000000..ac4ada51be --- /dev/null +++ b/modelchecking/m3c/src/test/java/net/automatalib/modelcheckers/m3c/solver/WitnessExtractorTest.java @@ -0,0 +1,157 @@ +/* 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.io.IOException; +import java.io.InputStream; +import java.io.Reader; +import java.io.StringWriter; +import java.util.Collections; + +import javax.xml.parsers.ParserConfigurationException; + +import com.google.common.io.CharStreams; +import net.automatalib.commons.util.IOUtil; +import net.automatalib.graphs.ContextFreeModalProcessSystem; +import net.automatalib.modelcheckers.m3c.formula.FormulaNode; +import net.automatalib.modelcheckers.m3c.formula.NotNode; +import net.automatalib.modelcheckers.m3c.formula.parser.M3CParser; +import net.automatalib.modelcheckers.m3c.formula.parser.ParseException; +import net.automatalib.modelcheckers.m3c.visualization.ColorVisualizationHelper; +import net.automatalib.modelcheckers.m3c.visualization.EdgeVisualizationHelper; +import net.automatalib.modelcheckers.m3c.visualization.HTMLVisualizationHelper; +import net.automatalib.modelcheckers.m3c.visualization.NodeVisualizationHelper; +import net.automatalib.serialization.dot.GraphDOT; +import net.automatalib.words.Word; +import org.testng.Assert; +import org.testng.annotations.DataProvider; +import org.testng.annotations.Test; +import org.xml.sax.SAXException; + +/** + * @author freese + * @author frohme + */ +public class WitnessExtractorTest { + + @DataProvider + public static Object[][] formulasOnAnCBn() { + // @formatter:off + return new Object[][] {{"mu X.((true) || <>X)", Word.fromSymbols("a", "c", "b")}, + {"mu X.((true) || <>X || (true))", Word.fromLetter("c")}, + {"mu X.((true) || <>X || (true))", Word.fromSymbols("a", "a", "c", "b", "b")}, + {"mu X.(mu Y.(true) || <>X || (true))", Word.fromSymbols("a", "c", "b")}, + {"mu X.(true || <>X) || mu Y. (true || <>Y)", Word.fromSymbols("a", "a")}, + {"mu X.(true || X) || mu Y. (true || Y)", Word.fromSymbols("a", "a", "c", "b", "b")}, + {"mu X.((true) || <>X )", Word.fromLetter("a")}, + {"true || false", Word.epsilon()}}; + // @formatter:on + } + + @Test(dataProvider = "formulasOnAnCBn") + public void checkFormulasOnAnCBn(String formula, Word expectedWitness) + throws IOException, ParserConfigurationException, SAXException, ParseException { + + final ContextFreeModalProcessSystem cfmps = parseCFMPS("/cfmps/witness/an_c_bn.xml"); + final BDDSolver m3c = new BDDSolver<>(cfmps); + + final FormulaNode f = M3CParser.parse(formula, l -> l, ap -> null); + final WitnessTree tree = m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f)); + + Assert.assertNotNull(tree); + Assert.assertEquals(tree.getWitness(), expectedWitness); + } + + @Test + public void checkPalindrome() throws ParseException, IOException, ParserConfigurationException, SAXException { + + final ContextFreeModalProcessSystem cfmps = parseCFMPS("/cfmps/palindrome/seed.xml"); + final BDDSolver m3c = new BDDSolver<>(cfmps); + + final FormulaNode f1 = M3CParser.parse("mu X. (<>X || [] false)", l -> l, ap -> null); + Assert.assertThrows(IllegalArgumentException.class, + () -> m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f1))); + + final FormulaNode f2 = M3CParser.parse("true", l -> l, ap -> null); + Assert.assertNull(m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f2))); + + final FormulaNode f3 = M3CParser.parse("<>true", l -> l, ap -> null); + final WitnessTree tree = + m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f3)); + + Assert.assertNotNull(tree); + Assert.assertEquals(tree.getWitness(), Word.fromSymbols("S", "a", "S", "T", "c")); + + final StringWriter sw = new StringWriter(); + GraphDOT.write(tree, + sw, + new ColorVisualizationHelper(tree), + new EdgeVisualizationHelper(tree), + new NodeVisualizationHelper(tree), + new HTMLVisualizationHelper(tree)); + final String expectedDOT = parseDOT("palindrome.dot"); + + Assert.assertEquals(sw.toString(), expectedDOT); + } + + @Test + public void checkLoopSystem() throws ParseException, IOException, ParserConfigurationException, SAXException { + + final ContextFreeModalProcessSystem cfmps = parseCFMPS("/cfmps/witness/loop.xml"); + final BDDSolver m3c = new BDDSolver<>(cfmps); + + // good + final FormulaNode f1 = M3CParser.parse("true", l -> l, ap -> null); + final WitnessTree t1 = m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f1)); + + Assert.assertNotNull(t1); + Assert.assertEquals(t1.getWitness(), Word.fromSymbols("a", "b", "b", "c")); + + // good + final FormulaNode f2 = M3CParser.parse("true", l -> l, ap -> null); + final WitnessTree t2 = m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f2)); + + Assert.assertNotNull(t2); + Assert.assertEquals(t2.getWitness(), Word.fromSymbols("a", "b", "b", "b", "c", "a", "b", "b", "c")); + + // should fail on single b in second iteration + final FormulaNode f3 = M3CParser.parse("true", l -> l, ap -> null); + final WitnessTree t3 = m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f3)); + + Assert.assertNull(t3); + + // should fail on single b + final FormulaNode f4 = M3CParser.parse("true", l -> l, ap -> null); + final WitnessTree t4 = m3c.findCounterExample(cfmps, Collections.emptyList(), new NotNode<>(f4)); + + Assert.assertNull(t4); + } + + private ContextFreeModalProcessSystem parseCFMPS(String name) + throws IOException, ParserConfigurationException, SAXException { + try (InputStream is = WitnessExtractorTest.class.getResourceAsStream(name)) { + return ExternalSystemDeserializer.parse(is); + } + } + + private String parseDOT(String name) throws IOException { + try (InputStream is = WitnessExtractorTest.class.getResourceAsStream("/dot/witness/" + name); + Reader r = IOUtil.asBufferedUTF8Reader(is)) { + return CharStreams.toString(r); + } + } + +} diff --git a/modelchecking/m3c/src/test/resources/cfmps/witness/an_c_bn.xml b/modelchecking/m3c/src/test/resources/cfmps/witness/an_c_bn.xml new file mode 100644 index 0000000000..69153eefa8 --- /dev/null +++ b/modelchecking/m3c/src/test/resources/cfmps/witness/an_c_bn.xml @@ -0,0 +1,57 @@ + + + P + + + 0 + + true + + + + 1 + + + 2 + + + end + + + + + 0 + 1 + + + true + + + + 0 + end + + + true + + + + 1 + 2 + + + true + true + + + + 2 + end + + + true + + + + + \ No newline at end of file diff --git a/modelchecking/m3c/src/test/resources/cfmps/witness/loop.xml b/modelchecking/m3c/src/test/resources/cfmps/witness/loop.xml new file mode 100755 index 0000000000..9696736b9d --- /dev/null +++ b/modelchecking/m3c/src/test/resources/cfmps/witness/loop.xml @@ -0,0 +1,111 @@ + + + a + + + start + + true + + + + s1 + + + s2 + + + s3 + + + end + + + + + start + s1 + + + true + + + + s1 + s2 + + + true + true + + + + s2 + s3 + + + true + + + + s2 + end + + + true + + + + s3 + s1 + + + true + + + + + + b + + + start + + true + + + + s1 + + + end + + + + + start + s1 + + + true + + + + s1 + s1 + + + true + + + + s1 + end + + + true + + + + + diff --git a/modelchecking/m3c/src/test/resources/dot/witness/palindrome.dot b/modelchecking/m3c/src/test/resources/dot/witness/palindrome.dot new file mode 100644 index 0000000000..372093cfaf --- /dev/null +++ b/modelchecking/m3c/src/test/resources/dot/witness/palindrome.dot @@ -0,0 +1,39 @@ +digraph g { + + s0 [shape="box" color="green" style="bold" label=<
State:0
Context:[5]
Procedure:S
ReturnAddress:null
Formula:(<S> (<> (<S> (<T> (<c> true)))))
>]; + s1 [shape="box" color="green" style="bold" label=<
State:1
Context:[5]
Procedure:S
ReturnAddress:null
Formula:(<> (<S> (<T> (<c> true))))
>]; + s2 [shape="box" color="green" style="bold" label=<
State:2
Context:[5]
Procedure:S
ReturnAddress:null
Formula:(<S> (<T> (<c> true)))
>]; + s3 [shape="box" color="red" style="dashed" label=<
State:3
Context:[5]
Procedure:S
ReturnAddress:null
Formula:(<S> (<T> (<c> true)))
>]; + s4 [shape="box" color="red" style="dashed" label=<
State:0
Context:[5]
Procedure:T
ReturnAddress:6
Formula:(<> (<S> (<T> (<c> true))))
>]; + s5 [shape="box" color="green" style="bold" label=<
State:0
Context:[5]
Procedure:S
ReturnAddress:4
Formula:(<S> (<T> (<c> true)))
>]; + s6 [shape="box" color="red" style="dashed" label=<
State:0
Context:[5]
Procedure:S
ReturnAddress:5
Formula:(<S> (<T> (<c> true)))
>]; + s7 [shape="box" color="red" style="dashed" label=<
State:1
Context:[5]
Procedure:T
ReturnAddress:6
Formula:(<S> (<T> (<c> true)))
>]; + s8 [shape="box" color="green" style="bold" label=<
State:1
Context:[5]
Procedure:S
ReturnAddress:4
Formula:(<T> (<c> true))
>]; + s9 [shape="box" color="red" style="dashed" label=<
State:1
Context:[5]
Procedure:S
ReturnAddress:5
Formula:(<T> (<c> true))
>]; + s10 [shape="box" color="red" style="dashed" label=<
State:0
Context:[5]
Procedure:S
ReturnAddress:4
Formula:(<S> (<T> (<c> true)))
>]; + s11 [shape="box" color="green" style="bold" label=<
State:0
Context:[5]
Procedure:T
ReturnAddress:6
Formula:(<T> (<c> true))
>]; + s12 [shape="box" color="red" style="dashed" label=<
State:0
Context:[5]
Procedure:T
ReturnAddress:6
Formula:(<T> (<c> true))
>]; + s13 [shape="box" color="red" style="dashed" label=<
State:1
Context:[5]
Procedure:S
ReturnAddress:4
Formula:(<T> (<c> true))
>]; + s14 [shape="box" color="green" style="bold" label=<
State:1
Context:[5]
Procedure:T
ReturnAddress:6
Formula:(<c> true)
>]; + s15 [shape="box" color="red" style="dashed" label=<
State:1
Context:[5]
Procedure:T
ReturnAddress:6
Formula:(<c> true)
>]; + s16 [shape="box" color="red" style="dashed" label=<
State:0
Context:[5]
Procedure:T
ReturnAddress:6
Formula:(<T> (<c> true))
>]; + s17 [shape="box" color="green" style="bold" label=<
State:2
Context:[5]
Procedure:T
ReturnAddress:6
Formula:true
>]; + s0 -> s1 [color="green" style="bold" label="S" arrowhead="none"]; + s1 -> s2 [color="green" style="bold" label="a" arrowhead="none"]; + s1 -> s3 [color="red" style="dashed" label="b" arrowhead="none"]; + s1 -> s4 [color="red" style="dashed" label="T" arrowhead="none"]; + s2 -> s5 [color="green" style="bold" label="S" arrowhead="none"]; + s3 -> s6 [color="red" style="dashed" label="S" arrowhead="none"]; + s4 -> s7 [color="red" style="dashed" label="T" arrowhead="none"]; + s5 -> s8 [color="green" style="bold" label="S" arrowhead="none"]; + s6 -> s9 [color="red" style="dashed" label="S" arrowhead="none"]; + s7 -> s10 [color="red" style="dashed" label="S" arrowhead="none"]; + s8 -> s11 [color="green" style="bold" label="T" arrowhead="none"]; + s9 -> s12 [color="red" style="dashed" label="T" arrowhead="none"]; + s10 -> s13 [color="red" style="dashed" label="S" arrowhead="none"]; + s11 -> s14 [color="green" style="bold" label="T" arrowhead="none"]; + s12 -> s15 [color="red" style="dashed" label="T" arrowhead="none"]; + s13 -> s16 [color="red" style="dashed" label="T" arrowhead="none"]; + s14 -> s17 [color="green" style="bold" label="c" arrowhead="none"]; + +} diff --git a/pom.xml b/pom.xml index d29d47de02..733cc722fd 100644 --- a/pom.xml +++ b/pom.xml @@ -114,6 +114,14 @@ limitations under the License. + + Maximilian Freese + TU Dortmund, Chair for Programming Systems + http://ls5-www.cs.tu-dortmund.de/ + + Developer + +