Merge pull request #380 from ftsrg/coordination

XSTS MDD improvements

Author: mondokm

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.17.2"
+    version = "6.17.3"
 
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))

subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java

@@ -103,7 +103,8 @@ public void test() throws Exception {
                                 MddChecker.IterationStrategy.GSAT,
                                 valuation -> monolithicExpr.getValToState().invoke(valuation),
                                 (Valuation v1, Valuation v2) ->
-                                        monolithicExpr.getBiValToAction().invoke(v1, v2));
+                                        monolithicExpr.getBiValToAction().invoke(v1, v2),
+                                true);
                 status = checker.check(null);
             }
 

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.kt

@@ -27,8 +27,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs
 import hu.bme.mit.theta.core.type.booltype.BoolLitExpr
 import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.type.booltype.IffExpr
-import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And
-import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*
 import hu.bme.mit.theta.core.utils.ExprUtils
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 import java.util.HashMap
@@ -81,9 +80,11 @@ fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr {
     }
   }
 
+  val transExpr = Or(this.split().map { And(lambdaList + lambdaPrimeList + it) })
+
   return MonolithicExpr(
     initExpr = And(And(lambdaList), initExpr),
-    transExpr = And(And(lambdaList), And(lambdaPrimeList), transExpr),
+    transExpr = transExpr,
     propExpr = Not(And(And(lambdaList), Not(propExpr))),
     transOffsetIndex = indexingBuilder.build(),
     initOffsetIndex = VarIndexingFactory.indexing(0),

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt

@@ -152,6 +152,21 @@ constructor(
     val bmcSolver = this.bmcSolver!!
     logger.write(Logger.Level.MAINSTEP, "\tStarting BMC\n")
 
+    if (iteration == 1) {
+      WithPushPop(bmcSolver).use {
+        bmcSolver.add(Not(unfoldedPropExpr(indices.first())))
+
+        if (bmcSolver.check().isSat) {
+          val trace = getTrace(bmcSolver.model)
+          logger.write(
+            Logger.Level.MAINSTEP,
+            "CeX found in the initial state (length ${trace.length()})\n",
+          )
+          return SafetyResult.unsafe(trace, PredState.of(), BoundedStatistics(iteration))
+        }
+      }
+    }
+
     bmcSolver.add(exprs.last())
 
     if (lfPathOnly()) { // indices contains currIndex as last()
@@ -249,6 +264,22 @@ constructor(
     val b = itpSolver.createMarker()
     val pattern = itpSolver.createBinPattern(a, b)
 
+    if (iteration == 1) {
+      WithPushPop(itpSolver).use {
+        itpSolver.add(a, unfoldedInitExpr)
+        itpSolver.add(a, Not(unfoldedPropExpr(indices.first())))
+
+        if (itpSolver.check().isSat) {
+          val trace = getTrace(itpSolver.model)
+          logger.write(
+            Logger.Level.MAINSTEP,
+            "CeX found in the initial state (length ${trace.length()})\n",
+          )
+          return SafetyResult.unsafe(trace, PredState.of(), BoundedStatistics(iteration))
+        }
+      }
+    }
+
     itpSolver.push()
 
     itpSolver.add(a, unfoldedInitExpr)

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprCegarChecker.java

@@ -28,6 +28,7 @@
 import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceFwBinItpChecker;
 import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceStatus;
 import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation;
+import hu.bme.mit.theta.analysis.pred.ExprSplitters;
 import hu.bme.mit.theta.analysis.pred.PredPrec;
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.common.logging.Logger;
@@ -122,9 +123,12 @@ public MonolithicExprCegarChecker(
                     } else {
                         final var ref = concretizationResult.asInfeasible().getRefutation();
                         final var newPred = ref.get(ref.getPruneIndex());
-                        final var newPrec = PredPrec.of(newPred);
-                        predPrec = predPrec.join(newPrec);
-                        logger.write(Logger.Level.INFO, "Added new predicate " + newPrec + "\n");
+                        for (var splitPred : ExprSplitters.conjuncts().apply(newPred)) {
+                            final var newPrec = PredPrec.of(splitPred);
+                            predPrec = predPrec.join(newPrec);
+                        }
+
+                        logger.write(Logger.Level.INFO, "Added new predicate " + newPred + "\n");
                     }
                 }
             }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExprVarOrdering.kt

@@ -0,0 +1,51 @@
+/*
+ *  Copyright 2025 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.bounded
+
+import hu.bme.mit.theta.analysis.algorithm.mdd.varordering.Event
+import hu.bme.mit.theta.analysis.algorithm.mdd.varordering.orderVarsFromRandomStartingPoints
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.model.BasicSubstitution
+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.PathUtils
+import hu.bme.mit.theta.core.utils.indexings.VarIndexing
+
+fun MonolithicExpr.orderVars(): List<VarDecl<*>> {
+  val events = this.split().map { MonolithicExprEvent(it, this.transOffsetIndex) }.toSet()
+  val orderedVars = orderVarsFromRandomStartingPoints(this.vars, events)
+  return orderedVars
+}
+
+// Filters affected variables
+class MonolithicExprEvent : Event {
+
+  constructor(expr: Expr<BoolType>, transOffsetIndex: VarIndexing) {
+    val vars = ExprUtils.getVars(expr)
+    var sub = BasicSubstitution.builder()
+    for (v in vars) {
+      sub = sub.put(v.getConstDecl(transOffsetIndex.get(v)), v.getConstDecl(0).ref)
+    }
+    val identityRemovedExpr = ExprUtils.simplify(sub.build().apply(PathUtils.unfold(expr, 0)))
+    val remainingConstants = ExprUtils.getConstants(identityRemovedExpr)
+    this.affectedVars = vars.filter { it.getConstDecl(0) in remainingConstants }.toSet()
+  }
+
+  private val affectedVars: Set<VarDecl<*>>
+
+  override fun getAffectedVars(): Set<VarDecl<*>> = affectedVars
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java

@@ -32,6 +32,7 @@
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr;
 import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExprKt;
+import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExprVarOrderingKt;
 import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor;
 import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl.*;
 import hu.bme.mit.theta.analysis.algorithm.mdd.expressionnode.ExprLatticeDefinition;
@@ -67,6 +68,7 @@ public class MddChecker<S extends ExprState, A extends ExprAction>
     private final IterationStrategy iterationStrategy;
     private final Function<Valuation, S> valToState;
     private final BiFunction<Valuation, Valuation, A> biValToAction;
+    private final boolean forwardTrace;
 
     public enum IterationStrategy {
         BFS,
@@ -81,14 +83,16 @@ private MddChecker(
             Logger logger,
             IterationStrategy iterationStrategy,
             Function<Valuation, S> valToState,
-            BiFunction<Valuation, Valuation, A> biValToAction) {
+            BiFunction<Valuation, Valuation, A> biValToAction,
+            boolean forwardTrace) {
         this.monolithicExpr = monolithicExpr;
         this.variableOrdering = variableOrdering;
         this.solverPool = solverPool;
         this.logger = logger;
         this.iterationStrategy = iterationStrategy;
         this.valToState = valToState;
         this.biValToAction = biValToAction;
+        this.forwardTrace = forwardTrace;
     }
 
     public static <S extends ExprState, A extends ExprAction> MddChecker<S, A> create(
@@ -97,15 +101,17 @@ public static <S extends ExprState, A extends ExprAction> MddChecker<S, A> creat
             SolverPool solverPool,
             Logger logger,
             Function<Valuation, S> valToState,
-            BiFunction<Valuation, Valuation, A> biValToAction) {
+            BiFunction<Valuation, Valuation, A> biValToAction,
+            boolean forwardTrace) {
         return new MddChecker<S, A>(
                 monolithicExpr,
                 variableOrdering,
                 solverPool,
                 logger,
                 IterationStrategy.GSAT,
                 valToState,
-                biValToAction);
+                biValToAction,
+                forwardTrace);
     }
 
     public static <S extends ExprState, A extends ExprAction> MddChecker<S, A> create(
@@ -115,15 +121,17 @@ public static <S extends ExprState, A extends ExprAction> MddChecker<S, A> creat
             Logger logger,
             IterationStrategy iterationStrategy,
             Function<Valuation, S> valToState,
-            BiFunction<Valuation, Valuation, A> biValToAction) {
+            BiFunction<Valuation, Valuation, A> biValToAction,
+            boolean forwardTrace) {
         return new MddChecker<S, A>(
                 monolithicExpr,
                 variableOrdering,
                 solverPool,
                 logger,
                 iterationStrategy,
                 valToState,
-                biValToAction);
+                biValToAction,
+                forwardTrace);
     }
 
     @Override
@@ -147,7 +155,8 @@ public SafetyResult<MddProof, Trace<S, A>> check(UnitPrec prec) {
                 variableOrdering.size() == Containers.createSet(variableOrdering).size(),
                 "Variable ordering contains duplicates");
         final var identityExprs = new ArrayList<Expr<BoolType>>();
-        for (var v : Lists.reverse(variableOrdering)) {
+        final var orderedVars = MonolithicExprVarOrderingKt.orderVars(monolithicExpr);
+        for (var v : Lists.reverse(orderedVars)) {
             var domainSize = Math.max(v.getType().getDomainSize().getFiniteSize().intValue(), 0);
 
             //     if (domainSize > 100) {
@@ -285,9 +294,17 @@ public SafetyResult<MddProof, Trace<S, A>> check(UnitPrec prec) {
                 }
             }
 
-            result =
-                    SafetyResult.unsafe(
-                            Trace.of(states, actions), MddProof.of(stateSpace), statistics);
+            if (forwardTrace) {
+                result =
+                        SafetyResult.unsafe(
+                                Trace.of(states, actions), MddProof.of(stateSpace), statistics);
+            } else {
+                result =
+                        SafetyResult.unsafe(
+                                Trace.of(Lists.reverse(states), Lists.reverse(actions)),
+                                MddProof.of(stateSpace),
+                                statistics);
+            }
         } else {
             result = SafetyResult.safe(MddProof.of(stateSpace), statistics);
         }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/fixedpoint/TraceProvider.java

@@ -20,8 +20,8 @@
 import hu.bme.mit.delta.mdd.MddInterpreter;
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddSinglePathExtractor;
 import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor;
-import java.util.ArrayList;
 import java.util.List;
+import java.util.Stack;
 
 public final class TraceProvider implements MddGraph.CleanupListener {
     public static boolean verbose = false;
@@ -48,10 +48,10 @@ public List<MddHandle> compute(
             MddHandle initialStates,
             MddVariableHandle highestAffectedVariable) {
 
-        MddHandle alreadyExplored = targetStates;
         MddHandle currentState = targetStates;
-        final List<MddHandle> states = new ArrayList<>();
-        states.add(targetStates);
+        MddHandle alreadyExplored = currentState;
+        final Stack<MddHandle> states = new Stack<>();
+        states.push(currentState);
 
         while (MddInterpreter.calculateNonzeroCount(currentState.intersection(initialStates))
                 <= 0) {
@@ -62,9 +62,14 @@ public List<MddHandle> compute(
                                     reversedNextStateRelation,
                                     highestAffectedVariable)
                             .minus(alreadyExplored);
-            currentState = MddSinglePathExtractor.INSTANCE.transform((MddHandle) newLayer);
-            states.add(currentState);
-            alreadyExplored = (MddHandle) alreadyExplored.union(currentState);
+            if (MddInterpreter.calculateNonzeroCount(newLayer) > 0) {
+                currentState = MddSinglePathExtractor.INSTANCE.transform((MddHandle) newLayer);
+                states.push(currentState);
+                alreadyExplored = (MddHandle) alreadyExplored.union(currentState);
+            } else {
+                states.pop();
+                currentState = states.peek();
+            }
         }
 
         return Lists.reverse(states);

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/varordering/ForceVarOrdering.kt

@@ -16,17 +16,19 @@
 package hu.bme.mit.theta.analysis.algorithm.mdd.varordering
 
 import hu.bme.mit.theta.core.decl.VarDecl
-import hu.bme.mit.theta.core.stmt.Stmt
-import hu.bme.mit.theta.core.utils.StmtUtils
 import kotlin.random.Random
 
+interface Event {
+  fun getAffectedVars(): Set<VarDecl<*>>
+}
+
 /**
  * Variable ordering based on the 'FORCE' variable ordering heuristic.
  * https://doi.org/10.1145/764808.764839
  */
 fun orderVarsFromRandomStartingPoints(
   vars: List<VarDecl<*>>,
-  events: Set<Stmt>,
+  events: Set<Event>,
   numStartingPoints: Int = 5,
 ): List<VarDecl<*>> {
   val random = Random(0)
@@ -35,9 +37,9 @@ fun orderVarsFromRandomStartingPoints(
   return orderings.minBy { eventSpans(it, events) }
 }
 
-fun orderVars(vars: List<VarDecl<*>>, events: Set<Stmt>): List<VarDecl<*>> {
+fun orderVars(vars: List<VarDecl<*>>, events: Set<Event>): List<VarDecl<*>> {
 
-  val affectedVars = events.associateWith { event -> StmtUtils.getVars(event) }
+  val affectedVars = events.associateWith { it.getAffectedVars() }
 
   val affectingEvents =
     vars.associateWith { varDecl -> events.filter { varDecl in affectedVars[it]!! }.toSet() }
@@ -73,10 +75,10 @@ fun orderVars(vars: List<VarDecl<*>>, events: Set<Stmt>): List<VarDecl<*>> {
   return currentVarOrdering
 }
 
-private fun eventSpans(vars: List<VarDecl<*>>, events: Set<Stmt>) =
+private fun eventSpans(vars: List<VarDecl<*>>, events: Set<Event>) =
   events
     .map { event ->
-      StmtUtils.getVars(event).let {
+      event.getAffectedVars().let {
         when (it.isEmpty()) {
           true -> 0
           else -> {

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java

@@ -185,7 +185,8 @@ public void testWithIterationStrategy(MddChecker.IterationStrategy iterationStra
                             iterationStrategy,
                             valuation -> monolithicExpr.getValToState().invoke(valuation),
                             (Valuation v1, Valuation v2) ->
-                                    monolithicExpr.getBiValToAction().invoke(v1, v2));
+                                    monolithicExpr.getBiValToAction().invoke(v1, v2),
+                            true);
             status = checker.check(null);
         }