From 37089d3fe6333dce88d1a7d5483524165355fc41 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Thu, 19 Sep 2024 09:21:15 +0200 Subject: [PATCH] added v0 trace metadata, wip refactor tracegen checker --- .../tracegeneration/TraceGenerationChecker.kt | 5 +- .../tracegeneration/TraceMetadata.kt | 115 +++++++++++++++++- 2 files changed, 112 insertions(+), 8 deletions(-) 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 ab681b826a..a8909a2dfc 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 @@ -4,6 +4,7 @@ import com.google.common.base.Preconditions import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.Trace import hu.bme.mit.theta.analysis.algorithm.* +import hu.bme.mit.theta.analysis.algorithm.arg.ARG 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 @@ -17,7 +18,7 @@ class TraceGenerationChecker( private val logger: Logger, private val abstractor: Abstractor, private val getFullTraces : Boolean, -) : SafetyChecker { +) : SafetyChecker, Trace, P> { // TODO refactor templates? private var traces: List> = ArrayList() companion object { @@ -30,7 +31,7 @@ class TraceGenerationChecker( } } - override fun check(prec: P): SafetyResult { + override fun check(prec: P): SafetyResult, Trace> { logger.write(Logger.Level.SUBSTEP, "Printing prec for trace generation...\n" + System.lineSeparator()) logger.write(Logger.Level.SUBSTEP, prec.toString()) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt index 78b2ba5e25..9b77c54ff9 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt @@ -1,16 +1,119 @@ 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.algorithm.arg.ArgNode +import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace + +class TraceGenerationMetadataBuilder { + + val argTraces: MutableList> = mutableListOf() + + fun addTrace(trace: ArgTrace) { + argTraces.add(trace) + } + + fun build(): Collection> { + // first create the meta traces and states + val metadataTraces = mutableMapOf, TraceMetadata>() + val metadataStates = mutableMapOf, ArgNode>, StateMetadata>() + + for (argTrace in argTraces) { + val states: MutableSet> = mutableSetOf() + for (argNode in argTrace) { + val state = StateMetadata(argNode.state) + metadataStates[Pair(argTrace, argNode)] = state + states.add(state) + } + val traceMetadata = TraceMetadata.create(states) + metadataTraces[argTrace] = traceMetadata + } + + collectCoverStates(metadataTraces, metadataStates) + + print(metadataTraces.values) + return metadataTraces.values + } + + private fun collectCoverStates( + metadataTraces: Map, TraceMetadata>, + metadataStates: Map, ArgNode>, StateMetadata>) + { + // connect the meta states based on coverages. + // must be done after creation of all meta states, + // so that they can reference each other + for (entry in metadataStates) { + val node = entry.key.second + val state = entry.value + + node.coveredNodes.forEach { coveredNode -> + metadataTraces.keys.forEach { trace -> + metadataStates[Pair(trace, coveredNode)]?.let { coveredMetaState -> + if (coveredMetaState != state) { + coveredMetaState.coveringState.add(state) + } + } + } + } + + node.coveringNode.get().let { coveringNode -> + metadataTraces.keys.forEach { trace -> + metadataStates[Pair(trace, coveringNode)]?.let { coveredMetaState -> + if (coveredMetaState != state) { + coveredMetaState.coveringState.add(state) + } + } + } + } + } + } +} /** * Represents the metadata for a set of traces generated from an ARG - * The following information is created/collected here: - * - a unique identifier for each trace - * - a unique id for each state in each trace - * - coverages (how?) + * The goal here is to have unique identifier for each trace and each state in each trace + * Also, coverage information (even though we don't have ArgNode-s here) */ -class TraceMetadata() { - fun addTrace() { +class TraceMetadata private constructor(val id : Long, val states : Set>) { + companion object { + var counter : Long = 0 + + fun create(states : Set>) + : TraceMetadata { + val traceMetadata = TraceMetadata(counter, states) + counter++ + return traceMetadata + } + } + override fun toString(): String { + val sb = StringBuilder() + sb.append("T$id{") + sb.append("states: $states") + sb.append("}") + return sb.toString() } } + +/** + * We want to differentiate states based on the trace they are in + */ +class StateMetadata (val state: State, val id : Long = counter++) { + val coveringState: MutableSet> = mutableSetOf() // TODO() + val coveredState: MutableSet> = mutableSetOf() // TODO() + + companion object { + var counter : Long = 0 + } + + override fun toString(): String { + return "S$id" + } +} + +fun ArgNode.getStateMetadata() { + for(coveringNodes in this.coveredNodes) { + coveringNodes + } + this.coveringNode +} \ No newline at end of file