Add var ordering for cfa and xcfa

ftsrg · Nov 5, 2024 · ef9654b · ef9654b
1 parent 98b7473
commit ef9654b
Show file tree

Hide file tree

Showing 8 changed files with 23 additions and 12 deletions.
diff --git a/...cts/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt b/...cts/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/...jects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java b/...jects/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/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
@@ -76,7 +76,7 @@ constructor(
   private val logger: Logger,
 ) : SafetyChecker<EmptyProof, Trace<S, A>, 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/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt b/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt
@@ -28,10 +28,6 @@ data class MonolithicExpr(
     val transExpr: Expr<BoolType>,
     val propExpr: Expr<BoolType>,
     val transOffsetIndex: VarIndexing = VarIndexingFactory.indexing(1),
-    val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0)
-) {
-
-    fun vars(): Collection<VarDecl<*>> {
-        return getVars(initExpr) union getVars(transExpr) union getVars(propExpr)
-    }
-}
+    val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0),
+    val vars: List<VarDecl<*>> = (getVars(initExpr) union getVars(transExpr) union getVars(propExpr)).toList()
+)
diff --git a/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java b/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java
@@ -55,6 +55,7 @@ public class MddChecker<A extends ExprAction> implements SafetyChecker<MddProof,
     private final VarIndexing initIndexing;
     private final A transRel;
     private final Expr<BoolType> safetyProperty;
+    private final List<VarDecl<?>> 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<BoolType> safetyProperty,
+            List<VarDecl<?>> 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,13 +90,15 @@ public static <A extends ExprAction> MddChecker<A> create(
             VarIndexing initIndexing,
             A transRel,
             Expr<BoolType> safetyProperty,
+            List<VarDecl<?>> variableOrdering,
             SolverPool solverPool,
             Logger logger) {
         return new MddChecker<A>(
                 initRel,
                 initIndexing,
                 transRel,
                 safetyProperty,
+                variableOrdering,
                 solverPool,
                 logger,
                 IterationStrategy.GSAT);
@@ -104,6 +109,7 @@ public static <A extends ExprAction> MddChecker<A> create(
             VarIndexing initIndexing,
             A transRel,
             Expr<BoolType> safetyProperty,
+            List<VarDecl<?>> variableOrdering,
             SolverPool solverPool,
             Logger logger,
             IterationStrategy iterationStrategy) {
@@ -112,6 +118,7 @@ public static <A extends ExprAction> MddChecker<A> create(
                 initIndexing,
                 transRel,
                 safetyProperty,
+                variableOrdering,
                 solverPool,
                 logger,
                 iterationStrategy);
@@ -128,9 +135,7 @@ public SafetyResult<MddProof, MddCex> check(Void input) {
         final MddVariableOrder transOrder =
                 JavaMddFactory.getDefault().createMddVariableOrder(mddGraph);
 
-        final Set<VarDecl<?>> 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/...common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java b/...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/...jects/sts/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsMddCheckerTest.java b/...jects/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/...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaToMonolithicExpr.kt b/...s/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()
   )
 }