Fixed trace in L2S

ftsrg · Feb 16, 2025 · 7936e18 · 7936e18
1 parent ec8bf91
commit 7936e18
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 4 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.11.1"
+    version = "6.11.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/l2s/MonolithicL2S.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/l2s/MonolithicL2S.kt
@@ -83,8 +83,8 @@ fun MonolithicExpr.createMonolithicL2S(): MonolithicExpr {
     transOffsetIndex = newIndexing,
     valToState = valToState,
     biValToAction = biValToAction,
-    ctrlVars = ctrlVars,
-    vars = this.vars,
+    //    ctrlVars = ctrlVars,
+    //    vars = this.vars,
     initOffsetIndex = initOffsetIndex,
   )
 }
diff --git a/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt b/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesses/TraceToWitness.kt
@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.cli.witnesses
 import com.google.common.collect.Lists
 import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.c2xcfa.getCMetaData
 import hu.bme.mit.theta.core.model.Valuation
@@ -32,6 +33,7 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.analysis.getXcfaErrorPredicate
 import hu.bme.mit.theta.xcfa.model.*
 import java.math.BigInteger
+import java.util.function.Predicate
 
 enum class Verbosity {
   NECESSARY,
@@ -49,7 +51,10 @@ fun traceToWitness(
   val newStates = ArrayList<WitnessNode>()
   val newActions = ArrayList<WitnessEdge>()
 
-  val isError = getXcfaErrorPredicate(property)
+  val isError =
+    if (property == ErrorDetection.TERMINATION) {
+      Predicate<XcfaState<out PtrState<out ExprState>>> { false }
+    } else getXcfaErrorPredicate(property)
 
   var lastNode =
     WitnessNode(id = "N${newStates.size}", entry = true, sink = false, violation = false)