Fix trace creation of reversed ic3

ftsrg · Feb 20, 2025 · e5c7a85 · e5c7a85
1 parent 3e83d75
commit e5c7a85
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 15 deletions.
diff --git a/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ic3/Ic3Checker.java b/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ic3/Ic3Checker.java
@@ -366,14 +366,8 @@ public Trace<S, A> traceMaker(LinkedList<ProofObligation> forwardProofObligation
         var abstractStates = new ArrayList<ExprState>();
         var abstractActions = new ArrayList<ExprAction>();
         while (!forwardProofObligations.isEmpty()) {
-            final ProofObligation currentProofObligation;
-            if (forwardTrace) {
-                currentProofObligation = forwardProofObligations.getLast();
-                forwardProofObligations.removeLast();
-            } else {
-                currentProofObligation = forwardProofObligations.getFirst();
-                forwardProofObligations.removeFirst();
-            }
+            final ProofObligation currentProofObligation = forwardProofObligations.getLast();
+            forwardProofObligations.removeLast();
 
             if (!abstractStates.isEmpty())
                 abstractActions.add(MonolithicExprKt.action(monolithicExpr));
@@ -392,7 +386,8 @@ public Trace<S, A> traceMaker(LinkedList<ProofObligation> forwardProofObligation
                 checker.check(Trace.of(abstractStates, abstractActions));
         checkArgument(status.isFeasible(), "Infeasible trace.");
 
-        final Trace<Valuation, ? extends Action> valuations = status.asFeasible().getValuations();
+        Trace<Valuation, ? extends Action> valuations = status.asFeasible().getValuations();
+        if (!forwardTrace) valuations = valuations.reverse();
         final List<S> states = new ArrayList<>();
         final List<A> actions = new ArrayList<>();
         for (int i = 0; i < valuations.getStates().size(); ++i) {

diff --git a/...s/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt b/...s/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt
@@ -15,10 +15,8 @@
  */
 package hu.bme.mit.theta.xsts.cli
 
-import com.github.ajalt.clikt.parameters.options.default
 import com.github.ajalt.clikt.parameters.options.flag
 import com.github.ajalt.clikt.parameters.options.option
-import com.github.ajalt.clikt.parameters.types.boolean
 import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr
 import hu.bme.mit.theta.analysis.algorithm.bounded.createMonolithicL2S
 import hu.bme.mit.theta.analysis.algorithm.bounded.createReversed
@@ -28,12 +26,10 @@ import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithi
 abstract class XstsCliMonolithicBaseCommand(name: String? = null, help: String = "") :
   XstsCliBaseCommand(name = name, help = help) {
 
-  protected val reversed: Boolean by
-    option(help = "Reversed state space exploration").flag()
+  protected val reversed: Boolean by option(help = "Reversed state space exploration").flag()
   protected val livenessToSafety: Boolean by
     option(help = "Use liveness to safety transformation").flag()
-  protected val abstracted: Boolean by
-    option(help = "Wrap analysis in CEGAR loop").flag()
+  protected val abstracted: Boolean by option(help = "Wrap analysis in CEGAR loop").flag()
 
   fun createMonolithicExpr(xsts: XSTS): MonolithicExpr {
     var monolithicExpr = xsts.toMonolithicExpr()