From 84cfdccd8da09c8d23cd05173c2e0926db795c48 Mon Sep 17 00:00:00 2001 From: RipplB Date: Wed, 4 Dec 2024 11:43:44 +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. --- .../abstraction/NdfsSearchStrategy.kt | 12 +- .../util/VarCollectorStmtVisitor.kt | 5 + .../loopchecker/ASGCegarVerifierTest.java | 156 +++++++++++------- .../loopchecker/ASGTraceCheckerTest.java | 12 +- .../utils/VarCollectorStmtVisitorTest.kt | 74 +++++++++ .../common/ltl/LtlCheckTestWithXstsPred.kt | 1 - 6 files changed, 187 insertions(+), 73 deletions(-) create mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt 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 41b4c35cfe..52e58f653b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/abstraction/NdfsSearchStrategy.kt @@ -52,7 +52,7 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { if (targetNode.state.isBottom) { return emptyList() } - if (targetNode == seed) { + if (targetNode == seed && trace.isNotEmpty()) { return trace + edge } if (redNodes.contains(targetNode)) { @@ -83,9 +83,11 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { // Edge source can only be null artificially, and is only used when calling other search // strategies val accNode = if (targetNode.accepting) targetNode else edge.source!! - val redSearch: List> = - redSearch(accNode, edge, trace, mutableSetOf(), target, expand) - if (redSearch.isNotEmpty()) return setOf(ASGTrace(redSearch, accNode)) + for (outEdge in expand(edge.target)) { + val redSearch: List> = + redSearch(accNode, outEdge, trace + edge, mutableSetOf(), target, expand) + if (redSearch.isNotEmpty()) return setOf(ASGTrace(redSearch, accNode)) + } } if (blueNodes.contains(targetNode)) { return emptyList() @@ -94,7 +96,7 @@ object NdfsSearchStrategy : ILoopcheckerSearchStrategy { for (nextEdge in expand(targetNode)) { val blueSearch: Collection> = blueSearch(nextEdge, trace + edge, blueNodes, redNodes, target, expand) - if (!blueSearch.isEmpty()) return blueSearch + if (blueSearch.isNotEmpty()) return blueSearch } return emptyList() } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt index 5eadd022c7..29fb6add20 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/util/VarCollectorStmtVisitor.kt @@ -20,6 +20,11 @@ import hu.bme.mit.theta.core.stmt.* import hu.bme.mit.theta.core.type.Type import hu.bme.mit.theta.core.utils.ExprUtils +/** + * Collects vars from a statement to a fixpoint. Collects recursively only variables that are + * dependant on the input set on themselves. To collect all variables from a statement, use + * [hu.bme.mit.theta.core.utils.StmtUtils.getVars] instead. + */ class VarCollectorStmtVisitor : StmtVisitor>, Set>> { companion object { diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java index e849ebead7..394737ca4a 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGCegarVerifierTest.java @@ -140,39 +140,56 @@ private void testWithXsts() throws IOException { final AcceptancePredicate, XstsAction> target = new AcceptancePredicate<>(statePredicate::test, Unit.INSTANCE); logger.write(Logger.Level.MAINSTEP, "Verifying %s%n", xsts.getProp()); - var abstractor = - new ASGAbstractor<>( - analysis, - lts, - target, - LoopcheckerSearchStrategy.Companion.getDefault(), - logger); - final Refiner< - PredPrec, - ASG, XstsAction>, - ASGTrace, XstsAction>> - refiner = - new SingleASGTraceRefiner<>( - ASGTraceCheckerStrategy.Companion.getDefault(), - solverFactory, - JoiningPrecRefiner.create( - new ItpRefToPredPrec(ExprSplitters.atoms())), - logger, - xsts.getInitFormula()); - final CegarChecker< - PredPrec, - ASG, XstsAction>, - ASGTrace, XstsAction>> - verifier = - CegarChecker.create( - abstractor, - refiner, - logger, - new AsgVisualizer<>(Objects::toString, Objects::toString)); + LoopcheckerSearchStrategy.getEntries() + .forEach( + lStrat -> { + ASGTraceCheckerStrategy.getEntries() + .forEach( + strat -> { + var abstractor = + new ASGAbstractor<>( + analysis, lts, target, lStrat, + logger); + final Refiner< + PredPrec, + ASG< + XstsState, + XstsAction>, + ASGTrace< + XstsState, + XstsAction>> + refiner = + new SingleASGTraceRefiner<>( + strat, + solverFactory, + JoiningPrecRefiner.create( + new ItpRefToPredPrec( + ExprSplitters + .atoms())), + logger, + xsts.getInitFormula()); + final CegarChecker< + PredPrec, + ASG< + XstsState, + XstsAction>, + ASGTrace< + XstsState, + XstsAction>> + verifier = + CegarChecker.create( + abstractor, + refiner, + logger, + new AsgVisualizer<>( + Objects::toString, + Objects::toString)); - final PredPrec precision = PredPrec.of(); - var result = verifier.check(precision); - Assert.assertEquals(this.result, result.isUnsafe()); + final PredPrec precision = PredPrec.of(); + var result = verifier.check(precision); + Assert.assertEquals(this.result, result.isUnsafe()); + }); + }); } private void testWithCfa() throws IOException { @@ -195,37 +212,50 @@ private void testWithCfa() throws IOException { new ItpRefToPredPrec(ExprSplitters.atoms()); final RefutationToGlobalCfaPrec cfaRefToPrec = new RefutationToGlobalCfaPrec<>(refToPrec, cfa.getInitLoc()); - var abstractor = - new ASGAbstractor<>( - analysis, - lts, - target, - LoopcheckerSearchStrategy.Companion.getDefault(), - logger); - final Refiner< - CfaPrec, - ASG, CfaAction>, - ASGTrace, CfaAction>> - refiner = - new SingleASGTraceRefiner<>( - ASGTraceCheckerStrategy.Companion.getDefault(), - solverFactory, - JoiningPrecRefiner.create(cfaRefToPrec), - logger, - True()); - final CegarChecker< - CfaPrec, - ASG, CfaAction>, - ASGTrace, CfaAction>> - verifier = - CegarChecker.create( - abstractor, - refiner, - logger, - new AsgVisualizer<>(Objects::toString, Objects::toString)); + LoopcheckerSearchStrategy.getEntries() + .forEach( + lStrat -> { + ASGTraceCheckerStrategy.getEntries() + .forEach( + strat -> { + var abstractor = + new ASGAbstractor<>( + analysis, lts, target, lStrat, + logger); + final Refiner< + CfaPrec, + ASG, CfaAction>, + ASGTrace< + CfaState, + CfaAction>> + refiner = + new SingleASGTraceRefiner<>( + strat, + solverFactory, + JoiningPrecRefiner.create( + cfaRefToPrec), + logger, + True()); + final CegarChecker< + CfaPrec, + ASG, CfaAction>, + ASGTrace< + CfaState, + CfaAction>> + verifier = + CegarChecker.create( + abstractor, + refiner, + logger, + new AsgVisualizer<>( + Objects::toString, + Objects::toString)); - final GlobalCfaPrec prec = GlobalCfaPrec.create(PredPrec.of()); - var res = verifier.check(prec); - Assert.assertEquals(result, res.isUnsafe()); + 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/ASGTraceCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java index 1b6eef1734..b985a309f2 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/ASGTraceCheckerTest.java @@ -84,9 +84,13 @@ public void testWithCounter3() throws IOException { abstractor.check(ASG, precision); ASGTrace, XstsAction> trace = ASG.getTraces().iterator().next(); - ExprTraceStatus status = - ASGTraceCheckerStrategy.Companion.getDefault() - .check(trace, solverFactory, xsts.getInitFormula(), logger); - Assert.assertTrue(status.isInfeasible()); + ASGTraceCheckerStrategy.getEntries() + .forEach( + strat -> { + ExprTraceStatus status = + strat.check( + trace, solverFactory, xsts.getInitFormula(), logger); + Assert.assertTrue(status.isInfeasible()); + }); } } diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt new file mode 100644 index 0000000000..fa7a141799 --- /dev/null +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/utils/VarCollectorStmtVisitorTest.kt @@ -0,0 +1,74 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.analysis.algorithm.loopchecker.utils + +import hu.bme.mit.theta.analysis.algorithm.loopchecker.util.VarCollectorStmtVisitor +import hu.bme.mit.theta.core.decl.Decls +import hu.bme.mit.theta.core.decl.VarDecl +import hu.bme.mit.theta.core.stmt.IfStmt +import hu.bme.mit.theta.core.stmt.Stmt +import hu.bme.mit.theta.core.stmt.Stmts +import hu.bme.mit.theta.core.type.booltype.BoolExprs +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.core.type.inttype.IntExprs +import hu.bme.mit.theta.core.type.inttype.IntType +import java.util.* +import org.junit.Assert +import org.junit.Test +import org.junit.runner.RunWith +import org.junit.runners.Parameterized + +@RunWith(Parameterized::class) +class VarCollectorStmtVisitorTest( + private val stmt: Stmt, + private val inputVars: Set>, + private val expectedVars: Set>, +) { + + @Test + fun test() { + val vars = VarCollectorStmtVisitor.visitAll(listOf(stmt), inputVars) + Assert.assertEquals(expectedVars, vars) + } + + companion object { + + private val VA: VarDecl = Decls.Var("a", BoolExprs.Bool()) + private val VB: VarDecl = Decls.Var("b", IntExprs.Int()) + private val VC: VarDecl = Decls.Var("d", IntExprs.Int()) + + @JvmStatic + @Parameterized.Parameters + fun data(): Collection> { + return listOf( + arrayOf(Stmts.Skip(), emptySet>(), emptySet>()), + arrayOf(Stmts.Havoc(VA), emptySet>(), setOf(VA)), + arrayOf(Stmts.Havoc(VB), emptySet>(), setOf(VB)), + arrayOf(Stmts.Havoc(VA), setOf(VA), setOf(VA)), + arrayOf(Stmts.Havoc(VB), setOf(VA), setOf(VA, VB)), + arrayOf(Stmts.Assign(VB, IntExprs.Int(0)), setOf(VB), setOf(VB)), + arrayOf(Stmts.Assign(VB, IntExprs.Add(VB.ref, IntExprs.Int(1))), setOf(VB), setOf(VB)), + arrayOf(Stmts.Assign(VB, IntExprs.Add(VC.ref, VC.ref)), setOf(VC), setOf(VB, VC)), + arrayOf( + Stmts.Assume(BoolExprs.And(VA.ref, IntExprs.Eq(VB.ref, VC.ref))), + setOf(VC), + setOf(VC), + ), + arrayOf(IfStmt.of(BoolExprs.False(), Stmts.Havoc(VB)), emptySet>(), setOf(VB)), + ) + } + } +} diff --git a/subprojects/common/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 178ed745d4..dcc83fa154 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 @@ -17,7 +17,6 @@ package hu.bme.mit.theta.common.ltl import hu.bme.mit.theta.analysis.algorithm.loopchecker.abstraction.LoopcheckerSearchStrategy import hu.bme.mit.theta.analysis.algorithm.loopchecker.refinement.ASGTraceCheckerStrategy -import hu.bme.mit.theta.analysis.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