diff --git a/build.gradle.kts b/build.gradle.kts index b8b5767ba5..6dbea77c7d 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.8.6" + version = "6.9.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties index efb2dbd0eb..144d0ea9d7 100644 --- a/buildSrc/gradle.properties +++ b/buildSrc/gradle.properties @@ -17,7 +17,7 @@ javaVersion=17 kotlinVersion=1.9.25 shadowVersion=7.1.2 -antlrVersion=4.9.2 +antlrVersion=4.12.0 guavaVersion=31.1-jre jcommanderVersion=1.72 z3Version=4.5.0 @@ -41,4 +41,5 @@ javasmtVersion=4.1.1 sosylabVersion=0.3000-569-g89796f98 cliktVersion=4.4.0 spotlessVersion=6.25.0 -kamlVersion=0.59.0 \ No newline at end of file +kamlVersion=0.59.0 +nuprocessVersion=2.0.6 diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt index 5fc6cc9b53..9c869af882 100644 --- a/buildSrc/src/main/kotlin/Deps.kt +++ b/buildSrc/src/main/kotlin/Deps.kt @@ -81,4 +81,6 @@ object Deps { val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}" val kaml = "com.charleskorn.kaml:kaml:${Versions.kaml}" + + val nuprocess = "com.zaxxer:nuprocess:${Versions.nuprocess}" } diff --git a/lib/jhoafparser-1.1.1.jar b/lib/jhoafparser-1.1.1.jar new file mode 100644 index 0000000000..750256100b Binary files /dev/null and b/lib/jhoafparser-1.1.1.jar differ diff --git a/settings.gradle.kts b/settings.gradle.kts index 5421f34ea0..b7711bbe31 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -21,6 +21,8 @@ include( "common/core", "common/grammar", "common/multi-tests", + "common/ltl", + "common/ltl-cli", "frontends/c-frontend", "frontends/petrinet-frontend/petrinet-model", diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java index 213fafdd07..87da3778b6 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java @@ -15,15 +15,6 @@ */ package hu.bme.mit.theta.cfa.analysis.utils; -import java.awt.Color; - -import hu.bme.mit.theta.common.container.Containers; - -import java.util.LinkedHashSet; -import java.util.Map; -import java.util.Optional; -import java.util.Set; - import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.cfa.CFA; @@ -31,16 +22,18 @@ import hu.bme.mit.theta.cfa.CFA.Loc; import hu.bme.mit.theta.cfa.analysis.CfaAction; import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.common.table.TableWriter; -import hu.bme.mit.theta.common.visualization.Alignment; -import hu.bme.mit.theta.common.visualization.EdgeAttributes; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.LineStyle; -import hu.bme.mit.theta.common.visualization.NodeAttributes; +import hu.bme.mit.theta.common.visualization.*; import hu.bme.mit.theta.common.visualization.Shape; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.dsl.CoreDslManager; +import java.awt.*; +import java.util.LinkedHashSet; +import java.util.Map; +import java.util.Optional; +import java.util.Set; public final class CfaVisualizer { @@ -51,10 +44,10 @@ public final class CfaVisualizer { private static final Color LINE_COLOR = Color.BLACK; private static final LineStyle LOC_LINE_STYLE = LineStyle.NORMAL; private static final LineStyle EDGE_LINE_STYLE = LineStyle.NORMAL; + private static final LineStyle ACC_EDGE_LINE_STYLE = LineStyle.DASHED; private static final String EDGE_FONT = "courier"; - private CfaVisualizer() { - } + private CfaVisualizer() {} public static Graph visualize(final CFA cfa) { final Graph graph = new Graph(CFA_ID, CFA_LABEL); @@ -64,7 +57,7 @@ public static Graph visualize(final CFA cfa) { addLocation(graph, cfa, loc, ids); } for (final Edge edge : cfa.getEdges()) { - addEdge(graph, edge, ids); + addEdge(graph, edge, cfa.getAcceptingEdges().contains(edge), ids); } return graph; } @@ -74,16 +67,20 @@ private static void addVars(final Graph graph, final CFA cfa) { for (final VarDecl var : cfa.getVars()) { sb.append('\n').append(var.getName()).append(": ").append(var.getType()); } - final NodeAttributes attrs = NodeAttributes.builder().label(sb.toString()) - .shape(Shape.RECTANGLE) - .fillColor(FILL_COLOR).lineColor(LINE_COLOR).lineStyle(LineStyle.DASHED) - .alignment(Alignment.LEFT) - .build(); + final NodeAttributes attrs = + NodeAttributes.builder() + .label(sb.toString()) + .shape(Shape.RECTANGLE) + .fillColor(FILL_COLOR) + .lineColor(LINE_COLOR) + .lineStyle(LineStyle.DASHED) + .alignment(Alignment.LEFT) + .build(); graph.addNode(CFA_ID + "_vars", attrs); } - private static void addLocation(final Graph graph, final CFA cfa, final Loc loc, - final Map ids) { + private static void addLocation( + final Graph graph, final CFA cfa, final Loc loc, final Map ids) { final String id = LOC_ID_PREFIX + ids.size(); ids.put(loc, id); String label = loc.getName(); @@ -96,21 +93,34 @@ private static void addLocation(final Graph graph, final CFA cfa, final Loc loc, label += " (error)"; } final int peripheries = isError ? 2 : 1; - final NodeAttributes nAttrs = NodeAttributes.builder().label(label).fillColor(FILL_COLOR) - .lineColor(LINE_COLOR) - .lineStyle(LOC_LINE_STYLE).peripheries(peripheries).build(); + final NodeAttributes nAttrs = + NodeAttributes.builder() + .label(label) + .fillColor(FILL_COLOR) + .lineColor(LINE_COLOR) + .lineStyle(LOC_LINE_STYLE) + .peripheries(peripheries) + .build(); graph.addNode(id, nAttrs); } - private static void addEdge(final Graph graph, final Edge edge, final Map ids) { - final EdgeAttributes eAttrs = EdgeAttributes.builder() - .label(new CoreDslManager().writeStmt(edge.getStmt())) - .color(LINE_COLOR).lineStyle(EDGE_LINE_STYLE).font(EDGE_FONT).build(); + private static void addEdge( + final Graph graph, + final Edge edge, + final boolean accepting, + final Map ids) { + final EdgeAttributes eAttrs = + EdgeAttributes.builder() + .label(new CoreDslManager().writeStmt(edge.getStmt())) + .color(LINE_COLOR) + .lineStyle(accepting ? ACC_EDGE_LINE_STYLE : EDGE_LINE_STYLE) + .font(EDGE_FONT) + .build(); graph.addEdge(ids.get(edge.getSource()), ids.get(edge.getTarget()), eAttrs); } - public static void printTraceTable(final Trace, CfaAction> trace, - final TableWriter writer) { + public static void printTraceTable( + final Trace, CfaAction> trace, final TableWriter writer) { final Set> allVars = new LinkedHashSet<>(); for (final CfaState state : trace.getStates()) { allVars.addAll(state.getState().getDecls()); @@ -132,7 +142,8 @@ public static void printTraceTable(final Trace, CfaAction> t writer.newRow(); if (i < trace.getActions().size()) { final StringBuilder sb = new StringBuilder(); - trace.getAction(i).getStmts() + trace.getAction(i) + .getStmts() .forEach(s -> sb.append(s.toString()).append(System.lineSeparator())); writer.cell(sb.toString(), nCols); writer.newRow(); diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java index 49c2dc1efc..ecd5e3fa90 100644 --- a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java @@ -15,22 +15,18 @@ */ package hu.bme.mit.theta.cfa; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static com.google.common.base.Preconditions.checkState; +import static com.google.common.base.Preconditions.*; import static com.google.common.collect.ImmutableSet.toImmutableSet; import static java.lang.String.format; -import java.util.*; - import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; - import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.utils.StmtUtils; +import java.util.*; /** * Represents an immutable Control Flow Automata (CFA). Use the builder class to create a new @@ -45,6 +41,7 @@ public final class CFA { private final Collection> vars; private final Collection locs; private final Collection edges; + private final Collection acceptingEdges; private CFA(final Builder builder) { initLoc = builder.initLoc; @@ -52,14 +49,18 @@ private CFA(final Builder builder) { errorLoc = Optional.ofNullable(builder.errorLoc); locs = ImmutableSet.copyOf(builder.locs); edges = ImmutableList.copyOf(builder.edges); - vars = edges.stream().flatMap(e -> StmtUtils.getVars(e.getStmt()).stream()) - .collect(toImmutableSet()); + vars = + edges.stream() + .flatMap(e -> StmtUtils.getVars(e.getStmt()).stream()) + .collect(toImmutableSet()); Set varNames = Containers.createSet(); for (var v : vars) { - checkArgument(!varNames.contains(v.getName()), + checkArgument( + !varNames.contains(v.getName()), "Variable with name '" + v.getName() + "' already exists in the CFA."); varNames.add(v.getName()); } + acceptingEdges = builder.acceptingEdges; } public Loc getInitLoc() { @@ -74,9 +75,7 @@ public Optional getErrorLoc() { return errorLoc; } - /** - * Get the variables appearing on the edges of the CFA. - */ + /** Get the variables appearing on the edges of the CFA. */ public Collection> getVars() { return vars; } @@ -89,15 +88,23 @@ public Collection getEdges() { return edges; } + public Collection getAcceptingEdges() { + return acceptingEdges; + } + public static Builder builder() { return new Builder(); } @Override public String toString() { - return Utils.lispStringBuilder("process").aligned().addAll(vars).body() + return Utils.lispStringBuilder("process") + .aligned() + .addAll(vars) + .body() .addAll(locs.stream().map(this::locToString)) - .addAll(edges.stream().map(this::edgeToString)).toString(); + .addAll(edges.stream().map(this::edgeToString)) + .toString(); } private String locToString(final Loc loc) { @@ -113,9 +120,11 @@ private String locToString(final Loc loc) { } private String edgeToString(final Edge edge) { - return Utils.lispStringBuilder("edge").add(edge.getSource().getName()) + return Utils.lispStringBuilder("edge") + .add(edge.getSource().getName()) .add(edge.getTarget().getName()) - .add(edge.getStmt()).toString(); + .add(edge.getStmt()) + .toString(); } public static final class Loc { @@ -185,6 +194,7 @@ public static final class Builder { private final Collection locs; private final Collection edges; + private final Collection acceptingEdges; private final Set locNames; @@ -196,6 +206,7 @@ private Builder() { locs = Containers.createSet(); locNames = Containers.createSet(); edges = new LinkedList<>(); + acceptingEdges = Containers.createSet(); built = false; } @@ -240,7 +251,8 @@ public void setErrorLoc(final Loc errorLoc) { public Loc createLoc(final String name) { checkNotBuilt(); - checkArgument(!locNames.contains(name), + checkArgument( + !locNames.contains(name), "Location with name '" + name + "' already exists in the CFA."); final Loc loc = new Loc(name); locs.add(loc); @@ -264,14 +276,23 @@ public Edge createEdge(final Loc source, final Loc target, final Stmt stmt) { return edge; } + public void setAcceptingEdge(final Edge acceptingEdge) { + checkNotBuilt(); + checkNotNull(acceptingEdge); + checkArgument(edges.contains(acceptingEdge), "Accepting edge not present in CFA."); + acceptingEdges.add(acceptingEdge); + } + public CFA build() { checkState(initLoc != null, "Initial location must be set."); if (finalLoc != null) { - checkState(finalLoc.getOutEdges().isEmpty(), + checkState( + finalLoc.getOutEdges().isEmpty(), "Final location cannot have outgoing edges."); } if (errorLoc != null) { - checkState(errorLoc.getOutEdges().isEmpty(), + checkState( + errorLoc.getOutEdges().isEmpty(), "Error location cannot have outgoing edges."); } built = true; @@ -282,5 +303,4 @@ private void checkNotBuilt() { checkState(!built, "A CFA was already built."); } } - } diff --git a/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFAVarChanger.kt similarity index 57% rename from subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt rename to subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFAVarChanger.kt index e3260c6bce..5a58186c9a 100644 --- a/subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt +++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFAVarChanger.kt @@ -13,29 +13,27 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.cfa import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.utils.changeVars /** - * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable whose name is present in - * the parameter gets replaced to the associated instance. + * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable + * whose name is present in the parameter gets replaced to the associated instance. */ fun CFA.copyWithReplacingVars(variableMapping: Map>): CFA { - val builder = CFA.builder() - val locationMap: Map = locs.associate { it.name to builder.createLoc(it.name) } - builder.initLoc = locationMap[initLoc.name] - if (errorLoc.isPresent) - builder.errorLoc = locationMap[errorLoc.get().name] - if (finalLoc.isPresent) - builder.finalLoc = locationMap[finalLoc.get().name] - edges.forEach { - builder.createEdge( - locationMap[it.source.name], locationMap[it.target.name], - it.stmt.changeVars(variableMapping) - ) - } - return builder.build() + val builder = CFA.builder() + val locationMap: Map = locs.associate { it.name to builder.createLoc(it.name) } + builder.initLoc = locationMap[initLoc.name] + if (errorLoc.isPresent) builder.errorLoc = locationMap[errorLoc.get().name] + if (finalLoc.isPresent) builder.finalLoc = locationMap[finalLoc.get().name] + edges.forEach { + builder.createEdge( + locationMap[it.source.name], + locationMap[it.target.name], + it.stmt.changeVars(variableMapping), + ) + } + return builder.build() } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASG.kt similarity index 57% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASG.kt index 098ce639a4..d7b7816895 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASG.kt @@ -13,21 +13,21 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg +package hu.bme.mit.theta.analysis.algorithm.asg import hu.bme.mit.theta.analysis.algorithm.Proof import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState -class LDG( +/** Abstract state graph */ +class ASG( private val acceptancePredicate: AcceptancePredicate ) : Proof { - val nodes: MutableMap> = mutableMapOf() - val initNodes: MutableList> = mutableListOf() - var traces: List> = emptyList() + val nodes: MutableMap> = mutableMapOf() + val initNodes: MutableList> = mutableListOf() + var traces: List> = emptyList() fun isUninitialised() = initNodes.isEmpty() @@ -42,52 +42,48 @@ class LDG( initNodes.addAll(initStates.map(this::getOrCreateNode)) } - fun getOrCreateNode(state: S): LDGNode = - nodes.computeIfAbsent(state) { s -> LDGNode(s, acceptancePredicate.test(Pair(s, null))) } + fun getOrCreateNode(state: S): ASGNode = + nodes.computeIfAbsent(state) { s -> ASGNode(s, acceptancePredicate.test(Pair(s, null))) } fun containsNode(state: S) = nodes.containsKey(state) fun drawEdge( - source: LDGNode, - target: LDGNode, + source: ASGNode, + target: ASGNode, action: A?, accepting: Boolean, - ): LDGEdge { - val edge = LDGEdge(source, target, action, accepting) + ): ASGEdge { + val edge = ASGEdge(source, target, action, accepting) source.addOutEdge(edge) target.addInEdge(edge) return edge } } -data class LDGEdge( - val source: LDGNode?, - val target: LDGNode, +data class ASGEdge( + val source: ASGNode?, + val target: ASGNode, val action: A?, val accepting: Boolean, ) -class LDGNode(val state: S, val accepting: Boolean) { +class ASGNode(val state: S, val accepting: Boolean) { companion object { var idCounter: Long = 0 } - val inEdges: MutableList> = mutableListOf() - val outEdges: MutableList> = mutableListOf() + val inEdges: MutableList> = mutableListOf() + val outEdges: MutableList> = mutableListOf() val id = idCounter++ - var validLoopHondas: MutableSet> = hashSetOf() + var validLoopHondas: MutableSet> = hashSetOf() var expanded: Boolean = false set(value) { - if (!value) { - throw IllegalArgumentException("Can't set expanded to false") - } + require(value) { "Can't set expanded to false" } field = true } - fun addInEdge(edge: LDGEdge) = inEdges.add(edge) + fun addInEdge(edge: ASGEdge) = inEdges.add(edge) - fun addOutEdge(edge: LDGEdge) = outEdges.add(edge) - - fun smallerEdgeCollection() = if (inEdges.size > outEdges.size) inEdges else outEdges + fun addOutEdge(edge: ASGEdge) = outEdges.add(edge) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTrace.kt similarity index 85% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTrace.kt index 97ce7b9f9e..b10f075527 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTrace.kt @@ -13,28 +13,26 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.loopchecker +package hu.bme.mit.theta.analysis.algorithm.asg import hu.bme.mit.theta.analysis.Cex import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.common.logging.Logger.Level -class LDGTrace( - val tail: List>, - val honda: LDGNode, - val loop: List>, +class ASGTrace( + val tail: List>, + val honda: ASGNode, + val loop: List>, ) : Cex { val edges by lazy { tail + loop } constructor( - edges: List>, - honda: LDGNode, + edges: List>, + honda: ASGNode, ) : this(edges.takeWhile { it.source != honda }, honda, edges.dropWhile { it.source != honda }) init { @@ -51,7 +49,7 @@ class LDGTrace( override fun length() = edges.size - fun getEdge(index: Int): LDGEdge { + fun getEdge(index: Int): ASGEdge { check(index >= 0) { "Can't get negative indexed edge (${index})" } check(index < length()) { "Index out of range $index < ${length()}" } return if (index < tail.size) tail[index] else loop[index - tail.size] diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTraceRefiner.kt similarity index 73% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTraceRefiner.kt index ad174271f3..5257d04143 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTraceRefiner.kt @@ -13,14 +13,12 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement +package hu.bme.mit.theta.analysis.algorithm.asg import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState -interface LDGTraceRefiner : - Refiner, LDGTrace> {} +interface ASGTraceRefiner : + Refiner, ASGTrace> diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java index dac497e043..6c648fe50c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java @@ -45,7 +45,7 @@ public final class CegarChecker

