fixed coverage vs equality issue in bad end remover

ftsrg · Jan 26, 2025 · d7db9d4 · d7db9d4
1 parent ce57c6d
commit d7db9d4
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 6 deletions.
diff --git a/...src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt b/...src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt
@@ -37,9 +37,7 @@ class DoubleEndNodeRemover<S : State, A : Action> {
       val parent = node.parent.get()
       if (parent.parent.isEmpty) return false
       val grandParent = node.parent.get().parent.get()
-      return if (
-        node.isCovered && parent.parent.get() == node.coveringNode.get()
-      ) { // node is covered and parent is checked above
+      return if (node.state == grandParent.state) { // node is covered and parent is checked above
         // bad node
         true
       } else {
@@ -49,7 +47,7 @@ class DoubleEndNodeRemover<S : State, A : Action> {
       var transitionFired = false
       if (node.parent.isPresent && node.parent.get().parent.isPresent) {
         val grandParent = node.parent.get().parent.get()
-        if (!(node.isCovered && node.coveringNode.get() == grandParent)) return false
+        if (node.state != grandParent.state) return false
 
         val state = node.parent.get().state.toString()
         val bufReader = BufferedReader(StringReader(state))

diff --git a/...c/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt b/...c/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt
@@ -26,7 +26,6 @@ import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTrace
 import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationResult
 import hu.bme.mit.theta.common.logging.Logger
 import java.util.function.Consumer
-import kotlin.collections.ArrayList
 
 class TraceGenerationChecker<S : State, A : Action, P : Prec>(
   private val logger: Logger,

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt
@@ -80,7 +80,7 @@ class XstsCliTracegen :
 
     for (node in summaryStateMap.keys) {
       for (outEdge in node.outEdges) {
-        sb.add("${node.id} -> ${outEdge.target.id}")
+        sb.add("_${node.id} -> _${outEdge.target.id}")
       }
     }
 
@@ -200,6 +200,7 @@ class XstsCliTracegen :
       traceDirPath.mkdir()
     }
 
+    // TODO FIX: if prop at end of xsts, it uses that, not this one
     val propStream = ByteArrayInputStream(("prop {\n" + "\ttrue\n" + "}\n").toByteArray())
     val xsts =
       XstsDslManager.createXsts(SequenceInputStream(FileInputStream(modelFile), propStream))