changing return value of trace generation

ftsrg · Sep 21, 2024 · 388a9cc · 388a9cc
1 parent 9b8c51e
commit 388a9cc
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 12 deletions.
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
@@ -7,12 +7,11 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyResult
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace
 import hu.bme.mit.theta.analysis.algorithm.cegar.Abstractor
+import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationResult
 import hu.bme.mit.theta.common.logging.Logger
-import java.util.*
 import java.util.function.Consumer
 import kotlin.collections.ArrayList
 
-
 class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
     private val logger: Logger,
     private val abstractor: Abstractor<S, A, P>,
@@ -93,7 +92,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
         logger.write(Logger.Level.SUBSTEP, "-- Trace generation done --\n")
 
         // TODO return unsafe if coverage not full? (is that known here? not yet)
-        return SafetyResult.safe(TraceGenerationResult(traceMetadata, traces))
+        return SafetyResult.safe(TraceGenerationResult(traceMetadata))
     }
 
     private fun filterEndNodes(

diff --git a/...rc/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt b/...rc/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt
@@ -22,6 +22,5 @@ import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.algorithm.Witness
 
 data class TraceGenerationResult<S : State, A : Action> (
-    val metadata: Collection<TraceMetadata<S, A>>,
-    val traces: Collection<Trace<S, A>>
+    val traces: Map<Trace<S, A>, TraceMetadata<S, A>>
 ) : Witness
diff --git a/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt b/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt
@@ -2,21 +2,21 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration
 
 import hu.bme.mit.theta.analysis.Action
 import hu.bme.mit.theta.analysis.State
+import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace
 import kotlin.jvm.optionals.getOrNull
 
 class TraceGenerationMetadataBuilder<S : State, A : Action> {
-
     val argTraces: MutableList<ArgTrace<S, A>> = mutableListOf()
 
     fun addTrace(trace: ArgTrace<S, A>) {
         argTraces.add(trace)
     }
 
-    fun build(): Collection<TraceMetadata<S, A>> {
+    fun build(): Map<Trace<S, A>, TraceMetadata<S, A>> {
         // first create the meta traces and states
-        val metadataTraces = mutableMapOf<ArgTrace<S, A>, TraceMetadata<S, A>>()
+        val metadataArgTraces = mutableMapOf<ArgTrace<S, A>, TraceMetadata<S, A>>()
         val metadataStates = mutableMapOf<Pair<ArgTrace<S, A>, ArgNode<S, A>>, StateMetadata<S, A>>()
 
         for (argTrace in argTraces) {
@@ -27,13 +27,15 @@ class TraceGenerationMetadataBuilder<S : State, A : Action> {
                 states.add(state)
             }
             val traceMetadata = TraceMetadata.create(states)
-            metadataTraces[argTrace] = traceMetadata
+            metadataArgTraces[argTrace] = traceMetadata
         }
 
-        collectCoverStates(metadataTraces, metadataStates)
+        collectCoverStates(metadataArgTraces, metadataStates)
+
+        val metadataTraces = mutableMapOf<Trace<S, A>, TraceMetadata<S, A>>()
+        metadataArgTraces.forEach { entry -> metadataTraces[entry.key.toTrace()] = entry.value }
 
-        print(metadataTraces.values)
-        return metadataTraces.values
+        return metadataTraces
     }
 
     private fun collectCoverStates(