From 2896980becb5a66bd78f70aa4d3b485ffdaf0d53 Mon Sep 17 00:00:00 2001 From: RipplB Date: Wed, 20 Nov 2024 10:08:33 +0100 Subject: [PATCH] LTL checking capability Add possibility of checking LTL properties with CEGAR. CFA is now extended with optional accepting edges. Classes are available that convert LTL string to such CFA. --- .../{loopchecker/ldg/LDG.kt => asg/ASG.kt} | 48 ++-- .../LDGTrace.kt => asg/ASGTrace.kt} | 18 +- .../ASGTraceRefiner.kt} | 8 +- .../algorithm/cegar/CegarChecker.java | 2 +- .../{LDGAbstractor.kt => ASGAbstractor.kt} | 30 +-- .../abstraction/GdfsSearchStrategies.kt | 38 +-- .../abstraction/LoopcheckerSearchStrategy.kt | 18 +- .../abstraction/NdfsSearchStrategy.kt | 38 +-- ...Strategy.kt => ASGTraceCheckerStrategy.kt} | 18 +- ...oundedUnrollingASGTraceCheckerStrategy.kt} | 8 +- ...gy.kt => MilanoASGTraceCheckerStrategy.kt} | 8 +- ...aceRefiner.kt => SingleASGTraceRefiner.kt} | 13 +- .../mit/theta/analysis/unit/UnitInitFunc.java | 5 +- .../mit/theta/analysis/utils/LDGVisualizer.kt | 34 +-- ...st.java => ASGAbstractorCheckingTest.java} | 21 +- ...ierTest.java => ASGCegarVerifierTest.java} | 45 ++-- ...ckerTest.java => ASGTraceCheckerTest.java} | 21 +- .../{LDGTraceTest.java => ASGTraceTest.java} | 28 +- .../kotlin/common/ltl/cli/LtlCliOptions.kt | 8 +- .../common/cfa/buchi/hoa/BuchiBuilder.kt | 2 +- .../hu/bme/mit/theta/common/ltl/LtlChecker.kt | 53 ++-- .../common/ltl/LtlCheckTestWithCfaExpl.kt | 8 +- .../common/ltl/LtlCheckTestWithCfaPred.kt | 10 +- .../common/ltl/LtlCheckTestWithXstsExpl.kt | 8 +- .../common/ltl/LtlCheckTestWithXstsPred.kt | 21 +- ...28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa | 20 ++ .../test/kotlin/multi/MultiAlternatingTest.kt | 246 ++++++++++-------- .../analysis/util/XstsCombineExtractUtils.kt | 4 +- .../bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt | 67 ++++- 29 files changed, 479 insertions(+), 369 deletions(-) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/{loopchecker/ldg/LDG.kt => asg/ASG.kt} (57%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/{loopchecker/LDGTrace.kt => asg/ASGTrace.kt} (85%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/{loopchecker/refinement/LDGTraceRefiner.kt => asg/ASGTraceRefiner.kt} (73%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/{LDGAbstractor.kt => ASGAbstractor.kt} (69%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/{LDGTraceCheckerStrategy.kt => ASGTraceCheckerStrategy.kt} (93%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/{BoundedUnrollingLDGTraceCheckerStrategy.kt => BoundedUnrollingASGTraceCheckerStrategy.kt} (96%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/{MilanoLDGTraceCheckerStrategy.kt => MilanoASGTraceCheckerStrategy.kt} (93%) rename subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/{SingleLDGTraceRefiner.kt => SingleASGTraceRefiner.kt} (83%) rename subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/{LDGAbstractorCheckingTest.java => ASGAbstractorCheckingTest.java} (91%) rename subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/{LDGCegarVerifierTest.java => ASGCegarVerifierTest.java} (88%) rename subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/{LDGTraceCheckerTest.java => ASGTraceCheckerTest.java} (88%) rename subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/{LDGTraceTest.java => ASGTraceTest.java} (72%) create mode 100644 subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASG.kt similarity index 57% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASG.kt index 098ce639a4..d7b7816895 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDG.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASG.kt @@ -13,21 +13,21 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg +package hu.bme.mit.theta.analysis.algorithm.asg import hu.bme.mit.theta.analysis.algorithm.Proof import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState -class LDG( +/** Abstract state graph */ +class ASG( private val acceptancePredicate: AcceptancePredicate ) : Proof { - val nodes: MutableMap> = mutableMapOf() - val initNodes: MutableList> = mutableListOf() - var traces: List> = emptyList() + val nodes: MutableMap> = mutableMapOf() + val initNodes: MutableList> = mutableListOf() + var traces: List> = emptyList() fun isUninitialised() = initNodes.isEmpty() @@ -42,52 +42,48 @@ class LDG( initNodes.addAll(initStates.map(this::getOrCreateNode)) } - fun getOrCreateNode(state: S): LDGNode = - nodes.computeIfAbsent(state) { s -> LDGNode(s, acceptancePredicate.test(Pair(s, null))) } + fun getOrCreateNode(state: S): ASGNode = + nodes.computeIfAbsent(state) { s -> ASGNode(s, acceptancePredicate.test(Pair(s, null))) } fun containsNode(state: S) = nodes.containsKey(state) fun drawEdge( - source: LDGNode, - target: LDGNode, + source: ASGNode, + target: ASGNode, action: A?, accepting: Boolean, - ): LDGEdge { - val edge = LDGEdge(source, target, action, accepting) + ): ASGEdge { + val edge = ASGEdge(source, target, action, accepting) source.addOutEdge(edge) target.addInEdge(edge) return edge } } -data class LDGEdge( - val source: LDGNode?, - val target: LDGNode, +data class ASGEdge( + val source: ASGNode?, + val target: ASGNode, val action: A?, val accepting: Boolean, ) -class LDGNode(val state: S, val accepting: Boolean) { +class ASGNode(val state: S, val accepting: Boolean) { companion object { var idCounter: Long = 0 } - val inEdges: MutableList> = mutableListOf() - val outEdges: MutableList> = mutableListOf() + val inEdges: MutableList> = mutableListOf() + val outEdges: MutableList> = mutableListOf() val id = idCounter++ - var validLoopHondas: MutableSet> = hashSetOf() + var validLoopHondas: MutableSet> = hashSetOf() var expanded: Boolean = false set(value) { - if (!value) { - throw IllegalArgumentException("Can't set expanded to false") - } + require(value) { "Can't set expanded to false" } field = true } - fun addInEdge(edge: LDGEdge) = inEdges.add(edge) + fun addInEdge(edge: ASGEdge) = inEdges.add(edge) - fun addOutEdge(edge: LDGEdge) = outEdges.add(edge) - - fun smallerEdgeCollection() = if (inEdges.size > outEdges.size) inEdges else outEdges + fun addOutEdge(edge: ASGEdge) = outEdges.add(edge) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTrace.kt similarity index 85% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTrace.kt index 97ce7b9f9e..b10f075527 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTrace.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTrace.kt @@ -13,28 +13,26 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.loopchecker +package hu.bme.mit.theta.analysis.algorithm.asg import hu.bme.mit.theta.analysis.Cex import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.common.logging.Logger.Level -class LDGTrace( - val tail: List>, - val honda: LDGNode, - val loop: List>, +class ASGTrace( + val tail: List>, + val honda: ASGNode, + val loop: List>, ) : Cex { val edges by lazy { tail + loop } constructor( - edges: List>, - honda: LDGNode, + edges: List>, + honda: ASGNode, ) : this(edges.takeWhile { it.source != honda }, honda, edges.dropWhile { it.source != honda }) init { @@ -51,7 +49,7 @@ class LDGTrace( override fun length() = edges.size - fun getEdge(index: Int): LDGEdge { + fun getEdge(index: Int): ASGEdge { check(index >= 0) { "Can't get negative indexed edge (${index})" } check(index < length()) { "Index out of range $index < ${length()}" } return if (index < tail.size) tail[index] else loop[index - tail.size] diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTraceRefiner.kt similarity index 73% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTraceRefiner.kt index ad174271f3..5257d04143 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceRefiner.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/ASGTraceRefiner.kt @@ -13,14 +13,12 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement +package hu.bme.mit.theta.analysis.algorithm.asg import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState -interface LDGTraceRefiner : - Refiner, LDGTrace> {} +interface ASGTraceRefiner : + Refiner, ASGTrace> diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java index dac497e043..6c648fe50c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java @@ -45,7 +45,7 @@ public final class CegarChecker

private final Refiner refiner; private final Logger logger; private final Pr proof; - private final ProofVisualizer proofVisualizer; + public final ProofVisualizer proofVisualizer; private CegarChecker( final Abstractor abstractor, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/ASGAbstractor.kt similarity index 69% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/ASGAbstractor.kt index 6b26395fcb..1bfe96a05c 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LDGAbstractor.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/ASGAbstractor.kt @@ -18,45 +18,45 @@ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction import hu.bme.mit.theta.analysis.Analysis import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger -class LDGAbstractor( +class ASGAbstractor( private val analysis: Analysis, private val lts: LTS, private val acceptancePredicate: AcceptancePredicate, private val searchStrategy: LoopcheckerSearchStrategy, private val logger: Logger, -) : Abstractor> { +) : Abstractor> { - override fun createProof() = LDG(acceptancePredicate) + override fun createProof() = ASG(acceptancePredicate) - override fun check(ldg: LDG, prec: P): AbstractorResult { - if (ldg.isUninitialised()) { - ldg.initialise(analysis.initFunc.getInitStates(prec)) - ldg.traces = emptyList() + override fun check(ASG: ASG, prec: P): AbstractorResult { + if (ASG.isUninitialised()) { + ASG.initialise(analysis.initFunc.getInitStates(prec)) + ASG.traces = emptyList() } val expander: NodeExpander = - fun(node: LDGNode): Collection> { + fun(node: ASGNode): Collection> { if (node.expanded) { return node.outEdges } node.expanded = true return lts.getEnabledActionsFor(node.state).flatMap { action -> - analysis.transFunc.getSuccStates(node.state, action, prec).map(ldg::getOrCreateNode).map { - ldg.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) + analysis.transFunc.getSuccStates(node.state, action, prec).map(ASG::getOrCreateNode).map { + ASG.drawEdge(node, it, action, acceptancePredicate.test(Pair(it.state, action))) } } } - val searchResult = searchStrategy.search(ldg, acceptancePredicate, expander, logger) - ldg.traces = searchResult.toList() + val searchResult = searchStrategy.search(ASG, acceptancePredicate, expander, logger) + ASG.traces = searchResult.toList() return AbstractorResult(searchResult.isEmpty()) } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt index 2a56838da3..7d09704af8 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/GdfsSearchStrategies.kt @@ -15,30 +15,30 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger -typealias BacktrackResult = Pair>?, List>?> +typealias BacktrackResult = Pair>?, List>?> fun combineLassos(results: Collection>) = - Pair(setOf>(), results.flatMap { it.second ?: emptyList() }) + Pair(setOf>(), results.flatMap { it.second ?: emptyList() }) abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { internal fun expandFromInitNodeUntilTarget( - initNode: LDGNode, + initNode: ASGNode, stopAtLasso: Boolean, expand: NodeExpander, logger: Logger, - ): Collection> { + ): Collection> { return expandThroughNode( emptyMap(), - LDGEdge(null, initNode, null, false), + ASGEdge(null, initNode, null, false), emptyList(), 0, stopAtLasso, @@ -49,15 +49,15 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { } private fun expandThroughNode( - pathSoFar: Map, Int>, - incomingEdge: LDGEdge, - edgesSoFar: List>, + pathSoFar: Map, Int>, + incomingEdge: ASGEdge, + edgesSoFar: List>, targetsSoFar: Int, stopAtLasso: Boolean, expand: NodeExpander, logger: Logger, ): BacktrackResult { - val expandingNode: LDGNode = incomingEdge.target + val expandingNode: ASGNode = incomingEdge.target logger.write( Logger.Level.VERBOSE, "Expanding through %s edge to %s node with state %s%n", @@ -86,7 +86,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { targetsThatFar, ) } - val lasso: LDGTrace = LDGTrace(edgesSoFar + incomingEdge, expandingNode) + val lasso: ASGTrace = ASGTrace(edgesSoFar + incomingEdge, expandingNode) logger.write(Logger.Level.DETAIL, "Built the following lasso:%n") lasso.print(logger, Logger.Level.DETAIL) return BacktrackResult(null, listOf(lasso)) @@ -102,7 +102,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { } val expandStrategy: NodeExpander = if (needsTraversing) expand else { _ -> mutableSetOf() } - val outgoingEdges: Collection> = expandStrategy(expandingNode) + val outgoingEdges: Collection> = expandStrategy(expandingNode) val results: MutableList> = mutableListOf() for (newEdge in outgoingEdges) { val result: BacktrackResult = @@ -120,7 +120,7 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { } val result: BacktrackResult = combineLassos(results) if (result.second != null) return result - val validLoopHondas: Collection> = results.flatMap { it.first ?: emptyList() } + val validLoopHondas: Collection> = results.flatMap { it.first ?: emptyList() } expandingNode.validLoopHondas.addAll(validLoopHondas) return BacktrackResult(validLoopHondas.toSet(), null) } @@ -129,13 +129,13 @@ abstract class AbstractSearchStrategy : ILoopcheckerSearchStrategy { object GdfsSearchStrategy : AbstractSearchStrategy() { override fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, - ): Collection> { + ): Collection> { for (initNode in initNodes) { - val possibleTraces: Collection> = + val possibleTraces: Collection> = expandFromInitNodeUntilTarget(initNode, true, expand, logger) if (!possibleTraces.isEmpty()) { return possibleTraces @@ -148,7 +148,7 @@ object GdfsSearchStrategy : AbstractSearchStrategy() { object FullSearchStrategy : AbstractSearchStrategy() { override fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt index 541a9976eb..e3d3f35b9e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/LoopcheckerSearchStrategy.kt @@ -15,17 +15,17 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.common.logging.NullLogger -typealias NodeExpander = (LDGNode) -> Collection> +typealias NodeExpander = (ASGNode) -> Collection> enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStrategy) { GDFS(GdfsSearchStrategy), @@ -38,19 +38,19 @@ enum class LoopcheckerSearchStrategy(private val strategy: ILoopcheckerSearchStr } fun search( - ldg: LDG, + ASG: ASG, target: AcceptancePredicate, expand: NodeExpander, logger: Logger = NullLogger.getInstance(), - ): Collection> = strategy.search(ldg.initNodes, target, expand, logger) + ): Collection> = strategy.search(ASG.initNodes, target, expand, logger) } interface ILoopcheckerSearchStrategy { fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, - ): Collection> + ): Collection> } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt index 096165a371..41b4c35cfe 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt @@ -15,10 +15,10 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.logging.Logger @@ -26,11 +26,11 @@ import hu.bme.mit.theta.common.logging.Logger object NdfsSearchStrategy : ILoopcheckerSearchStrategy { override fun search( - initNodes: Collection>, + initNodes: Collection>, target: AcceptancePredicate, expand: NodeExpander, logger: Logger, - ): Collection> { + ): Collection> { for (node in initNodes) { for (edge in expand(node)) { val result = blueSearch(edge, emptyList(), mutableSetOf(), mutableSetOf(), target, expand) @@ -41,13 +41,13 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { } private fun redSearch( - seed: LDGNode, - edge: LDGEdge, - trace: List>, - redNodes: MutableSet>, + seed: ASGNode, + edge: ASGEdge, + trace: List>, + redNodes: MutableSet>, target: AcceptancePredicate, expand: NodeExpander, - ): List> { + ): List> { val targetNode = edge.target if (targetNode.state.isBottom) { return emptyList() @@ -60,7 +60,7 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { } redNodes.add(edge.target) for (nextEdge in expand(targetNode)) { - val redSearch: List> = + val redSearch: List> = redSearch(seed, nextEdge, trace + edge, redNodes, target, expand) if (redSearch.isNotEmpty()) return redSearch } @@ -68,13 +68,13 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { } private fun blueSearch( - edge: LDGEdge, - trace: List>, - blueNodes: MutableSet>, - redNodes: Set>, + edge: ASGEdge, + trace: List>, + blueNodes: MutableSet>, + redNodes: Set>, target: AcceptancePredicate, expand: NodeExpander, - ): Collection> { + ): Collection> { val targetNode = edge.target if (targetNode.state.isBottom) { return emptyList() @@ -83,16 +83,16 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { // Edge source can only be null artificially, and is only used when calling other search // strategies val accNode = if (targetNode.accepting) targetNode else edge.source!! - val redSearch: List> = + val redSearch: List> = redSearch(accNode, edge, trace, mutableSetOf(), target, expand) - if (redSearch.isNotEmpty()) return setOf(LDGTrace(redSearch, accNode)) + if (redSearch.isNotEmpty()) return setOf(ASGTrace(redSearch, accNode)) } if (blueNodes.contains(targetNode)) { return emptyList() } blueNodes.add(edge.target) for (nextEdge in expand(targetNode)) { - val blueSearch: Collection> = + val blueSearch: Collection> = blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand) if (!blueSearch.isEmpty()) return blueSearch } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/ASGTraceCheckerStrategy.kt similarity index 93% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/ASGTraceCheckerStrategy.kt index 7a950a91e8..e59e8a0561 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/LDGTraceCheckerStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/ASGTraceCheckerStrategy.kt @@ -16,7 +16,7 @@ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement import hu.bme.mit.theta.analysis.Trace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState @@ -35,26 +35,26 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexing import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory import hu.bme.mit.theta.solver.* -enum class LDGTraceCheckerStrategy { +enum class ASGTraceCheckerStrategy { MILANO { override fun check( - trace: LDGTrace, + trace: ASGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger, - ) = MilanoLDGTraceCheckerStrategy(trace, solverFactory, init, logger).check() + ) = MilanoASGTraceCheckerStrategy(trace, solverFactory, init, logger).check() }, BOUNDED_UNROLLING { override fun check( - trace: LDGTrace, + trace: ASGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger, ): ExprTraceStatus { try { - return BoundedUnrollingLDGTraceCheckerStrategy(trace, solverFactory, init, 100, logger) + return BoundedUnrollingASGTraceCheckerStrategy(trace, solverFactory, init, 100, logger) .check() } catch (t: TraceCheckingFailedException) { logger.write(Logger.Level.INFO, "${t.message}\n") @@ -70,15 +70,15 @@ enum class LDGTraceCheckerStrategy { } abstract fun check( - trace: LDGTrace, + trace: ASGTrace, solverFactory: SolverFactory, init: Expr = True(), logger: Logger = NullLogger.getInstance(), ): ExprTraceStatus } -abstract class AbstractLDGTraceCheckerStrategy( - private val trace: LDGTrace, +abstract class AbstractASGTraceCheckerStrategy( + private val trace: ASGTrace, solverFactory: SolverFactory, private val init: Expr, private val logger: Logger, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingASGTraceCheckerStrategy.kt similarity index 96% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingASGTraceCheckerStrategy.kt index 4eeb5acbaf..8afff23418 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingLDGTraceCheckerStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/BoundedUnrollingASGTraceCheckerStrategy.kt @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.loopchecker.exception.TraceCheckingFailedException import hu.bme.mit.theta.analysis.algorithm.loopchecker.util.VarCollectorStmtVisitor import hu.bme.mit.theta.analysis.expl.ExplPrec @@ -42,13 +42,13 @@ import hu.bme.mit.theta.solver.ItpMarker import hu.bme.mit.theta.solver.SolverFactory import java.util.function.Consumer -class BoundedUnrollingLDGTraceCheckerStrategy( - private val trace: LDGTrace, +class BoundedUnrollingASGTraceCheckerStrategy( + private val trace: ASGTrace, private val solverFactory: SolverFactory, init: Expr, private val bound: Int, private val logger: Logger, -) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { +) : AbstractASGTraceCheckerStrategy(trace, solverFactory, init, logger) { override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { val indexingBeforeLoop = indexings[trace.tail.size] diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoASGTraceCheckerStrategy.kt similarity index 93% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoASGTraceCheckerStrategy.kt index feef72e00f..a391387f75 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoLDGTraceCheckerStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/MilanoASGTraceCheckerStrategy.kt @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus @@ -35,12 +35,12 @@ import hu.bme.mit.theta.core.utils.indexings.VarIndexing import hu.bme.mit.theta.solver.Interpolant import hu.bme.mit.theta.solver.SolverFactory -class MilanoLDGTraceCheckerStrategy( - private val trace: LDGTrace, +class MilanoASGTraceCheckerStrategy( + private val trace: ASGTrace, solverFactory: SolverFactory, init: Expr, logger: Logger, -) : AbstractLDGTraceCheckerStrategy(trace, solverFactory, init, logger) { +) : AbstractASGTraceCheckerStrategy(trace, solverFactory, init, logger) { override fun evaluateLoop(valuation: Valuation): ExprTraceStatus { for (variable in variables) { diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleASGTraceRefiner.kt similarity index 83% rename from subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt rename to subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleASGTraceRefiner.kt index 77062d71c5..aefb9135ed 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleLDGTraceRefiner.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/refinement/SingleASGTraceRefiner.kt @@ -16,9 +16,10 @@ package hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement import hu.bme.mit.theta.analysis.Prec +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTraceRefiner import hu.bme.mit.theta.analysis.algorithm.cegar.RefinerResult -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus @@ -30,15 +31,15 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.solver.SolverFactory -class SingleLDGTraceRefiner( - private val strategy: LDGTraceCheckerStrategy, +class SingleASGTraceRefiner( + private val strategy: ASGTraceCheckerStrategy, private val solverFactory: SolverFactory, private val refiner: JoiningPrecRefiner, private val logger: Logger, private val init: Expr = True(), -) : LDGTraceRefiner { +) : ASGTraceRefiner { - override fun refine(witness: LDG, prec: P): RefinerResult> { + override fun refine(witness: ASG, prec: P): RefinerResult> { val ldgTraces = witness.traces check(ldgTraces.isNotEmpty()) { "${this.javaClass.simpleName} needs at least one trace!" } val ldgTrace = ldgTraces[0] diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java index 87326268f1..78289cc1e0 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/unit/UnitInitFunc.java @@ -15,13 +15,12 @@ */ package hu.bme.mit.theta.analysis.unit; +import static com.google.common.base.Preconditions.checkNotNull; + import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.analysis.InitFunc; - import java.util.Collection; -import static com.google.common.base.Preconditions.checkNotNull; - public final class UnitInitFunc implements InitFunc { private static final UnitInitFunc INSTANCE = new UnitInitFunc(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt index 511efb266f..4ee2553a90 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/LDGVisualizer.kt @@ -15,10 +15,10 @@ */ package hu.bme.mit.theta.analysis.utils -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGEdge -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.common.visualization.* @@ -26,34 +26,34 @@ import hu.bme.mit.theta.common.visualization.Alignment.LEFT import hu.bme.mit.theta.common.visualization.Shape.RECTANGLE import java.awt.Color -class LdgVisualizer( +class AsgVisualizer( private val stateToString: (S) -> String, private val actionToString: (A) -> String, -) : ProofVisualizer> { +) : ProofVisualizer> { - private var traceNodes: MutableSet> = mutableSetOf() - private var traceEdges: MutableSet> = mutableSetOf() + private var traceNodes: MutableSet> = mutableSetOf() + private var traceEdges: MutableSet> = mutableSetOf() - override fun visualize(ldg: LDG): Graph { + override fun visualize(ASG: ASG): Graph { traceNodes = mutableSetOf() traceEdges = mutableSetOf() - return createVisualization(ldg) + return createVisualization(ASG) } - fun visualize(ldg: LDG, trace: LDGTrace): Graph { + fun visualize(ASG: ASG, trace: ASGTrace): Graph { traceEdges = mutableSetOf() traceEdges.addAll(trace.edges) traceNodes = mutableSetOf() trace.edges.map { it.source!! }.forEach(traceNodes::add) - return createVisualization(ldg) + return createVisualization(ASG) } - private fun createVisualization(ldg: LDG): Graph { + private fun createVisualization(ASG: ASG): Graph { val graph = Graph(LDG_ID, LDG_LABEL) - val traversed: MutableSet> = mutableSetOf() + val traversed: MutableSet> = mutableSetOf() - for (initNode in ldg.initNodes) { + for (initNode in ASG.initNodes) { traverse(graph, initNode, traversed) val nAttributes = NodeAttributes.builder() @@ -78,8 +78,8 @@ class LdgVisualizer( private fun traverse( graph: Graph, - node: LDGNode, - traversed: MutableSet>, + node: ASGNode, + traversed: MutableSet>, ) { if (traversed.contains(node)) { return diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGAbstractorCheckingTest.java similarity index 91% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java rename to subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGAbstractorCheckingTest.java index 4c6acec5e1..1877a54da8 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGAbstractorCheckingTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGAbstractorCheckingTest.java @@ -19,10 +19,10 @@ import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.asg.ASG; import hu.bme.mit.theta.analysis.algorithm.cegar.AbstractorResult; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor; import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; import hu.bme.mit.theta.analysis.expl.ExplPrec; import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.analysis.expl.ExplStatePredicate; @@ -59,7 +59,7 @@ import org.junit.runners.Parameterized; @RunWith(Parameterized.class) -public class LDGAbstractorCheckingTest { +public class ASGAbstractorCheckingTest { @Parameterized.Parameter public String fileName; @@ -80,7 +80,6 @@ public static Collection data() { {"counter6to7.xsts", "x_eq_7.prop", "", true}, {"counter6to7.xsts", "x_eq_6.prop", "", true}, {"infinitehavoc.xsts", "x_eq_7.prop", "", true}, - {"colors.xsts", "currentColor_eq_Green.prop", "", true}, {"counter5.xsts", "x_eq_5.prop", "", true}, {"forever5.xsts", "x_eq_5.prop", "", true}, {"counter6to7.xsts", "x_eq_5.prop", "", false}, @@ -116,14 +115,14 @@ private void testWithXsts() throws IOException { new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); final ExplPrec precision = new XstsAllVarsInitPrec().createExpl(xsts); var abstractor = - new LDGAbstractor<>( + new ASGAbstractor<>( analysis, lts, target, LoopcheckerSearchStrategy.Companion.getDefault(), new ConsoleLogger(Logger.Level.DETAIL)); - LDG, XstsAction> ldg = new LDG<>(target); - AbstractorResult result = abstractor.check(ldg, precision); + ASG, XstsAction> ASG = new ASG<>(target); + AbstractorResult result = abstractor.check(ASG, precision); Assert.assertEquals(isLassoPresent, result.isUnsafe()); } @@ -142,15 +141,15 @@ private void testWithCfa() throws IOException { cfaState -> cfaState.getLoc().getName().equals(acceptingLocationName); AcceptancePredicate, CfaAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); - LDGAbstractor, CfaAction, CfaPrec> abstractor = - new LDGAbstractor<>( + ASGAbstractor, CfaAction, CfaPrec> abstractor = + new ASGAbstractor<>( analysis, lts, target, LoopcheckerSearchStrategy.Companion.getDefault(), new ConsoleLogger(Logger.Level.DETAIL)); - LDG, CfaAction> ldg = new LDG<>(target); - AbstractorResult result = abstractor.check(ldg, precision); + ASG, CfaAction> ASG = new ASG<>(target); + AbstractorResult result = abstractor.check(ASG, precision); Assert.assertEquals(isLassoPresent, result.isUnsafe()); } } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java similarity index 88% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGCegarVerifierTest.java rename to subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java index 8e8a4929be..e849ebead7 100644 --- 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/ASGCegarVerifierTest.java @@ -19,20 +19,21 @@ import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; +import hu.bme.mit.theta.analysis.algorithm.asg.ASG; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker; import hu.bme.mit.theta.analysis.algorithm.cegar.Refiner; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor; import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleLDGTraceRefiner; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleASGTraceRefiner; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec; import hu.bme.mit.theta.analysis.pred.*; import hu.bme.mit.theta.analysis.stmtoptimizer.DefaultStmtOptimizer; -import hu.bme.mit.theta.analysis.utils.LdgVisualizer; +import hu.bme.mit.theta.analysis.utils.AsgVisualizer; import hu.bme.mit.theta.cfa.CFA; import hu.bme.mit.theta.cfa.analysis.CfaAction; import hu.bme.mit.theta.cfa.analysis.CfaAnalysis; @@ -68,7 +69,7 @@ import org.junit.runners.Parameterized; @RunWith(Parameterized.class) -public class LDGCegarVerifierTest { +public class ASGCegarVerifierTest { private static Solver abstractionSolver; private static ItpSolver itpSolver; @@ -140,7 +141,7 @@ private void testWithXsts() throws IOException { new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp()); var abstractor = - new LDGAbstractor<>( + new ASGAbstractor<>( analysis, lts, target, @@ -148,11 +149,11 @@ private void testWithXsts() throws IOException { logger); final Refiner< PredPrec, - LDG, XstsAction>, - LDGTrace, XstsAction>> + ASG, XstsAction>, + ASGTrace, XstsAction>> refiner = - new SingleLDGTraceRefiner<>( - LDGTraceCheckerStrategy.Companion.getDefault(), + new SingleASGTraceRefiner<>( + ASGTraceCheckerStrategy.Companion.getDefault(), solverFactory, JoiningPrecRefiner.create( new ItpRefToPredPrec(ExprSplitters.atoms())), @@ -160,14 +161,14 @@ private void testWithXsts() throws IOException { xsts.getInitFormula()); final CegarChecker< PredPrec, - LDG, XstsAction>, - LDGTrace, XstsAction>> + ASG, XstsAction>, + ASGTrace, XstsAction>> verifier = CegarChecker.create( abstractor, refiner, logger, - new LdgVisualizer<>(Objects::toString, Objects::toString)); + new AsgVisualizer<>(Objects::toString, Objects::toString)); final PredPrec precision = PredPrec.of(); var result = verifier.check(precision); @@ -195,7 +196,7 @@ private void testWithCfa() throws IOException { final RefutationToGlobalCfaPrec cfaRefToPrec = new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc()); var abstractor = - new LDGAbstractor<>( + new ASGAbstractor<>( analysis, lts, target, @@ -203,25 +204,25 @@ private void testWithCfa() throws IOException { logger); final Refiner< CfaPrec, - LDG, CfaAction>, - LDGTrace, CfaAction>> + ASG, CfaAction>, + ASGTrace, CfaAction>> refiner = - new SingleLDGTraceRefiner<>( - LDGTraceCheckerStrategy.Companion.getDefault(), + new SingleASGTraceRefiner<>( + ASGTraceCheckerStrategy.Companion.getDefault(), solverFactory, JoiningPrecRefiner.create(cfaRefToPrec), logger, True()); final CegarChecker< CfaPrec, - LDG, CfaAction>, - LDGTrace, CfaAction>> + ASG, CfaAction>, + ASGTrace, CfaAction>> verifier = CegarChecker.create( abstractor, refiner, logger, - new LdgVisualizer<>(Objects::toString, Objects::toString)); + new AsgVisualizer<>(Objects::toString, Objects::toString)); final GlobalCfaPrec prec = GlobalCfaPrec.create(PredPrec.of()); var res = verifier.check(prec); diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java similarity index 88% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java rename to subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java index dfab147cc9..1b6eef1734 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/LDGTraceCheckerTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java @@ -17,10 +17,11 @@ import hu.bme.mit.theta.analysis.Analysis; import hu.bme.mit.theta.analysis.LTS; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor; +import hu.bme.mit.theta.analysis.algorithm.asg.ASG; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor; import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy; +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus; import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; @@ -46,7 +47,7 @@ import org.junit.Assert; import org.junit.Test; -public class LDGTraceCheckerTest { +public class ASGTraceCheckerTest { @Test public void testWithCounter3() throws IOException { XSTS xsts; @@ -72,19 +73,19 @@ public void testWithCounter3() throws IOException { new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); final PredPrec precision = PredPrec.of(); final Logger logger = new ConsoleLogger(Logger.Level.DETAIL); - final LDGAbstractor, XstsAction, PredPrec> abstractor = - new LDGAbstractor<>( + final ASGAbstractor, XstsAction, PredPrec> abstractor = + new ASGAbstractor<>( analysis, lts, target, LoopcheckerSearchStrategy.Companion.getDefault(), logger); - LDG, XstsAction> ldg = new LDG<>(target); - abstractor.check(ldg, precision); - LDGTrace, XstsAction> trace = ldg.getTraces().iterator().next(); + ASG, XstsAction> ASG = new ASG<>(target); + abstractor.check(ASG, precision); + ASGTrace, XstsAction> trace = ASG.getTraces().iterator().next(); ExprTraceStatus status = - LDGTraceCheckerStrategy.Companion.getDefault() + ASGTraceCheckerStrategy.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/ASGTraceTest.java similarity index 72% rename from subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java rename to subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/ASGTraceTest.java index f059bccaac..0abf99ff82 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/LDGTraceTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ldg/ASGTraceTest.java @@ -17,7 +17,9 @@ import static org.mockito.Mockito.mock; -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGEdge; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGNode; +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace; import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import java.util.List; @@ -27,22 +29,22 @@ import org.mockito.junit.MockitoJUnitRunner; @RunWith(MockitoJUnitRunner.class) -public class LDGTraceTest { +public class ASGTraceTest { @Test public void testSimpleLasso() { - LDGNode initNode = new LDGNode<>(mock(ExprState.class), false); - LDGNode hondaNode = new LDGNode<>(mock(ExprState.class), true); - LDGNode loopNode = new LDGNode<>(mock(ExprState.class), false); + ASGNode initNode = new ASGNode<>(mock(ExprState.class), false); + ASGNode hondaNode = new ASGNode<>(mock(ExprState.class), true); + ASGNode loopNode = new ASGNode<>(mock(ExprState.class), false); Assert.assertNotEquals(initNode, hondaNode); Assert.assertNotEquals(initNode, loopNode); Assert.assertNotEquals(loopNode, hondaNode); - LDGEdge firstEdge = - new LDGEdge<>(initNode, hondaNode, mock(ExprAction.class), false); - LDGEdge secondEdge = - new LDGEdge<>(hondaNode, loopNode, mock(ExprAction.class), false); - LDGEdge thirdEdge = - new LDGEdge<>(loopNode, hondaNode, mock(ExprAction.class), false); + ASGEdge firstEdge = + new ASGEdge<>(initNode, hondaNode, mock(ExprAction.class), false); + ASGEdge secondEdge = + new ASGEdge<>(hondaNode, loopNode, mock(ExprAction.class), false); + ASGEdge thirdEdge = + new ASGEdge<>(loopNode, hondaNode, mock(ExprAction.class), false); initNode.addOutEdge(firstEdge); hondaNode.addInEdge(firstEdge); hondaNode.addOutEdge(secondEdge); @@ -50,8 +52,8 @@ public void testSimpleLasso() { loopNode.addOutEdge(thirdEdge); hondaNode.addInEdge(thirdEdge); - LDGTrace trace = - new LDGTrace<>(List.of(firstEdge, secondEdge, thirdEdge), hondaNode); + ASGTrace trace = + new ASGTrace<>(List.of(firstEdge, secondEdge, thirdEdge), hondaNode); Assert.assertEquals(1, trace.getTail().size()); Assert.assertEquals(2, trace.getLoop().size()); diff --git a/subprojects/common/ltl-cli/src/main/kotlin/common/ltl/cli/LtlCliOptions.kt b/subprojects/common/ltl-cli/src/main/kotlin/common/ltl/cli/LtlCliOptions.kt index 2a0ab0b3b0..2b68427ec9 100644 --- a/subprojects/common/ltl-cli/src/main/kotlin/common/ltl/cli/LtlCliOptions.kt +++ b/subprojects/common/ltl-cli/src/main/kotlin/common/ltl/cli/LtlCliOptions.kt @@ -21,9 +21,9 @@ import com.github.ajalt.clikt.parameters.options.option import com.github.ajalt.clikt.parameters.options.required import com.github.ajalt.clikt.parameters.types.enum import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy -class LtlCliOptions : +open class LtlCliOptions : OptionGroup(name = "LTL options", help = "Options related to LTL property checking") { val ltlExpression by option(help = "LTL expression to check").required() val ltl2BuchiCommand by @@ -39,6 +39,6 @@ class LtlCliOptions : .default(LoopcheckerSearchStrategy.GDFS) val refinerStrategy by option(help = "Which strategy to use for search") - .enum() - .default(LDGTraceCheckerStrategy.MILANO) + .enum() + .default(ASGTraceCheckerStrategy.MILANO) } diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt index d4e5df5b8a..3820cc1876 100644 --- a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/cfa/buchi/hoa/BuchiBuilder.kt @@ -21,12 +21,12 @@ import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.type.Expr import hu.bme.mit.theta.core.type.booltype.BoolExprs import hu.bme.mit.theta.core.type.booltype.BoolType +import java.util.function.Consumer import jhoafparser.ast.AtomAcceptance import jhoafparser.ast.AtomLabel import jhoafparser.ast.BooleanExpression import jhoafparser.consumer.HOAConsumer import jhoafparser.consumer.HOAConsumerException -import java.util.function.Consumer class BuchiBuilder internal constructor( diff --git a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt index d1d4870080..bfe0c7cf79 100644 --- a/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt +++ b/subprojects/common/ltl/src/main/kotlin/hu/bme/mit/theta/common/ltl/LtlChecker.kt @@ -20,14 +20,14 @@ import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.algorithm.SafetyChecker import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.cegar.CegarChecker import hu.bme.mit.theta.analysis.algorithm.loopchecker.AcceptancePredicate -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LDGAbstractor +import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.ASGAbstractor import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleLDGTraceRefiner +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.SingleASGTraceRefiner import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.StmtAction import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation @@ -36,6 +36,7 @@ import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec import hu.bme.mit.theta.analysis.multi.MultiAnalysisSide import hu.bme.mit.theta.analysis.multi.MultiPrec import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.analysis.multi.NextSideFunctions.Alternating import hu.bme.mit.theta.analysis.multi.RefToMultiPrec import hu.bme.mit.theta.analysis.multi.builder.stmt.StmtMultiBuilder import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState @@ -43,7 +44,7 @@ import hu.bme.mit.theta.analysis.multi.stmt.StmtMultiAction import hu.bme.mit.theta.analysis.unit.UnitInitFunc import hu.bme.mit.theta.analysis.unit.UnitPrec import hu.bme.mit.theta.analysis.unit.UnitState -import hu.bme.mit.theta.analysis.utils.LdgVisualizer +import hu.bme.mit.theta.analysis.utils.AsgVisualizer import hu.bme.mit.theta.cfa.CFA import hu.bme.mit.theta.cfa.analysis.* import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts @@ -75,21 +76,29 @@ class LtlChecker< solverFactory: SolverFactory, logger: Logger, searchStrategy: LoopcheckerSearchStrategy, - refinerStrategy: LDGTraceCheckerStrategy, + refinerStrategy: ASGTraceCheckerStrategy, ltl2BuchiTransformer: Ltl2BuchiTransformer, variables: Collection>, initExpr: Expr = True(), + nextSideFunction: + NextSideFunctions.NextSideFunction< + ControlS, + CfaState, + DataS, + ExprMultiState, DataS>, + > = + Alternating(), ) : SafetyChecker< - LDG, DataS>, StmtMultiAction>, - LDGTrace, DataS>, StmtMultiAction>, + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, MultiPrec, DataP>, > { - private val checker: + val checker: CegarChecker< MultiPrec, DataP>, - LDG, DataS>, StmtMultiAction>, - LDGTrace, DataS>, StmtMultiAction>, + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, > init { @@ -108,12 +117,12 @@ class LtlChecker< val product = StmtMultiBuilder(multiSide, lts) .addRightSide(buchiSide, CfaSbeLts.getInstance()) - .build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + .build(nextSideFunction, dataAnalysis.initFunc) val buchiRefToPrec = RefutationToGlobalCfaPrec(dataRefToPrec, buchiAutomaton.initLoc) val multiRefToPrec = RefToMultiPrec(refToPrec, buchiRefToPrec, dataRefToPrec) val multiAnalysis = product.side.analysis val abstractor = - LDGAbstractor( + ASGAbstractor( multiAnalysis, product.lts, buchiPredicate(buchiAutomaton), @@ -121,12 +130,12 @@ class LtlChecker< logger, ) val refiner: - SingleLDGTraceRefiner< + SingleASGTraceRefiner< ExprMultiState, DataS>, StmtMultiAction, MultiPrec, DataP>, > = - SingleLDGTraceRefiner( + SingleASGTraceRefiner( refinerStrategy, solverFactory, JoiningPrecRefiner.create(multiRefToPrec), @@ -134,12 +143,12 @@ class LtlChecker< initExpr, ) val visualizer = - LdgVisualizer< + AsgVisualizer< ExprMultiState, DataS>, StmtMultiAction, >( { it.toString() }, - { it.toString() }, + { "" }, ) checker = CegarChecker.create(abstractor, refiner, logger, visualizer) } @@ -160,8 +169,8 @@ class LtlChecker< override fun check( input: MultiPrec, DataP> ): SafetyResult< - LDG, DataS>, StmtMultiAction>, - LDGTrace, DataS>, StmtMultiAction>, + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, > { return checker.check(input) } @@ -170,8 +179,8 @@ class LtlChecker< prec: P, dataPrec: DataP, ): SafetyResult< - LDG, DataS>, StmtMultiAction>, - LDGTrace, DataS>, StmtMultiAction>, + ASG, DataS>, StmtMultiAction>, + ASGTrace, DataS>, StmtMultiAction>, > { return check(MultiPrec(prec, GlobalCfaPrec.create(dataPrec), dataPrec)) } diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt index d00d91bf49..b64a468142 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaExpl.kt @@ -16,10 +16,11 @@ package hu.bme.mit.theta.common.ltl import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy import hu.bme.mit.theta.analysis.expl.ExplAnalysis import hu.bme.mit.theta.analysis.expl.ExplPrec import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec +import hu.bme.mit.theta.analysis.multi.NextSideFunctions import hu.bme.mit.theta.cfa.CFA import hu.bme.mit.theta.cfa.analysis.CfaPrec import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder @@ -33,12 +34,12 @@ import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.solver.Solver import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithCfaExpl( @@ -98,9 +99,10 @@ class LtlCheckTestWithCfaExpl( itpSolverFactory, logger, LoopcheckerSearchStrategy.GDFS, - LDGTraceCheckerStrategy.MILANO, + ASGTraceCheckerStrategy.MILANO, Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), variables, + nextSideFunction = NextSideFunctions.Alternating(), ) Assert.assertEquals(result, checker.check(initPrec, dataInitPrec).isSafe) diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt index 8c95a84921..95ce8b6652 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithCfaPred.kt @@ -16,8 +16,9 @@ package hu.bme.mit.theta.common.ltl import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.multi.NextSideFunctions import hu.bme.mit.theta.analysis.pred.* import hu.bme.mit.theta.cfa.CFA import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder @@ -30,12 +31,12 @@ import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.solver.Solver import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithCfaPred( @@ -43,7 +44,7 @@ class LtlCheckTestWithCfaPred( private val ltlExpr: String, private val result: Boolean, private val searchStrategy: LoopcheckerSearchStrategy, - private val refinerStrategy: LDGTraceCheckerStrategy, + private val refinerStrategy: ASGTraceCheckerStrategy, ) { private val itpSolverFactory = Z3LegacySolverFactory.getInstance() @@ -76,7 +77,7 @@ class LtlCheckTestWithCfaPred( @Parameterized.Parameters(name = "{3}-{4}: {0}") fun params() = listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> - listOf(LDGTraceCheckerStrategy.MILANO, LDGTraceCheckerStrategy.BOUNDED_UNROLLING).flatMap { + listOf(ASGTraceCheckerStrategy.MILANO, ASGTraceCheckerStrategy.BOUNDED_UNROLLING).flatMap { ref -> data().map { arrayOf(*it, search, ref) } } @@ -124,6 +125,7 @@ class LtlCheckTestWithCfaPred( refinerStrategy, Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), variables, + nextSideFunction = NextSideFunctions.Alternating(), ) Assert.assertEquals(result, checker.check(configBuilder.createInitPrec(), dataInitPrec).isSafe) diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt index f55c04544b..28508c1288 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsExpl.kt @@ -16,9 +16,10 @@ package hu.bme.mit.theta.common.ltl import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy import hu.bme.mit.theta.analysis.expl.ExplPrec import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.multi.NextSideFunctions import hu.bme.mit.theta.analysis.unit.UnitPrec import hu.bme.mit.theta.analysis.unit.UnitState import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf @@ -32,12 +33,12 @@ import hu.bme.mit.theta.xsts.analysis.XstsState import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.dsl.XstsDslManager import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithXstsExpl( @@ -103,10 +104,11 @@ class LtlCheckTestWithXstsExpl( solverFactory, logger, LoopcheckerSearchStrategy.GDFS, - LDGTraceCheckerStrategy.MILANO, + ASGTraceCheckerStrategy.MILANO, Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), xsts.vars, xsts.initFormula, + NextSideFunctions.Alternating(), ) val checkResult = checker.check(initPrec, initPrec) diff --git a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt index 7ce8759ee6..1a9177f01e 100644 --- a/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt +++ b/subprojects/common/ltl/src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt @@ -16,7 +16,8 @@ package hu.bme.mit.theta.common.ltl import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy -import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.LDGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy +import hu.bme.mit.theta.analysis.multi.MultiSide import hu.bme.mit.theta.analysis.pred.ExprSplitters import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf @@ -29,12 +30,12 @@ import hu.bme.mit.theta.xsts.XSTS import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.dsl.XstsDslManager import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass +import java.io.FileInputStream import junit.framework.TestCase.fail import org.junit.Assert import org.junit.Test import org.junit.runner.RunWith import org.junit.runners.Parameterized -import java.io.FileInputStream @RunWith(Parameterized::class) class LtlCheckTestWithXstsPred( @@ -42,7 +43,7 @@ class LtlCheckTestWithXstsPred( private val ltlExpr: String, private val result: Boolean, private val searchStrategy: LoopcheckerSearchStrategy, - private val refinerStrategy: LDGTraceCheckerStrategy, + private val refinerStrategy: ASGTraceCheckerStrategy, ) { private val itpSolverFactory = Z3LegacySolverFactory.getInstance() @@ -60,7 +61,7 @@ class LtlCheckTestWithXstsPred( arrayOf("counter6to7", "G(x=1)", false), arrayOf("counter6to7", "G(x=7)", false), arrayOf("counter6to7", "G F(x=7)", true), - // arrayOf("counter50", "G(x<49)", false), + // arrayOf("counter50", "G(x<49)", false), arrayOf( "trafficlight_v2", "G(LightCommands_displayRed -> X(not LightCommands_displayGreen))", @@ -68,7 +69,7 @@ class LtlCheckTestWithXstsPred( ), arrayOf( "trafficlight_v2", - "G((normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle) -> X(normal = Normal.Green))", + "G((main_region = Main_region.Normal and normal = Normal.Red and (not PoliceInterrupt_police) and Control_toggle and (X(not PoliceInterrupt_police))) -> X(X(normal = Normal.Green)))", true, ), arrayOf( @@ -109,7 +110,7 @@ class LtlCheckTestWithXstsPred( @Parameterized.Parameters(name = "{3}-{4}: {0}") fun params() = listOf(LoopcheckerSearchStrategy.GDFS, LoopcheckerSearchStrategy.NDFS).flatMap { search -> - LDGTraceCheckerStrategy.entries.flatMap { ref -> data().map { arrayOf(*it, search, ref) } } + ASGTraceCheckerStrategy.entries.flatMap { ref -> data().map { arrayOf(*it, search, ref) } } } } @@ -149,8 +150,12 @@ class LtlCheckTestWithXstsPred( Ltl2BuchiThroughHoaf(Ltl2HoafFromDir("src/test/resources/hoa"), logger), variables, xsts.initFormula, - ) + ) { + if (it.sourceSide == MultiSide.RIGHT || it.leftState.lastActionWasEnv()) MultiSide.LEFT + else MultiSide.RIGHT + } - Assert.assertEquals(result, checker.check(initPrec, initPrec).isSafe) + val safetyResult = checker.check(initPrec, initPrec) + Assert.assertEquals(result, safetyResult.isSafe) } } diff --git a/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa new file mode 100644 index 0000000000..4f293da548 --- /dev/null +++ b/subprojects/common/ltl/src/test/resources/hoa/%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa @@ -0,0 +1,20 @@ +HOA: v1 +tool: "owl ltl2ngba" "21.0" +name: "Automaton for F(((ap0) & (ap1) & (ap2) & (ap3) & (X(ap4)) & (X(X(!ap5)))))" +owlArgs: "ltl2ngba" "-f" "!(G ((ap0 & ap1 & ap2 & ap3 & (X ap4)) -> X (X ap5)))" "-o" "%21%28G+%28%28ap0+%26+ap1+%26+ap2+%26+ap3+%26+%28X+ap4%29%29+-%3E+X+%28X+ap5%29%29%29.hoa" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-acc no-univ-branch +AP: 6 "ap0" "ap1" "ap2" "ap3" "ap4" "ap5" +--BODY-- +State: 0 +[t] 0 +[0 & 1 & 2 & 3] 1 +State: 1 +[4] 2 +State: 2 +[!5] 3 +State: 3 +[t] 3 {0} +--END-- diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt index 0e22456a0d..1408a365aa 100644 --- a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt +++ b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt @@ -41,132 +41,150 @@ import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory import hu.bme.mit.theta.xsts.XSTS import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.dsl.XstsDslManager -import org.junit.Test -import org.junit.jupiter.api.Assertions.assertEquals -import org.junit.jupiter.api.Assertions.assertTrue import java.io.FileInputStream import java.io.IOException import java.io.SequenceInputStream +import org.junit.Test +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue class MultiAlternatingTest { - val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP) - val solver: Solver = Z3LegacySolverFactory.getInstance().createSolver() - - @Test - fun testExplPrec() { - var xsts: XSTS - try { - SequenceInputStream( - FileInputStream("src/test/resources/xsts/incrementor.xsts"), - FileInputStream("src/test/resources/xsts/xneq7.prop") - ).use { inputStream -> - xsts = XstsDslManager.createXsts(inputStream) - } - } catch (e: IOException) { - throw RuntimeException(e) - } - - val xstsConfigBuilder = XstsConfigBuilder( - XstsConfigBuilder.Domain.EXPL, - XstsConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance(), - Z3LegacySolverFactory.getInstance() - ) - val xstsExplBuilder = xstsConfigBuilder.ExplStrategy(xsts) - - val variables = xsts.vars + val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP) + val solver: Solver = Z3LegacySolverFactory.getInstance().createSolver() - var originalCfa: CFA - FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> - originalCfa = CfaDslManager.createCfa(inputStream) - } - val cfa = originalCfa.copyWithReplacingVars(variables.associateBy { it.name }) - val cfaConfigBuilder = CfaConfigBuilder( - CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance() + @Test + fun testExplPrec() { + var xsts: XSTS + try { + SequenceInputStream( + FileInputStream("src/test/resources/xsts/incrementor.xsts"), + FileInputStream("src/test/resources/xsts/xneq7.prop"), ) - cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) - val cfaExplBuilder = cfaConfigBuilder.ExplStrategy(cfa) - - val dataAnalysis = xstsExplBuilder.dataAnalysis - val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) - val dataInitPrec = ExplPrec.of(variables) - val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) - val product = StmtMultiBuilder(cfaExplBuilder.multiSide, cfaExplBuilder.lts).addRightSide( - xstsExplBuilder.multiSide, xstsExplBuilder.lts - ).build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) - val prop = Not(xsts.prop) - val dataPredicate = ExplStatePredicate(prop, solver) - val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( - product, prop, - MultiStatePredicate(dataPredicate), - cfaRefToPrec, ItpRefToExplPrec(), ItpRefToExplPrec(), cfaInitPrec, - dataInitPrec, dataInitPrec, Z3LegacySolverFactory.getInstance(), logger - ) - val result = multiConfigBuilder.build().check() - - assertTrue(result.isUnsafe) - assertEquals(8, result.asUnsafe().cex.length()) + .use { inputStream -> xsts = XstsDslManager.createXsts(inputStream) } + } catch (e: IOException) { + throw RuntimeException(e) } - @Test - fun testPredPrec() { - var xsts: XSTS - try { - SequenceInputStream( - FileInputStream("src/test/resources/xsts/incrementor.xsts"), - FileInputStream("src/test/resources/xsts/xneq7.prop") - ).use { inputStream -> - xsts = XstsDslManager.createXsts(inputStream) - } - } catch (e: IOException) { - throw RuntimeException(e) - } - - val xstsConfigBuilder = XstsConfigBuilder( - XstsConfigBuilder.Domain.PRED_BOOL, - XstsConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance(), - Z3LegacySolverFactory.getInstance() - ) - val xstsPredBuilder = xstsConfigBuilder.PredStrategy(xsts) - val dataAnalysis = xstsPredBuilder.dataAnalysis - - var cfa: CFA - FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> - cfa = CfaDslManager.createCfa(inputStream) - } - cfa = cfa.copyWithReplacingVars(xsts.vars.associateBy { it.name }) - val cfaConfigBuilder = CfaConfigBuilder( - CfaConfigBuilder.Domain.PRED_BOOL, - CfaConfigBuilder.Refinement.SEQ_ITP, - Z3LegacySolverFactory.getInstance() - ) - cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) - val cfaPredBuilder = cfaConfigBuilder.PredStrategy(cfa) - val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) - val dataInitPrec = PredPrec.of() - val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val xstsConfigBuilder = + XstsConfigBuilder( + XstsConfigBuilder.Domain.EXPL, + XstsConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + Z3LegacySolverFactory.getInstance(), + ) + val xstsExplBuilder = xstsConfigBuilder.ExplStrategy(xsts) - val product = StmtMultiBuilder(cfaPredBuilder.multiSide, cfaPredBuilder.lts) - .addRightSide(xstsPredBuilder.multiSide, xstsPredBuilder.lts) - .build( - NextSideFunctions.Alternating(), - dataAnalysis.initFunc - ) - val prop = Not(xsts.prop) - val dataPredicate = ExprStatePredicate(prop, solver) + val variables = xsts.vars - val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( - product, prop, - MultiStatePredicate(dataPredicate), - cfaRefToPrec, ItpRefToPredPrec(ExprSplitters.atoms()), ItpRefToPredPrec(ExprSplitters.atoms()), cfaInitPrec, - dataInitPrec, dataInitPrec, Z3LegacySolverFactory.getInstance(), logger + var originalCfa: CFA + FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> + originalCfa = CfaDslManager.createCfa(inputStream) + } + val cfa = originalCfa.copyWithReplacingVars(variables.associateBy { it.name }) + val cfaConfigBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.EXPL, + CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + ) + cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfaExplBuilder = cfaConfigBuilder.ExplStrategy(cfa) + + val dataAnalysis = xstsExplBuilder.dataAnalysis + val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) + val dataInitPrec = ExplPrec.of(variables) + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val product = + StmtMultiBuilder(cfaExplBuilder.multiSide, cfaExplBuilder.lts) + .addRightSide(xstsExplBuilder.multiSide, xstsExplBuilder.lts) + .build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val prop = Not(xsts.prop) + val dataPredicate = ExplStatePredicate(prop, solver) + val multiConfigBuilder = + StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( + product, + prop, + MultiStatePredicate(dataPredicate), + cfaRefToPrec, + ItpRefToExplPrec(), + ItpRefToExplPrec(), + cfaInitPrec, + dataInitPrec, + dataInitPrec, + Z3LegacySolverFactory.getInstance(), + logger, + ) + val result = multiConfigBuilder.build().check() + + assertTrue(result.isUnsafe) + assertEquals(8, result.asUnsafe().cex.length()) + } + + @Test + fun testPredPrec() { + var xsts: XSTS + try { + SequenceInputStream( + FileInputStream("src/test/resources/xsts/incrementor.xsts"), + FileInputStream("src/test/resources/xsts/xneq7.prop"), ) - val result = multiConfigBuilder.build().check() - - assertTrue(result.isUnsafe) + .use { inputStream -> xsts = XstsDslManager.createXsts(inputStream) } + } catch (e: IOException) { + throw RuntimeException(e) } -} \ No newline at end of file + val xstsConfigBuilder = + XstsConfigBuilder( + XstsConfigBuilder.Domain.PRED_BOOL, + XstsConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + Z3LegacySolverFactory.getInstance(), + ) + val xstsPredBuilder = xstsConfigBuilder.PredStrategy(xsts) + val dataAnalysis = xstsPredBuilder.dataAnalysis + + var cfa: CFA + FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> + cfa = CfaDslManager.createCfa(inputStream) + } + cfa = cfa.copyWithReplacingVars(xsts.vars.associateBy { it.name }) + val cfaConfigBuilder = + CfaConfigBuilder( + CfaConfigBuilder.Domain.PRED_BOOL, + CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + ) + cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfaPredBuilder = cfaConfigBuilder.PredStrategy(cfa) + val cfaRefToPrec = + RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) + val dataInitPrec = PredPrec.of() + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + + val product = + StmtMultiBuilder(cfaPredBuilder.multiSide, cfaPredBuilder.lts) + .addRightSide(xstsPredBuilder.multiSide, xstsPredBuilder.lts) + .build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val prop = Not(xsts.prop) + val dataPredicate = ExprStatePredicate(prop, solver) + + val multiConfigBuilder = + StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( + product, + prop, + MultiStatePredicate(dataPredicate), + cfaRefToPrec, + ItpRefToPredPrec(ExprSplitters.atoms()), + ItpRefToPredPrec(ExprSplitters.atoms()), + cfaInitPrec, + dataInitPrec, + dataInitPrec, + Z3LegacySolverFactory.getInstance(), + logger, + ) + val result = multiConfigBuilder.build().check() + + assertTrue(result.isUnsafe) + } +} diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt index 579deaab67..e8afeb3081 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/util/XstsCombineExtractUtils.kt @@ -22,9 +22,7 @@ import hu.bme.mit.theta.analysis.unit.UnitState import hu.bme.mit.theta.xsts.analysis.XstsState fun xstsCombineStates(xstsState: XstsState, dataState: S): XstsState { - // TODO here initialized should be xstsState.isInitialized, but that fails - // LtlCheckTestWithXstsPred - return XstsState.of(dataState, xstsState.lastActionWasEnv(), true) + return XstsState.of(dataState, xstsState.lastActionWasEnv(), xstsState.isInitialized) } fun xstsExtractControlState(xstsState: XstsState<*>): XstsState { diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt index 96c18df436..49aa4cffce 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliLtlCegar.kt @@ -17,25 +17,82 @@ package hu.bme.mit.theta.xsts.cli import com.github.ajalt.clikt.parameters.groups.provideDelegate import com.github.ajalt.clikt.parameters.options.default +import com.github.ajalt.clikt.parameters.options.help import com.github.ajalt.clikt.parameters.options.option import com.github.ajalt.clikt.parameters.types.enum import com.google.common.base.Stopwatch import hu.bme.mit.theta.analysis.algorithm.SafetyResult +import hu.bme.mit.theta.analysis.algorithm.asg.ASG +import hu.bme.mit.theta.analysis.algorithm.asg.ASGTrace import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics -import hu.bme.mit.theta.analysis.algorithm.loopchecker.LDGTrace -import hu.bme.mit.theta.analysis.algorithm.loopchecker.ldg.LDG +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.multi.MultiSide +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.analysis.multi.NextSideFunctions.Alternating +import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState +import hu.bme.mit.theta.analysis.unit.UnitState +import hu.bme.mit.theta.cfa.analysis.CfaState import hu.bme.mit.theta.common.cfa.buchi.hoa.ExternalLtl2Hoaf import hu.bme.mit.theta.common.cfa.buchi.hoa.Ltl2BuchiThroughHoaf import hu.bme.mit.theta.common.ltl.LtlChecker import hu.bme.mit.theta.common.ltl.cli.LtlCliOptions import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.xsts.XSTS +import hu.bme.mit.theta.xsts.analysis.XstsState import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder.* import hu.bme.mit.theta.xsts.passes.XstsNormalizerPass import java.util.concurrent.TimeUnit import kotlin.system.exitProcess +private typealias NSF = + NextSideFunctions.NextSideFunction< + XstsState, + CfaState, + D, + ExprMultiState, CfaState, D>, + > + +class XstsLtlCliOptions() : LtlCliOptions() { + enum class EnvtranSeparation() { + COMBINED { + + override fun getNextsideFunction(): + NextSideFunctions.NextSideFunction< + XstsState, + CfaState, + D, + ExprMultiState, CfaState, D>, + > { + return Alternating() + } + }, + SEPARATE { + + override fun getNextsideFunction(): NSF = NSF { ms -> + if (ms.sourceSide == MultiSide.RIGHT || ms.leftState.lastActionWasEnv()) MultiSide.LEFT + else MultiSide.RIGHT + } + }; + + abstract fun getNextsideFunction(): + NextSideFunctions.NextSideFunction< + XstsState, + CfaState, + D, + ExprMultiState, CfaState, D>, + > + } + + val envtranSeparation: EnvtranSeparation by + option( + help = + "Whether Buchi evaluation should happen between env and trans transitions or not (SEPARATED and COMBINED, respectively)" + ) + .enum() + .default(EnvtranSeparation.SEPARATE) +} + class XstsCliLtlCegar : XstsCliBaseCommand( name = "LTLCEGAR", @@ -50,10 +107,10 @@ class XstsCliLtlCegar : private val refinementSolver: String? by option(help = "Use a different solver for abstraction") private val abstractionSolver: String? by option(help = "Use a different solver for refinement") private val initprec: InitPrec by option().enum().default(InitPrec.EMPTY) - private val ltlOptions by LtlCliOptions() + private val ltlOptions by XstsLtlCliOptions() private fun printResult( - status: SafetyResult?, out LDGTrace<*, *>?>, + status: SafetyResult?, out ASGTrace<*, *>?>, xsts: XSTS, totalTimeMs: Long, ) { @@ -108,6 +165,7 @@ class XstsCliLtlCegar : Ltl2BuchiThroughHoaf(ExternalLtl2Hoaf(ltlOptions.ltl2BuchiCommand), logger), xsts.vars, xsts.initFormula, + ltlOptions.envtranSeparation.getNextsideFunction(), ) val sw = Stopwatch.createStarted() val result = checker.check(configBuilder.initPrec, configBuilder.initPrec) @@ -132,6 +190,7 @@ class XstsCliLtlCegar : Ltl2BuchiThroughHoaf(ExternalLtl2Hoaf(ltlOptions.ltl2BuchiCommand), logger), xsts.vars, xsts.initFormula, + NextSideFunctions.Alternating(), ) val sw = Stopwatch.createStarted() val result = checker.check(configBuilder.initPrec, configBuilder.initPrec)