From d7db9d41b96a6a71f77a7b879d526678d49cf23d Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sun, 26 Jan 2025 21:07:42 +0100 Subject: [PATCH] fixed coverage vs equality issue in bad end remover --- .../algorithm/tracegeneration/DoubleEndNodeRemover.kt | 6 ++---- .../algorithm/tracegeneration/TraceGenerationChecker.kt | 1 - .../kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt | 3 ++- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt index 43cc5534d8..8f20874577 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt @@ -37,9 +37,7 @@ class DoubleEndNodeRemover { 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 { 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/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt index 15365f2661..bc9661006b 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt +++ b/subprojects/common/analysis/src/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( 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 index 9c526657af..bedd0a1874 100644 --- 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))