private final Refiner refiner; private final Logger logger; private final Pr proof; - private final ProofVisualizer proofVisualizer; + public final ProofVisualizer proofVisualizer; private CegarChecker( final Abstractor abstractor, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/ASGAbstractor.kt similarity index 69% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/ASGAbstractor.kt index 6b26395fcb..1bfe96a05c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/ASGAbstractor.kt @@ -18,45 +18,45 @@ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction import hu.bme.mit.theta.analysis.Analysis import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger -class LDGAbstractor( +class ASGAbstractor( private val analysis: Analysis, private val lts: LTS, private val acceptancePredicate: AcceptancePredicate, private val searchStrategy: LoopcheckerSearchStrategy, private val logger: Logger, -) : Abstractor> { +) : Abstractor> { - override fun createProof() = LDG(acceptancePredicate) + override fun createProof() = ASG(acceptancePredicate) - override fun check(ldg: LDG, prec: P): AbstractorResult { - if (ldg.isUninitialised()) { - ldg.initialise(analysis.initFunc.getInitStates(prec)) - ldg.traces = emptyList() + override fun check(ASG: ASG, prec: P): AbstractorResult { + if (ASG.isUninitialised()) { + ASG.initialise(analysis.initFunc.getInitStates(prec)) + ASG.traces = emptyList() } val expander: NodeExpander = - fun(node: LDGNode): Collection> { + fun(node: ASGNode): Collection> { if (node.expanded) { return node.outEdges } node.expanded = true return lts.getEnabledActionsFor(node.state).flatMap { action -> - analysis.transFunc.getSuccStates(node.state, action, prec).map(ldg::getOrCreateNode).map { - ldg.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) + analysis.transFunc.getSuccStates(node.state, action, prec).map(ASG::getOrCreateNode).map { + ASG.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) } } } - val searchResult = searchStrategy.search(ldg, acceptancePredicate, expander, logger) - ldg.traces = searchResult.toList() + val searchResult = searchStrategy.search(ASG, acceptancePredicate, expander, logger) + ASG.traces = searchResult.toList() return AbstractorResult(searchResult.isEmpty()) } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt index 2a56838da3..7d09704af8 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt @@ -15,30 +15,30 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger -typealias BacktrackResult = Pair>?, List>?> +typealias BacktrackResult = Pair>?, List>?> fun combineLassos(results: Collection>) = - Pair(setOf>(), results.flatMap { it.second ?: emptyList() }) + Pair(setOf>(), results.flatMap { it.second ?: emptyList() }) abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { internal fun expandFromInitNodeUntilTarget( - initNode: LDGNode, + initNode: ASGNode, stopAtLasso: Boolean, expand: NodeExpander, logger: Logger, - ): Collection> { + ): Collection> { return expandThroughNode( emptyMap(), - LDGEdge(null, initNode, null, false), + ASGEdge(null, initNode, null, false), emptyList(), 0, stopAtLasso, @@ -49,15 +49,15 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { } private fun expandThroughNode( - pathSoFar: Map, Int>, - incomingEdge: LDGEdge, - edgesSoFar: List>, + pathSoFar: Map, Int>, + incomingEdge: ASGEdge, + edgesSoFar: List>, targetsSoFar: Int, stopAtLasso: Boolean, expand: NodeExpander, logger: Logger, ): BacktrackResult { - val expandingNode: LDGNode = incomingEdge.target + val expandingNode: ASGNode = incomingEdge.target logger.write( Logger.Level.VERBOSE, "Expanding through %s edge to %s node with state %s%n", @@ -86,7 +86,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { targetsThatFar, ) } - val lasso: LDGTrace = LDGTrace(edgesSoFar + incomingEdge, expandingNode) + val lasso: ASGTrace = ASGTrace(edgesSoFar + incomingEdge, expandingNode) logger.write(Logger.Level.DETAIL, "Built the following lasso:%n") lasso.print(logger, Logger.Level.DETAIL) return BacktrackResult(null, listOf(lasso)) @@ -102,7 +102,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { } val expandStrategy: NodeExpander = if (needsTraversing) expand else { _ -> mutableSetOf() } - val outgoingEdges: Collection> = expandStrategy(expandingNode) + val outgoingEdges: Collection> = expandStrategy(expandingNode) val results: MutableList> = mutableListOf() for (newEdge in outgoingEdges) { val result: BacktrackResult = @@ -120,7 +120,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { } val result: BacktrackResult = combineLassos(results) if (result.second != null) return result - val validLoopHondas: Collection> = results.flatMap { it.first ?: emptyList() } + val validLoopHondas: Collection> = results.flatMap { it.first ?: emptyList() } expandingNode.validLoopHondas.addAll(validLoopHondas) return BacktrackResult(validLoopHondas.toSet(), null) } @@ -129,13 +129,13 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { object GdfsSearchStrategy : AbstractSearchStrategy() { override fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, - ): Collection> { + ): Collection> { for (initNode in initNodes) { - val possibleTraces: Collection> = + val possibleTraces: Collection> = expandFromInitNodeUntilTarget(initNode, true, expand, logger) if (!possibleTraces.isEmpty()) { return possibleTraces @@ -148,7 +148,7 @@ object GdfsSearchStrategy : AbstractSearchStrategy() { object FullSearchStrategy : AbstractSearchStrategy() { override fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt index 541a9976eb..e3d3f35b9e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt @@ -15,17 +15,17 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.common.logging.NullLogger -typealias NodeExpander = (LDGNode) -> Collection> +typealias NodeExpander = (ASGNode) -> Collection> enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStrategy) { GDFS(GdfsSearchStrategy), @@ -38,19 +38,19 @@ enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStr } fun search( - ldg: LDG, + ASG: ASG, target: AcceptancePredicate, expand: NodeExpander, logger: Logger = NullLogger.getInstance(), - ): Collection> = strategy.search(ldg.initNodes, target, expand, logger) + ): Collection> = strategy.search(ASG.initNodes, target, expand, logger) } interface ILoopcheckerSearchStrategy { fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, - ): Collection> + ): Collection> } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt index 096165a371..52e58f653b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt @@ -15,10 +15,10 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger @@ -26,11 +26,11 @@ import hu.bme.mit.theta.common.logging.Logger object NdfsSearchStrategy : ILoopcheckerSearchStrategy { override fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, - ): Collection> { + ): Collection> { for (node in initNodes) { for (edge in expand(node)) { val result = blueSearch(edge, emptyList(), mutableSetOf(), mutableSetOf(), target, expand) @@ -41,18 +41,18 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { } private fun redSearch( - seed: LDGNode, - edge: LDGEdge, - trace: List>, - redNodes: MutableSet>, + seed: ASGNode, + edge: ASGEdge, + trace: List>, + redNodes: MutableSet>, target: AcceptancePredicate, expand: NodeExpander, - ): List> { + ): List> { val targetNode = edge.target if (targetNode.state.isBottom) { return emptyList() } - if (targetNode == seed) { + if (targetNode == seed && trace.isNotEmpty()) { return trace + edge } if (redNodes.contains(targetNode)) { @@ -60,7 +60,7 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { } redNodes.add(edge.target) for (nextEdge in expand(targetNode)) { - val redSearch: List> = + val redSearch: List> = redSearch(seed, nextEdge, trace + edge, redNodes, target, expand) if (redSearch.isNotEmpty()) return redSearch } @@ -68,13 +68,13 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { } private fun blueSearch( - edge: LDGEdge, - trace: List>, - blueNodes: MutableSet>, - redNodes: Set>, + edge: ASGEdge, + trace: List>, + blueNodes: MutableSet>, + redNodes: Set>, target: AcceptancePredicate, expand: NodeExpander, - ): Collection> { + ): Collection> { val targetNode = edge.target if (targetNode.state.isBottom) { return emptyList() @@ -83,18 +83,20 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { // Edge source can only be null artificially, and is only used when calling other search // strategies val accNode = if (targetNode.accepting) targetNode else edge.source!! - val redSearch: List> = - redSearch(accNode, edge, trace, mutableSetOf(), target, expand) - if (redSearch.isNotEmpty()) return setOf(LDGTrace(redSearch, accNode)) + for (outEdge in expand(edge.target)) { + val redSearch: List> = + redSearch(accNode, outEdge, trace + edge, mutableSetOf(), target, expand) + if (redSearch.isNotEmpty()) return setOf(ASGTrace(redSearch, accNode)) + } } if (blueNodes.contains(targetNode)) { return emptyList() } blueNodes.add(edge.target) for (nextEdge in expand(targetNode)) { - val blueSearch: Collection> = + val blueSearch: Collection> = blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand) - if (!blueSearch.isEmpty()) return blueSearch + if (blueSearch.isNotEmpty()) return blueSearch } return emptyList() } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/ASGTraceCheckerStrategy.kt similarity index 93% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/ASGTraceCheckerStrategy.kt index 7a950a91e8..e59e8a0561 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/ASGTraceCheckerStrategy.kt @@ -16,7 +16,7 @@ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState @@ -35,26 +35,26 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexing import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory import hu.bme.mit.theta.solver.* -enum class LDGTraceCheckerStrategy { +enum class ASGTraceCheckerStrategy { MILANO { override fun check( - trace: LDGTrace, + trace: ASGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger, - ) = MilanoLDGTraceCheckerStrategy(trace, solverFactory, init, logger).check() + ) = MilanoASGTraceCheckerStrategy(trace, solverFactory, init, logger).check() }, BOUNDED_UNROLLING { override fun check( - trace: LDGTrace, + trace: ASGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger, ): ExprTraceStatus { try { - return BoundedUnrollingLDGTraceCheckerStrategy(trace, solverFactory, init, 100, logger) + return BoundedUnrollingASGTraceCheckerStrategy(trace, solverFactory, init, 100, logger) .check() } catch (t: TraceCheckingFailedException) { logger.write(Logger.Level.INFO, "${t.message}\n") @@ -70,15 +70,15 @@ enum class LDGTraceCheckerStrategy { } abstract fun check( - trace: LDGTrace, + trace: ASGTrace, solverFactory: SolverFactory, init: Expr = True(), logger: Logger = NullLogger.getInstance(), ): ExprTraceStatus } -abstract class AbstractLDGTraceCheckerStrategy( - private val trace: LDGTrace, +abstract class AbstractASGTraceCheckerStrategy( + private val trace: ASGTrace, solverFactory: SolverFactory, private val init: Expr, private val logger: Logger, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingASGTraceCheckerStrategy.kt similarity index 96% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingASGTraceCheckerStrategy.kt index 4eeb5acbaf..8afff23418 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingASGTraceCheckerStrategy.kt @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException import hu.bme.mit.theta.analysis.algorithm.loopchecker.util.VarCollectorStmtVisitor import hu.bme.mit.theta.analysis.expl.ExplPrec @@ -42,13 +42,13 @@ import hu.bme.mit.theta.solver.ItpMarker import hu.bme.mit.theta.solver.SolverFactory import java.util.function.Consumer -class BoundedUnrollingLDGTraceCheckerStrategy( - private val trace: LDGTrace, +class BoundedUnrollingASGTraceCheckerStrategy( + private val trace: ASGTrace, private val solverFactory: SolverFactory, init: Expr, private val bound: Int, private val logger: Logger, -) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { +) : AbstractASGTraceCheckerStrategy(trace, solverFactory, init, logger) { override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { val indexingBeforeLoop = indexings[trace.tail.size] diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoASGTraceCheckerStrategy.kt similarity index 93% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoASGTraceCheckerStrategy.kt index feef72e00f..a391387f75 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoASGTraceCheckerStrategy.kt @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus @@ -35,12 +35,12 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexing import hu.bme.mit.theta.solver.Interpolant import hu.bme.mit.theta.solver.SolverFactory -class MilanoLDGTraceCheckerStrategy( - private val trace: LDGTrace, +class MilanoASGTraceCheckerStrategy( + private val trace: ASGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger, -) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { +) : AbstractASGTraceCheckerStrategy(trace, solverFactory, init, logger) { override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { for (variable in variables) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleASGTraceRefiner.kt similarity index 83% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleASGTraceRefiner.kt index 77062d71c5..aefb9135ed 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleASGTraceRefiner.kt @@ -16,9 +16,10 @@ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTraceRefiner import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus @@ -30,15 +31,15 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.solver.SolverFactory -class SingleLDGTraceRefiner( - private val strategy: LDGTraceCheckerStrategy, +class SingleASGTraceRefiner( + private val strategy: ASGTraceCheckerStrategy, private val solverFactory: SolverFactory, private val refiner: JoiningPrecRefiner, private val logger: Logger, private val init: Expr = True(), -) : LDGTraceRefiner { +) : ASGTraceRefiner { - override fun refine(witness: LDG, prec: P): RefinerResult> { + override fun refine(witness: ASG, prec: P): RefinerResult> { val ldgTraces = witness.traces check(ldgTraces.isNotEmpty()) { "${this.javaClass.simpleName} needs at least one trace!" } val ldgTrace = ldgTraces[0] diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt index 5eadd022c7..29fb6add20 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt @@ -20,6 +20,11 @@ import hu.bme.mit.theta.core.stmt.* import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.core.utils.ExprUtils +/** + * Collects vars from a statement to a fixpoint. Collects recursively only variables that are + * dependant on the input set on themselves. To collect all variables from a statement, use + * [hu.bme.mit.theta.core.utils.StmtUtils.getVars] instead. + */ class VarCollectorStmtVisitor : StmtVisitor>, Set>> { companion object { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java index 8efb0961b9..78289cc1e0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java @@ -17,19 +17,16 @@ import static com.google.common.base.Preconditions.checkNotNull; -import java.util.Collection; - import com.google.common.collect.ImmutableList; - import hu.bme.mit.theta.analysis.InitFunc; +import java.util.Collection; -final class UnitInitFunc implements InitFunc { +public final class UnitInitFunc implements InitFunc { private static final UnitInitFunc INSTANCE = new UnitInitFunc(); private static final Collection RESULT = ImmutableList.of(UnitState.getInstance()); - private UnitInitFunc() { - } + private UnitInitFunc() {} public static UnitInitFunc getInstance() { return INSTANCE; @@ -40,5 +37,4 @@ public Collection getInitStates(final UnitPrec prec) { checkNotNull(prec); return RESULT; } - } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt index 511efb266f..4ee2553a90 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt @@ -15,10 +15,10 @@ */ package hu.bme.mit.theta.analysis.utils -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.visualization.* @@ -26,34 +26,34 @@ import hu.bme.mit.theta.common.visualization.Alignment.LEFT import hu.bme.mit.theta.common.visualization.Shape.RECTANGLE import java.awt.Color -class LdgVisualizer( +class AsgVisualizer( private val stateToString: (S) -> String, private val actionToString: (A) -> String, -) : ProofVisualizer> { +) : ProofVisualizer> { - private var traceNodes: MutableSet> = mutableSetOf() - private var traceEdges: MutableSet> = mutableSetOf() + private var traceNodes: MutableSet> = mutableSetOf() + private var traceEdges: MutableSet> = mutableSetOf() - override fun visualize(ldg: LDG): Graph { + override fun visualize(ASG: ASG): Graph { traceNodes = mutableSetOf() traceEdges = mutableSetOf() - return createVisualization(ldg) + return createVisualization(ASG) } - fun visualize(ldg: LDG, trace: LDGTrace): Graph { + fun visualize(ASG: ASG, trace: ASGTrace): Graph { traceEdges = mutableSetOf() traceEdges.addAll(trace.edges) traceNodes = mutableSetOf() trace.edges.map { it.source!! }.forEach(traceNodes::add) - return createVisualization(ldg) + return createVisualization(ASG) } - private fun createVisualization(ldg: LDG): Graph { + private fun createVisualization(ASG: ASG): Graph { val graph = Graph(LDG_ID, LDG_LABEL) - val traversed: MutableSet> = mutableSetOf() + val traversed: MutableSet> = mutableSetOf() - for (initNode in ldg.initNodes) { + for (initNode in ASG.initNodes) { traverse(graph, initNode, traversed) val nAttributes = NodeAttributes.builder() @@ -78,8 +78,8 @@ class LdgVisualizer( private fun traverse( graph: Graph, - node: LDGNode, - traversed: MutableSet>, + node: ASGNode, + traversed: MutableSet>, ) { if (traversed.contains(node)) { return diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGAbstractorCheckingTest.java similarity index 91% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java rename to subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGAbstractorCheckingTest.java index 4c6acec5e1..1877a54da8 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGAbstractorCheckingTest.java @@ -19,10 +19,10 @@ import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.asg.ASG; import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor; import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; import hu.bme.mit.theta.analysis.expl.ExplPrec; import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.analysis.expl.ExplStatePredicate; @@ -59,7 +59,7 @@ import org.junit.runners.Parameterized; @RunWith(Parameterized.class) -public class LDGAbstractorCheckingTest { +public class ASGAbstractorCheckingTest { @Parameterized.Parameter public String fileName; @@ -80,7 +80,6 @@ public static Collection data() { {"counter6to7.xsts", "x_eq_7.prop", "", true}, {"counter6to7.xsts", "x_eq_6.prop", "", true}, {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, - {"colors.xsts", "currentColor_eq_Green.prop", "", true}, {"counter5.xsts", "x_eq_5.prop", "", true}, {"forever5.xsts", "x_eq_5.prop", "", true}, {"counter6to7.xsts", "x_eq_5.prop", "", false}, @@ -116,14 +115,14 @@ private void testWithXsts() throws IOException { new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); final ExplPrec precision = new XstsAllVarsInitPrec().createExpl(xsts); var abstractor = - new LDGAbstractor<>( + new ASGAbstractor<>( analysis, lts, target, LoopcheckerSearchStrategy.Companion.getDefault(), new ConsoleLogger(Logger.Level.DETAIL)); - LDG, XstsAction> ldg = new LDG<>(target); - AbstractorResult result = abstractor.check(ldg, precision); + ASG, XstsAction> ASG = new ASG<>(target); + AbstractorResult result = abstractor.check(ASG, precision); Assert.assertEquals(isLassoPresent, result.isUnsafe()); } @@ -142,15 +141,15 @@ private void testWithCfa() throws IOException { cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); AcceptancePredicate, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); - LDGAbstractor, CfaAction, CfaPrec> abstractor = - new LDGAbstractor<>( + ASGAbstractor, CfaAction, CfaPrec> abstractor = + new ASGAbstractor<>( analysis, lts, target, LoopcheckerSearchStrategy.Companion.getDefault(), new ConsoleLogger(Logger.Level.DETAIL)); - LDG, CfaAction> ldg = new LDG<>(target); - AbstractorResult result = abstractor.check(ldg, precision); + ASG, CfaAction> ASG = new ASG<>(target); + AbstractorResult result = abstractor.check(ASG, precision); Assert.assertEquals(isLassoPresent, result.isUnsafe()); } } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java new file mode 100644 index 0000000000..394737ca4a --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java @@ -0,0 +1,261 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.analysis.algorithm.loopchecker; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.asg.ASG; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace; +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleASGTraceRefiner; +import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; +import hu.bme.mit.theta.analysis.pred.*; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +import hu.bme.mit.theta.analysis.utils.AsgVisualizer; +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.CfaAction; +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; +import hu.bme.mit.theta.cfa.analysis.CfaPrec; +import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec; +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec; +import hu.bme.mit.theta.cfa.dsl.CfaDslManager; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; +import java.util.Arrays; +import java.util.Collection; +import java.util.Objects; +import java.util.function.Predicate; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.BeforeClass; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +@RunWith(Parameterized.class) +public class ASGCegarVerifierTest { + + private static Solver abstractionSolver; + private static ItpSolver itpSolver; + private static SolverFactory solverFactory; + private static Logger logger; + + @BeforeClass + public static void init() { + abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); + solverFactory = Z3LegacySolverFactory.getInstance(); + logger = new ConsoleLogger(Logger.Level.INFO); + } + + @Parameterized.Parameter public String fileName; + + @Parameterized.Parameter(1) + public String propFileName; + + @Parameterized.Parameter(2) + public String acceptingLocationName; + + @Parameterized.Parameter(3) + public boolean result; + + @Parameterized.Parameters + public static Collection data() { + return Arrays.asList( + new Object[][] { + {"counter3.xsts", "x_eq_3.prop", "", false}, + {"counter6to7.xsts", "x_eq_7.prop", "", true}, + {"counter6to7.cfa", "", "IS6", true}, + {"counter2to3.cfa", "", "IS3", true}, + {"counter6to7.xsts", "x_eq_6.prop", "", true}, + {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, + {"colors.xsts", "currentColor_eq_Green.prop", "", true}, + {"counter5.xsts", "x_eq_5.prop", "", true}, + {"forever5.xsts", "x_eq_5.prop", "", true}, + {"counter6to7.xsts", "x_eq_5.prop", "", false} + }); + } + + @Test + public void test() throws IOException { + if (propFileName.isBlank() && !acceptingLocationName.isBlank()) testWithCfa(); + if (!propFileName.isBlank() && acceptingLocationName.isBlank()) testWithXsts(); + } + + private void testWithXsts() throws IOException { + XSTS xsts; + try (InputStream inputStream = + new SequenceInputStream( + new FileInputStream(String.format("src/test/resources/xsts/%s", fileName)), + new FileInputStream( + String.format("src/test/resources/prop/%s", propFileName)))) { + xsts = XstsDslManager.createXsts(inputStream); + } + final Analysis, XstsAction, PredPrec> analysis = + XstsAnalysis.create( + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + xsts.getInitFormula())); + final LTS, XstsAction> lts = + XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + final Predicate> statePredicate = + new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); + final AcceptancePredicate, XstsAction> target = + new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp()); + LoopcheckerSearchStrategy.getEntries() + .forEach( + lStrat -> { + ASGTraceCheckerStrategy.getEntries() + .forEach( + strat -> { + var abstractor = + new ASGAbstractor<>( + analysis, lts, target, lStrat, + logger); + final Refiner< + PredPrec, + ASG< + XstsState, + XstsAction>, + ASGTrace< + XstsState, + XstsAction>> + refiner = + new SingleASGTraceRefiner<>( + strat, + solverFactory, + JoiningPrecRefiner.create( + new ItpRefToPredPrec( + ExprSplitters + .atoms())), + logger, + xsts.getInitFormula()); + final CegarChecker< + PredPrec, + ASG< + XstsState, + XstsAction>, + ASGTrace< + XstsState, + XstsAction>> + verifier = + CegarChecker.create( + abstractor, + refiner, + logger, + new AsgVisualizer<>( + Objects::toString, + Objects::toString)); + + final PredPrec precision = PredPrec.of(); + var result = verifier.check(precision); + Assert.assertEquals(this.result, result.isUnsafe()); + }); + }); + } + + private void testWithCfa() throws IOException { + final CFA cfa = + CfaDslManager.createCfa( + new FileInputStream(String.format("src/test/resources/cfa/%s", fileName))); + final CfaLts lts = CfaConfigBuilder.Encoding.SBE.getLts(null); + final Analysis, CfaAction, CfaPrec> analysis = + CfaAnalysis.create( + cfa.getInitLoc(), + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + True())); + final Predicate> statePredicate = + cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); + final AcceptancePredicate, CfaAction> target = + new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + final RefutationToPrec refToPrec = + new ItpRefToPredPrec(ExprSplitters.atoms()); + final RefutationToGlobalCfaPrec cfaRefToPrec = + new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc()); + LoopcheckerSearchStrategy.getEntries() + .forEach( + lStrat -> { + ASGTraceCheckerStrategy.getEntries() + .forEach( + strat -> { + var abstractor = + new ASGAbstractor<>( + analysis, lts, target, lStrat, + logger); + final Refiner< + CfaPrec, + ASG, CfaAction>, + ASGTrace< + CfaState, + CfaAction>> + refiner = + new SingleASGTraceRefiner<>( + strat, + solverFactory, + JoiningPrecRefiner.create( + cfaRefToPrec), + logger, + True()); + final CegarChecker< + CfaPrec, + ASG, CfaAction>, + ASGTrace< + CfaState, + CfaAction>> + verifier = + CegarChecker.create( + abstractor, + refiner, + logger, + new AsgVisualizer<>( + Objects::toString, + Objects::toString)); + + final GlobalCfaPrec prec = + GlobalCfaPrec.create(PredPrec.of()); + var res = verifier.check(prec); + Assert.assertEquals(result, res.isUnsafe()); + }); + }); + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java similarity index 81% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java rename to subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java index dfab147cc9..b985a309f2 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java @@ -17,10 +17,11 @@ import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.asg.ASG; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor; import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; @@ -46,7 +47,7 @@ import org.junit.Assert; import org.junit.Test; -public class LDGTraceCheckerTest { +public class ASGTraceCheckerTest { @Test public void testWithCounter3() throws IOException { XSTS xsts; @@ -72,20 +73,24 @@ public void testWithCounter3() throws IOException { new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); final PredPrec precision = PredPrec.of(); final Logger logger = new ConsoleLogger(Logger.Level.DETAIL); - final LDGAbstractor, XstsAction, PredPrec> abstractor = - new LDGAbstractor<>( + final ASGAbstractor, XstsAction, PredPrec> abstractor = + new ASGAbstractor<>( analysis, lts, target, LoopcheckerSearchStrategy.Companion.getDefault(), logger); - LDG, XstsAction> ldg = new LDG<>(target); - abstractor.check(ldg, precision); - LDGTrace, XstsAction> trace = ldg.getTraces().iterator().next(); + ASG, XstsAction> ASG = new ASG<>(target); + abstractor.check(ASG, precision); + ASGTrace, XstsAction> trace = ASG.getTraces().iterator().next(); - ExprTraceStatus status = - LDGTraceCheckerStrategy.Companion.getDefault() - .check(trace, solverFactory, xsts.getInitFormula(), logger); - Assert.assertTrue(status.isInfeasible()); + ASGTraceCheckerStrategy.getEntries() + .forEach( + strat -> { + ExprTraceStatus status = + strat.check( + trace, solverFactory, xsts.getInitFormula(), logger); + Assert.assertTrue(status.isInfeasible()); + }); } } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java deleted file mode 100644 index 8e8a4929be..0000000000 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java +++ /dev/null @@ -1,230 +0,0 @@ -/* - * Copyright 2024 Budapest University of Technology and Economics - * - * 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 hu.bme.mit.theta.analysis.algorithm.loopchecker; - -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; - -import hu.bme.mit.theta.analysis.Analysis; -import hu.bme.mit.theta.analysis.LTS; -import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; -import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleLDGTraceRefiner; -import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; -import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; -import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; -import hu.bme.mit.theta.analysis.pred.*; -import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; -import hu.bme.mit.theta.analysis.utils.LdgVisualizer; -import hu.bme.mit.theta.cfa.CFA; -import hu.bme.mit.theta.cfa.analysis.CfaAction; -import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; -import hu.bme.mit.theta.cfa.analysis.CfaPrec; -import hu.bme.mit.theta.cfa.analysis.CfaState; -import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; -import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; -import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec; -import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec; -import hu.bme.mit.theta.cfa.dsl.CfaDslManager; -import hu.bme.mit.theta.common.logging.ConsoleLogger; -import hu.bme.mit.theta.common.logging.Logger; -import hu.bme.mit.theta.solver.ItpSolver; -import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.SolverFactory; -import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; -import hu.bme.mit.theta.xsts.XSTS; -import hu.bme.mit.theta.xsts.analysis.*; -import hu.bme.mit.theta.xsts.dsl.XstsDslManager; -import java.io.FileInputStream; -import java.io.IOException; -import java.io.InputStream; -import java.io.SequenceInputStream; -import java.util.Arrays; -import java.util.Collection; -import java.util.Objects; -import java.util.function.Predicate; -import kotlin.Unit; -import org.junit.Assert; -import org.junit.BeforeClass; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; - -@RunWith(Parameterized.class) -public class LDGCegarVerifierTest { - - private static Solver abstractionSolver; - private static ItpSolver itpSolver; - private static SolverFactory solverFactory; - private static Logger logger; - - @BeforeClass - public static void init() { - abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); - itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); - solverFactory = Z3LegacySolverFactory.getInstance(); - logger = new ConsoleLogger(Logger.Level.INFO); - } - - @Parameterized.Parameter public String fileName; - - @Parameterized.Parameter(1) - public String propFileName; - - @Parameterized.Parameter(2) - public String acceptingLocationName; - - @Parameterized.Parameter(3) - public boolean result; - - @Parameterized.Parameters - public static Collection data() { - return Arrays.asList( - new Object[][] { - {"counter3.xsts", "x_eq_3.prop", "", false}, - {"counter6to7.xsts", "x_eq_7.prop", "", true}, - {"counter6to7.cfa", "", "IS6", true}, - {"counter2to3.cfa", "", "IS3", true}, - {"counter6to7.xsts", "x_eq_6.prop", "", true}, - {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, - {"colors.xsts", "currentColor_eq_Green.prop", "", true}, - {"counter5.xsts", "x_eq_5.prop", "", true}, - {"forever5.xsts", "x_eq_5.prop", "", true}, - {"counter6to7.xsts", "x_eq_5.prop", "", false} - }); - } - - @Test - public void test() throws IOException { - if (propFileName.isBlank() && !acceptingLocationName.isBlank()) testWithCfa(); - if (!propFileName.isBlank() && acceptingLocationName.isBlank()) testWithXsts(); - } - - private void testWithXsts() throws IOException { - XSTS xsts; - try (InputStream inputStream = - new SequenceInputStream( - new FileInputStream(String.format("src/test/resources/xsts/%s", fileName)), - new FileInputStream( - String.format("src/test/resources/prop/%s", propFileName)))) { - xsts = XstsDslManager.createXsts(inputStream); - } - final Analysis, XstsAction, PredPrec> analysis = - XstsAnalysis.create( - PredAnalysis.create( - abstractionSolver, - PredAbstractors.booleanSplitAbstractor(abstractionSolver), - xsts.getInitFormula())); - final LTS, XstsAction> lts = - XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); - final Predicate> statePredicate = - new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); - final AcceptancePredicate, XstsAction> target = - new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); - logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp()); - var abstractor = - new LDGAbstractor<>( - analysis, - lts, - target, - LoopcheckerSearchStrategy.Companion.getDefault(), - logger); - final Refiner< - PredPrec, - LDG, XstsAction>, - LDGTrace, XstsAction>> - refiner = - new SingleLDGTraceRefiner<>( - LDGTraceCheckerStrategy.Companion.getDefault(), - solverFactory, - JoiningPrecRefiner.create( - new ItpRefToPredPrec(ExprSplitters.atoms())), - logger, - xsts.getInitFormula()); - final CegarChecker< - PredPrec, - LDG, XstsAction>, - LDGTrace, XstsAction>> - verifier = - CegarChecker.create( - abstractor, - refiner, - logger, - new LdgVisualizer<>(Objects::toString, Objects::toString)); - - final PredPrec precision = PredPrec.of(); - var result = verifier.check(precision); - Assert.assertEquals(this.result, result.isUnsafe()); - } - - private void testWithCfa() throws IOException { - final CFA cfa = - CfaDslManager.createCfa( - new FileInputStream(String.format("src/test/resources/cfa/%s", fileName))); - final CfaLts lts = CfaConfigBuilder.Encoding.SBE.getLts(null); - final Analysis, CfaAction, CfaPrec> analysis = - CfaAnalysis.create( - cfa.getInitLoc(), - PredAnalysis.create( - abstractionSolver, - PredAbstractors.booleanSplitAbstractor(abstractionSolver), - True())); - final Predicate> statePredicate = - cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); - final AcceptancePredicate, CfaAction> target = - new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); - final RefutationToPrec refToPrec = - new ItpRefToPredPrec(ExprSplitters.atoms()); - final RefutationToGlobalCfaPrec cfaRefToPrec = - new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc()); - var abstractor = - new LDGAbstractor<>( - analysis, - lts, - target, - LoopcheckerSearchStrategy.Companion.getDefault(), - logger); - final Refiner< - CfaPrec, - LDG, CfaAction>, - LDGTrace, CfaAction>> - refiner = - new SingleLDGTraceRefiner<>( - LDGTraceCheckerStrategy.Companion.getDefault(), - solverFactory, - JoiningPrecRefiner.create(cfaRefToPrec), - logger, - True()); - final CegarChecker< - CfaPrec, - LDG, CfaAction>, - LDGTrace, CfaAction>> - verifier = - CegarChecker.create( - abstractor, - refiner, - logger, - new LdgVisualizer<>(Objects::toString, Objects::toString)); - - final GlobalCfaPrec prec = GlobalCfaPrec.create(PredPrec.of()); - var res = verifier.check(prec); - Assert.assertEquals(result, res.isUnsafe()); - } -} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/ASGTraceTest.java similarity index 72% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java rename to subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/ASGTraceTest.java index f059bccaac..0abf99ff82 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/ASGTraceTest.java @@ -17,7 +17,9 @@ import static org.mockito.Mockito.mock; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import java.util.List; @@ -27,22 +29,22 @@ import org.mockito.junit.MockitoJUnitRunner; @RunWith(MockitoJUnitRunner.class) -public class LDGTraceTest { +public class ASGTraceTest { @Test public void testSimpleLasso() { - LDGNode initNode = new LDGNode<>(mock(ExprState.class), false); - LDGNode hondaNode = new LDGNode<>(mock(ExprState.class), true); - LDGNode loopNode = new LDGNode<>(mock(ExprState.class), false); + ASGNode initNode = new ASGNode<>(mock(ExprState.class), false); + ASGNode hondaNode = new ASGNode<>(mock(ExprState.class), true); + ASGNode loopNode = new ASGNode<>(mock(ExprState.class), false); Assert.assertNotEquals(initNode, hondaNode); Assert.assertNotEquals(initNode, loopNode); Assert.assertNotEquals(loopNode, hondaNode); - LDGEdge firstEdge = - new LDGEdge<>(initNode, hondaNode, mock(ExprAction.class), false); - LDGEdge secondEdge = - new LDGEdge<>(hondaNode, loopNode, mock(ExprAction.class), false); - LDGEdge thirdEdge = - new LDGEdge<>(loopNode, hondaNode, mock(ExprAction.class), false); + ASGEdge firstEdge = + new ASGEdge<>(initNode, hondaNode, mock(ExprAction.class), false); + ASGEdge secondEdge = + new ASGEdge<>(hondaNode, loopNode, mock(ExprAction.class), false); + ASGEdge thirdEdge = + new ASGEdge<>(loopNode, hondaNode, mock(ExprAction.class), false); initNode.addOutEdge(firstEdge); hondaNode.addInEdge(firstEdge); hondaNode.addOutEdge(secondEdge); @@ -50,8 +52,8 @@ public void testSimpleLasso() { loopNode.addOutEdge(thirdEdge); hondaNode.addInEdge(thirdEdge); - LDGTrace trace = - new LDGTrace<>(List.of(firstEdge, secondEdge, thirdEdge), hondaNode); + ASGTrace trace = + new ASGTrace<>(List.of(firstEdge, secondEdge, thirdEdge), hondaNode); Assert.assertEquals(1, trace.getTail().size()); Assert.assertEquals(2, trace.getLoop().size()); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt new file mode 100644 index 0000000000..fa7a141799 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt @@ -0,0 +1,74 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.analysis.algorithm.loopchecker.utils + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.util.VarCollectorStmtVisitor +import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.IfStmt +import hu.bme.mit.theta.core.stmt.Stmt +import hu.bme.mit.theta.core.stmt.Stmts +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.inttype.IntExprs +import hu.bme.mit.theta.core.type.inttype.IntType +import java.util.* +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized + +@RunWith(Parameterized::class) +class VarCollectorStmtVisitorTest( + private val stmt: Stmt, + private val inputVars: Set>, + private val expectedVars: Set>, +) { + + @Test + fun test() { + val vars = VarCollectorStmtVisitor.visitAll(listOf(stmt), inputVars) + Assert.assertEquals(expectedVars, vars) + } + + companion object { + + private val VA: VarDecl = Decls.Var("a", BoolExprs.Bool()) + private val VB: VarDecl = Decls.Var("b", IntExprs.Int()) + private val VC: VarDecl = Decls.Var("d", IntExprs.Int()) + + @JvmStatic + @Parameterized.Parameters + fun data(): Collection> { + return listOf( + arrayOf(Stmts.Skip(), emptySet>(), emptySet>()), + arrayOf(Stmts.Havoc(VA), emptySet>(), setOf(VA)), + arrayOf(Stmts.Havoc(VB), emptySet>(), setOf(VB)), + arrayOf(Stmts.Havoc(VA), setOf(VA), setOf(VA)), + arrayOf(Stmts.Havoc(VB), setOf(VA), setOf(VA, VB)), + arrayOf(Stmts.Assign(VB, IntExprs.Int(0)), setOf(VB), setOf(VB)), + arrayOf(Stmts.Assign(VB, IntExprs.Add(VB.ref, IntExprs.Int(1))), setOf(VB), setOf(VB)), + arrayOf(Stmts.Assign(VB, IntExprs.Add(VC.ref, VC.ref)), setOf(VC), setOf(VB, VC)), + arrayOf( + Stmts.Assume(BoolExprs.And(VA.ref, IntExprs.Eq(VB.ref, VC.ref))), + setOf(VC), + setOf(VC), + ), + arrayOf(IfStmt.of(BoolExprs.False(), Stmts.Havoc(VB)), emptySet>(), setOf(VB)), + ) + } + } +} diff --git a/subprojects/common/common/build.gradle.kts b/subprojects/common/common/build.gradle.kts index 5f55ec589f..971b6106d4 100644 --- a/subprojects/common/common/build.gradle.kts +++ b/subprojects/common/common/build.gradle.kts @@ -15,4 +15,9 @@ */ plugins { id("java-common") + id("kotlin-common") +} + +dependencies { + implementation(Deps.nuprocess) } diff --git a/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/process/SimpleProcessRunner.kt b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/process/SimpleProcessRunner.kt new file mode 100644 index 0000000000..a7964e735e --- /dev/null +++ b/subprojects/common/common/src/main/java/hu/bme/mit/theta/common/process/SimpleProcessRunner.kt @@ -0,0 +1,66 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.process + +import com.zaxxer.nuprocess.NuAbstractProcessHandler +import com.zaxxer.nuprocess.NuProcessBuilder +import java.nio.ByteBuffer +import java.util.concurrent.TimeUnit + +object SimpleProcessRunner { + + fun run(cmd: String, timeout: Long = 0): String { + val processBuilder = NuProcessBuilder(cmd.split(" ")) + val handler = ProcessHandler() + processBuilder.setProcessListener(handler) + processBuilder.start().waitFor(timeout, TimeUnit.SECONDS) + return handler.output + } + + class ProcessHandler : NuAbstractProcessHandler() { + var output: String = "" + var error: String = "" + + override fun onStdout(buffer: ByteBuffer?, closed: Boolean) { + if (!closed && buffer != null) { + val bytes = ByteArray(buffer.remaining()) + buffer[bytes] + output = String(bytes) + } + } + + override fun onStderr(buffer: ByteBuffer?, closed: Boolean) { + if (!closed && buffer != null) { + val bytes = ByteArray(buffer.remaining()) + buffer[bytes] + error = "$error\n${String(bytes)}" + } + } + + override fun onExit(statusCode: Int) { + if (statusCode == Integer.MIN_VALUE) { + throw ProcessException("Nuprocess launch error") + } + if (statusCode != 0) { + throw ProcessException( + if (error != "") error else "Process exit with non-zero code: $statusCode" + ) + } + } + } +} + +class ProcessException(err: String) : Exception(err) diff --git a/subprojects/common/ltl-cli/build.gradle.kts b/subprojects/common/ltl-cli/build.gradle.kts new file mode 100644 index 0000000000..227805593a --- /dev/null +++ b/subprojects/common/ltl-cli/build.gradle.kts @@ -0,0 +1,23 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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. + */ +plugins { + id("kotlin-common") +} + +dependencies { + implementation(project(":theta-analysis")) + implementation(Deps.clikt) +} diff --git a/subprojects/common/ltl-cli/src/main/kotlin/common/ltl/cli/LtlCliOptions.kt b/subprojects/common/ltl-cli/src/main/kotlin/common/ltl/cli/LtlCliOptions.kt new file mode 100644 index 0000000000..2b68427ec9 --- /dev/null +++ b/subprojects/common/ltl-cli/src/main/kotlin/common/ltl/cli/LtlCliOptions.kt @@ -0,0 +1,44 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.ltl.cli + +import com.github.ajalt.clikt.parameters.groups.OptionGroup +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.options.required +import com.github.ajalt.clikt.parameters.types.enum +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy + +open class LtlCliOptions : + OptionGroup(name = "LTL options", help = "Options related to LTL property checking") { + val ltlExpression by option(help = "LTL expression to check").required() + val ltl2BuchiCommand by + option( + help = + "A command that runs on your system. The expression gets appended at the end of it." + + "For example, if you use SPOT, this should be: `spot ltl2tgba -f`" + ) + .required() + val searchStrategy by + option(help = "Which strategy to use for search") + .enum() + .default(LoopcheckerSearchStrategy.GDFS) + val refinerStrategy by + option(help = "Which strategy to use for search") + .enum() + .default(ASGTraceCheckerStrategy.MILANO) +} diff --git a/subprojects/common/ltl/build.gradle.kts b/subprojects/common/ltl/build.gradle.kts new file mode 100644 index 0000000000..6624b9f823 --- /dev/null +++ b/subprojects/common/ltl/build.gradle.kts @@ -0,0 +1,32 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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. + */ +plugins { + id("java-common") + id("kotlin-common") + id("antlr-grammar") +} + +dependencies { + implementation(project(":theta-common")) + implementation(project(":theta-core")) + implementation(project(":theta-solver")) + implementation(project(":theta-analysis")) + implementation(project(":theta-cfa")) + api(project(":theta-cfa-analysis")) + testImplementation(project(":theta-solver-z3-legacy")) + testImplementation(project(":theta-xsts-analysis")) + testImplementation(project(":theta-xsts")) +} diff --git a/subprojects/common/ltl/src/main/antlr/LTLGrammar.g4 b/subprojects/common/ltl/src/main/antlr/LTLGrammar.g4 new file mode 100644 index 0000000000..e133f146ff --- /dev/null +++ b/subprojects/common/ltl/src/main/antlr/LTLGrammar.g4 @@ -0,0 +1,138 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +grammar LTLGrammar; + +model: + rules+=implyExpression*; + +implyExpression: + ops+=orExpr (IMPLIES ops+=orExpr)? +; + +orExpr: + ops+=andExpr (OR ops+=andExpr)* +; + +andExpr: + ops+=notExpr (AND ops+=notExpr)* +; + +notExpr: + binaryLtlExpr| + NOT ops+=notExpr +; + +binaryLtlExpr: + ltlExpr | + ops+=binaryLtlExpr type=binaryLtlOp ops+=binaryLtlExpr; + +binaryLtlOp: + M_OP | W_OP | U_OP | R_OP; + +ltlExpr: + eqExpr | + type=ltlOp ops+=ltlExpr +; + +ltlOp: + F_OP|G_OP|X_OP + ; + +eqExpr: + ops+=relationExpr (oper=eqOperator ops+=relationExpr)? +; + +eqOperator: + EQ|NEQ +; + +relationExpr: + ops+=additiveExpr (oper=relationOperator ops+=additiveExpr)? +; + +relationOperator: + LT|GT|LEQ|GEQ +; + +additiveExpr: + ops+=multiplicativeExpr (opers+=additiveOperator ops+=multiplicativeExpr)* +; + +additiveOperator: + PLUS|MINUS +; + +multiplicativeExpr: + ops+=negExpr (opers+=multiplicativeOperator ops+=negExpr)* +; + +multiplicativeOperator: + MUL|DIV|MOD +; + +negExpr: + primaryExpr| + MINUS ops+=negExpr +; + +primaryExpr: + boolLitExpr| + intLitExpr| + enumLitExpr| + parenExpr +; + +boolLitExpr: + value=BOOLLIT +; + +parenExpr: + LPAREN ops+=implyExpression RPAREN | variable +; + +intLitExpr: + value=INTLIT +; + +enumLitExpr: + type=ID DOT lit=ID +; + +variable: + name=ID +; + +AND: 'and' | '&&'; +OR: 'or' | '|' | '||'; +IMPLIES: '->' | '=>'; +NOT: 'not' | '!'; +EQ: '=' | '=='; +NEQ: '/=' | '!='; +LT: '<'; +GT: '>'; +LEQ: '<='; +GEQ: '>='; +PLUS: '+'; +MINUS: '-'; +MUL: '*'; +DIV: '/'; +MOD: '%'; +LPAREN: '('; +RPAREN: ')'; +F_OP: 'F'; +G_OP: 'G'; +U_OP: 'U'; +W_OP: 'W'; +M_OP: 'M'; +R_OP: 'R'; +X_OP: 'X'; +INTLIT: [0-9]+; +BOOLLIT: 'true' | 'false'; +ID: [a-zA-Z][a-zA-Z0-9_]*; +DOT: '.'; +WS: (' '| '\t' | '\n' | '\r') -> skip; + diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/Ltl2BuchiTransformer.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/Ltl2BuchiTransformer.kt new file mode 100644 index 0000000000..5422c540f7 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/Ltl2BuchiTransformer.kt @@ -0,0 +1,27 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi + +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.core.decl.VarDecl + +fun interface Ltl2BuchiTransformer { + + fun transform(ltl: String, variableMapping: Map>): CFA + + fun transform(ltl: String, variables: Collection>): CFA = + transform(ltl, variables.associateBy { it.name }) +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/APGeneratorVisitor.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/APGeneratorVisitor.kt new file mode 100644 index 0000000000..9668c2f3fa --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/APGeneratorVisitor.kt @@ -0,0 +1,190 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr +import hu.bme.mit.theta.core.type.enumtype.EnumType +import hu.bme.mit.theta.core.type.inttype.IntExprs +import hu.bme.mit.theta.core.type.inttype.IntType +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarBaseVisitor +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarParser +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarParser.* + +class APGeneratorVisitor( + private val vars: Map>, + private val enumTypes: Map, +) : LTLGrammarBaseVisitor?>() { + + override fun visitModel(ctx: ModelContext): Expr<*> { + return super.visitModel(ctx)!! + } + + override fun visitImplyExpression(ctx: ImplyExpressionContext): Expr<*> { + return if (ctx.ops.size > 1) { + BoolExprs.Imply( + visitOrExpr(ctx.ops[0]) as Expr, + visitOrExpr(ctx.ops[1]) as Expr, + ) + } else visitOrExpr(ctx.ops[0]) + } + + override fun visitOrExpr(ctx: LTLGrammarParser.OrExprContext): Expr<*> { + if (ctx.ops.size == 1) return visitAndExpr(ctx.ops[0]) + val ops: MutableList> = ArrayList() + for (child in ctx.ops) { + ops.add(visitAndExpr(child)) + } + return BoolExprs.Or(ops) + } + + override fun visitAndExpr(ctx: LTLGrammarParser.AndExprContext): Expr { + if (ctx.ops.size == 1) return visitNotExpr(ctx.ops[0]) + val ops: MutableList> = ArrayList() + for (child in ctx.ops) { + ops.add(visitNotExpr(child)) + } + return BoolExprs.And(ops) + } + + override fun visitNotExpr(ctx: LTLGrammarParser.NotExprContext): Expr { + return if (ctx.ops.size > 0) BoolExprs.Not(visitNotExpr(ctx.ops[0])) + else visitBinaryLtlExpr(ctx.binaryLtlExpr()) as Expr + } + + override fun visitBinaryLtlExpr(ctx: BinaryLtlExprContext): Expr<*> { + return visitLtlExpr(ctx.ltlExpr()) + } + + override fun visitBinaryLtlOp(ctx: BinaryLtlOpContext): Expr<*> { + return super.visitBinaryLtlOp(ctx)!! + } + + override fun visitLtlExpr(ctx: LtlExprContext): Expr<*> { + return visitEqExpr(ctx.eqExpr()) + } + + override fun visitLtlOp(ctx: LtlOpContext): Expr<*> { + return super.visitLtlOp(ctx)!! + } + + override fun visitEqExpr(ctx: EqExprContext): Expr<*> { + return if (ctx.ops.size > 1) { + if (ctx.oper.EQ() != null) + AbstractExprs.Eq(visitRelationExpr(ctx.ops[0]), visitRelationExpr(ctx.ops[1])) + else AbstractExprs.Neq(visitRelationExpr(ctx.ops[0]), visitRelationExpr(ctx.ops[1])) + } else visitRelationExpr(ctx.ops[0]) + } + + override fun visitEqOperator(ctx: EqOperatorContext): Expr<*> { + return super.visitEqOperator(ctx)!! + } + + override fun visitRelationExpr(ctx: LTLGrammarParser.RelationExprContext): Expr<*> { + return if (ctx.ops.size > 1) { + if (ctx.oper.LEQ() != null) { + AbstractExprs.Leq(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else if (ctx.oper.GEQ() != null) { + AbstractExprs.Geq(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else if (ctx.oper.LT() != null) { + AbstractExprs.Lt(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else AbstractExprs.Gt(visitAdditiveExpr(ctx.ops[0]), visitAdditiveExpr(ctx.ops[1])) + } else visitAdditiveExpr(ctx.ops[0]) + } + + override fun visitRelationOperator(ctx: RelationOperatorContext): Expr<*> { + return super.visitRelationOperator(ctx)!! + } + + override fun visitAdditiveExpr(ctx: LTLGrammarParser.AdditiveExprContext): Expr<*> { + var res = visitMultiplicativeExpr(ctx.ops[0]) + for (i in 1 until ctx.ops.size) { + res = + if (ctx.opers[i - 1].PLUS() != null) { + AbstractExprs.Add(res, visitMultiplicativeExpr(ctx.ops[i])) + } else { + AbstractExprs.Sub(res, visitMultiplicativeExpr(ctx.ops[i])) + } + } + return res + } + + override fun visitAdditiveOperator(ctx: AdditiveOperatorContext): Expr<*> { + return super.visitAdditiveOperator(ctx)!! + } + + override fun visitMultiplicativeExpr(ctx: LTLGrammarParser.MultiplicativeExprContext): Expr<*> { + var res = visitNegExpr(ctx.ops[0]) + for (i in 1 until ctx.ops.size) { + res = + if (ctx.opers[i - 1].DIV() != null) { + AbstractExprs.Div(res, visitNegExpr(ctx.ops[i])) + } else if (ctx.opers[i - 1].MOD() != null) { + IntExprs.Mod(res as Expr, visitNegExpr(ctx.ops[i]) as Expr) + } else { + AbstractExprs.Mul(res, visitNegExpr(ctx.ops[i])) + } + } + return res + } + + override fun visitMultiplicativeOperator(ctx: MultiplicativeOperatorContext): Expr<*> { + return super.visitMultiplicativeOperator(ctx)!! + } + + override fun visitNegExpr(ctx: LTLGrammarParser.NegExprContext): Expr<*> { + return if (ctx.ops.size > 0) { + AbstractExprs.Neg(visitNegExpr(ctx.ops[0])) + } else visitPrimaryExpr(ctx.primaryExpr()) + } + + override fun visitPrimaryExpr(ctx: LTLGrammarParser.PrimaryExprContext): Expr<*> { + return if (ctx.boolLitExpr() != null) { + visitBoolLitExpr(ctx.boolLitExpr()) + } else if (ctx.intLitExpr() != null) { + visitIntLitExpr(ctx.intLitExpr()) + } else if (ctx.enumLitExpr() != null) { + visitEnumLitExpr(ctx.enumLitExpr()) + } else visitParenExpr(ctx.parenExpr()) + } + + override fun visitBoolLitExpr(ctx: BoolLitExprContext): Expr<*> { + return if (ctx.value.text == "true") BoolExprs.True() else BoolExprs.False() + } + + override fun visitParenExpr(ctx: LTLGrammarParser.ParenExprContext): Expr<*> { + return if (ctx.variable() != null) visitVariable(ctx.variable()) + else visitImplyExpression(ctx.ops[0]) + } + + override fun visitIntLitExpr(ctx: LTLGrammarParser.IntLitExprContext): Expr<*> { + return IntExprs.Int(ctx.value.text.toInt()) + } + + override fun visitEnumLitExpr(ctx: EnumLitExprContext): Expr<*> { + return EnumLitExpr.of(enumTypes[ctx.type.text], ctx.lit.text) + } + + override fun visitVariable(ctx: LTLGrammarParser.VariableContext): Expr<*> { + val decl = vars[ctx.name.text] + if (decl == null) println("Variable [" + ctx.name.text + "] not found") + return decl!!.ref + } +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt new file mode 100644 index 0000000000..3820cc1876 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt @@ -0,0 +1,189 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.stmt.Stmts +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.type.booltype.BoolType +import java.util.function.Consumer +import jhoafparser.ast.AtomAcceptance +import jhoafparser.ast.AtomLabel +import jhoafparser.ast.BooleanExpression +import jhoafparser.consumer.HOAConsumer +import jhoafparser.consumer.HOAConsumerException + +class BuchiBuilder +internal constructor( + private val logger: Logger, + private val swappedExpressions: Map>, +) : HOAConsumer { + + private val builder: CFA.Builder = CFA.builder() + private var initLocNumber: Int? = null + private var aps: MutableList? = null + private val locations: MutableMap = HashMap() + + fun build(): CFA { + return builder.build() + } + + private fun getOrCreateLocation(locName: Int): CFA.Loc { + return locations.computeIfAbsent(locName) { i: Int -> builder.createLoc(i.toString()) } + } + + private fun apBoolExpressionToInternal( + booleanExpression: BooleanExpression + ): Expr { + return when (booleanExpression.type) { + BooleanExpression.Type.EXP_AND -> + BoolExprs.And( + apBoolExpressionToInternal(booleanExpression.left), + apBoolExpressionToInternal(booleanExpression.right), + ) + + BooleanExpression.Type.EXP_OR -> + BoolExprs.Or( + apBoolExpressionToInternal(booleanExpression.left), + apBoolExpressionToInternal(booleanExpression.right), + ) + + BooleanExpression.Type.EXP_NOT -> + BoolExprs.Not(apBoolExpressionToInternal(booleanExpression.left)) + BooleanExpression.Type.EXP_TRUE -> BoolExprs.True() + BooleanExpression.Type.EXP_ATOM -> + swappedExpressions[aps!![booleanExpression.atom.toString().toInt()]]!! + else -> BoolExprs.False() + } + } + + override fun parserResolvesAliases(): Boolean { + return false + } + + override fun notifyHeaderStart(s: String) { + logger.write(Logger.Level.VERBOSE, "HOA consumer header: %s%n", s) + } + + override fun setNumberOfStates(i: Int) { + logger.write(Logger.Level.VERBOSE, "HOA automaton has %d states%n", i) + } + + @Throws(HOAConsumerException::class) + override fun addStartStates(list: List) { + if (list.isEmpty()) return + if (list.size != 1 || initLocNumber != null) + throw HOAConsumerException("HOA automaton should have exactly 1 starting location%n") + initLocNumber = list[0] + } + + override fun addAlias(s: String, booleanExpression: BooleanExpression) { + // currently does not get called by the Owl library + } + + override fun setAPs(list: List) { + if (aps == null) aps = java.util.List.copyOf(list) else aps!!.addAll(list) + } + + @Throws(HOAConsumerException::class) + override fun setAcceptanceCondition( + i: Int, + booleanExpression: BooleanExpression, + ) { + logger.write(Logger.Level.VERBOSE, "Acceptance condition: %s%n", booleanExpression) + } + + override fun provideAcceptanceName(s: String, list: List) { + logger.write(Logger.Level.VERBOSE, "Acceptance name received: %s%n", s) + list.forEach( + Consumer { o: Any? -> + logger.write(Logger.Level.VERBOSE, "\tobject under acceptance: %s%n", o) + } + ) + } + + @Throws(HOAConsumerException::class) + override fun setName(s: String) { + logger.write(Logger.Level.VERBOSE, "Automaton named {}%n", s) + } + + override fun setTool(s: String, s1: String) { + logger.write(Logger.Level.VERBOSE, "Tool named %s %s%n", s, s1) + } + + override fun addProperties(list: List) { + if (list.isEmpty()) return + logger.write(Logger.Level.VERBOSE, "Properties:%n") + list.forEach(Consumer { prop: String? -> logger.write(Logger.Level.VERBOSE, "%s", prop) }) + logger.write(Logger.Level.VERBOSE, "%n") + } + + override fun addMiscHeader(s: String, list: List) { + // we don't really care for these yet + } + + override fun notifyBodyStart() { + // no action needed + } + + override fun addState( + i: Int, + s: String?, + booleanExpression: BooleanExpression?, + list: List?, + ) { + getOrCreateLocation(i) + } + + override fun addEdgeImplicit(i: Int, list: List, list1: List) { + TODO("This should only be called for state-based acceptance which is not yet supported") + } + + @Throws(HOAConsumerException::class) + override fun addEdgeWithLabel( + i: Int, + booleanExpression: BooleanExpression, + list: List, + list1: List?, + ) { + val from = getOrCreateLocation(i) + val to = getOrCreateLocation(list[0]) + val edge = + builder.createEdge(from, to, Stmts.Assume(apBoolExpressionToInternal(booleanExpression))) + if (list1 != null && !list1.isEmpty()) builder.setAcceptingEdge(edge) + } + + override fun notifyEndOfState(i: Int) { + // no action needed + } + + @Throws(HOAConsumerException::class) + override fun notifyEnd() { + if (initLocNumber == null) throw HOAConsumerException("No initial location named") + builder.initLoc = locations[initLocNumber] + } + + override fun notifyAbort() { + // never gets called yet + } + + @Throws(HOAConsumerException::class) + override fun notifyWarning(s: String) { + throw HOAConsumerException(s) + } +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/ExternalLtl2Hoaf.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/ExternalLtl2Hoaf.kt new file mode 100644 index 0000000000..4b4ab5b9ae --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/ExternalLtl2Hoaf.kt @@ -0,0 +1,25 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +import hu.bme.mit.theta.common.process.SimpleProcessRunner + +class ExternalLtl2Hoaf(private val cmd: String) : Ltl2Hoaf { + + override fun transform(ltl: String): String { + return SimpleProcessRunner.run("$cmd '$ltl'", 20) + } +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/LTLExprVisitor.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/LTLExprVisitor.kt new file mode 100644 index 0000000000..6d4b8b42e0 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/LTLExprVisitor.kt @@ -0,0 +1,233 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarBaseVisitor +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarParser +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarParser.* +import org.antlr.v4.runtime.ParserRuleContext + +/** + * Returns whether an AST element represents an LTL expression that has no temporal operators. We + * need to convert all these into atomic propositions that Spot can interpret. So in the AST, the F + * G(not err), the largest expression (not err) will be converted to atomic proposition ap0. The + * resulting LTL expression, which now Spot can interpret, is F G ap0. Whether there is an LTL + * expression, is returned by LTLExprVisitor. The link is stored in APGeneratorVisitor's result. + */ +object LTLExprVisitor : LTLGrammarBaseVisitor() { + + var ltl: HashMap = HashMap() + + override fun visitModel(ctx: ModelContext): Boolean { + return super.visitModel(ctx)!! + } + + override fun visitImplyExpression(ctx: ImplyExpressionContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitOrExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitAndExpr(ctx: LTLGrammarParser.AndExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNotExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitNotExpr(ctx: LTLGrammarParser.NotExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNotExpr(op)) { + ltl[ctx] = true + return true + } + } + if (ctx.binaryLtlExpr() != null && visitBinaryLtlExpr(ctx.binaryLtlExpr())) { + ltl[ctx] = true + return true + } + ltl[ctx] = false + return false + } + + override fun visitBinaryLtlExpr(ctx: BinaryLtlExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + if (ctx.type != null) { + ltl[ctx] = true + return true + } + val child = visitLtlExpr(ctx.ltlExpr()) + ltl[ctx] = child + return child + } + + override fun visitBinaryLtlOp(ctx: BinaryLtlOpContext): Boolean { + return false + } + + override fun visitLtlExpr(ctx: LtlExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + if (ctx.type != null) { + ltl[ctx] = true + return true + } + val child = visitEqExpr(ctx.eqExpr()) + ltl[ctx] = child + return child + } + + override fun visitLtlOp(ctx: LtlOpContext): Boolean { + return false + } + + override fun visitEqExpr(ctx: EqExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitRelationExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitEqOperator(ctx: EqOperatorContext): Boolean { + return false + } + + override fun visitRelationExpr(ctx: LTLGrammarParser.RelationExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitAdditiveExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitRelationOperator(ctx: RelationOperatorContext): Boolean { + return false + } + + override fun visitAdditiveExpr(ctx: LTLGrammarParser.AdditiveExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitMultiplicativeExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitAdditiveOperator(ctx: AdditiveOperatorContext): Boolean { + return false + } + + override fun visitMultiplicativeExpr(ctx: LTLGrammarParser.MultiplicativeExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNegExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitMultiplicativeOperator(ctx: MultiplicativeOperatorContext): Boolean { + return false + } + + override fun visitNegExpr(ctx: LTLGrammarParser.NegExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitNegExpr(op)) { + ltl[ctx] = true + return true + } + } + if (ctx.primaryExpr() != null && visitPrimaryExpr(ctx.primaryExpr())) { + ltl[ctx] = true + return true + } + ltl[ctx] = false + return false + } + + override fun visitPrimaryExpr(ctx: LTLGrammarParser.PrimaryExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + var child = false + if (ctx.boolLitExpr() != null) child = visitBoolLitExpr(ctx.boolLitExpr()) + if (ctx.intLitExpr() != null) child = visitIntLitExpr(ctx.intLitExpr()) + if (ctx.parenExpr() != null) child = visitParenExpr(ctx.parenExpr()) + ltl[ctx] = child + return child + } + + override fun visitBoolLitExpr(ctx: BoolLitExprContext): Boolean { + return false + } + + override fun visitParenExpr(ctx: LTLGrammarParser.ParenExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitImplyExpression(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } + + override fun visitIntLitExpr(ctx: LTLGrammarParser.IntLitExprContext): Boolean { + return false + } + + override fun visitVariable(ctx: LTLGrammarParser.VariableContext): Boolean { + return false + } + + override fun visitOrExpr(ctx: LTLGrammarParser.OrExprContext): Boolean { + if (ltl[ctx] != null) return ltl[ctx]!! + for (op in ctx.ops) { + if (visitAndExpr(op)) { + ltl[ctx] = true + return true + } + } + ltl[ctx] = false + return false + } +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2BuchiThroughHoaf.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2BuchiThroughHoaf.kt new file mode 100644 index 0000000000..6244119cf5 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2BuchiThroughHoaf.kt @@ -0,0 +1,46 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.common.cfa.buchi.Ltl2BuchiTransformer +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.enumtype.EnumType +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarLexer +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarParser +import jhoafparser.parser.HOAFParser +import org.antlr.v4.runtime.CharStreams +import org.antlr.v4.runtime.CommonTokenStream + +class Ltl2BuchiThroughHoaf(private val converter: Ltl2Hoaf, private val logger: Logger) : + Ltl2BuchiTransformer { + + override fun transform(ltl: String, namedVariables: Map>): CFA { + val variables = namedVariables.values + val modelContext = + LTLGrammarParser(CommonTokenStream(LTLGrammarLexer(CharStreams.fromString(ltl)))).model() + val enumTypes: Map = + variables.mapNotNull { it.type as? EnumType }.associateBy { it.name } + val toStringVisitor = ToStringVisitor(APGeneratorVisitor(namedVariables, enumTypes)) + val swappedLtl = toStringVisitor.visitModel(modelContext) + val negatedLtl = "!($swappedLtl)" + val hoafExpression = converter.transform(negatedLtl) + val buchiBuilder = BuchiBuilder(logger, toStringVisitor.aps) + HOAFParser.parseHOA(hoafExpression.byteInputStream(), buchiBuilder) + return buchiBuilder.build() + } +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2Hoaf.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2Hoaf.kt new file mode 100644 index 0000000000..e0da409ba3 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2Hoaf.kt @@ -0,0 +1,21 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +fun interface Ltl2Hoaf { + + fun transform(ltl: String): String +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2HoafFromDir.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2HoafFromDir.kt new file mode 100644 index 0000000000..cd27f0c9c5 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/Ltl2HoafFromDir.kt @@ -0,0 +1,30 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +import java.net.URLEncoder +import java.nio.file.Path + +/** + * Provide a directory which contains HOAF files named as their respective LTL expression .hoa. E.g. + * if you have the hoaf representation of `F a` as `/tmp/ltls/F a.hoa`, create this class with + * `/tmp/ltls` and simply call the transform with the ltl expression. + */ +class Ltl2HoafFromDir(private val dir: String) : Ltl2Hoaf { + + override fun transform(ltl: String) = + Path.of("""$dir/${URLEncoder.encode(ltl, "UTF-8")}.hoa""").toFile().readText() +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/ToStringVisitor.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/ToStringVisitor.kt new file mode 100644 index 0000000000..a97a05486a --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/ToStringVisitor.kt @@ -0,0 +1,298 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.cfa.buchi.hoa + +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarBaseVisitor +import hu.bme.mit.theta.ltl.dsl.gen.LTLGrammarParser.* + +class ToStringVisitor(private val apGeneratorVisitor: APGeneratorVisitor) : + LTLGrammarBaseVisitor() { + + var aps: HashMap> = HashMap() + private var counter = 0 + + override fun visitModel(ctx: ModelContext): String { + return visitImplyExpression(ctx.implyExpression) + } + + override fun visitImplyExpression(ctx: ImplyExpressionContext): String { + if (!LTLExprVisitor.visitImplyExpression(ctx)) { + val name = generateApName() + val expr = apGeneratorVisitor.visitImplyExpression(ctx) + aps[name] = expr as Expr + return name + } + return if (ctx.ops.size > 1) { + visitOrExpr(ctx.ops[0]) + " -> " + visitOrExpr(ctx.ops[1]) + } else { + visitOrExpr(ctx.ops[0]) + } + } + + override fun visitOrExpr(ctx: OrExprContext): String { + if (!LTLExprVisitor.visitOrExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitOrExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitAndExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(" | ") + builder.append(visitAndExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitAndExpr(ctx: AndExprContext): String { + if (!LTLExprVisitor.visitAndExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitAndExpr(ctx) + return name + } + val builder = StringBuilder() + builder.append(visitNotExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(" & ") + builder.append(visitNotExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitNotExpr(ctx: NotExprContext): String { + if (!LTLExprVisitor.visitNotExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitNotExpr(ctx) + return name + } + return if (ctx.ops.isNotEmpty()) { + "! " + visitNotExpr(ctx.ops[0]) + } else { + visitBinaryLtlExpr(ctx.binaryLtlExpr()) + } + } + + override fun visitBinaryLtlExpr(ctx: BinaryLtlExprContext): String { + if (!LTLExprVisitor.visitBinaryLtlExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitBinaryLtlExpr(ctx) as Expr + return name + } + return if (ctx.type != null) { + (visitBinaryLtlExpr(ctx.ops[0]) + + " " + + visitBinaryLtlOp(ctx.type) + + " " + + visitBinaryLtlExpr(ctx.ops[1])) + } else { + visitLtlExpr(ctx.ltlExpr()) + } + } + + override fun visitBinaryLtlOp(ctx: BinaryLtlOpContext): String { + return if (ctx.U_OP() != null) { + "U" + } else if (ctx.M_OP() != null) { + "M" + } else if (ctx.W_OP() != null) { + "W" + } else { + "R" + } + } + + override fun visitLtlExpr(ctx: LtlExprContext): String { + if (!LTLExprVisitor.visitLtlExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitLtlExpr(ctx) as Expr + return name + } + return if (ctx.ops.size > 0) { + visitLtlOp(ctx.type) + " " + visitLtlExpr(ctx.ops[0]) + } else { + visitEqExpr(ctx.eqExpr()) + } + } + + override fun visitLtlOp(ctx: LtlOpContext): String { + return if (ctx.F_OP() != null) { + "F" + } else if (ctx.G_OP() != null) { + "G" + } else { + "X" + } + } + + override fun visitEqExpr(ctx: EqExprContext): String { + if (!LTLExprVisitor.visitEqExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitEqExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitRelationExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitEqOperator(ctx.oper)) + builder.append(visitRelationExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitEqOperator(ctx: EqOperatorContext): String { + return if (ctx.EQ() != null) { + "=" + } else { + "/=" + } + } + + override fun visitRelationExpr(ctx: RelationExprContext): String { + if (!LTLExprVisitor.visitRelationExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitRelationExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitAdditiveExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitRelationOperator(ctx.oper)) + builder.append(visitAdditiveExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitRelationOperator(ctx: RelationOperatorContext): String { + return if (ctx.LT() != null) { + "<" + } else if (ctx.GT() != null) { + ">" + } else if (ctx.LEQ() != null) { + "<=" + } else ">=" + } + + override fun visitAdditiveExpr(ctx: AdditiveExprContext): String { + if (!LTLExprVisitor.visitAdditiveExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitAdditiveExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitMultiplicativeExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitAdditiveOperator(ctx.opers[i - 1])) + builder.append(visitMultiplicativeExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitAdditiveOperator(ctx: AdditiveOperatorContext): String { + return if (ctx.PLUS() != null) { + "+" + } else "-" + } + + override fun visitMultiplicativeExpr(ctx: MultiplicativeExprContext): String { + if (!LTLExprVisitor.visitMultiplicativeExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitMultiplicativeExpr(ctx) as Expr + return name + } + val builder = StringBuilder() + builder.append(visitNegExpr(ctx.ops[0])) + for (i in 1 until ctx.ops.size) { + builder.append(visitMultiplicativeOperator(ctx.opers[i - 1])) + builder.append(visitNegExpr(ctx.ops[i])) + } + return builder.toString() + } + + override fun visitMultiplicativeOperator(ctx: MultiplicativeOperatorContext): String { + return if (ctx.MUL() != null) { + "*" + } else if (ctx.MOD() != null) { + "%" + } else "/" + } + + override fun visitNegExpr(ctx: NegExprContext): String { + if (!LTLExprVisitor.visitNegExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitNegExpr(ctx) as Expr + return name + } + return if (ctx.ops.size > 0) { + "- " + visitNegExpr(ctx.ops[0]) + } else { + visitPrimaryExpr(ctx.primaryExpr()) + } + } + + override fun visitPrimaryExpr(ctx: PrimaryExprContext): String { + if (!LTLExprVisitor.visitPrimaryExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitPrimaryExpr(ctx) as Expr + return name + } + return if (ctx.parenExpr() != null) { + visitParenExpr(ctx.parenExpr()) + } else if (ctx.intLitExpr() != null) { + visitIntLitExpr(ctx.intLitExpr()) + } else visitBoolLitExpr(ctx.boolLitExpr()) + } + + override fun visitBoolLitExpr(ctx: BoolLitExprContext): String { + return ctx.value.text + } + + override fun visitParenExpr(ctx: ParenExprContext): String { + if (!LTLExprVisitor.visitParenExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitParenExpr(ctx) as Expr + return name + } + return if (ctx.variable() != null) { + visitVariable(ctx.variable()) + } else { + "(" + visitImplyExpression(ctx.ops[0]) + ")" + } + } + + override fun visitIntLitExpr(ctx: IntLitExprContext): String { + if (!LTLExprVisitor.visitIntLitExpr(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitIntLitExpr(ctx) as Expr + return name + } + return ctx.value.text + } + + override fun visitVariable(ctx: VariableContext): String { + if (!LTLExprVisitor.visitVariable(ctx)) { + val name = generateApName() + aps[name] = apGeneratorVisitor.visitVariable(ctx) as Expr + return name + } + return ctx.name.text + } + + private fun generateApName(): String { + return "ap" + (counter++) + } +} diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt new file mode 100644 index 0000000000..bfe0c7cf79 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt @@ -0,0 +1,187 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.ltl + +import hu.bme.mit.theta.analysis.Analysis +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.SafetyChecker +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleASGTraceRefiner +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.StmtAction +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec +import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide +import hu.bme.mit.theta.analysis.multi.MultiPrec +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.analysis.multi.NextSideFunctions.Alternating +import hu.bme.mit.theta.analysis.multi.RefToMultiPrec +import hu.bme.mit.theta.analysis.multi.builder.stmt.StmtMultiBuilder +import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState +import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction +import hu.bme.mit.theta.analysis.unit.UnitInitFunc +import hu.bme.mit.theta.analysis.unit.UnitPrec +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.analysis.utils.AsgVisualizer +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.* +import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.common.cfa.buchi.Ltl2BuchiTransformer +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.solver.SolverFactory + +class LtlChecker< + S : ExprState, + ControlS : ExprState, + A : StmtAction, + P : Prec, + ControlP : Prec, + DataP : Prec, + DataS : ExprState, +>( + multiSide: MultiAnalysisSide, + lts: LTS, + refToPrec: RefutationToPrec, + dataRefToPrec: RefutationToPrec, + dataAnalysis: Analysis, + ltl: String, + solverFactory: SolverFactory, + logger: Logger, + searchStrategy: LoopcheckerSearchStrategy, + refinerStrategy: ASGTraceCheckerStrategy, + ltl2BuchiTransformer: Ltl2BuchiTransformer, + variables: Collection>, + initExpr: Expr = True(), + nextSideFunction: + NextSideFunctions.NextSideFunction< + ControlS, + CfaState, + DataS, + ExprMultiState, DataS>, + > = + Alternating(), +) : + SafetyChecker< + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, + MultiPrec, DataP>, + > { + val checker: + CegarChecker< + MultiPrec, DataP>, + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, + > + + init { + val buchiAutomaton = ltl2BuchiTransformer.transform(ltl, variables) + val cfaAnalysis: Analysis, CfaAction, CfaPrec> = + CfaAnalysis.create(buchiAutomaton.initLoc, dataAnalysis) + val buchiSide = + MultiAnalysisSide( + cfaAnalysis, + CfaInitFunc.create(buchiAutomaton.initLoc, UnitInitFunc.getInstance()), + ::cfaCombineStates, + ::cfaExtractControlState, + { it.state }, + { _ -> GlobalCfaPrec.create(UnitPrec.getInstance()) }, + ) + val product = + StmtMultiBuilder(multiSide, lts) + .addRightSide(buchiSide, CfaSbeLts.getInstance()) + .build(nextSideFunction, dataAnalysis.initFunc) + val buchiRefToPrec = RefutationToGlobalCfaPrec(dataRefToPrec, buchiAutomaton.initLoc) + val multiRefToPrec = RefToMultiPrec(refToPrec, buchiRefToPrec, dataRefToPrec) + val multiAnalysis = product.side.analysis + val abstractor = + ASGAbstractor( + multiAnalysis, + product.lts, + buchiPredicate(buchiAutomaton), + searchStrategy, + logger, + ) + val refiner: + SingleASGTraceRefiner< + ExprMultiState, DataS>, + StmtMultiAction, + MultiPrec, DataP>, + > = + SingleASGTraceRefiner( + refinerStrategy, + solverFactory, + JoiningPrecRefiner.create(multiRefToPrec), + logger, + initExpr, + ) + val visualizer = + AsgVisualizer< + ExprMultiState, DataS>, + StmtMultiAction, + >( + { it.toString() }, + { "" }, + ) + checker = CegarChecker.create(abstractor, refiner, logger, visualizer) + } + + private fun buchiPredicate( + buchiAutomaton: CFA + ): AcceptancePredicate< + ExprMultiState, DataS>, + StmtMultiAction, + > = + AcceptancePredicate( + actionPredicate = { a -> + (a?.rightAction != null && + a.rightAction.edges.any { e -> buchiAutomaton.acceptingEdges.contains(e) }) + } + ) + + override fun check( + input: MultiPrec, DataP> + ): SafetyResult< + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, + > { + return checker.check(input) + } + + fun check( + prec: P, + dataPrec: DataP, + ): SafetyResult< + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, + > { + return check(MultiPrec(prec, GlobalCfaPrec.create(dataPrec), dataPrec)) + } +} diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt new file mode 100644 index 0000000000..b64a468142 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt @@ -0,0 +1,110 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expl.ExplAnalysis +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.CfaPrec +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.dsl.CfaDslManager +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2HoafFromDir +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import java.io.FileInputStream +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized + +@RunWith(Parameterized::class) +class LtlCheckTestWithCfaExpl( + private val cfaName: String, + private val ltlExpr: String, + private val result: Boolean, +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE) + + companion object { + @JvmStatic + @Parameterized.Parameters + fun data() = + listOf( + arrayOf("counter2inf", "G(x=1)", false), + arrayOf("counter2inf", "G(x=2)", false), + arrayOf("counter2inf", "F G(x=2)", true), + arrayOf("counter2inf", "F(x=1)", true), + arrayOf("counter2inf", "F(x=3)", false), + ) + } + + @Test + fun test() { + abstractionSolver.reset() + var cfaI: CFA? + FileInputStream(String.format("src/test/resources/cfa/%s.cfa", cfaName)).use { inputStream -> + cfaI = CfaDslManager.createCfa(inputStream) + } + if (cfaI == null) fail("Couldn't read cfa $cfaName") + val cfa = cfaI!! + val configBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.EXPL, + CfaConfigBuilder.Refinement.SEQ_ITP, + itpSolverFactory, + ) + .encoding(CfaConfigBuilder.Encoding.SBE) + .ExplStrategy(cfa) + val dataAnalysis = ExplAnalysis.create(abstractionSolver, True()) + val refToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) + val variables = cfa.vars + val dataInitPrec = ExplPrec.of(variables) + val initPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + refToPrec, + configBuilder.itpRefToPrec, + dataAnalysis, + ltlExpr, + itpSolverFactory, + logger, + LoopcheckerSearchStrategy.GDFS, + ASGTraceCheckerStrategy.MILANO, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), + variables, + nextSideFunction = NextSideFunctions.Alternating(), + ) + + Assert.assertEquals(result, checker.check(initPrec, dataInitPrec).isSafe) + } +} diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt new file mode 100644 index 0000000000..95ce8b6652 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt @@ -0,0 +1,133 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.analysis.pred.* +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.dsl.CfaDslManager +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2HoafFromDir +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.type.booltype.BoolExprs.True +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import java.io.FileInputStream +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized + +@RunWith(Parameterized::class) +class LtlCheckTestWithCfaPred( + private val cfaName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: ASGTraceCheckerStrategy, +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.INFO) + + companion object { + fun data() = + listOf( + arrayOf("wave_flags", "F G(x)", false), + arrayOf("wave_flags", "F G(x and y)", false), + arrayOf("wave_flag", "G F(x)", true), + arrayOf("wave_flag", "G(x)", false), + arrayOf("wave_flag", "F G(x)", false), + arrayOf("counter5inf", "G(not(x=6))", true), + arrayOf("counter5inf", "G(x=1)", false), + arrayOf("counter5inf", "G(x=5)", false), + arrayOf("counter5inf", "F G(x=5)", true), + arrayOf("counter5inf", "F(x=1)", true), + arrayOf("counter5inf", "F(x=5)", true), + arrayOf("wave_flags", "G F(y)", true), + arrayOf("wave_flags", "F G(x)", false), + arrayOf("indicator", "G (x -> y)", true), + // arrayOf("indicator_multiassign", "G (x -> y)", true), + arrayOf("indicator", "G (x -> X (not x))", true), + arrayOf("indicator", "G (y -> X (not y))", false), + ) + + @JvmStatic + @Parameterized.Parameters(name = "{3}-{4}: {0}") + fun params() = + listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> + listOf(ASGTraceCheckerStrategy.MILANO, ASGTraceCheckerStrategy.BOUNDED_UNROLLING).flatMap { + ref -> + data().map { arrayOf(*it, search, ref) } + } + } + } + + @Test + fun test() { + abstractionSolver.reset() + var cfaI: CFA? + FileInputStream(String.format("src/test/resources/cfa/%s.cfa", cfaName)).use { inputStream -> + cfaI = CfaDslManager.createCfa(inputStream) + } + if (cfaI == null) fail("Couldn't read cfa $cfaName") + val cfa = cfaI!! + val configBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.PRED_SPLIT, + CfaConfigBuilder.Refinement.SEQ_ITP, + itpSolverFactory, + ) + .encoding(CfaConfigBuilder.Encoding.SBE) + .PredStrategy(cfa) + val variables = cfa.vars + val dataAnalysis = + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + True(), + ) + val refToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) + val dataInitPrec = PredPrec.of() + + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + refToPrec, + configBuilder.itpRefToPrec, + dataAnalysis, + ltlExpr, + itpSolverFactory, + logger, + searchStrategy, + refinerStrategy, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), + variables, + nextSideFunction = NextSideFunctions.Alternating(), + ) + + Assert.assertEquals(result, checker.check(configBuilder.createInitPrec(), dataInitPrec).isSafe) + } +} diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt new file mode 100644 index 0000000000..28508c1288 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt @@ -0,0 +1,117 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.analysis.unit.UnitPrec +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2HoafFromDir +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.XstsAction +import hu.bme.mit.theta.xsts.analysis.XstsState +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass +import java.io.FileInputStream +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized + +@RunWith(Parameterized::class) +class LtlCheckTestWithXstsExpl( + private val xstsName: String, + private val ltlExpr: String, + private val result: Boolean, +) { + + private val solverFactory = Z3LegacySolverFactory.getInstance() + private val logger: Logger = ConsoleLogger(Logger.Level.VERBOSE) + + companion object { + @JvmStatic + @Parameterized.Parameters + fun data() = + listOf( + arrayOf("counter3inf", "F G(x=3)", true), + arrayOf("counter3inf", "F(x=2)", true), + arrayOf("counter3inf", "G(x<4)", true), + arrayOf("counter3inf", "G(x=1)", false), + arrayOf("counter6to7", "G(x=1)", false), + arrayOf("counter6to7", "G(x=7)", false), + arrayOf("counter6to7", "G F(x=7)", true), + ) + } + + @Test + fun test() { + var xstsI: XSTS? + FileInputStream(String.format("src/test/resources/xsts/%s.xsts", xstsName)).use { inputStream -> + xstsI = XstsDslManager.createXsts(inputStream) + } + if (xstsI == null) fail("Couldn't read xsts $xstsName") + val xsts = XstsNormalizerPass.transform(xstsI!!) + val configBuilder: XstsConfigBuilder.ExplStrategy = + XstsConfigBuilder( + XstsConfigBuilder.Domain.EXPL, + XstsConfigBuilder.Refinement.SEQ_ITP, + solverFactory, + solverFactory, + ) + .initPrec(XstsConfigBuilder.InitPrec.EMPTY) + .ExplStrategy(xsts) + val initPrec = configBuilder.initPrec + + val checker: + LtlChecker< + XstsState, + XstsState, + XstsAction, + ExplPrec, + UnitPrec, + ExplPrec, + ExplState, + > = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + configBuilder.itpRefToPrec, + configBuilder.itpRefToPrec, + configBuilder.dataAnalysis, + ltlExpr, + solverFactory, + logger, + LoopcheckerSearchStrategy.GDFS, + ASGTraceCheckerStrategy.MILANO, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), + xsts.vars, + xsts.initFormula, + NextSideFunctions.Alternating(), + ) + val checkResult = checker.check(initPrec, initPrec) + + Assert.assertEquals(result, checkResult.isSafe) + } +} diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt new file mode 100644 index 0000000000..dcc83fa154 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt @@ -0,0 +1,157 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.common.ltl + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.pred.ExprSplitters +import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2HoafFromDir +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.dsl.XstsDslManager +import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass +import java.io.FileInputStream +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized + +@RunWith(Parameterized::class) +class LtlCheckTestWithXstsPred( + private val xstsName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: ASGTraceCheckerStrategy, +) { + + private val itpSolverFactory = Z3LegacySolverFactory.getInstance() + private val abstractionSolver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + private val logger: Logger = ConsoleLogger(Logger.Level.INFO) + + companion object { + private fun data() = + listOf( + arrayOf("simple_types", "F G(color = Colors.Red)", false), + arrayOf("counter3inf", "F G(x=3)", true), + arrayOf("counter3inf", "F(x=2)", true), + arrayOf("counter3inf", "G(x<4)", true), + arrayOf("counter3inf", "G(x=1)", false), + arrayOf("counter6to7", "G(x=1)", false), + arrayOf("counter6to7", "G(x=7)", false), + arrayOf("counter6to7", "G F(x=7)", true), + // arrayOf("counter50", "G(x<49)", false), + arrayOf( + "trafficlight_v2", + "G(LightCommands_displayRed -> X(not LightCommands_displayGreen))", + true, + ), + arrayOf( + "trafficlight_v2", + "G((main_region = Main_region.Normal and normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle and (X(not PoliceInterrupt_police))) -> X(X(normal = Normal.Green)))", + true, + ), + arrayOf( + "trafficlight_v2", + "G(PoliceInterrupt_police -> F(LightCommands_displayYellow))", + true, + ), + arrayOf("forever5", "G(x=5)", true), + arrayOf("forever5", "F(x=6)", false), + arrayOf("randomincreasingeven", "not F(x=1)", true), + arrayOf("randomincreasingeven", "F(x>10)", true), + arrayOf("randomincreasingeven", "G(x>=0)", true), + arrayOf("simple_color", "G(envColor = Colors.Green -> X(modelColor = Colors.Blue))", true), + arrayOf( + "simple_color", + "G(envColor = Colors.Green -> X(modelColor = Colors.Green))", + false, + ), + arrayOf("simple_color", "F G(envColor = modelColor)", false), + arrayOf("weather", "G F(isClever and isWet)", false), + arrayOf("weather", "F G(not isWet)", true), + arrayOf( + "weather", + "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))", + true, + ), + // arrayOf("weather", "F G(weather = Weather.Foggy -> (clothing = + // Clothing.Nothing or clothing = Clothing.Warm))", true), + // arrayOf("weather_noinit", "G F(isClever and isWet)", false), + // arrayOf("weather_noinit", "F G(not isWet)", true), + // arrayOf("weather_noinit", "G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon + // or time = TimeOfDay.Afternoon))", true), + // arrayOf("weather_noinit", "F G(weather = Weather.Foggy -> (clothing = + // Clothing.Nothing or clothing = Clothing.Warm))", true), + ) + + @JvmStatic + @Parameterized.Parameters(name = "{3}-{4}: {0}") + fun params() = + listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> + ASGTraceCheckerStrategy.entries.flatMap { ref -> data().map { arrayOf(*it, search, ref) } } + } + } + + @Test + fun test() { + var xstsI: XSTS? + FileInputStream("src/test/resources/xsts/$xstsName.xsts").use { inputStream -> + xstsI = XstsDslManager.createXsts(inputStream) + } + if (xstsI == null) fail("Couldn't read xsts $xstsName") + val xsts = XstsNormalizerPass.transform(xstsI!!) + val configBuilder = + XstsConfigBuilder( + XstsConfigBuilder.Domain.PRED_SPLIT, + XstsConfigBuilder.Refinement.SEQ_ITP, + itpSolverFactory, + itpSolverFactory, + ) + .initPrec(XstsConfigBuilder.InitPrec.EMPTY) + .PredStrategy(xsts) + val variables = xsts.vars + val refToPrec = ItpRefToPredPrec(ExprSplitters.atoms()) + val initPrec = configBuilder.initPrec + + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + refToPrec, + refToPrec, + configBuilder.dataAnalysis, + ltlExpr, + itpSolverFactory, + logger, + searchStrategy, + refinerStrategy, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), + variables, + xsts.initFormula, + ) + + val safetyResult = checker.check(initPrec, initPrec) + Assert.assertEquals(result, safetyResult.isSafe) + } +} diff --git a/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa b/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa new file mode 100644 index 0000000000..81e578cc5d --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/counter2inf.cfa @@ -0,0 +1,12 @@ +main process cfa { + var x : int + + init loc I + loc L0 + loc L1 + + I -> L0 { x := 0 } + L0 -> L1 { assume x < 2 } + L1 -> L0 { x := x + 1 } + L0 -> L0 { assume x = 2 } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa b/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa new file mode 100644 index 0000000000..6fb102aaf8 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/counter5inf.cfa @@ -0,0 +1,12 @@ +main process cfa { + var x : int + + init loc I + loc L0 + loc L1 + + I -> L0 { x := 0 } + L0 -> L1 { assume x < 5 } + L1 -> L0 { x := x + 1 } + L0 -> L0 { assume x = 5 } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa b/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa new file mode 100644 index 0000000000..c8a7062768 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/indicator.cfa @@ -0,0 +1,14 @@ +main process cfa { + var x : bool + var y : bool + + loc L0 + loc L1 + init loc L2 + loc L3 + + L0 -> L1 { y := true } + L1 -> L2 { x := true } + L2 -> L3 { x := false } + L3 -> L0 { y := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa b/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa new file mode 100644 index 0000000000..8330500158 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/indicator_multiassign.cfa @@ -0,0 +1,12 @@ +main process cfa { + var x : bool + var y : bool + + loc L0 + loc L1 + init loc L2 + + L0 -> L1 { y := true } + L1 -> L2 { x := true } + L2 -> L0 { y := false x := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa b/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa new file mode 100644 index 0000000000..77322ac49d --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/wave_flag.cfa @@ -0,0 +1,9 @@ +main process cfa { + var x : bool + + init loc L0 + loc L1 + + L0 -> L1 { x := true } + L1 -> L0 { x := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa b/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa new file mode 100644 index 0000000000..dc192bb7e5 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/cfa/wave_flags.cfa @@ -0,0 +1,18 @@ +main process cfa { + var x : bool + var y : bool + + init loc I0 + loc I1 + loc L0 + loc L1 + loc L2 + loc L3 + + I0 -> I1 { x := false } + I1 -> L0 { y := false } + L0 -> L1 { y := true } + L1 -> L2 { y := false x := true } + L2 -> L3 { y := true } + L3 -> L0 { y := false x := false } +} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28%21+F+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28%21+F+ap0%29.hoa new file mode 100644 index 0000000000..5feaea29ec --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28%21+F+ap0%29.hoa @@ -0,0 +1,18 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(ap0)" +owlArgs: "ltl2nba" "-f" "!(! F ap0)" "-o" "src/test/resources/hoa/%21%28%21+F+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +properties: complete +AP: 1 "ap0" +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[t] 1 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28F+G+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+G+ap0%29.hoa new file mode 100644 index 0000000000..26792660e6 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+G+ap0%29.hoa @@ -0,0 +1,16 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for G(F(!ap0))" +owlArgs: "ltl2nba" "-f" "!(F G ap0)" "-o" "src/test/resources/hoa/%21%28F+G+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +properties: complete +AP: 1 "ap0" +--BODY-- +State: 0 +[!0] 0 {0} +[0] 0 +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28F+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+ap0%29.hoa new file mode 100644 index 0000000000..aa31b46518 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28F+ap0%29.hoa @@ -0,0 +1,14 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for G(!ap0)" +owlArgs: "ltl2nba" "-f" "!(F ap0)" "-o" "src/test/resources/hoa/%21%28F+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +AP: 1 "ap0" +--BODY-- +State: 0 +[!0] 0 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa new file mode 100644 index 0000000000..4f293da548 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa @@ -0,0 +1,20 @@ +HOA: v1 +tool: "owl ltl2ngba" "21.0" +name: "Automaton for F(((ap0) & (ap1) & (ap2) & (ap3) & (X(ap4)) & (X(X(!ap5)))))" +owlArgs: "ltl2ngba" "-f" "!(G ((ap0 & ap1 & ap2 & ap3 & (X ap4)) -> X (X ap5)))" "-o" "%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 6 "ap0" "ap1" "ap2" "ap3" "ap4" "ap5" +--BODY-- +State: 0 +[t] 0 +[0 & 1 & 2 & 3] 1 +State: 1 +[4] 2 +State: 2 +[!5] 3 +State: 3 +[t] 3 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa new file mode 100644 index 0000000000..5da3686644 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa @@ -0,0 +1,16 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(((ap0) & (G(!ap1))))" +owlArgs: "ltl2nba" "-f" "!(G (ap0 -> F ap1))" "-o" "src/test/resources/hoa/%21%28G+%28ap0+-%3E+F+ap1%29%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 2 "ap0" "ap1" +--BODY-- +State: 0 +[t] 0 +[0 & !1] 1 +State: 1 +[!1] 1 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa new file mode 100644 index 0000000000..abb333bb18 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa @@ -0,0 +1,18 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(((ap0) & (X(!ap1))))" +owlArgs: "ltl2nba" "-f" "!(G (ap0 -> X ap1))" "-o" "src/test/resources/hoa/%21%28G+%28ap0+-%3E+X+ap1%29%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 2 "ap0" "ap1" +--BODY-- +State: 0 +[t] 0 +[0] 1 +State: 1 +[!1] 2 +State: 2 +[t] 2 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+F+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+F+ap0%29.hoa new file mode 100644 index 0000000000..a51520dce0 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+F+ap0%29.hoa @@ -0,0 +1,16 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(G(!ap0))" +owlArgs: "ltl2nba" "-f" "!(G F ap0)" "-o" "src/test/resources/hoa/%21%28G+F+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 1 "ap0" +--BODY-- +State: 0 +[t] 0 +[!0] 1 +State: 1 +[!0] 1 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+ap0%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+ap0%29.hoa new file mode 100644 index 0000000000..f132de74f4 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+ap0%29.hoa @@ -0,0 +1,18 @@ +HOA: v1 +tool: "owl ltl2nba" "21.0" +name: "Automaton for F(!ap0)" +owlArgs: "ltl2nba" "-f" "!(G ap0)" "-o" "src/test/resources/hoa/%21%28G+ap0%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +properties: deterministic unambiguous +properties: complete +AP: 1 "ap0" +--BODY-- +State: 0 +[0] 0 +[!0] 1 +State: 1 +[t] 1 {0} +--END-- diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts new file mode 100644 index 0000000000..af2080f290 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/counter3inf.xsts @@ -0,0 +1,12 @@ +var x: integer = 0 + +trans { + assume x<3; + x:=x+1; +} or { + assume x>=3; +} + +init {} +env {} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts new file mode 100644 index 0000000000..ffed019bc4 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/counter50.xsts @@ -0,0 +1,16 @@ +ctrl var x: integer = 0 + +trans { + choice { + assume x<50; + x:=x+1; + } or { + assume x == 50; + } +} + +init {} + +env {} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts b/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts new file mode 100644 index 0000000000..f331be2ee6 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/counter6to7.xsts @@ -0,0 +1,13 @@ +var x: integer = 0 + +trans { + assume x<=6; + x:=x+1; +} or { + assume x==7; + x:=x-1; +} + +init {} +env {} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts b/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts new file mode 100644 index 0000000000..975cfc8f93 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/forever5.xsts @@ -0,0 +1,9 @@ +var x: integer = 5 + +trans { + x:=x; +} + +init {} +env {} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts b/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts new file mode 100644 index 0000000000..d6f9c53796 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/randomincreasingeven.xsts @@ -0,0 +1,14 @@ +var x: integer = 0 +var y: integer = 0 + +trans { + if (y < 0) y := -y; + if (y == 0) y := 1; + if (y % 2 == 1) y := y + 1; + x:= x + y; +} +init {} +env { + havoc y; +} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts b/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts new file mode 100644 index 0000000000..6443992dff --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/simple_color.xsts @@ -0,0 +1,24 @@ +type Colors : { Red, Green, Blue} +var envColor : Colors = Red +var modelColor : Colors = Red + +trans { + choice { + assume envColor == Red; + modelColor := Green; + } or { + assume envColor == Green; + modelColor := Blue; + } or { + assume envColor == Blue; + modelColor := Red; + } +} + +init{} + +env { + havoc envColor; +} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts b/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts new file mode 100644 index 0000000000..3f1dda287f --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/simple_types.xsts @@ -0,0 +1,16 @@ +type Abc : { A, B, C, D} +type Colors : { Red, Green, Blue} +var letter : Abc = A +var color : Colors = Red + +trans { + havoc letter; +} + +init{} + +env { + havoc color; +} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts b/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts new file mode 100644 index 0000000000..e2f50cef51 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/trafficlight_v2.xsts @@ -0,0 +1,169 @@ +type Main_region : { __Inactive__, Interrupted, Normal} +type Normal : { __Inactive__, Green, Red, Yellow} +type Interrupted : { __Inactive__, Black, BlinkingYellow} +var PoliceInterrupt_police : boolean = false +var LightCommands_displayRed : boolean = false +var Control_toggle : boolean = false +var LightCommands_displayYellow : boolean = false +var LightCommands_displayNone : boolean = false +var LightCommands_displayGreen : boolean = false +ctrl var main_region : Main_region = __Inactive__ +ctrl var normal : Normal = __Inactive__ +ctrl var interrupted : Interrupted = __Inactive__ +ctrl var BlackTimeout3 : integer = 500 +ctrl var BlinkingYellowTimeout4 : integer = 500 +var c : boolean = true +var b : integer = 0 +var asd : integer = 0 +var a : boolean = false + +trans { + choice { + assume ((!(((main_region == Interrupted) && (PoliceInterrupt_police == true)))) && (((main_region == Interrupted) && (interrupted == BlinkingYellow)) && (500 <= BlinkingYellowTimeout4))); + assume (interrupted == BlinkingYellow); + interrupted := Black; + assume (interrupted == Black); + BlackTimeout3 := 0; + LightCommands_displayNone := true; + } or { + assume ((!(((main_region == Interrupted) && (PoliceInterrupt_police == true)))) && (((main_region == Interrupted) && (interrupted == Black)) && (500 <= BlackTimeout3))); + assume (interrupted == Black); + interrupted := BlinkingYellow; + assume (interrupted == BlinkingYellow); + BlinkingYellowTimeout4 := 0; + LightCommands_displayYellow := true; + } or { + assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Green)) && (Control_toggle == true))); + assume (normal == Green); + b := 4; + normal := Yellow; + assume (normal == Yellow); + LightCommands_displayYellow := true; + } or { + assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Red)) && (Control_toggle == true))); + assume (normal == Red); + a := true; + normal := Green; + assume (normal == Green); + LightCommands_displayGreen := true; + } or { + assume ((!(((main_region == Normal) && (PoliceInterrupt_police == true)))) && (((main_region == Normal) && (normal == Yellow)) && (Control_toggle == true))); + assume (normal == Yellow); + normal := Red; + assume (normal == Red); + LightCommands_displayRed := true; + } or { + assume (((main_region == Interrupted) && (PoliceInterrupt_police == true))); + assume (main_region == Interrupted); + interrupted := __Inactive__; + main_region := Normal; + choice { + assume (normal == __Inactive__); + normal := Red; + } or { + assume !((normal == __Inactive__)); + } + assume (main_region == Normal); + choice { + assume (normal == Green); + LightCommands_displayGreen := true; + } or { + assume (normal == Red); + LightCommands_displayRed := true; + } or { + assume (normal == Yellow); + LightCommands_displayYellow := true; + } + } or { + assume (((main_region == Normal) && (PoliceInterrupt_police == true))); + assume (main_region == Normal); + choice { + assume (normal == Green); + } or { + assume (normal == Red); + a := true; + } or { + assume (normal == Yellow); + } + asd := 321; + main_region := Interrupted; + interrupted := BlinkingYellow; + assume (main_region == Interrupted); + choice { + assume (interrupted == Black); + BlackTimeout3 := 0; + LightCommands_displayNone := true; + } or { + assume (interrupted == BlinkingYellow); + BlinkingYellowTimeout4 := 0; + LightCommands_displayYellow := true; + } + } +} + +init { + c := true; + b := 0; + a := false; + asd := 0; + BlackTimeout3 := 500; + BlinkingYellowTimeout4 := 500; + normal := __Inactive__; + interrupted := __Inactive__; + PoliceInterrupt_police := false; + Control_toggle := false; + LightCommands_displayRed := false; + LightCommands_displayYellow := false; + LightCommands_displayNone := false; + LightCommands_displayGreen := false; + main_region := Normal; + choice { + assume (normal == __Inactive__); + normal := Red; + } or { + assume !((normal == __Inactive__)); + } + choice { + assume (main_region == Interrupted); + choice { + assume (interrupted == Black); + BlackTimeout3 := 0; + LightCommands_displayNone := true; + } or { + assume (interrupted == BlinkingYellow); + BlinkingYellowTimeout4 := 0; + LightCommands_displayYellow := true; + } + } or { + assume (main_region == Normal); + choice { + assume (normal == Green); + LightCommands_displayGreen := true; + } or { + assume (normal == Red); + LightCommands_displayRed := true; + } or { + assume (normal == Yellow); + LightCommands_displayYellow := true; + } + } +} + +env { + choice { + PoliceInterrupt_police := true; + } or { + PoliceInterrupt_police := false; + } + choice { + Control_toggle := true; + } or { + Control_toggle := false; + } + LightCommands_displayYellow := false; + LightCommands_displayRed := false; + LightCommands_displayNone := false; + LightCommands_displayGreen := false; +} + +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather.xsts new file mode 100644 index 0000000000..b5d9da75dc --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/weather.xsts @@ -0,0 +1,104 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { Morning , Noon, Afternoon, Night } +type Clothing : { Nothing, Shorts, Warm, Waterproof } +var isWet : boolean = false +var looksOut : boolean = false +var isClever : boolean = false +var weather : Weather = Sunny +var time : TimeOfDay +var clothing : Clothing = Nothing + +trans { + choice { + assume time == Morning; + choice { + assume (looksOut == false && isClever == false); + havoc clothing; + } or { + assume (looksOut == true && isClever == false); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Foggy); + clothing := Warm; + } or { + assume weather == Rainy; + clothing := Waterproof; + } + } or { + assume (isClever == true); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Rainy); + clothing := Waterproof; + } or { + assume weather == Foggy; + clothing := Warm; + } + } + } or { + assume time == Noon; + if (isWet == true) looksOut := true; + } or { + assume time == Afternoon; + } or { + assume time == Night; + if (isWet == true) isClever := true; + clothing := Nothing; + } +} + +init { + havoc weather; + time := Morning; +} + +env { + if (clothing != Waterproof && weather == Rainy) isWet := true; + if (time == Noon || time == Night) isWet := false; + choice { + assume time == Morning; + time := Noon; + } or { + assume time == Noon; + time := Afternoon; + } or { + assume time == Afternoon; + time := Night; + } or { + assume time == Night; + time := Morning; + } + + choice { + assume time != Noon; + choice { + assume (weather == Sunny || weather == Cloudy || weather == Foggy); + choice { + weather := Cloudy; + } or { + weather := Sunny; + } or { + assume weather == Cloudy; + weather := Rainy; + } + } or { + assume (weather == Rainy); + choice { + weather := Rainy; + } or { + weather := Sunny; + } + } or { + assume time == Morning; + weather := Foggy; + } + } or { + assume time == Noon; + } + +} +prop {true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts new file mode 100644 index 0000000000..78f5efe332 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/weather_noinit.xsts @@ -0,0 +1,106 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { __init__, Morning , Noon, Afternoon, Night } +type Clothing : { Nothing, Shorts, Warm, Waterproof } +var isWet : boolean = false +var looksOut : boolean = false +var isClever : boolean = false +var weather : Weather = Sunny +var time : TimeOfDay = __init__ +var clothing : Clothing = Nothing + +trans { + choice { + assume time == Morning; + choice { + assume (looksOut == false && isClever == false); + havoc clothing; + } or { + assume (looksOut == true && isClever == false); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Foggy); + clothing := Warm; + } or { + assume weather == Rainy; + clothing := Waterproof; + } + } or { + assume (isClever == true); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Rainy); + clothing := Waterproof; + } or { + assume weather == Foggy; + clothing := Warm; + } + } + } or { + assume time == Noon; + if (isWet == true) looksOut := true; + } or { + assume time == Afternoon; + } or { + assume time == Night; + if (isWet == true) isClever := true; + clothing := Nothing; + } +} + +init { } + +env { + choice { + assume time == __init__; + time := Morning; + } or { + assume time != __init__; + if (clothing != Waterproof && weather == Rainy) isWet := true; + if (time == Noon || time == Night) isWet := false; + choice { + assume time == Morning; + time := Noon; + } or { + assume time == Noon; + time := Afternoon; + } or { + assume time == Afternoon; + time := Night; + } or { + assume time == Night; + time := Morning; + } + + choice { + assume time != Noon; + choice { + assume (weather == Sunny || weather == Cloudy || weather == Foggy); + choice { + weather := Cloudy; + } or { + weather := Sunny; + } or { + assume weather == Cloudy; + weather := Rainy; + } + } or { + assume (weather == Rainy); + choice { + weather := Rainy; + } or { + weather := Sunny; + } + } or { + assume time == Morning; + weather := Foggy; + } + } or { + assume time == Noon; + } + } +} +prop{true} \ No newline at end of file diff --git a/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts b/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts new file mode 100644 index 0000000000..4cdde5291a --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/xsts/weather_withprops.xsts @@ -0,0 +1,105 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { Morning , Noon, Afternoon, Night } +type Clothing : { Nothing, Shorts, Warm, Waterproof } +var isWet : boolean = false +var looksOut : boolean = false +var isClever : boolean = false +var weather : Weather = Sunny +var time : TimeOfDay +var clothing : Clothing = Nothing + +trans { + choice { + assume time == Morning; + choice { + assume (looksOut == false && isClever == false); + havoc clothing; + } or { + assume (looksOut == true && isClever == false); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Foggy); + clothing := Warm; + } or { + assume weather == Rainy; + clothing := Waterproof; + } + } or { + assume (isClever == true); + choice { + assume weather == Sunny; + clothing := Shorts; + } or { + assume (weather == Cloudy || weather == Rainy); + clothing := Waterproof; + } or { + assume weather == Foggy; + clothing := Warm; + } + } + } or { + assume time == Noon; + if (isWet == true) looksOut := true; + } or { + assume time == Afternoon; + } or { + assume time == Night; + if (isWet == true) isClever := true; + clothing := Nothing; + } +} + +init { + havoc weather; + time := Morning; +} + +env { + if (clothing != Waterproof && weather == Rainy) isWet := true; + if (time == Noon || time == Night) isWet := false; + choice { + assume time == Morning; + time := Noon; + } or { + assume time == Noon; + time := Afternoon; + } or { + assume time == Afternoon; + time := Night; + } or { + assume time == Night; + time := Morning; + } + + choice { + assume time != Noon; + choice { + assume (weather == Sunny || weather == Cloudy || weather == Foggy); + choice { + weather := Cloudy; + } or { + weather := Sunny; + } or { + assume weather == Cloudy; + weather := Rainy; + } + } or { + assume (weather == Rainy); + choice { + weather := Rainy; + } or { + weather := Sunny; + } + } or { + assume time == Morning; + weather := Foggy; + } + } or { + assume time == Noon; + } + +} +prop{true} +ltl{G(time = TimeOfDay.Noon -> X(time = TimeOfDay.Noon or time = TimeOfDay.Afternoon))} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt index 0e22456a0d..1408a365aa 100644 --- a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt +++ b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt @@ -41,132 +41,150 @@ import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory import hu.bme.mit.theta.xsts.XSTS import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.dsl.XstsDslManager -import org.junit.Test -import org.junit.jupiter.api.Assertions.assertEquals -import org.junit.jupiter.api.Assertions.assertTrue import java.io.FileInputStream import java.io.IOException import java.io.SequenceInputStream +import org.junit.Test +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue class MultiAlternatingTest { - val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP) - val solver: Solver = Z3LegacySolverFactory.getInstance().createSolver() - - @Test - fun testExplPrec() { - var xsts: XSTS - try { - SequenceInputStream( - FileInputStream("src/test/resources/xsts/incrementor.xsts"), - FileInputStream("src/test/resources/xsts/xneq7.prop") - ).use { inputStream -> - xsts = XstsDslManager.createXsts(inputStream) - } - } catch (e: IOException) { - throw RuntimeException(e) - } - - val xstsConfigBuilder = XstsConfigBuilder( - XstsConfigBuilder.Domain.EXPL, - XstsConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance(), - Z3LegacySolverFactory.getInstance() - ) - val xstsExplBuilder = xstsConfigBuilder.ExplStrategy(xsts) - - val variables = xsts.vars + val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP) + val solver: Solver = Z3LegacySolverFactory.getInstance().createSolver() - var originalCfa: CFA - FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> - originalCfa = CfaDslManager.createCfa(inputStream) - } - val cfa = originalCfa.copyWithReplacingVars(variables.associateBy { it.name }) - val cfaConfigBuilder = CfaConfigBuilder( - CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance() + @Test + fun testExplPrec() { + var xsts: XSTS + try { + SequenceInputStream( + FileInputStream("src/test/resources/xsts/incrementor.xsts"), + FileInputStream("src/test/resources/xsts/xneq7.prop"), ) - cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) - val cfaExplBuilder = cfaConfigBuilder.ExplStrategy(cfa) - - val dataAnalysis = xstsExplBuilder.dataAnalysis - val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) - val dataInitPrec = ExplPrec.of(variables) - val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) - val product = StmtMultiBuilder(cfaExplBuilder.multiSide, cfaExplBuilder.lts).addRightSide( - xstsExplBuilder.multiSide, xstsExplBuilder.lts - ).build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) - val prop = Not(xsts.prop) - val dataPredicate = ExplStatePredicate(prop, solver) - val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( - product, prop, - MultiStatePredicate(dataPredicate), - cfaRefToPrec, ItpRefToExplPrec(), ItpRefToExplPrec(), cfaInitPrec, - dataInitPrec, dataInitPrec, Z3LegacySolverFactory.getInstance(), logger - ) - val result = multiConfigBuilder.build().check() - - assertTrue(result.isUnsafe) - assertEquals(8, result.asUnsafe().cex.length()) + .use { inputStream -> xsts = XstsDslManager.createXsts(inputStream) } + } catch (e: IOException) { + throw RuntimeException(e) } - @Test - fun testPredPrec() { - var xsts: XSTS - try { - SequenceInputStream( - FileInputStream("src/test/resources/xsts/incrementor.xsts"), - FileInputStream("src/test/resources/xsts/xneq7.prop") - ).use { inputStream -> - xsts = XstsDslManager.createXsts(inputStream) - } - } catch (e: IOException) { - throw RuntimeException(e) - } - - val xstsConfigBuilder = XstsConfigBuilder( - XstsConfigBuilder.Domain.PRED_BOOL, - XstsConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance(), - Z3LegacySolverFactory.getInstance() - ) - val xstsPredBuilder = xstsConfigBuilder.PredStrategy(xsts) - val dataAnalysis = xstsPredBuilder.dataAnalysis - - var cfa: CFA - FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> - cfa = CfaDslManager.createCfa(inputStream) - } - cfa = cfa.copyWithReplacingVars(xsts.vars.associateBy { it.name }) - val cfaConfigBuilder = CfaConfigBuilder( - CfaConfigBuilder.Domain.PRED_BOOL, - CfaConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance() - ) - cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) - val cfaPredBuilder = cfaConfigBuilder.PredStrategy(cfa) - val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) - val dataInitPrec = PredPrec.of() - val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val xstsConfigBuilder = + XstsConfigBuilder( + XstsConfigBuilder.Domain.EXPL, + XstsConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + Z3LegacySolverFactory.getInstance(), + ) + val xstsExplBuilder = xstsConfigBuilder.ExplStrategy(xsts) - val product = StmtMultiBuilder(cfaPredBuilder.multiSide, cfaPredBuilder.lts) - .addRightSide(xstsPredBuilder.multiSide, xstsPredBuilder.lts) - .build( - NextSideFunctions.Alternating(), - dataAnalysis.initFunc - ) - val prop = Not(xsts.prop) - val dataPredicate = ExprStatePredicate(prop, solver) + val variables = xsts.vars - val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( - product, prop, - MultiStatePredicate(dataPredicate), - cfaRefToPrec, ItpRefToPredPrec(ExprSplitters.atoms()), ItpRefToPredPrec(ExprSplitters.atoms()), cfaInitPrec, - dataInitPrec, dataInitPrec, Z3LegacySolverFactory.getInstance(), logger + var originalCfa: CFA + FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> + originalCfa = CfaDslManager.createCfa(inputStream) + } + val cfa = originalCfa.copyWithReplacingVars(variables.associateBy { it.name }) + val cfaConfigBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.EXPL, + CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + ) + cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfaExplBuilder = cfaConfigBuilder.ExplStrategy(cfa) + + val dataAnalysis = xstsExplBuilder.dataAnalysis + val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) + val dataInitPrec = ExplPrec.of(variables) + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val product = + StmtMultiBuilder(cfaExplBuilder.multiSide, cfaExplBuilder.lts) + .addRightSide(xstsExplBuilder.multiSide, xstsExplBuilder.lts) + .build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val prop = Not(xsts.prop) + val dataPredicate = ExplStatePredicate(prop, solver) + val multiConfigBuilder = + StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( + product, + prop, + MultiStatePredicate(dataPredicate), + cfaRefToPrec, + ItpRefToExplPrec(), + ItpRefToExplPrec(), + cfaInitPrec, + dataInitPrec, + dataInitPrec, + Z3LegacySolverFactory.getInstance(), + logger, + ) + val result = multiConfigBuilder.build().check() + + assertTrue(result.isUnsafe) + assertEquals(8, result.asUnsafe().cex.length()) + } + + @Test + fun testPredPrec() { + var xsts: XSTS + try { + SequenceInputStream( + FileInputStream("src/test/resources/xsts/incrementor.xsts"), + FileInputStream("src/test/resources/xsts/xneq7.prop"), ) - val result = multiConfigBuilder.build().check() - - assertTrue(result.isUnsafe) + .use { inputStream -> xsts = XstsDslManager.createXsts(inputStream) } + } catch (e: IOException) { + throw RuntimeException(e) } -} \ No newline at end of file + val xstsConfigBuilder = + XstsConfigBuilder( + XstsConfigBuilder.Domain.PRED_BOOL, + XstsConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + Z3LegacySolverFactory.getInstance(), + ) + val xstsPredBuilder = xstsConfigBuilder.PredStrategy(xsts) + val dataAnalysis = xstsPredBuilder.dataAnalysis + + var cfa: CFA + FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> + cfa = CfaDslManager.createCfa(inputStream) + } + cfa = cfa.copyWithReplacingVars(xsts.vars.associateBy { it.name }) + val cfaConfigBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.PRED_BOOL, + CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + ) + cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfaPredBuilder = cfaConfigBuilder.PredStrategy(cfa) + val cfaRefToPrec = + RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) + val dataInitPrec = PredPrec.of() + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + + val product = + StmtMultiBuilder(cfaPredBuilder.multiSide, cfaPredBuilder.lts) + .addRightSide(xstsPredBuilder.multiSide, xstsPredBuilder.lts) + .build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val prop = Not(xsts.prop) + val dataPredicate = ExprStatePredicate(prop, solver) + + val multiConfigBuilder = + StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( + product, + prop, + MultiStatePredicate(dataPredicate), + cfaRefToPrec, + ItpRefToPredPrec(ExprSplitters.atoms()), + ItpRefToPredPrec(ExprSplitters.atoms()), + cfaInitPrec, + dataInitPrec, + dataInitPrec, + Z3LegacySolverFactory.getInstance(), + logger, + ) + val result = multiConfigBuilder.build().check() + + assertTrue(result.isUnsafe) + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt index afda5eb642..e8afeb3081 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.analysis.util import hu.bme.mit.theta.analysis.Prec @@ -23,15 +22,19 @@ import hu.bme.mit.theta.analysis.unit.UnitState import hu.bme.mit.theta.xsts.analysis.XstsState fun xstsCombineStates(xstsState: XstsState, dataState: S): XstsState { - return XstsState.of(dataState, xstsState.lastActionWasEnv(), xstsState.isInitialized) + return XstsState.of(dataState, xstsState.lastActionWasEnv(), xstsState.isInitialized) } fun xstsExtractControlState(xstsState: XstsState<*>): XstsState { - return XstsState.of(UnitState.getInstance(), xstsState.lastActionWasEnv(), xstsState.isInitialized) + return XstsState.of( + UnitState.getInstance(), + xstsState.lastActionWasEnv(), + xstsState.isInitialized, + ) } fun xstsExtractDataState(xstsState: XstsState): S { - return xstsState.state + return xstsState.state } -fun

xstsExtractControlPrec(p: P): UnitPrec = UnitPrec.getInstance() \ No newline at end of file +fun

xstsExtractControlPrec(p: P): UnitPrec = UnitPrec.getInstance() diff --git a/subprojects/xsts/xsts-cli/build.gradle.kts b/subprojects/xsts/xsts-cli/build.gradle.kts index b3a2eec787..209b728b48 100644 --- a/subprojects/xsts/xsts-cli/build.gradle.kts +++ b/subprojects/xsts/xsts-cli/build.gradle.kts @@ -27,6 +27,9 @@ dependencies { implementation(project(":theta-analysis")) implementation(project(":theta-core")) implementation(project(":theta-common")) + implementation(project(":theta-ltl")) + implementation(project(":theta-ltl-cli")) + implementation(project(":theta-cfa")) implementation(project(":theta-solver")) implementation(project(":theta-solver-z3-legacy")) implementation(project(":theta-solver-z3")) diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt new file mode 100644 index 0000000000..49aa4cffce --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt @@ -0,0 +1,202 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.xsts.cli + +import com.github.ajalt.clikt.parameters.groups.provideDelegate +import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.help +import com.github.ajalt.clikt.parameters.options.option +import com.github.ajalt.clikt.parameters.types.enum +import com.google.common.base.Stopwatch +import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.multi.MultiSide +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.analysis.multi.NextSideFunctions.Alternating +import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.cfa.analysis.CfaState +import hu.bme.mit.theta.common.cfa.buchi.hoa.ExternalLtl2Hoaf +import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf +import hu.bme.mit.theta.common.ltl.LtlChecker +import hu.bme.mit.theta.common.ltl.cli.LtlCliOptions +import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.XstsState +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.* +import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass +import java.util.concurrent.TimeUnit +import kotlin.system.exitProcess + +private typealias NSF = + NextSideFunctions.NextSideFunction< + XstsState, + CfaState, + D, + ExprMultiState, CfaState, D>, + > + +class XstsLtlCliOptions() : LtlCliOptions() { + enum class EnvtranSeparation() { + COMBINED { + + override fun getNextsideFunction(): + NextSideFunctions.NextSideFunction< + XstsState, + CfaState, + D, + ExprMultiState, CfaState, D>, + > { + return Alternating() + } + }, + SEPARATE { + + override fun getNextsideFunction(): NSF = NSF { ms -> + if (ms.sourceSide == MultiSide.RIGHT || ms.leftState.lastActionWasEnv()) MultiSide.LEFT + else MultiSide.RIGHT + } + }; + + abstract fun getNextsideFunction(): + NextSideFunctions.NextSideFunction< + XstsState, + CfaState, + D, + ExprMultiState, CfaState, D>, + > + } + + val envtranSeparation: EnvtranSeparation by + option( + help = + "Whether Buchi evaluation should happen between env and trans transitions or not (SEPARATED and COMBINED, respectively)" + ) + .enum() + .default(EnvtranSeparation.SEPARATE) +} + +class XstsCliLtlCegar : + XstsCliBaseCommand( + name = "LTLCEGAR", + help = "Model checking using the CEGAR algorithm with an LTL property", + ) { + + private val domain: Domain by + option(help = "Abstraction domain to use").enum().default(Domain.PRED_CART) + private val refinement: Refinement by + option(help = "Refinement strategy to use").enum().default(Refinement.SEQ_ITP) + private val predsplit: PredSplit by option().enum().default(PredSplit.ATOMS) + private val refinementSolver: String? by option(help = "Use a different solver for abstraction") + private val abstractionSolver: String? by option(help = "Use a different solver for refinement") + private val initprec: InitPrec by option().enum().default(InitPrec.EMPTY) + private val ltlOptions by XstsLtlCliOptions() + + private fun printResult( + status: SafetyResult?, out ASGTrace<*, *>?>, + xsts: XSTS, + totalTimeMs: Long, + ) { + if (!outputOptions.benchmarkMode) return + printCommonResult(status, xsts, totalTimeMs) + val stats = status.stats.orElse(CegarStatistics(0, 0, 0, 0)) as CegarStatistics + listOf( + stats.algorithmTimeMs, + stats.abstractorTimeMs, + stats.refinerTimeMs, + stats.iterations, + 0, + 0, + 0, + ) + .forEach(writer::cell) + writer.newRow() + } + + override fun run() { + try { + doRun() + } catch (e: Exception) { + printError(e) + exitProcess(1) + } + } + + private fun doRun() { + registerSolverManagers() + val abstractionSolverFactory = SolverManager.resolveSolverFactory(abstractionSolver ?: solver) + val refinementSolverFactory = SolverManager.resolveSolverFactory(refinementSolver ?: solver) + val xsts = XstsNormalizerPass.transform(inputOptions.loadXsts()) + val config = + XstsConfigBuilder(domain, refinement, abstractionSolverFactory, refinementSolverFactory) + .initPrec(initprec) + .predSplit(predsplit) + if (domain == Domain.EXPL) { + val configBuilder = config.ExplStrategy(xsts) + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + configBuilder.itpRefToPrec, + configBuilder.itpRefToPrec, + configBuilder.dataAnalysis, + ltlOptions.ltlExpression, + abstractionSolverFactory, + logger, + ltlOptions.searchStrategy, + ltlOptions.refinerStrategy, + Ltl2BuchiThroughHoaf(ExternalLtl2Hoaf(ltlOptions.ltl2BuchiCommand), logger), + xsts.vars, + xsts.initFormula, + ltlOptions.envtranSeparation.getNextsideFunction(), + ) + val sw = Stopwatch.createStarted() + val result = checker.check(configBuilder.initPrec, configBuilder.initPrec) + sw.stop() + printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + writeCex(result, xsts) + } + if (domain in setOf(Domain.PRED_CART, Domain.PRED_SPLIT, Domain.PRED_BOOL)) { + val configBuilder = config.PredStrategy(xsts) + val checker = + LtlChecker( + configBuilder.multiSide, + configBuilder.lts, + configBuilder.itpRefToPrec, + configBuilder.itpRefToPrec, + configBuilder.dataAnalysis, + ltlOptions.ltlExpression, + abstractionSolverFactory, + logger, + ltlOptions.searchStrategy, + ltlOptions.refinerStrategy, + Ltl2BuchiThroughHoaf(ExternalLtl2Hoaf(ltlOptions.ltl2BuchiCommand), logger), + xsts.vars, + xsts.initFormula, + NextSideFunctions.Alternating(), + ) + val sw = Stopwatch.createStarted() + val result = checker.check(configBuilder.initPrec, configBuilder.initPrec) + sw.stop() + printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS)) + writeCex(result, xsts) + } + } +} diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt index 73b01a8568..2f49876547 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.core.CliktCommand @@ -23,23 +22,32 @@ import com.github.ajalt.clikt.parameters.options.option class XstsCliMainCommand : CliktCommand() { - val algorithm by option(eager = true).deprecated( - "--algorithm switch is now deprecated, use the respective subcommands", error = true - ) - val metrics by option(eager = true).deprecated( - "--metrics switch is now deprecated, use the `metrics` subcommand", error = true - ) - val header by option(eager = true).deprecated( - "--header switch is now deprecated, use the `header` subcommand", error = true - ) - - override fun run() = Unit + val algorithm by + option(eager = true) + .deprecated( + "--algorithm switch is now deprecated, use the respective subcommands", + error = true, + ) + val metrics by + option(eager = true) + .deprecated("--metrics switch is now deprecated, use the `metrics` subcommand", error = true) + val header by + option(eager = true) + .deprecated("--header switch is now deprecated, use the `header` subcommand", error = true) + override fun run() = Unit } fun main(args: Array) = - XstsCliMainCommand().subcommands( - XstsCliCegar(), XstsCliBounded(), XstsCliMdd(), XstsCliPetrinetMdd(), XstsCliChc(), XstsCliHeader(), - XstsCliMetrics() + XstsCliMainCommand() + .subcommands( + XstsCliCegar(), + XstsCliLtlCegar(), + XstsCliBounded(), + XstsCliMdd(), + XstsCliPetrinetMdd(), + XstsCliChc(), + XstsCliHeader(), + XstsCliMetrics(), ) - .main(args) \ No newline at end of file + .main(args) diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/XstsNormalizerPass.kt b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/XstsNormalizerPass.kt new file mode 100644 index 0000000000..14c7087ff4 --- /dev/null +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/XstsNormalizerPass.kt @@ -0,0 +1,68 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.xsts.passes + +import hu.bme.mit.theta.core.stmt.NonDetStmt +import hu.bme.mit.theta.core.stmt.SequenceStmt +import hu.bme.mit.theta.core.stmt.SkipStmt +import hu.bme.mit.theta.core.stmt.Stmt +import hu.bme.mit.theta.xsts.XSTS + +object XstsNormalizerPass : XstsPass { + + override fun transform(input: XSTS): XSTS { + val normalizedInit = normalize(input.init) + val normalizedTran = normalize(input.tran) + val normalizedEnv = normalize(input.env) + + return XSTS( + input.ctrlVars, + normalizedInit, + normalizedTran, + normalizedEnv, + input.initFormula, + input.prop, + ) + } + + private fun normalize(stmt: Stmt): NonDetStmt { + val collector = mutableListOf>() + collector.add(mutableListOf()) + normalize(stmt, collector) + return NonDetStmt.of(collector.map { SequenceStmt.of(it) }.toList()) + } + + private fun normalize(stmt: Stmt, collector: MutableList>) { + when (stmt) { + is SequenceStmt -> stmt.stmts.forEach { normalize(it, collector) } + is NonDetStmt -> { + val newCollector = mutableListOf>() + stmt.stmts.forEach { nondetBranch -> + val copy = collector.copy() + normalize(nondetBranch, copy) + newCollector.addAll(copy) + } + collector.clear() + collector.addAll(newCollector) + } + + is SkipStmt -> {} + else -> collector.forEach { it.add(stmt) } + } + } +} + +private fun MutableList>.copy() = map { it.toMutableList() }.toMutableList() diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/XstsPass.kt b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/XstsPass.kt new file mode 100644 index 0000000000..dc2dfc5f07 --- /dev/null +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/XstsPass.kt @@ -0,0 +1,23 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * 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 hu.bme.mit.theta.xsts.passes + +import hu.bme.mit.theta.xsts.XSTS + +fun interface XstsPass { + + fun transform(input: XSTS): XSTS +} diff --git a/subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt similarity index 100% rename from subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt rename to subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt