-
Notifications
You must be signed in to change notification settings - Fork 41
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor trace metadata to trace summary
- Loading branch information
Showing
5 changed files
with
163 additions
and
145 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
142 changes: 0 additions & 142 deletions
142
...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceMetadata.kt
This file was deleted.
Oops, something went wrong.
113 changes: 113 additions & 0 deletions
113
...ysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceSetSummary.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,113 @@ | ||
| package hu.bme.mit.theta.analysis.algorithm.tracegeneration | ||
|
|
||
| import com.google.common.base.Preconditions.checkState | ||
| 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 | ||
|
|
||
| sealed class TraceGenerationSummaryBuilder<S : State, A : Action> { | ||
| val argTraces: MutableList<ArgTrace<S, A>> = mutableListOf() | ||
|
|
||
| fun addTrace(trace: ArgTrace<S, A>) { | ||
| argTraces.add(trace) | ||
| } | ||
|
|
||
| fun build(): TraceSetSummary<S, A> { | ||
| val argNodes: Set<ArgNode<S, A>> = argTraces.map { trace -> trace.nodes() }.flatten().toSet() | ||
|
|
||
| // grouping nodes covering each other for state summaries | ||
| val nodeGroups: MutableList<MutableSet<ArgNode<S, A>>> = mutableListOf() | ||
| for (node in argNodes) { | ||
| if (nodeGroups.isEmpty()) { | ||
| nodeGroups.add(mutableSetOf(node)) | ||
| } else { | ||
| val inCoverRelationWithNode: MutableList<ArgNode<S, A>> = mutableListOf() | ||
| inCoverRelationWithNode.addAll(node.coveredNodes.toList()) | ||
| if (node.coveringNode.isPresent) inCoverRelationWithNode.add(node.coveringNode.get()) | ||
|
|
||
| val nodeGroup = nodeGroups.filter( | ||
| fun(group: MutableSet<ArgNode<S, A>>): Boolean { | ||
| for (coverNode in inCoverRelationWithNode) { | ||
| if (group.contains(coverNode)) { | ||
| return true | ||
| } | ||
| } | ||
| return false | ||
| } | ||
| ).toList() | ||
|
|
||
| checkState(nodeGroup.size == 1) | ||
|
|
||
| nodeGroup[0].add(node) | ||
| } | ||
| } | ||
|
|
||
| // create state summaries | ||
| val nodeSummaries = mutableSetOf<NodeSummary<S, A>>() | ||
| for (nodeGroup in nodeGroups) { | ||
| nodeSummaries.add(NodeSummary.create(nodeGroup)) | ||
| } | ||
|
|
||
| return TraceSetSummary<S, A>(argTraces, nodeSummaries) | ||
| } | ||
| } | ||
|
|
||
| data class TraceSetSummary<S : State, A : Action> constructor( | ||
| val sourceTraces : Collection<ArgTrace<S, A>>, | ||
| val stateSummaries : Collection<NodeSummary<S, A>>, | ||
| ) { | ||
|
|
||
| override fun toString(): String { | ||
| TODO() | ||
| } | ||
| } | ||
|
|
||
| /** | ||
| * Groups arg nodes based on coverages, but also stores the traces they appear in, coverage relations and arg nodes | ||
| */ | ||
| class NodeSummary<S : State, A: Action> private constructor (val nodeSummaryId: Long, val argNodes: Set<ArgNode<S, A>>) { | ||
| companion object { | ||
| var counter : Long = 0 | ||
|
|
||
| fun <S : State, A : Action> create(argNodes: MutableSet<ArgNode<S, A>>) : NodeSummary<S, A> { | ||
| // all of the nodes should be in some kind of coverage relationship with each other | ||
| for(node in argNodes) { | ||
| for (node2 in argNodes) { | ||
| checkState( | ||
| (node == node2) || | ||
| (node.coveringNode.isPresent() && node.coveringNode.get() == node2) || | ||
| (node.coveredNodes.anyMatch { n -> n==node2 }) | ||
| ) | ||
| } | ||
| } | ||
|
|
||
| return NodeSummary(counter++, argNodes) | ||
| } | ||
| } | ||
|
|
||
| fun getOutEdges() { | ||
| TODO() | ||
| } | ||
|
|
||
| fun getInEdges() { | ||
| TODO() | ||
| } | ||
|
|
||
| fun getLabel() : String { | ||
| val sb = StringBuilder() | ||
|
|
||
| for (node in argNodes) { | ||
| val label = node.state.toString() | ||
| if(label !in sb) { | ||
| sb.append(label) | ||
| } | ||
| } | ||
|
|
||
| return sb.toString() | ||
| } | ||
|
|
||
| override fun toString(): String { | ||
| return getLabel() | ||
| } | ||
| } |
46 changes: 46 additions & 0 deletions
46
...s/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceSummaryVisualizer.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,46 @@ | ||
| /* | ||
| * Copyright 2024 Budapest University of Technology and Economics | ||
| * | ||
| * Licensed under the Apache License, Version 2.0 (the "License"); | ||
| * you may not use this file except in compliance with the License. | ||
| * You may obtain a copy of the License at | ||
| * | ||
| * http://www.apache.org/licenses/LICENSE-2.0 | ||
| * | ||
| * Unless required by applicable law or agreed to in writing, software | ||
| * distributed under the License is distributed on an "AS IS" BASIS, | ||
| * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. | ||
| * See the License for the specific language governing permissions and | ||
| * limitations under the License. | ||
| */ | ||
|
|
||
| package hu.bme.mit.theta.analysis.utils | ||
|
|
||
| import hu.bme.mit.theta.analysis.Action | ||
| import hu.bme.mit.theta.analysis.State | ||
| import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationResult | ||
| import hu.bme.mit.theta.common.visualization.Graph | ||
|
|
||
| /** | ||
| * This class visualizes not single traces, but a group of traces, | ||
| * connected by trace metadata. | ||
| * The result is an automata-like summary of executions. | ||
| */ | ||
| sealed class TraceSummaryVisualizer<S: State, A: Action> ( | ||
| val stateToString: (S) -> String = { it.toString() }, | ||
| val actionToString: (A) -> String = { it.toString() }, | ||
| ) { | ||
|
|
||
| // TODO TraceVisualizer has an unused, similar part (visualizeMerged) | ||
| // it does not use metadata, but visualizes a collection of traces | ||
| // (ie, it is not completely the same as TraceSummaryVisualizer::visualize) | ||
| fun visualize(traceGenerationResult : TraceGenerationResult<S, A>, | ||
| traceSummaryId : String = "trace_summary", | ||
| traceSummaryLabel : String = "Trace Summary", | ||
| ) { | ||
| val traces = traceGenerationResult.traces | ||
| val graph : Graph = Graph(traceSummaryId, traceSummaryLabel) | ||
|
|
||
|
|
||
| } | ||
| } |