Bounded-like checker for LTS

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgBuilder.java

@@ -42,6 +42,14 @@ private ArgBuilder(
         this.excludeBottom = excludeBottom;
     }
 
+    public Analysis<S, ? super A, ? super P> getAnalysis() {
+        return analysis;
+    }
+
+    public Predicate<? super S> getTarget() {
+        return target;
+    }
+
     public static <S extends State, A extends Action, P extends Prec> ArgBuilder<S, A, P> create(
             final LTS<? super S, A> lts,
             final Analysis<S, ? super A, ? super P> analysis,

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

@@ -0,0 +1,199 @@
+/*
+ *  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 static com.google.common.base.Preconditions.checkNotNull;
+
+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.Trace;
+import hu.bme.mit.theta.analysis.algorithm.EmptyProof;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.expr.ExprAction;
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.core.model.ImmutableValuation;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolLitExpr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.ExprSimplifier;
+import hu.bme.mit.theta.core.utils.PathUtils;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
+import hu.bme.mit.theta.solver.Solver;
+import hu.bme.mit.theta.solver.utils.WithPushPop;
+import java.util.ArrayDeque;
+import java.util.Deque;
+import java.util.function.Predicate;
+
+public class BoundedLtsChecker<S extends ExprState, A extends ExprAction, P extends Prec>
+        implements SafetyChecker<EmptyProof, Trace<S, A>, P> {
+    private final Solver solver;
+    private final Analysis<S, A, ? super P> analysis;
+    private final Predicate<? super S> target;
+    private final LTS<? super S, A> lts;
+    private final int bound;
+    private final P defaultPrec;
+    private final Deque<Transition<S, A>> transitions;
+    private final ExprSimplifier simplifier = ExprSimplifier.create();
+
+    public BoundedLtsChecker(
+            LTS<? super S, A> lts,
+            Analysis<S, A, ? super P> analysis,
+            Predicate<? super S> target,
+            int bound,
+            Solver solver) {
+        this(lts, analysis, target, bound, null, solver);
+    }
+
+    public BoundedLtsChecker(
+            LTS<? super S, A> lts,
+            Analysis<S, A, ? super P> analysis,
+            Predicate<? super S> target,
+            int bound,
+            P defaultPrec,
+            Solver solver) {
+        this.solver = solver;
+        this.analysis = analysis;
+        this.target = target;
+        this.lts = lts;
+        this.bound = bound;
+        this.defaultPrec = defaultPrec;
+        transitions = new ArrayDeque<>(bound + 1);
+    }
+
+    private int depth() {
+        return transitions.size();
+    }
+
+    @Override
+    public SafetyResult<EmptyProof, Trace<S, A>> check(P prec) {
+        return doCheck(prec == null ? defaultPrec : prec);
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> doCheck(P prec) {
+        checkNotNull(prec, "No prec provided");
+        var indexing = VarIndexingFactory.indexing(0);
+        boolean safe = true;
+        for (var initialState : analysis.getInitFunc().getInitStates(prec)) {
+            if (initialState.isBottom()) {
+                continue;
+            }
+            try (var wpp = new WithPushPop(solver)) {
+                solver.add(PathUtils.unfold(initialState.toExpr(), indexing));
+                if (!solver.check().isSat()) {
+                    continue;
+                }
+                try {
+                    transitions.addLast(new Transition<>(null, initialState, indexing));
+                    var result = expand(prec);
+                    if (result.isUnsafe()) {
+                        return result;
+                    }
+                    if (!result.isSafe()) {
+                        safe = false;
+                    }
+                } finally {
+                    transitions.removeLast();
+                }
+            }
+        }
+        return getSafeResult(safe);
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> expand(P prec) {
+        var transition = transitions.peekLast();
+        assert transition != null : "No transition available";
+        var state = transition.succState();
+        if (target.test(state)) {
+            return getCex();
+        }
+        if (bound > 0 && depth() > bound) {
+            return SafetyResult.unknown();
+        }
+        var indexing = transition.succIndexing();
+        var actions = lts.getEnabledActionsFor(state);
+        boolean safe = true;
+        for (var action : actions) {
+            try (var wpp = new WithPushPop(solver)) {
+                solver.add(PathUtils.unfold(action.toExpr(), indexing));
+                if (!solver.check().isSat()) {
+                    continue;
+                }
+                var nextIndexing = action.nextIndexing();
+                for (var succState : analysis.getTransFunc().getSuccStates(state, action, prec)) {
+                    if (succState.isBottom()) {
+                        continue;
+                    }
+                    // Simplify the state expressions and do not call the SMT solver if it is
+                    // trivially satisfied. This reduces the number of SMT solver calls with,
+                    // e.g., UnitState, where the state expression is always trivial.
+                    var succExpr =
+                            simplifier.simplify(succState.toExpr(), ImmutableValuation.empty());
+                    boolean needsCheck = !isTrue(succExpr);
+                    if (needsCheck) {
+                        solver.push();
+                    }
+                    try {
+                        var succIndexing = indexing.add(nextIndexing);
+                        if (needsCheck) {
+                            solver.add(PathUtils.unfold(succExpr, succIndexing));
+                            if (!solver.check().isSat()) {
+                                continue;
+                            }
+                        }
+                        try {
+                            transitions.addLast(new Transition<>(action, succState, succIndexing));
+                            var result = expand(prec);
+                            if (result.isUnsafe()) {
+                                return result;
+                            }
+                            if (!result.isSafe()) {
+                                safe = false;
+                            }
+                        } finally {
+                            transitions.removeLast();
+                        }
+                    } finally {
+                        if (needsCheck) {
+                            solver.pop();
+                        }
+                    }
+                }
+            }
+        }
+        return getSafeResult(safe);
+    }
+
+    boolean isTrue(Expr<BoolType> expr) {
+        return expr instanceof BoolLitExpr boolLitExpr && boolLitExpr.getValue();
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> getCex() {
+        var states = transitions.stream().map(Transition::succState).toList();
+        var actions = transitions.stream().skip(1).map(Transition::action).toList();
+        var trace = Trace.of(states, actions);
+        return SafetyResult.unsafe(trace, EmptyProof.getInstance());
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> getSafeResult(boolean safe) {
+        return safe ? SafetyResult.safe(EmptyProof.getInstance()) : SafetyResult.unknown();
+    }
+
+    private record Transition<S extends ExprState, A extends ExprAction>(
+            A action, S succState, VarIndexing succIndexing) {}
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java

@@ -19,10 +19,13 @@
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 
 /**
  * Common interface for the abstractor component. It can create an initial ARG and check an ARG with
  * a given precision.
  */
 public interface ArgAbstractor<S extends State, A extends Action, P extends Prec>
-        extends Abstractor<P, ARG<S, A>> {}
+        extends Abstractor<P, ARG<S, A>> {
+    ArgBuilder<S, A, P> getArgBuilder();
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java

@@ -65,6 +65,11 @@ public static <S extends State, A extends Action, P extends Prec> Builder<S, A,
         return new Builder<>(argBuilder);
     }
 
+    @Override
+    public ArgBuilder<S, A, P> getArgBuilder() {
+        return argBuilder;
+    }
+
     @Override
     public ARG<S, A> createProof() {
         return argBuilder.createArg();

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt

@@ -22,6 +22,8 @@ import hu.bme.mit.theta.analysis.expl.ExplState
 import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.pred.PredPrec
 import hu.bme.mit.theta.analysis.pred.PredState
+import hu.bme.mit.theta.analysis.unit.UnitPrec
+import hu.bme.mit.theta.analysis.unit.UnitState
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.*
 import hu.bme.mit.theta.core.stmt.Stmts.Assume
@@ -208,6 +210,7 @@ fun <S : ExprState> S.patch(writeTriples: WriteTriples): S =
   when (this) {
     is PredState -> PredState.of(preds.map { it.patch(writeTriples) }) as S
     is ExplState -> this
+    is UnitState -> this
     is PtrState<*> ->
       (this as PtrState<ExprState>).copy(innerState = innerState.patch(writeTriples)) as S
     else -> error("State $this is not supported")
@@ -217,6 +220,7 @@ fun <P : Prec> P.patch(writeTriples: WriteTriples): P =
   when (this) {
     is PredPrec -> PredPrec.of(preds.map { it.patch(writeTriples) }) as P
     is ExplPrec -> this
+    is UnitPrec -> this
     else -> error("Prec $this is not supported")
   }
 
@@ -231,13 +235,15 @@ fun <P : Prec> P.repatch(): P =
   when (this) {
     is PredPrec -> PredPrec.of(preds.map { it.repatch() }) as P
     is ExplPrec -> this
+    is UnitPrec -> this
     else -> error("Prec $this is not supported")
   }
 
 fun <S : ExprState> S.repatch(): S =
   when (this) {
     is PredState -> PredState.of(preds.map(Expr<BoolType>::repatch)) as S
     is ExplState -> this
+    is UnitState -> this
     else -> error("State $this is not supported")
   }
 

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt

@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.analysis
 import hu.bme.mit.theta.analysis.*
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
+import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedLtsChecker
 import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion
 import hu.bme.mit.theta.analysis.expl.ExplInitFunc
@@ -32,7 +33,9 @@ import hu.bme.mit.theta.analysis.pred.PredAbstractors.PredAbstractor
 import hu.bme.mit.theta.analysis.ptr.PtrPrec
 import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.analysis.ptr.getPtrInitFunc
+import hu.bme.mit.theta.analysis.ptr.getPtrPartialOrd
 import hu.bme.mit.theta.analysis.ptr.getPtrTransFunc
+import hu.bme.mit.theta.analysis.unit.*
 import hu.bme.mit.theta.analysis.waitlist.Waitlist
 import hu.bme.mit.theta.common.Try
 import hu.bme.mit.theta.common.logging.Logger
@@ -431,3 +434,83 @@ class PredXcfaAnalysis(
     coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor),
     coreTransFunc = getPredXcfaTransFunc(predAbstractor, isHavoc),
   )
+
+private fun getUnitXcfaPartialOrd(xcfa: XCFA): PartialOrd<XcfaState<PtrState<UnitState>>> {
+  val ptrPartialOrd = UnitAnalysis.getInstance().partialOrd.getPtrPartialOrd()
+  return if (xcfa.isInlined) {
+    getPartialOrder(ptrPartialOrd)
+  } else {
+    getStackPartialOrder(ptrPartialOrd)
+  }
+}
+
+private fun getUnitXcfaInitFunc(
+  xcfa: XCFA
+): (XcfaPrec<PtrPrec<UnitPrec>>) -> List<XcfaState<PtrState<UnitState>>> {
+  val processInitState =
+    xcfa.initProcedures
+      .mapIndexed { i, it ->
+        val initLocStack: LinkedList<XcfaLocation> = LinkedList()
+        initLocStack.add(it.first.initLoc)
+        Pair(
+          i,
+          XcfaProcessState(
+            initLocStack,
+            prefix = "T$i",
+            varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))),
+          ),
+        )
+      }
+      .toMap()
+  return { p ->
+    InitFunc<UnitState, UnitPrec> { _ -> listOf(UnitState.getInstance()) }
+      .getPtrInitFunc()
+      .getInitStates(p.p)
+      .map { XcfaState(xcfa, processInitState, it) }
+  }
+}
+
+private fun getUnitXcfaTransFunc(
+  isHavoc: Boolean
+): (XcfaState<PtrState<UnitState>>, XcfaAction, XcfaPrec<PtrPrec<UnitPrec>>) -> List<
+    XcfaState<PtrState<UnitState>>
+  > {
+  val unitTransFunc =
+    TransFunc<UnitState, ExprAction, UnitPrec> { s, _, _ -> listOf(s) }.getPtrTransFunc(isHavoc)
+  return { s, a, p ->
+    val (newSt, newAct) = s.apply(a)
+    unitTransFunc.getSuccStates(s.sGlobal, newAct, p.p).map { newSt.withState(it) }
+  }
+}
+
+class UnitXcfaAnalysis(xcfa: XCFA, isHavoc: Boolean) :
+  XcfaAnalysis<UnitState, PtrPrec<UnitPrec>>(
+    corePartialOrd = getUnitXcfaPartialOrd(xcfa),
+    coreInitFunc = getUnitXcfaInitFunc(xcfa),
+    coreTransFunc = getUnitXcfaTransFunc(isHavoc),
+  )
+
+fun getBoundedXcfaChecker(
+  xcfa: XCFA,
+  errorDetection: ErrorDetection,
+  bound: Int,
+  solver: Solver,
+  isHavoc: Boolean = false,
+): BoundedLtsChecker<XcfaState<PtrState<UnitState>>, XcfaAction, XcfaPrec<PtrPrec<UnitPrec>>> {
+  val lts = getXcfaLts()
+  return getBoundedXcfaChecker(xcfa, lts, errorDetection, bound, solver, isHavoc)
+}
+
+fun getBoundedXcfaChecker(
+  xcfa: XCFA,
+  lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
+  errorDetection: ErrorDetection,
+  bound: Int,
+  solver: Solver,
+  isHavoc: Boolean = false,
+): BoundedLtsChecker<XcfaState<PtrState<UnitState>>, XcfaAction, XcfaPrec<PtrPrec<UnitPrec>>> {
+  val analysis = UnitXcfaAnalysis(xcfa, isHavoc)
+  val target = getXcfaErrorPredicate(errorDetection)
+  val prec = XcfaPrec(PtrPrec(UnitPrec.getInstance()))
+  return BoundedLtsChecker(lts, analysis, target, bound, prec, solver)
+}