From ef9654bd4725111ca72e00b190383c79017a613e Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 5 Nov 2024 22:09:17 +0100 Subject: [PATCH] Add var ordering for cfa and xcfa --- .../bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt | 2 +- .../bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java | 1 + .../analysis/algorithm/bounded/BoundedChecker.kt | 2 +- .../analysis/algorithm/bounded/MonolithicExpr.kt | 10 +++------- .../mit/theta/analysis/algorithm/mdd/MddChecker.java | 11 ++++++++--- .../theta/analysis/algorithm/mdd/MddCheckerTest.java | 4 ++++ .../bme/mit/theta/sts/analysis/StsMddCheckerTest.java | 4 ++++ .../mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt | 1 + 8 files changed, 23 insertions(+), 12 deletions(-) diff --git a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt index 3c3307a506..4b03648ce7 100644 --- a/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt +++ b/subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt @@ -79,7 +79,7 @@ fun CFA.toMonolithicExpr(): MonolithicExpr { val offsetIndex = transUnfold.indexing - return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex) + return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex, vars = listOf(locVar) + this.vars.toList()) } fun CFA.valToAction(val1: Valuation, val2: Valuation): CfaAction { diff --git a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java index 1113419eea..ca6abc822d 100644 --- a/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java +++ b/subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java @@ -112,6 +112,7 @@ public VarIndexing nextIndexing() { } }, monolithicExpr.getPropExpr(), + monolithicExpr.getVars(), solverPool, logger, MddChecker.IterationStrategy.GSAT); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt index 2c1273f87f..ed9405aaa4 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt @@ -76,7 +76,7 @@ constructor( private val logger: Logger, ) : SafetyChecker, UnitPrec> { - private val vars = monolithicExpr.vars() + private val vars = monolithicExpr.vars private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, VarIndexingFactory.indexing(0)) private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt index 65df7dfb65..c2b69b0475 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt @@ -28,10 +28,6 @@ data class MonolithicExpr( val transExpr: Expr, val propExpr: Expr, val transOffsetIndex: VarIndexing = VarIndexingFactory.indexing(1), - val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0) -) { - - fun vars(): Collection> { - return getVars(initExpr) union getVars(transExpr) union getVars(propExpr) - } -} \ No newline at end of file + val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0), + val vars: List> = (getVars(initExpr) union getVars(transExpr) union getVars(propExpr)).toList() +) \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java index 8f6c63f582..baff63cda4 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java @@ -55,6 +55,7 @@ public class MddChecker implements SafetyChecker safetyProperty; + private final List> variableOrdering; private final SolverPool solverPool; private final Logger logger; private IterationStrategy iterationStrategy = IterationStrategy.GSAT; @@ -70,12 +71,14 @@ private MddChecker( VarIndexing initIndexing, A transRel, Expr safetyProperty, + List> variableOrdering, SolverPool solverPool, Logger logger, IterationStrategy iterationStrategy) { this.initRel = initRel; this.initIndexing = initIndexing; this.transRel = transRel; + this.variableOrdering = variableOrdering; this.safetyProperty = safetyProperty; this.solverPool = solverPool; this.logger = logger; @@ -87,6 +90,7 @@ public static MddChecker create( VarIndexing initIndexing, A transRel, Expr safetyProperty, + List> variableOrdering, SolverPool solverPool, Logger logger) { return new MddChecker( @@ -94,6 +98,7 @@ public static MddChecker create( initIndexing, transRel, safetyProperty, + variableOrdering, solverPool, logger, IterationStrategy.GSAT); @@ -104,6 +109,7 @@ public static MddChecker create( VarIndexing initIndexing, A transRel, Expr safetyProperty, + List> variableOrdering, SolverPool solverPool, Logger logger, IterationStrategy iterationStrategy) { @@ -112,6 +118,7 @@ public static MddChecker create( initIndexing, transRel, safetyProperty, + variableOrdering, solverPool, logger, iterationStrategy); @@ -128,9 +135,7 @@ public SafetyResult check(Void input) { final MddVariableOrder transOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph); - final Set> vars = - ExprUtils.getVars(List.of(initRel, transRel.toExpr(), safetyProperty)); - for (var v : vars) { + for (var v : variableOrdering) { var domainSize = Math.max(v.getType().getDomainSize().getFiniteSize().intValue(), 0); if (domainSize > 100) { diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java index 0f9f524354..3fd8f58620 100644 --- a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java +++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java @@ -33,12 +33,15 @@ 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 hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import hu.bme.mit.theta.solver.SolverPool; import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory; import java.util.Arrays; import java.util.Collection; +import java.util.List; + import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; @@ -187,6 +190,7 @@ public VarIndexing nextIndexing() { } }, propExpr, + List.copyOf(ExprUtils.getVars(List.of(initExpr, tranExpr, propExpr))), solverPool, logger, iterationStrategy); diff --git a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java index 929a01e400..57b30f81d3 100644 --- a/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java +++ b/subprojects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java @@ -28,6 +28,7 @@ import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexing; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import hu.bme.mit.theta.solver.SolverPool; @@ -40,6 +41,8 @@ import java.io.FileInputStream; import java.util.Arrays; import java.util.Collection; +import java.util.List; + import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; @@ -104,6 +107,7 @@ public VarIndexing nextIndexing() { } }, sts.getProp(), + List.copyOf(sts.getVars()), solverPool, logger, IterationStrategy.GSAT); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt index 48f9ba280a..c5cc957828 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt @@ -109,6 +109,7 @@ fun XCFA.toMonolithicExpr(): MonolithicExpr { transExpr = And(transUnfold.exprs), propExpr = Neq(locVar.ref, Int(map[proc.errorLoc.get()]!!)), transOffsetIndex = transUnfold.indexing, + vars = listOf(locVar) + this.vars.map { it.wrappedVar }.toList() ) }