From 39ba5acfd0e30acc246b6b27bfa780216cad8c7d Mon Sep 17 00:00:00 2001 From: RipplB Date: Fri, 1 Nov 2024 19:57:42 +0100 Subject: [PATCH] Add loopchecker package This new package makes it possible to find lasso-like traces in any type of model. --- subprojects/common/analysis/build.gradle.kts | 4 + .../loopchecker/AcceptancePredicate.kt | 42 ++++ .../algorithm/loopchecker/LDGTrace.kt | 81 ++++++ .../abstraction/GdfsSearchStrategies.kt | 156 ++++++++++++ .../loopchecker/abstraction/LDGAbstractor.kt | 62 +++++ .../abstraction/LoopcheckerSearchStrategy.kt | 56 +++++ .../abstraction/NdfsSearchStrategy.kt | 101 ++++++++ .../exception/InvalidPathException.kt | 18 ++ .../exception/TraceCheckingFailedException.kt | 19 ++ .../analysis/algorithm/loopchecker/ldg/LDG.kt | 93 +++++++ ...BoundedUnrollingLDGTraceCheckerStrategy.kt | 159 ++++++++++++ .../refinement/LDGTraceCheckerStrategy.kt | 171 +++++++++++++ .../loopchecker/refinement/LDGTraceRefiner.kt | 26 ++ .../MilanoLDGTraceCheckerStrategy.kt | 87 +++++++ .../refinement/SingleLDGTraceRefiner.kt | 55 +++++ .../util/VarCollectorStmtVisitor.kt | 74 ++++++ .../mit/theta/analysis/utils/LDGVisualizer.kt | 134 ++++++++++ .../LDGAbstractorCheckingTest.java | 156 ++++++++++++ .../loopchecker/LDGCegarVerifierTest.java | 230 ++++++++++++++++++ .../loopchecker/LDGTraceCheckerTest.java | 91 +++++++ .../loopchecker/ldg/LDGTraceTest.java | 65 +++++ .../src/test/resources/cfa/counter2to3.cfa | 16 ++ .../src/test/resources/cfa/counter6to7.cfa | 19 ++ .../resources/prop/currentColor_eq_Green.prop | 3 + .../test/resources/prop/isWet_eq_true.prop | 3 + .../src/test/resources/prop/waterproof.prop | 3 + .../src/test/resources/prop/x_eq_3.prop | 3 + .../src/test/resources/prop/x_eq_5.prop | 3 + .../src/test/resources/prop/x_eq_6.prop | 3 + .../src/test/resources/prop/x_eq_7.prop | 3 + .../src/test/resources/xsts/colors.xsts | 35 +++ .../src/test/resources/xsts/counter3.xsts | 10 + .../src/test/resources/xsts/counter5.xsts | 12 + .../src/test/resources/xsts/counter6to7.xsts | 13 + .../src/test/resources/xsts/forever5.xsts | 9 + .../test/resources/xsts/infinitehavoc.xsts | 14 ++ .../src/test/resources/xsts/weather.xsts | 106 ++++++++ 37 files changed, 2135 insertions(+) create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/InvalidPathException.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/TraceCheckingFailedException.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt create mode 100644 subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt create mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java create mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java create mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java create mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java create mode 100644 subprojects/common/analysis/src/test/resources/cfa/counter2to3.cfa create mode 100644 subprojects/common/analysis/src/test/resources/cfa/counter6to7.cfa create mode 100644 subprojects/common/analysis/src/test/resources/prop/currentColor_eq_Green.prop create mode 100644 subprojects/common/analysis/src/test/resources/prop/isWet_eq_true.prop create mode 100644 subprojects/common/analysis/src/test/resources/prop/waterproof.prop create mode 100644 subprojects/common/analysis/src/test/resources/prop/x_eq_3.prop create mode 100644 subprojects/common/analysis/src/test/resources/prop/x_eq_5.prop create mode 100644 subprojects/common/analysis/src/test/resources/prop/x_eq_6.prop create mode 100644 subprojects/common/analysis/src/test/resources/prop/x_eq_7.prop create mode 100644 subprojects/common/analysis/src/test/resources/xsts/colors.xsts create mode 100644 subprojects/common/analysis/src/test/resources/xsts/counter3.xsts create mode 100644 subprojects/common/analysis/src/test/resources/xsts/counter5.xsts create mode 100644 subprojects/common/analysis/src/test/resources/xsts/counter6to7.xsts create mode 100644 subprojects/common/analysis/src/test/resources/xsts/forever5.xsts create mode 100644 subprojects/common/analysis/src/test/resources/xsts/infinitehavoc.xsts create mode 100644 subprojects/common/analysis/src/test/resources/xsts/weather.xsts diff --git a/subprojects/common/analysis/build.gradle.kts b/subprojects/common/analysis/build.gradle.kts index f8205f008d..4bb71e0bfe 100644 --- a/subprojects/common/analysis/build.gradle.kts +++ b/subprojects/common/analysis/build.gradle.kts @@ -31,4 +31,8 @@ dependencies { testImplementation(project(":theta-solver-z3-legacy")) testImplementation(project(":theta-solver-z3")) implementation("com.corundumstudio.socketio:netty-socketio:2.0.6") + testImplementation(project(mapOf("path" to ":theta-xsts-analysis"))) + testImplementation(project(mapOf("path" to ":theta-xsts"))) + testImplementation(project(mapOf("path" to ":theta-cfa-analysis"))) + testImplementation(project(mapOf("path" to ":theta-cfa"))) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt new file mode 100644 index 0000000000..a0ff8bc98b --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/AcceptancePredicate.kt @@ -0,0 +1,42 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker + +import hu.bme.mit.theta.analysis.Action +import hu.bme.mit.theta.analysis.State +import java.util.function.Predicate + +class AcceptancePredicate( + private val statePredicate: ((S?) -> Boolean)? = null, + private val actionPredicate: ((A?) -> Boolean)? = null, +) : Predicate> { + + constructor(statePredicate: (S?) -> Boolean = { _ -> true }, a: Unit) : this(statePredicate) + + fun testState(state: S): Boolean { + return statePredicate?.invoke(state) ?: false + } + + fun testAction(action: A) = actionPredicate?.invoke(action) ?: false + + override fun test(t: Pair): Boolean { + val state = t.first + val action = t.second + if (statePredicate == null && action == null) return false + return (statePredicate == null || statePredicate.invoke(state)) && + (actionPredicate == null || (action != null && actionPredicate.invoke(action))) + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt new file mode 100644 index 0000000000..97ce7b9f9e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt @@ -0,0 +1,81 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker + +import hu.bme.mit.theta.analysis.Cex +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.Logger.Level + +class LDGTrace( + val tail: List>, + val honda: LDGNode, + val loop: List>, +) : Cex { + + val edges by lazy { tail + loop } + + constructor( + edges: List>, + honda: LDGNode, + ) : this(edges.takeWhile { it.source != honda }, honda, edges.dropWhile { it.source != honda }) + + init { + check((1 until tail.size).none { tail[it - 1].target != tail[it].source }) { + "The edges of the tail have to connect into each other" + } + check(tail.isEmpty() || tail.last().target == honda) { "The tail has to finish in the honda" } + check(loop.first().source == honda) { "The loop has to start in the honda" } + check((1 until loop.size).none { loop[it - 1].target != loop[it].source }) { + "The edges of the loop have to connect into each other" + } + check(loop.last().target == honda) { "The loop has to finish in the honda" } + } + + override fun length() = edges.size + + fun getEdge(index: Int): LDGEdge { + check(index >= 0) { "Can't get negative indexed edge (${index})" } + check(index < length()) { "Index out of range $index < ${length()}" } + return if (index < tail.size) tail[index] else loop[index - tail.size] + } + + fun getAction(index: Int) = getEdge(index).action + + fun getState(index: Int) = if (index < length()) getEdge(index).source!!.state else honda.state + + fun toTrace(): Trace = + Trace.of(edges.map { it.source!!.state } + honda.state, edges.map { it.action!! }) + + fun print(logger: Logger, level: Level) { + tail.forEach { + logger.write( + level, + "%s%n---through action:---%n%s%n--------->%n", + it.source?.state, + it.action, + ) + } + logger.write(level, "---HONDA:---%n{ %s }---------%n", honda.state) + loop.forEach { + logger.write(level, "---through action:---%n%s%n--------->%n%s%n", it.action, it.target.state) + } + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt new file mode 100644 index 0000000000..2a56838da3 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.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.analysis.algorithm.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger + +typealias BacktrackResult = Pair>?, List>?> + +fun combineLassos(results: Collection>) = + Pair(setOf>(), results.flatMap { it.second ?: emptyList() }) + +abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { + + internal fun expandFromInitNodeUntilTarget( + initNode: LDGNode, + stopAtLasso: Boolean, + expand: NodeExpander, + logger: Logger, + ): Collection> { + return expandThroughNode( + emptyMap(), + LDGEdge(null, initNode, null, false), + emptyList(), + 0, + stopAtLasso, + expand, + logger, + ) + .second!! + } + + private fun expandThroughNode( + pathSoFar: Map, Int>, + incomingEdge: LDGEdge, + edgesSoFar: List>, + targetsSoFar: Int, + stopAtLasso: Boolean, + expand: NodeExpander, + logger: Logger, + ): BacktrackResult { + val expandingNode: LDGNode = incomingEdge.target + logger.write( + Logger.Level.VERBOSE, + "Expanding through %s edge to %s node with state %s%n", + if (incomingEdge.accepting) "accepting" else "not accepting", + if (expandingNode.accepting) "accepting" else "not accepting", + expandingNode.state, + ) + if (expandingNode.state.isBottom()) { + logger.write(Logger.Level.VERBOSE, "Node is a dead end since its bottom%n") + return BacktrackResult(null, null) + } + val totalTargets = + if (expandingNode.accepting || incomingEdge.accepting) targetsSoFar + 1 else targetsSoFar + if (pathSoFar.containsKey(expandingNode) && pathSoFar[expandingNode]!! < totalTargets) { + logger.write( + Logger.Level.SUBSTEP, + "Found trace with a length of %d, building lasso...%n", + pathSoFar.size, + ) + logger.write(Logger.Level.DETAIL, "Honda should be: %s", expandingNode.state) + pathSoFar.forEach { (node, targetsThatFar) -> + logger.write( + Logger.Level.VERBOSE, + "Node state %s | targets that far: %d%n", + node.state, + targetsThatFar, + ) + } + val lasso: LDGTrace = LDGTrace(edgesSoFar + incomingEdge, expandingNode) + logger.write(Logger.Level.DETAIL, "Built the following lasso:%n") + lasso.print(logger, Logger.Level.DETAIL) + return BacktrackResult(null, listOf(lasso)) + } + if (pathSoFar.containsKey(expandingNode)) { + logger.write(Logger.Level.VERBOSE, "Reached loop but no acceptance inside%n") + return BacktrackResult(setOf(expandingNode), null) + } + val needsTraversing = + !expandingNode.expanded || + expandingNode.validLoopHondas.filter(pathSoFar::containsKey).any { + pathSoFar[it]!! < targetsSoFar + } + val expandStrategy: NodeExpander = + if (needsTraversing) expand else { _ -> mutableSetOf() } + val outgoingEdges: Collection> = expandStrategy(expandingNode) + val results: MutableList> = mutableListOf() + for (newEdge in outgoingEdges) { + val result: BacktrackResult = + expandThroughNode( + pathSoFar + (expandingNode to totalTargets), + newEdge, + if (incomingEdge.source != null) edgesSoFar.plus(incomingEdge) else edgesSoFar, + totalTargets, + stopAtLasso, + expand, + logger, + ) + results.add(result) + if (stopAtLasso && result.second?.isNotEmpty() == true) break + } + val result: BacktrackResult = combineLassos(results) + if (result.second != null) return result + val validLoopHondas: Collection> = results.flatMap { it.first ?: emptyList() } + expandingNode.validLoopHondas.addAll(validLoopHondas) + return BacktrackResult(validLoopHondas.toSet(), null) + } +} + +object GdfsSearchStrategy : AbstractSearchStrategy() { + + override fun search( + initNodes: Collection>, + target: AcceptancePredicate, + expand: NodeExpander, + logger: Logger, + ): Collection> { + for (initNode in initNodes) { + val possibleTraces: Collection> = + expandFromInitNodeUntilTarget(initNode, true, expand, logger) + if (!possibleTraces.isEmpty()) { + return possibleTraces + } + } + return emptyList() + } +} + +object FullSearchStrategy : AbstractSearchStrategy() { + + override fun search( + initNodes: Collection>, + target: AcceptancePredicate, + expand: NodeExpander, + logger: Logger, + ) = initNodes.flatMap { expandFromInitNodeUntilTarget(it, false, expand, logger) } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt new file mode 100644 index 0000000000..6b26395fcb --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt @@ -0,0 +1,62 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.Analysis +import hu.bme.mit.theta.analysis.LTS +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor +import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger + +class LDGAbstractor( + private val analysis: Analysis, + private val lts: LTS, + private val acceptancePredicate: AcceptancePredicate, + private val searchStrategy: LoopcheckerSearchStrategy, + private val logger: Logger, +) : Abstractor> { + + override fun createProof() = LDG(acceptancePredicate) + + override fun check(ldg: LDG, prec: P): AbstractorResult { + if (ldg.isUninitialised()) { + ldg.initialise(analysis.initFunc.getInitStates(prec)) + ldg.traces = emptyList() + } + val expander: NodeExpander = + fun(node: LDGNode): Collection> { + if (node.expanded) { + return node.outEdges + } + node.expanded = true + return lts.getEnabledActionsFor(node.state).flatMap { action -> + analysis.transFunc.getSuccStates(node.state, action, prec).map(ldg::getOrCreateNode).map { + ldg.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) + } + } + } + val searchResult = searchStrategy.search(ldg, acceptancePredicate, expander, logger) + ldg.traces = searchResult.toList() + return AbstractorResult(searchResult.isEmpty()) + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt new file mode 100644 index 0000000000..541a9976eb --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt @@ -0,0 +1,56 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.NullLogger + +typealias NodeExpander = (LDGNode) -> Collection> + +enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStrategy) { + GDFS(GdfsSearchStrategy), + NDFS(NdfsSearchStrategy), + FULL(FullSearchStrategy); + + companion object { + + val default = GDFS + } + + fun search( + ldg: LDG, + target: AcceptancePredicate, + expand: NodeExpander, + logger: Logger = NullLogger.getInstance(), + ): Collection> = strategy.search(ldg.initNodes, target, expand, logger) +} + +interface ILoopcheckerSearchStrategy { + + fun search( + initNodes: Collection>, + target: AcceptancePredicate, + expand: NodeExpander, + logger: Logger, + ): Collection> +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt new file mode 100644 index 0000000000..096165a371 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt @@ -0,0 +1,101 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.logging.Logger + +object NdfsSearchStrategy : ILoopcheckerSearchStrategy { + + override fun search( + initNodes: Collection>, + target: AcceptancePredicate, + expand: NodeExpander, + logger: Logger, + ): Collection> { + for (node in initNodes) { + for (edge in expand(node)) { + val result = blueSearch(edge, emptyList(), mutableSetOf(), mutableSetOf(), target, expand) + if (!result.isEmpty()) return result + } + } + return emptyList() + } + + private fun redSearch( + seed: LDGNode, + edge: LDGEdge, + trace: List>, + redNodes: MutableSet>, + target: AcceptancePredicate, + expand: NodeExpander, + ): List> { + val targetNode = edge.target + if (targetNode.state.isBottom) { + return emptyList() + } + if (targetNode == seed) { + return trace + edge + } + if (redNodes.contains(targetNode)) { + return emptyList() + } + redNodes.add(edge.target) + for (nextEdge in expand(targetNode)) { + val redSearch: List> = + redSearch(seed, nextEdge, trace + edge, redNodes, target, expand) + if (redSearch.isNotEmpty()) return redSearch + } + return emptyList() + } + + private fun blueSearch( + edge: LDGEdge, + trace: List>, + blueNodes: MutableSet>, + redNodes: Set>, + target: AcceptancePredicate, + expand: NodeExpander, + ): Collection> { + val targetNode = edge.target + if (targetNode.state.isBottom) { + return emptyList() + } + if (target.test(Pair(targetNode.state, edge.action))) { + // Edge source can only be null artificially, and is only used when calling other search + // strategies + val accNode = if (targetNode.accepting) targetNode else edge.source!! + val redSearch: List> = + redSearch(accNode, edge, trace, mutableSetOf(), target, expand) + if (redSearch.isNotEmpty()) return setOf(LDGTrace(redSearch, accNode)) + } + if (blueNodes.contains(targetNode)) { + return emptyList() + } + blueNodes.add(edge.target) + for (nextEdge in expand(targetNode)) { + val blueSearch: Collection> = + blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand) + if (!blueSearch.isEmpty()) return blueSearch + } + return emptyList() + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/InvalidPathException.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/InvalidPathException.kt new file mode 100644 index 0000000000..080d013855 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/InvalidPathException.kt @@ -0,0 +1,18 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.exception + +class InvalidPathException : RuntimeException("The path given is not a lasso") diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/TraceCheckingFailedException.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/TraceCheckingFailedException.kt new file mode 100644 index 0000000000..3063ed43e0 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/exception/TraceCheckingFailedException.kt @@ -0,0 +1,19 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.exception + +class TraceCheckingFailedException(reason: String) : + Exception("The trace checker was unable to check the trace because of:\n$reason") diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt new file mode 100644 index 0000000000..098ce639a4 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt @@ -0,0 +1,93 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg + +import hu.bme.mit.theta.analysis.algorithm.Proof +import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState + +class LDG( + private val acceptancePredicate: AcceptancePredicate +) : Proof { + + val nodes: MutableMap> = mutableMapOf() + val initNodes: MutableList> = mutableListOf() + var traces: List> = emptyList() + + fun isUninitialised() = initNodes.isEmpty() + + fun pruneAll() { + initNodes.clear() + nodes.clear() + traces = emptyList() + } + + fun initialise(initStates: Collection) { + check(initStates.isNotEmpty()) + initNodes.addAll(initStates.map(this::getOrCreateNode)) + } + + fun getOrCreateNode(state: S): LDGNode = + nodes.computeIfAbsent(state) { s -> LDGNode(s, acceptancePredicate.test(Pair(s, null))) } + + fun containsNode(state: S) = nodes.containsKey(state) + + fun drawEdge( + source: LDGNode, + target: LDGNode, + action: A?, + accepting: Boolean, + ): LDGEdge { + val edge = LDGEdge(source, target, action, accepting) + source.addOutEdge(edge) + target.addInEdge(edge) + return edge + } +} + +data class LDGEdge( + val source: LDGNode?, + val target: LDGNode, + val action: A?, + val accepting: Boolean, +) + +class LDGNode(val state: S, val accepting: Boolean) { + companion object { + + var idCounter: Long = 0 + } + + val inEdges: MutableList> = mutableListOf() + val outEdges: MutableList> = mutableListOf() + val id = idCounter++ + var validLoopHondas: MutableSet> = hashSetOf() + var expanded: Boolean = false + set(value) { + if (!value) { + throw IllegalArgumentException("Can't set expanded to false") + } + field = true + } + + fun addInEdge(edge: LDGEdge) = inEdges.add(edge) + + fun addOutEdge(edge: LDGEdge) = outEdges.add(edge) + + fun smallerEdgeCollection() = if (inEdges.size > outEdges.size) inEdges else outEdges +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt new file mode 100644 index 0000000000..4eeb5acbaf --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt @@ -0,0 +1,159 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException +import hu.bme.mit.theta.analysis.algorithm.loopchecker.util.VarCollectorStmtVisitor +import hu.bme.mit.theta.analysis.expl.ExplPrec +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.ExprStates +import hu.bme.mit.theta.analysis.expr.StmtAction +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.DomainSize +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.PathUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory +import hu.bme.mit.theta.solver.ItpMarker +import hu.bme.mit.theta.solver.SolverFactory +import java.util.function.Consumer + +class BoundedUnrollingLDGTraceCheckerStrategy( + private val trace: LDGTrace, + private val solverFactory: SolverFactory, + init: Expr, + private val bound: Int, + private val logger: Logger, +) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { + + override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { + val indexingBeforeLoop = indexings[trace.tail.size] + val indexingAfterLoop = indexings[trace.length()] + val deltaIndexing = indexingAfterLoop.sub(indexingBeforeLoop) + val usedVariablesPrecision = ExplPrec.of(expandUsedVariables(emptySet())) + val requiredLoops: Int = findSmallestAbstractState(0, bound + 1, usedVariablesPrecision) + if (requiredLoops == bound + 1) { + throw TraceCheckingFailedException("Required number of unrolling is above $bound") + } + logger.write(Logger.Level.INFO, "Unrolling loop of trace at most %d times%n", requiredLoops) + solver.reset() + var loopIndexing = VarIndexingFactory.indexing(0) + for (i in 0 until requiredLoops) { + solver.push() + putLoopOnSolver(satMarker, loopIndexing) + if (solver.check().isUnsat) { + solver.pop() + putLoopOnSolver(unreachableMarker, loopIndexing) + logger.write(Logger.Level.INFO, "Unrolled loop of trace %d times%n", i + 1) + return infeasibleThroughInterpolant(trace.tail.size, loopIndexing) + } + loopIndexing = loopIndexing.add(deltaIndexing) + solver.push() + val finalLoopIndexing = loopIndexing + variables.forEach( + Consumer { variable: VarDecl<*> -> + solver.add( + unreachableMarker, + Eq( + PathUtils.unfold(variable.ref, VarIndexingFactory.indexing(0)), + PathUtils.unfold(variable.ref, finalLoopIndexing), + ), + ) + } + ) + if (solver.check().isSat) { + logger.write(Logger.Level.INFO, "Unrolled loop of trace %d times%n", i + 1) + return getItpRefutationFeasible() + } + solver.pop() + } + val finalLoopIndexing = loopIndexing + variables.forEach { variable -> + solver.add( + unreachableMarker, + Eq( + PathUtils.unfold(variable.ref, VarIndexingFactory.indexing(0)), + PathUtils.unfold(variable.ref, finalLoopIndexing), + ), + ) + } + return infeasibleThroughInterpolant(trace.tail.size, loopIndexing.sub(deltaIndexing)) + } + + private fun findSmallestAbstractState(i: Int, bound: Int, usedVariablesPrecision: ExplPrec): Int { + val loop = trace.loop + if (i == loop.size) return bound + val expr: Expr = loop[i].source!!.state.toExpr() + val statesForExpr: Collection = + ExprStates.createStatesForExpr( + solverFactory.createSolver(), + expr, + 0, + usedVariablesPrecision::createState, + VarIndexingFactory.indexing(0), + bound, + ) + val currentSize: DomainSize = + statesForExpr + .map { state -> + val filtVars = + usedVariablesPrecision.vars.filter(ExprUtils.getVars(state.toExpr())::contains) + val types = filtVars.map(VarDecl<*>::getType) + val sizes = types.map(Type::getDomainSize) + val res = sizes.fold(DomainSize.ONE, DomainSize::multiply) + res + } + .fold(DomainSize.ZERO, DomainSize::add) + return if (currentSize.isInfinite || currentSize.isBiggerThan(bound.toLong())) + findSmallestAbstractState(i + 1, bound, usedVariablesPrecision) + else findSmallestAbstractState(i + 1, currentSize.finiteSize.toInt(), usedVariablesPrecision) + } + + fun expandUsedVariables(usedVariables: Set>): Set> { + val expanded = + trace.loop.fold(emptySet>()) { acc, edge -> + if (edge.action is StmtAction) VarCollectorStmtVisitor.visitAll(edge.action.getStmts(), acc) + else emptySet() + } + + return if (expanded.size > usedVariables.size) expandUsedVariables(expanded) else usedVariables + } + + private fun putLoopOnSolver(marker: ItpMarker, startIndexing: VarIndexing) { + var loopIndexing = startIndexing + for (ldgEdge in trace.loop) { + solver.add(marker, PathUtils.unfold(ldgEdge.source!!.state.toExpr(), loopIndexing)) + val action = ldgEdge.action!! + solver.add(marker, PathUtils.unfold(action.toExpr(), loopIndexing)) + loopIndexing = loopIndexing.add(action.nextIndexing()) + } + solver.add( + marker, + PathUtils.unfold(trace.loop[trace.loop.size - 1].target.state.toExpr(), loopIndexing), + ) + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt new file mode 100644 index 0000000000..7a950a91e8 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt @@ -0,0 +1,171 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement + +import hu.bme.mit.theta.analysis.Trace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus.Feasible +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.logging.NullLogger +import hu.bme.mit.theta.core.model.Valuation +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.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.PathUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory +import hu.bme.mit.theta.solver.* + +enum class LDGTraceCheckerStrategy { + MILANO { + + override fun check( + trace: LDGTrace, + solverFactory: SolverFactory, + init: Expr, + logger: Logger, + ) = MilanoLDGTraceCheckerStrategy(trace, solverFactory, init, logger).check() + }, + BOUNDED_UNROLLING { + + override fun check( + trace: LDGTrace, + solverFactory: SolverFactory, + init: Expr, + logger: Logger, + ): ExprTraceStatus { + try { + return BoundedUnrollingLDGTraceCheckerStrategy(trace, solverFactory, init, 100, logger) + .check() + } catch (t: TraceCheckingFailedException) { + logger.write(Logger.Level.INFO, "${t.message}\n") + logger.write(Logger.Level.INFO, "Falling back to default strategy $default\n") + return default.check(trace, solverFactory, init, logger) + } + } + }; + + companion object { + + val default = MILANO + } + + abstract fun check( + trace: LDGTrace, + solverFactory: SolverFactory, + init: Expr = True(), + logger: Logger = NullLogger.getInstance(), + ): ExprTraceStatus +} + +abstract class AbstractLDGTraceCheckerStrategy( + private val trace: LDGTrace, + solverFactory: SolverFactory, + private val init: Expr, + private val logger: Logger, +) { + protected val solver: ItpSolver = solverFactory.createItpSolver() + protected val stateCount = trace.length() + 1 + protected val indexings = mutableListOf() + protected val satMarker: ItpMarker = solver.createMarker() + protected val unreachableMarker: ItpMarker = solver.createMarker() + protected val pattern: ItpPattern = solver.createBinPattern(satMarker, unreachableMarker) + protected val variables = + trace.edges.flatMap { + ExprUtils.getVars(it.source?.state?.toExpr() ?: True()) + + ExprUtils.getVars(it.action?.toExpr() ?: True()) + } + + private fun findSatIndex(): Int { + for (i in 1 until stateCount) { + solver.push() + indexings.add(indexings[i - 1].add(trace.getAction(i - 1)!!.nextIndexing())) + solver.add(satMarker, PathUtils.unfold(trace.getState(i).toExpr(), indexings[i])) + solver.add(satMarker, PathUtils.unfold(trace.getAction(i - 1)!!.toExpr(), indexings[i - 1])) + if (solver.check().isUnsat) { + solver.pop() + return i - 1 + } + } + return stateCount - 1 + } + + abstract fun evaluateLoop(valuation: Valuation): ExprTraceStatus + + fun check(): ExprTraceStatus { + solver.push() + indexings.add(VarIndexingFactory.indexing(0)) + solver.add(satMarker, PathUtils.unfold(init, indexings[0])) + solver.add(satMarker, PathUtils.unfold(trace.getState(0).toExpr(), indexings[0])) + + val satIndex = findSatIndex() + if (satIndex < stateCount - 1) return infeasibleAsLoopIsUnreachable(satIndex) + return evaluateLoop(solver.model) + } + + private fun infeasibleAsLoopIsUnreachable(satPrefix: Int): ExprTraceStatus { + logger.write(Logger.Level.INFO, "Loop was unreachable%n") + solver.add( + unreachableMarker, + PathUtils.unfold(trace.getState(satPrefix + 1).toExpr(), indexings[satPrefix + 1]), + ) + solver.add( + unreachableMarker, + PathUtils.unfold(trace.getAction(satPrefix)!!.toExpr(), indexings[satPrefix]), + ) + return infeasibleThroughInterpolant(satPrefix, indexings[satPrefix]) + } + + protected fun infeasibleThroughInterpolant( + satPrefix: Int, + indexing: VarIndexing, + ): ExprTraceStatus { + solver.check() + val interpolant: Interpolant = solver.getInterpolant(pattern) + val interpolantExpr: Expr = interpolant.eval(satMarker) + logInterpolant(interpolantExpr) + try { + val itpFolded: Expr = PathUtils.foldin(interpolantExpr, indexing) + return ExprTraceStatus.infeasible(ItpRefutation.binary(itpFolded, satPrefix, stateCount)) + } catch (e: IllegalArgumentException) { + logger.write( + Logger.Level.INFO, + "Interpolant expression: %s; indexing: %s%n", + interpolantExpr, + indexing, + ) + throw e + } + } + + protected fun getItpRefutationFeasible(): Feasible = + ExprTraceStatus.feasible( + Trace.of( + indexings.map { PathUtils.extractValuation(solver.model, it) }, + (trace.tail + trace.loop).map { it.action }, + ) + ) + + protected fun logInterpolant(expr: Expr) { + logger.write(Logger.Level.INFO, "Interpolant : $expr%n") + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt new file mode 100644 index 0000000000..ad174271f3 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt @@ -0,0 +1,26 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement + +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState + +interface LDGTraceRefiner : + Refiner, LDGTrace> {} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt new file mode 100644 index 0000000000..feef72e00f --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt @@ -0,0 +1,87 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.decl.IndexedConstDecl +import hu.bme.mit.theta.core.model.Valuation +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq +import hu.bme.mit.theta.core.type.anytype.Exprs.Prime +import hu.bme.mit.theta.core.type.anytype.RefExpr +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.core.utils.PathUtils +import hu.bme.mit.theta.core.utils.indexings.VarIndexing +import hu.bme.mit.theta.solver.Interpolant +import hu.bme.mit.theta.solver.SolverFactory + +class MilanoLDGTraceCheckerStrategy( + private val trace: LDGTrace, + solverFactory: SolverFactory, + init: Expr, + logger: Logger, +) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { + + override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { + for (variable in variables) { + solver.add( + unreachableMarker, + Eq( + PathUtils.unfold(variable.ref, indexings[trace.tail.size]), + PathUtils.unfold(variable.ref, indexings[stateCount - 1]), + ), + ) + if (solver.check().isSat) continue + val interpolant: Interpolant = solver.getInterpolant(pattern) + val interpolantExpr: Expr = + ExprUtils.simplify( + foldIn(interpolant.eval(satMarker), indexings[stateCount - 1], valuation) + ) + logInterpolant(interpolantExpr) + return ExprTraceStatus.infeasible( + ItpRefutation.binary(interpolantExpr, stateCount - 1, stateCount) + ) + } + return getItpRefutationFeasible() + } + + private fun foldIn( + expr: Expr, + indexing: VarIndexing, + valuation: Valuation, + ): Expr { + if (expr is RefExpr) { + val decl = expr.decl + if (decl is IndexedConstDecl) { + val varDecl = decl.varDecl + val nPrimes = decl.index - indexing[varDecl] + val varRef = varDecl.ref + if (nPrimes == 0) return varRef + if (nPrimes > 0) return Prime(varRef, nPrimes) + return expr.eval(valuation) + } + } + + return expr.map { foldIn(it, indexing, valuation) } + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt new file mode 100644 index 0000000000..77062d71c5 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt @@ -0,0 +1,55 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement + +import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation +import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner +import hu.bme.mit.theta.common.logging.Logger +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 SingleLDGTraceRefiner( + private val strategy: LDGTraceCheckerStrategy, + private val solverFactory: SolverFactory, + private val refiner: JoiningPrecRefiner, + private val logger: Logger, + private val init: Expr = True(), +) : LDGTraceRefiner { + + override fun refine(witness: LDG, prec: P): RefinerResult> { + val ldgTraces = witness.traces + check(ldgTraces.isNotEmpty()) { "${this.javaClass.simpleName} needs at least one trace!" } + val ldgTrace = ldgTraces[0] + val refutation: ExprTraceStatus = + strategy.check(ldgTrace, solverFactory, init, logger) + if (refutation.isInfeasible) { + val refinedPrecision: P = + refiner.refine(prec, ldgTrace.toTrace(), refutation.asInfeasible().refutation) + witness.pruneAll() + return RefinerResult.spurious(refinedPrecision) + } + return RefinerResult.unsafe(ldgTrace) + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt new file mode 100644 index 0000000000..5eadd022c7 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt @@ -0,0 +1,74 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.util + +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.Type +import hu.bme.mit.theta.core.utils.ExprUtils + +class VarCollectorStmtVisitor : StmtVisitor>, Set>> { + + companion object { + + fun visitAll(stmts: Collection, vars: Set>): Set> { + val visitor = VarCollectorStmtVisitor() + val expanded: Set> = + stmts.fold(emptySet()) { acc, stmt -> acc + stmt.accept(visitor, vars) } + return if (expanded.size > vars.size) visitAll(stmts, expanded) else expanded + } + } + + override fun visit(stmt: SkipStmt, param: Set>) = param + + override fun visit(stmt: AssumeStmt, param: Set>) = param + + override fun visit( + stmt: AssignStmt, + param: Set>, + ): Set> { + val rightVars: Collection> = ExprUtils.getVars(stmt.expr) + val leftVar = stmt.varDecl + for (rightVar in rightVars) { + if (rightVar == leftVar || param.contains(rightVar)) { + return param.plus(leftVar) + } + } + return param + } + + override fun visit(stmt: HavocStmt, param: Set>) = + param + stmt.varDecl + + override fun visit(stmt: SequenceStmt, param: Set>) = + param + visitAll(stmt.stmts, param) + + override fun visit(stmt: NonDetStmt, param: Set>) = param + visitAll(stmt.stmts, param) + + override fun visit(stmt: OrtStmt, param: Set>) = param + visitAll(stmt.stmts, param) + + override fun visit(stmt: LoopStmt, param: Set>) = param + stmt.stmt.accept(this, param) + + override fun visit(stmt: IfStmt, param: Set>) = + param + stmt.then.accept(this, param) + stmt.elze.accept(this, param) + + override fun visit( + stmt: MemoryAssignStmt?, + param: Set>?, + ): Set> { + TODO("Not yet implemented") + } +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt new file mode 100644 index 0000000000..511efb266f --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt @@ -0,0 +1,134 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.utils + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.common.visualization.* +import hu.bme.mit.theta.common.visualization.Alignment.LEFT +import hu.bme.mit.theta.common.visualization.Shape.RECTANGLE +import java.awt.Color + +class LdgVisualizer( + private val stateToString: (S) -> String, + private val actionToString: (A) -> String, +) : ProofVisualizer> { + + private var traceNodes: MutableSet> = mutableSetOf() + private var traceEdges: MutableSet> = mutableSetOf() + + override fun visualize(ldg: LDG): Graph { + traceNodes = mutableSetOf() + traceEdges = mutableSetOf() + return createVisualization(ldg) + } + + fun visualize(ldg: LDG, trace: LDGTrace): Graph { + traceEdges = mutableSetOf() + traceEdges.addAll(trace.edges) + traceNodes = mutableSetOf() + trace.edges.map { it.source!! }.forEach(traceNodes::add) + return createVisualization(ldg) + } + + private fun createVisualization(ldg: LDG): Graph { + val graph = Graph(LDG_ID, LDG_LABEL) + + val traversed: MutableSet> = mutableSetOf() + + for (initNode in ldg.initNodes) { + traverse(graph, initNode, traversed) + val nAttributes = + NodeAttributes.builder() + .label("") + .fillColor(FILL_COLOR) + .lineColor(FILL_COLOR) + .lineStyle(SUCC_EDGE_STYLE) + .peripheries(1) + .build() + graph.addNode(PHANTOM_INIT_ID + initNode.id, nAttributes) + val eAttributes = + EdgeAttributes.builder() + .label("") + .color(if (traceNodes.contains(initNode)) TARGET_COLOR else LINE_COLOR) + .lineStyle(SUCC_EDGE_STYLE) + .build() + graph.addEdge(PHANTOM_INIT_ID + initNode.id, NODE_ID_PREFIX + initNode.id, eAttributes) + } + + return graph + } + + private fun traverse( + graph: Graph, + node: LDGNode, + traversed: MutableSet>, + ) { + if (traversed.contains(node)) { + return + } else { + traversed.add(node) + } + val nodeId = NODE_ID_PREFIX + node.id + val peripheries = if (node.accepting) 2 else 1 + + val nAttributes = + NodeAttributes.builder() + .label(stateToString(node.state)) + .alignment(LEFT) + .shape(RECTANGLE) + .font(FONT) + .fillColor(FILL_COLOR) + .lineColor(if (traceNodes.contains(node)) TARGET_COLOR else LINE_COLOR) + .lineStyle(SUCC_EDGE_STYLE) + .peripheries(peripheries) + .build() + + graph.addNode(nodeId, nAttributes) + + for (edge in node.outEdges) { + traverse(graph, edge.target, traversed) + val sourceId = NODE_ID_PREFIX + edge.source?.id + val targetId = NODE_ID_PREFIX + edge.target.id + val eAttributes = + EdgeAttributes.builder() + .label(actionToString(edge.action!!)) + .alignment(LEFT) + .font(FONT) + .color(if (traceEdges.contains(edge)) TARGET_COLOR else LINE_COLOR) + .lineStyle(if (edge.accepting) LineStyle.DASHED else SUCC_EDGE_STYLE) + .build() + graph.addEdge(sourceId, targetId, eAttributes) + } + } + + companion object { + + private val SUCC_EDGE_STYLE = LineStyle.NORMAL + private const val LDG_LABEL = "" + private const val LDG_ID = "ldg" + private const val FONT = "courier" + private const val NODE_ID_PREFIX = "node_" + private val FILL_COLOR: Color = Color.WHITE + private val LINE_COLOR: Color = Color.BLACK + private val TARGET_COLOR: Color = Color.RED + private const val PHANTOM_INIT_ID = "phantom_init" + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java new file mode 100644 index 0000000000..4c6acec5e1 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java @@ -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.analysis.algorithm.loopchecker; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult; +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.expl.ExplPrec; +import hu.bme.mit.theta.analysis.expl.ExplState; +import hu.bme.mit.theta.analysis.expl.ExplStatePredicate; +import hu.bme.mit.theta.analysis.expl.ExplStmtAnalysis; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.CfaAction; +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; +import hu.bme.mit.theta.cfa.analysis.CfaPrec; +import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec; +import hu.bme.mit.theta.cfa.dsl.CfaDslManager; +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.*; +import hu.bme.mit.theta.xsts.analysis.initprec.XstsAllVarsInitPrec; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; +import java.util.Arrays; +import java.util.Collection; +import java.util.function.Predicate; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +@RunWith(Parameterized.class) +public class LDGAbstractorCheckingTest { + + @Parameterized.Parameter public String fileName; + + @Parameterized.Parameter(1) + public String propFileName; + + @Parameterized.Parameter(2) + public String acceptingLocationName; + + @Parameterized.Parameter(3) + public boolean isLassoPresent; + + @Parameterized.Parameters + public static Collection data() { + return Arrays.asList( + new Object[][] { + {"counter6to7.cfa", "", "IS6", true}, + {"counter6to7.xsts", "x_eq_7.prop", "", true}, + {"counter6to7.xsts", "x_eq_6.prop", "", true}, + {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, + {"colors.xsts", "currentColor_eq_Green.prop", "", true}, + {"counter5.xsts", "x_eq_5.prop", "", true}, + {"forever5.xsts", "x_eq_5.prop", "", true}, + {"counter6to7.xsts", "x_eq_5.prop", "", false}, + {"weather.xsts", "isWet_eq_true.prop", "", false}, + {"weather.xsts", "waterproof.prop", "", true} + }); + } + + @Test + public void test() throws IOException { + if (propFileName.isBlank() && !acceptingLocationName.isBlank()) testWithCfa(); + if (!propFileName.isBlank() && acceptingLocationName.isBlank()) testWithXsts(); + } + + private void testWithXsts() throws IOException { + XSTS xsts; + try (InputStream inputStream = + new SequenceInputStream( + new FileInputStream(String.format("src/test/resources/xsts/%s", fileName)), + new FileInputStream( + String.format("src/test/resources/prop/%s", propFileName)))) { + xsts = XstsDslManager.createXsts(inputStream); + } + final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + final Analysis, XstsAction, ExplPrec> analysis = + XstsAnalysis.create( + ExplStmtAnalysis.create(abstractionSolver, xsts.getInitFormula(), 250)); + final LTS, XstsAction> lts = + XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + final Predicate> statePredicate = + new XstsStatePredicate<>(new ExplStatePredicate(xsts.getProp(), abstractionSolver)); + final AcceptancePredicate, XstsAction> target = + new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + final ExplPrec precision = new XstsAllVarsInitPrec().createExpl(xsts); + var abstractor = + new LDGAbstractor<>( + analysis, + lts, + target, + LoopcheckerSearchStrategy.Companion.getDefault(), + new ConsoleLogger(Logger.Level.DETAIL)); + LDG, XstsAction> ldg = new LDG<>(target); + AbstractorResult result = abstractor.check(ldg, precision); + Assert.assertEquals(isLassoPresent, result.isUnsafe()); + } + + private void testWithCfa() throws IOException { + final CFA cfa = + CfaDslManager.createCfa( + new FileInputStream(String.format("src/test/resources/cfa/%s", fileName))); + final CfaLts lts = CfaConfigBuilder.Encoding.SBE.getLts(cfa.getInitLoc()); + final Analysis, CfaAction, CfaPrec> analysis = + CfaAnalysis.create( + cfa.getInitLoc(), + ExplStmtAnalysis.create( + Z3LegacySolverFactory.getInstance().createSolver(), True(), 250)); + final CfaPrec precision = GlobalCfaPrec.create(ExplPrec.of(cfa.getVars())); + Predicate> statePredicate = + cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); + AcceptancePredicate, CfaAction> target = + new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + LDGAbstractor, CfaAction, CfaPrec> abstractor = + new LDGAbstractor<>( + analysis, + lts, + target, + LoopcheckerSearchStrategy.Companion.getDefault(), + new ConsoleLogger(Logger.Level.DETAIL)); + LDG, CfaAction> ldg = new LDG<>(target); + AbstractorResult result = abstractor.check(ldg, precision); + Assert.assertEquals(isLassoPresent, result.isUnsafe()); + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java new file mode 100644 index 0000000000..8e8a4929be --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java @@ -0,0 +1,230 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; +import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleLDGTraceRefiner; +import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; +import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; +import hu.bme.mit.theta.analysis.pred.*; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +import hu.bme.mit.theta.analysis.utils.LdgVisualizer; +import hu.bme.mit.theta.cfa.CFA; +import hu.bme.mit.theta.cfa.analysis.CfaAction; +import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; +import hu.bme.mit.theta.cfa.analysis.CfaPrec; +import hu.bme.mit.theta.cfa.analysis.CfaState; +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder; +import hu.bme.mit.theta.cfa.analysis.lts.CfaLts; +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec; +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec; +import hu.bme.mit.theta.cfa.dsl.CfaDslManager; +import hu.bme.mit.theta.common.logging.ConsoleLogger; +import hu.bme.mit.theta.common.logging.Logger; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; +import java.util.Arrays; +import java.util.Collection; +import java.util.Objects; +import java.util.function.Predicate; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.BeforeClass; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +@RunWith(Parameterized.class) +public class LDGCegarVerifierTest { + + private static Solver abstractionSolver; + private static ItpSolver itpSolver; + private static SolverFactory solverFactory; + private static Logger logger; + + @BeforeClass + public static void init() { + abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver(); + solverFactory = Z3LegacySolverFactory.getInstance(); + logger = new ConsoleLogger(Logger.Level.INFO); + } + + @Parameterized.Parameter public String fileName; + + @Parameterized.Parameter(1) + public String propFileName; + + @Parameterized.Parameter(2) + public String acceptingLocationName; + + @Parameterized.Parameter(3) + public boolean result; + + @Parameterized.Parameters + public static Collection data() { + return Arrays.asList( + new Object[][] { + {"counter3.xsts", "x_eq_3.prop", "", false}, + {"counter6to7.xsts", "x_eq_7.prop", "", true}, + {"counter6to7.cfa", "", "IS6", true}, + {"counter2to3.cfa", "", "IS3", true}, + {"counter6to7.xsts", "x_eq_6.prop", "", true}, + {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, + {"colors.xsts", "currentColor_eq_Green.prop", "", true}, + {"counter5.xsts", "x_eq_5.prop", "", true}, + {"forever5.xsts", "x_eq_5.prop", "", true}, + {"counter6to7.xsts", "x_eq_5.prop", "", false} + }); + } + + @Test + public void test() throws IOException { + if (propFileName.isBlank() && !acceptingLocationName.isBlank()) testWithCfa(); + if (!propFileName.isBlank() && acceptingLocationName.isBlank()) testWithXsts(); + } + + private void testWithXsts() throws IOException { + XSTS xsts; + try (InputStream inputStream = + new SequenceInputStream( + new FileInputStream(String.format("src/test/resources/xsts/%s", fileName)), + new FileInputStream( + String.format("src/test/resources/prop/%s", propFileName)))) { + xsts = XstsDslManager.createXsts(inputStream); + } + final Analysis, XstsAction, PredPrec> analysis = + XstsAnalysis.create( + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + xsts.getInitFormula())); + final LTS, XstsAction> lts = + XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + final Predicate> statePredicate = + new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); + final AcceptancePredicate, XstsAction> target = + new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp()); + var abstractor = + new LDGAbstractor<>( + analysis, + lts, + target, + LoopcheckerSearchStrategy.Companion.getDefault(), + logger); + final Refiner< + PredPrec, + LDG, XstsAction>, + LDGTrace, XstsAction>> + refiner = + new SingleLDGTraceRefiner<>( + LDGTraceCheckerStrategy.Companion.getDefault(), + solverFactory, + JoiningPrecRefiner.create( + new ItpRefToPredPrec(ExprSplitters.atoms())), + logger, + xsts.getInitFormula()); + final CegarChecker< + PredPrec, + LDG, XstsAction>, + LDGTrace, XstsAction>> + verifier = + CegarChecker.create( + abstractor, + refiner, + logger, + new LdgVisualizer<>(Objects::toString, Objects::toString)); + + final PredPrec precision = PredPrec.of(); + var result = verifier.check(precision); + Assert.assertEquals(this.result, result.isUnsafe()); + } + + private void testWithCfa() throws IOException { + final CFA cfa = + CfaDslManager.createCfa( + new FileInputStream(String.format("src/test/resources/cfa/%s", fileName))); + final CfaLts lts = CfaConfigBuilder.Encoding.SBE.getLts(null); + final Analysis, CfaAction, CfaPrec> analysis = + CfaAnalysis.create( + cfa.getInitLoc(), + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanSplitAbstractor(abstractionSolver), + True())); + final Predicate> statePredicate = + cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); + final AcceptancePredicate, CfaAction> target = + new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + final RefutationToPrec refToPrec = + new ItpRefToPredPrec(ExprSplitters.atoms()); + final RefutationToGlobalCfaPrec cfaRefToPrec = + new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc()); + var abstractor = + new LDGAbstractor<>( + analysis, + lts, + target, + LoopcheckerSearchStrategy.Companion.getDefault(), + logger); + final Refiner< + CfaPrec, + LDG, CfaAction>, + LDGTrace, CfaAction>> + refiner = + new SingleLDGTraceRefiner<>( + LDGTraceCheckerStrategy.Companion.getDefault(), + solverFactory, + JoiningPrecRefiner.create(cfaRefToPrec), + logger, + True()); + final CegarChecker< + CfaPrec, + LDG, CfaAction>, + LDGTrace, CfaAction>> + verifier = + CegarChecker.create( + abstractor, + refiner, + logger, + new LdgVisualizer<>(Objects::toString, Objects::toString)); + + final GlobalCfaPrec prec = GlobalCfaPrec.create(PredPrec.of()); + var res = verifier.check(prec); + Assert.assertEquals(result, res.isUnsafe()); + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java new file mode 100644 index 0000000000..dfab147cc9 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java @@ -0,0 +1,91 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker; + +import hu.bme.mit.theta.analysis.Analysis; +import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.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.expr.ExprStatePredicate; +import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; +import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; +import hu.bme.mit.theta.analysis.pred.PredAbstractors; +import hu.bme.mit.theta.analysis.pred.PredAnalysis; +import hu.bme.mit.theta.analysis.pred.PredPrec; +import hu.bme.mit.theta.analysis.pred.PredState; +import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; +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.SolverFactory; +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; +import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.*; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; +import java.util.function.Predicate; +import kotlin.Unit; +import org.junit.Assert; +import org.junit.Test; + +public class LDGTraceCheckerTest { + @Test + public void testWithCounter3() throws IOException { + XSTS xsts; + try (InputStream inputStream = + new SequenceInputStream( + new FileInputStream("src/test/resources/xsts/counter3.xsts"), + new FileInputStream("src/test/resources/prop/x_eq_3.prop"))) { + xsts = XstsDslManager.createXsts(inputStream); + } + final SolverFactory solverFactory = Z3LegacySolverFactory.getInstance(); + final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver(); + final Analysis, XstsAction, PredPrec> analysis = + XstsAnalysis.create( + PredAnalysis.create( + abstractionSolver, + PredAbstractors.booleanAbstractor(abstractionSolver), + xsts.getInitFormula())); + final LTS, XstsAction> lts = + XstsLts.create(xsts, XstsStmtOptimizer.create(DefaultStmtOptimizer.create())); + final Predicate> statePredicate = + new XstsStatePredicate<>(new ExprStatePredicate(xsts.getProp(), abstractionSolver)); + final AcceptancePredicate, XstsAction> target = + new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); + final PredPrec precision = PredPrec.of(); + final Logger logger = new ConsoleLogger(Logger.Level.DETAIL); + final LDGAbstractor, XstsAction, PredPrec> abstractor = + new LDGAbstractor<>( + analysis, + lts, + target, + LoopcheckerSearchStrategy.Companion.getDefault(), + logger); + LDG, XstsAction> ldg = new LDG<>(target); + abstractor.check(ldg, precision); + LDGTrace, XstsAction> trace = ldg.getTraces().iterator().next(); + + ExprTraceStatus status = + LDGTraceCheckerStrategy.Companion.getDefault() + .check(trace, solverFactory, xsts.getInitFormula(), logger); + Assert.assertTrue(status.isInfeasible()); + } +} diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java new file mode 100644 index 0000000000..f059bccaac --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java @@ -0,0 +1,65 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg; + +import static org.mockito.Mockito.mock; + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace; +import hu.bme.mit.theta.analysis.expr.ExprAction; +import hu.bme.mit.theta.analysis.expr.ExprState; +import java.util.List; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.mockito.junit.MockitoJUnitRunner; + +@RunWith(MockitoJUnitRunner.class) +public class LDGTraceTest { + + @Test + public void testSimpleLasso() { + LDGNode initNode = new LDGNode<>(mock(ExprState.class), false); + LDGNode hondaNode = new LDGNode<>(mock(ExprState.class), true); + LDGNode loopNode = new LDGNode<>(mock(ExprState.class), false); + Assert.assertNotEquals(initNode, hondaNode); + Assert.assertNotEquals(initNode, loopNode); + Assert.assertNotEquals(loopNode, hondaNode); + LDGEdge firstEdge = + new LDGEdge<>(initNode, hondaNode, mock(ExprAction.class), false); + LDGEdge secondEdge = + new LDGEdge<>(hondaNode, loopNode, mock(ExprAction.class), false); + LDGEdge thirdEdge = + new LDGEdge<>(loopNode, hondaNode, mock(ExprAction.class), false); + initNode.addOutEdge(firstEdge); + hondaNode.addInEdge(firstEdge); + hondaNode.addOutEdge(secondEdge); + loopNode.addInEdge(secondEdge); + loopNode.addOutEdge(thirdEdge); + hondaNode.addInEdge(thirdEdge); + + LDGTrace trace = + new LDGTrace<>(List.of(firstEdge, secondEdge, thirdEdge), hondaNode); + + Assert.assertEquals(1, trace.getTail().size()); + Assert.assertEquals(2, trace.getLoop().size()); + Assert.assertEquals(initNode, trace.getTail().get(0).getSource()); + Assert.assertEquals(hondaNode, trace.getTail().get(0).getTarget()); + Assert.assertEquals(hondaNode, trace.getLoop().get(0).getSource()); + Assert.assertEquals(loopNode, trace.getLoop().get(0).getTarget()); + Assert.assertEquals(loopNode, trace.getLoop().get(1).getSource()); + Assert.assertEquals(hondaNode, trace.getLoop().get(1).getTarget()); + } +} diff --git a/subprojects/common/analysis/src/test/resources/cfa/counter2to3.cfa b/subprojects/common/analysis/src/test/resources/cfa/counter2to3.cfa new file mode 100644 index 0000000000..b5b2867b4f --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/cfa/counter2to3.cfa @@ -0,0 +1,16 @@ +main process cfa { + var x : int + + init loc I + loc L0 + loc L1 + loc IS2 + loc IS3 + + I -> L0 { x := 0 } + L0 -> L1 { assume x < 2 } + L1 -> L0 { x := x + 1 } + L0 -> IS2 { assume x = 2 } + IS2 -> IS3 { x := x + 1 } + IS3 -> IS2 { x := x - 1 } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/cfa/counter6to7.cfa b/subprojects/common/analysis/src/test/resources/cfa/counter6to7.cfa new file mode 100644 index 0000000000..3063a76786 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/cfa/counter6to7.cfa @@ -0,0 +1,19 @@ +main process cfa { + var x : int + + init loc L0 + loc L1 + loc L2 + loc L3 + loc IS6 + loc IS7 + error loc ERR + + L0 -> L1 { x := 0 } + L1 -> L2 { assume x < 5 } + L1 -> L3 { assume not (x < 5) } + L2 -> L1 { x := x + 1 } + L3 -> IS6 { x := x + 1 } + IS6 -> IS7 { x := x + 1 } + IS7 -> IS6 { x := x - 1 } +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/currentColor_eq_Green.prop b/subprojects/common/analysis/src/test/resources/prop/currentColor_eq_Green.prop new file mode 100644 index 0000000000..eeb441d7a5 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/currentColor_eq_Green.prop @@ -0,0 +1,3 @@ +prop { + currentColor == Green +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/isWet_eq_true.prop b/subprojects/common/analysis/src/test/resources/prop/isWet_eq_true.prop new file mode 100644 index 0000000000..b7ab97c829 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/isWet_eq_true.prop @@ -0,0 +1,3 @@ +prop { + isWet == true +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/waterproof.prop b/subprojects/common/analysis/src/test/resources/prop/waterproof.prop new file mode 100644 index 0000000000..bd2560743f --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/waterproof.prop @@ -0,0 +1,3 @@ +prop { + clothing == Waterproof +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_3.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_3.prop new file mode 100644 index 0000000000..02cceee940 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_3.prop @@ -0,0 +1,3 @@ +prop{ + x==3 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_5.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_5.prop new file mode 100644 index 0000000000..5fd56522e8 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_5.prop @@ -0,0 +1,3 @@ +prop{ + x==5 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_6.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_6.prop new file mode 100644 index 0000000000..46ab62325d --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_6.prop @@ -0,0 +1,3 @@ +prop{ + x==6 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/prop/x_eq_7.prop b/subprojects/common/analysis/src/test/resources/prop/x_eq_7.prop new file mode 100644 index 0000000000..c9b549c899 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/prop/x_eq_7.prop @@ -0,0 +1,3 @@ +prop{ + x==7 +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/colors.xsts b/subprojects/common/analysis/src/test/resources/xsts/colors.xsts new file mode 100644 index 0000000000..ee68377924 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/colors.xsts @@ -0,0 +1,35 @@ +type Color : { Red , Green , Blue } +type Mood : { Happy, Angry, Depressed } +var currentColor : Color = Red +var currentMood : Mood = Happy + +trans { + assume currentColor == Red; + choice { + assume currentMood == Happy; + currentColor := Green; + } or { + assume currentMood == Angry; + } or { + assume currentMood == Depressed; + currentColor := Blue; + } +} or { + assume currentColor == Green; + choice { + assume (currentMood == Happy || currentMood == Depressed); + currentColor := Blue; + } or { + assume currentMood == Angry; + currentColor := Red; + } +} or { + assume currentColor == Blue; + if (currentMood == Angry) currentColor := Red; +} + +init{} + +env { + havoc currentMood; +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/counter3.xsts b/subprojects/common/analysis/src/test/resources/xsts/counter3.xsts new file mode 100644 index 0000000000..3b7909e1db --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/counter3.xsts @@ -0,0 +1,10 @@ +var x: integer = 0 + +trans { + assume x<3; + x:=x+1; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/counter5.xsts b/subprojects/common/analysis/src/test/resources/xsts/counter5.xsts new file mode 100644 index 0000000000..ed7b207596 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/counter5.xsts @@ -0,0 +1,12 @@ +ctrl var x: integer = 0 + +trans { + assume x<5; + x:=x+1; +} or { + x:=x; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/counter6to7.xsts b/subprojects/common/analysis/src/test/resources/xsts/counter6to7.xsts new file mode 100644 index 0000000000..300a73f31a --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/counter6to7.xsts @@ -0,0 +1,13 @@ +ctrl var x: integer = 0 + +trans { + assume x<=6; + x:=x+1; +} or { + assume x==7; + x:=x-1; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/forever5.xsts b/subprojects/common/analysis/src/test/resources/xsts/forever5.xsts new file mode 100644 index 0000000000..d80dcaff9d --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/forever5.xsts @@ -0,0 +1,9 @@ +ctrl var x: integer = 5 + +trans { + x:=x; +} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/infinitehavoc.xsts b/subprojects/common/analysis/src/test/resources/xsts/infinitehavoc.xsts new file mode 100644 index 0000000000..d53b11cf4b --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/infinitehavoc.xsts @@ -0,0 +1,14 @@ +ctrl var x: integer = 0 +var y: integer = 0 + +trans { + havoc y; +} + +init { + x:=7; +} + +env { + havoc y; +} \ No newline at end of file diff --git a/subprojects/common/analysis/src/test/resources/xsts/weather.xsts b/subprojects/common/analysis/src/test/resources/xsts/weather.xsts new file mode 100644 index 0000000000..36d3e79442 --- /dev/null +++ b/subprojects/common/analysis/src/test/resources/xsts/weather.xsts @@ -0,0 +1,106 @@ +type Weather : { Sunny , Cloudy , Rainy, Foggy } +type TimeOfDay : { __init__, Morning , Noon, Afternoon, Night } +type Clothing : { 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 = Shorts + +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; + } +} + +init { + havoc weather; +} + +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; + } + } +} \ No newline at end of file