diff --git a/build.gradle.kts b/build.gradle.kts index e5be05ea9b..3b60d44bbc 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -29,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.7.0" + version = "6.8.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/unit/UnitInitFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java index 8efb0961b9..87326268f1 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 @@ -15,21 +15,19 @@ */ package hu.bme.mit.theta.analysis.unit; -import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.analysis.InitFunc; import java.util.Collection; -import com.google.common.collect.ImmutableList; - -import hu.bme.mit.theta.analysis.InitFunc; +import static com.google.common.base.Preconditions.checkNotNull; -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 +38,4 @@ public Collection getInitStates(final UnitPrec prec) { checkNotNull(prec); return RESULT; } - } 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..9d77f35f1f --- /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") + id("cli-tool") +} + +dependencies { + implementation(project(":theta-analysis")) +} 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..2a0ab0b3b0 --- /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.LDGTraceCheckerStrategy + +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(LDGTraceCheckerStrategy.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..d4e5df5b8a --- /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 jhoafparser.ast.AtomAcceptance +import jhoafparser.ast.AtomLabel +import jhoafparser.ast.BooleanExpression +import jhoafparser.consumer.HOAConsumer +import jhoafparser.consumer.HOAConsumerException +import java.util.function.Consumer + +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..d1d4870080 --- /dev/null +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt @@ -0,0 +1,178 @@ +/* + * 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.cegar.CegarChecker +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.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.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.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.LdgVisualizer +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: LDGTraceCheckerStrategy, + ltl2BuchiTransformer: Ltl2BuchiTransformer, + variables: Collection>, + initExpr: Expr = True(), +) : + SafetyChecker< + LDG, DataS>, StmtMultiAction>, + LDGTrace, DataS>, StmtMultiAction>, + MultiPrec, DataP>, + > { + private val checker: + CegarChecker< + MultiPrec, DataP>, + LDG, DataS>, StmtMultiAction>, + LDGTrace, 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(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val buchiRefToPrec = RefutationToGlobalCfaPrec(dataRefToPrec, buchiAutomaton.initLoc) + val multiRefToPrec = RefToMultiPrec(refToPrec, buchiRefToPrec, dataRefToPrec) + val multiAnalysis = product.side.analysis + val abstractor = + LDGAbstractor( + multiAnalysis, + product.lts, + buchiPredicate(buchiAutomaton), + searchStrategy, + logger, + ) + val refiner: + SingleLDGTraceRefiner< + ExprMultiState, DataS>, + StmtMultiAction, + MultiPrec, DataP>, + > = + SingleLDGTraceRefiner( + refinerStrategy, + solverFactory, + JoiningPrecRefiner.create(multiRefToPrec), + logger, + initExpr, + ) + val visualizer = + LdgVisualizer< + ExprMultiState, DataS>, + StmtMultiAction, + >( + { it.toString() }, + { 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< + LDG, DataS>, StmtMultiAction>, + LDGTrace, DataS>, StmtMultiAction>, + > { + return checker.check(input) + } + + fun check( + prec: P, + dataPrec: DataP, + ): SafetyResult< + LDG, DataS>, StmtMultiAction>, + LDGTrace, 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..d00d91bf49 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt @@ -0,0 +1,108 @@ +/* + * 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.LDGTraceCheckerStrategy +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.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 junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@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, + LDGTraceCheckerStrategy.MILANO, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), + variables, + ) + + 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..8c95a84921 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt @@ -0,0 +1,131 @@ +/* + * 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.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expr.ExprAction +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 junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@RunWith(Parameterized::class) +class LtlCheckTestWithCfaPred( + private val cfaName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: LDGTraceCheckerStrategy, +) { + + 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(LDGTraceCheckerStrategy.MILANO, LDGTraceCheckerStrategy.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, + ) + + 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..f2c0798f9f --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt @@ -0,0 +1,115 @@ +/* + * 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.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ExplState +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.normalize +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@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 = normalize(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, + LDGTraceCheckerStrategy.MILANO, + Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), + xsts.vars, + xsts.initFormula, + ) + 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..3b2b455323 --- /dev/null +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt @@ -0,0 +1,156 @@ +/* + * 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.LDGTraceCheckerStrategy +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.normalize +import junit.framework.TestCase.fail +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized +import java.io.FileInputStream + +@RunWith(Parameterized::class) +class LtlCheckTestWithXstsPred( + private val xstsName: String, + private val ltlExpr: String, + private val result: Boolean, + private val searchStrategy: LoopcheckerSearchStrategy, + private val refinerStrategy: LDGTraceCheckerStrategy, +) { + + 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((normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle) -> 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 -> + LDGTraceCheckerStrategy.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 = normalize(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, + ) + + Assert.assertEquals(result, checker.check(initPrec, initPrec).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+%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/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..579deaab67 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,21 @@ 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) + // TODO here initialized should be xstsState.isInitialized, but that fails + // LtlCheckTestWithXstsPred + return XstsState.of(dataState, xstsState.lastActionWasEnv(), true) } 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..e405e39812 --- /dev/null +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt @@ -0,0 +1,143 @@ +/* + * 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.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.cegar.CegarStatistics +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +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.config.XstsConfigBuilder +import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.* +import hu.bme.mit.theta.xsts.passes.normalize +import java.util.concurrent.TimeUnit +import kotlin.system.exitProcess + +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 LtlCliOptions() + + private fun printResult( + status: SafetyResult?, out LDGTrace<*, *>?>, + 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 = normalize(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, + ) + 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, + ) + 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/NormalizerPass.kt b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/NormalizerPass.kt new file mode 100644 index 0000000000..ee409c490e --- /dev/null +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/passes/NormalizerPass.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.xsts.passes + +import com.google.common.base.Preconditions.checkArgument +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 NormalizerPass : XstsPass { + + override fun transform(input: XSTS) = normalize(input) +} + +fun normalize(rawXsts: XSTS?): XSTS { + checkArgument(rawXsts != null, "Can't normalize null") + val xstsInput = rawXsts!! + + val normalizedInit = normalize(xstsInput.init) + val normalizedTran = normalize(xstsInput.tran) + val normalizedEnv = normalize(xstsInput.env) + + return XSTS( + xstsInput.ctrlVars, + normalizedInit, + normalizedTran, + normalizedEnv, + xstsInput.initFormula, + xstsInput.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