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 aeaf3d1011..82df0632f2 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 @@ -15,7 +15,7 @@ class TraceGenerationChecker( private val logger: Logger, private val abstractor: Abstractor, private val getFullTraces : Boolean, -) : SafetyChecker, EmptyCex, P> { // TODO refactor templates? +) : SafetyChecker, EmptyCex, P> { // TODO refactor templates? private var traces: List> = ArrayList() companion object { @@ -28,7 +28,7 @@ class TraceGenerationChecker( } } - override fun check(prec: P): SafetyResult, EmptyCex> { + override fun check(prec: P): SafetyResult, EmptyCex> { logger.write(Logger.Level.SUBSTEP, "Printing prec for trace generation...\n" + System.lineSeparator()) logger.write(Logger.Level.SUBSTEP, prec.toString()) @@ -71,7 +71,7 @@ class TraceGenerationChecker( assert(!getFullTraces) val metadataBuilder = TraceGenerationSummaryBuilder() argTraces.forEach { trace -> metadataBuilder.addTrace(trace) } - val traceMetadata = metadataBuilder.build() + val traceSetSummary = metadataBuilder.build() // filter 2, optional, to get full traces even where there is coverage // why?: otherwise we stop at the leaf, which is covered in many traces by other nodes @@ -91,7 +91,7 @@ class TraceGenerationChecker( 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)) + return SafetyResult.safe(traceSetSummary) } private fun filterEndNodes( diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt deleted file mode 100644 index 7fdb7fd089..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationResult.kt +++ /dev/null @@ -1,26 +0,0 @@ -/* - * 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.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.Witness - -data class TraceGenerationResult ( - val traces: Map, TraceSetSummary> -) : Witness diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceSetSummary.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceSetSummary.kt index 38ab5d172f..e665362400 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceSetSummary.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceSetSummary.kt @@ -3,10 +3,13 @@ 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.Witness +import hu.bme.mit.theta.analysis.algorithm.arg.ArgEdge import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode import hu.bme.mit.theta.analysis.algorithm.arg.ArgTrace +import hu.bme.mit.theta.analysis.utils.TraceSummaryVisualizer -sealed class TraceGenerationSummaryBuilder { +class TraceGenerationSummaryBuilder { val argTraces: MutableList> = mutableListOf() fun addTrace(trace: ArgTrace) { @@ -37,40 +40,64 @@ sealed class TraceGenerationSummaryBuilder { } ).toList() - checkState(nodeGroup.size == 1) - - nodeGroup[0].add(node) + checkState(nodeGroup.size <= 1) // either found one where node would fit OR found none and will create new one + if(nodeGroup.size>0) { + nodeGroup[0].add(node) + } else { + nodeGroups.add(mutableSetOf(node)) + } } } // create state summaries - val nodeSummaries = mutableSetOf>() + val summaryNodes = mutableSetOf>() for (nodeGroup in nodeGroups) { - nodeSummaries.add(NodeSummary.create(nodeGroup)) + summaryNodes.add(SummaryNode.create(nodeGroup)) } - return TraceSetSummary(argTraces, nodeSummaries) + // save edges as well, so we can easily connect edge sources and targets + val summaryEdges = mutableSetOf>() + + val inEdgeMap = mutableMapOf, SummaryNode>() + for(summaryNode in summaryNodes) { + for(edge in summaryNode.getInEdges()) { + checkState(!inEdgeMap.containsKey(edge)) + inEdgeMap[edge] = summaryNode + } + } + for(summaryNode in summaryNodes) { + val nodeOutEdges = summaryNode.getOutEdges() + for(nodeOutEdge in nodeOutEdges) { + if(inEdgeMap.containsKey(nodeOutEdge)) { + val targetSummaryNode = inEdgeMap[nodeOutEdge]!! + summaryEdges.add(SummaryEdge(nodeOutEdge, summaryNode, targetSummaryNode)) + } + } + } + return TraceSetSummary(argTraces, summaryNodes, summaryEdges) } } -data class TraceSetSummary constructor( +/** + * This class represents an automata, similar to an ARG, where covered and covering nodes + * are merged into a single node (which we thus call a summary node). + * In some sense this class represents a wrapper level over a set of arg traces. + */ +data class TraceSetSummary ( val sourceTraces : Collection>, - val stateSummaries : Collection>, - ) { - - override fun toString(): String { - TODO() - } + val summaryNodes : Collection>, + val summaryEdges : Collection> + ) : Witness { } /** * Groups arg nodes based on coverages, but also stores the traces they appear in, coverage relations and arg nodes */ -class NodeSummary private constructor (val nodeSummaryId: Long, val argNodes: Set>) { +class SummaryNode private constructor (val nodeSummaryId: Long, val argNodes: Set>) { companion object { var counter : Long = 0 - fun create(argNodes: MutableSet>) : NodeSummary { + fun create(argNodes: MutableSet>) : SummaryNode { // all of the nodes should be in some kind of coverage relationship with each other for(node in argNodes) { for (node2 in argNodes) { @@ -82,16 +109,18 @@ class NodeSummary private constructor (val nodeSummaryId: } } - return NodeSummary(counter++, argNodes) + return SummaryNode(counter++, argNodes) } } - fun getOutEdges() { - TODO() + fun getOutEdges(): Set> { + return argNodes.map { node -> node.outEdges.toList() }.flatten().toSet() } - fun getInEdges() { - TODO() + fun getInEdges() : Set> { + return argNodes + .filter { node -> node.inEdge.isPresent } + .map { node -> node.inEdge.get() }.toSet() } fun getLabel() : String { @@ -110,4 +139,14 @@ class NodeSummary private constructor (val nodeSummaryId: override fun toString(): String { return getLabel() } +} + +data class SummaryEdge( + val argEdge: ArgEdge, + val source: SummaryNode, + val target: SummaryNode +) { + fun getLabel() : String { + return argEdge.action.toString() + } } \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceSummaryVisualizer.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceSummaryVisualizer.kt index ef60c375ca..66604280a6 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceSummaryVisualizer.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/TraceSummaryVisualizer.kt @@ -18,29 +18,57 @@ 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.analysis.algorithm.tracegeneration.TraceSetSummary +import hu.bme.mit.theta.common.visualization.EdgeAttributes import hu.bme.mit.theta.common.visualization.Graph +import hu.bme.mit.theta.common.visualization.LineStyle +import hu.bme.mit.theta.common.visualization.NodeAttributes +import java.awt.Color /** * 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 ( - val stateToString: (S) -> String = { it.toString() }, - val actionToString: (A) -> String = { it.toString() }, - ) { +object TraceSummaryVisualizer { + val lineStyle: LineStyle = LineStyle.NORMAL + val fillColor: Color = Color.WHITE + val lineColor: Color = Color.BLACK // 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, - traceSummaryId : String = "trace_summary", - traceSummaryLabel : String = "Trace Summary", - ) { - val traces = traceGenerationResult.traces + fun visualize( + traceSetSummary: TraceSetSummary, + traceSummaryId: String = "trace_summary", + traceSummaryLabel: String = "Trace Summary", + ) : Graph { val graph : Graph = Graph(traceSummaryId, traceSummaryLabel) + // add nodes + val stateNodeSummaries = traceSetSummary.summaryNodes + for(stateNodeSummary in stateNodeSummaries) { + val nAttribute = NodeAttributes.builder() + .label(stateNodeSummary.getLabel()) + .fillColor(fillColor).lineColor(lineColor) + .lineStyle(lineStyle).build() + graph.addNode(stateNodeSummary.nodeSummaryId.toString(), nAttribute) + } + + for(summaryEdge in traceSetSummary.summaryEdges) { + val eAttribute = EdgeAttributes.builder() + .label(summaryEdge.getLabel()) + .color(lineColor) + .lineStyle(lineStyle).build() + + graph.addEdge( + summaryEdge.source.nodeSummaryId.toString(), + summaryEdge.target.nodeSummaryId.toString(), + eAttribute + ) + } + + return graph } } \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt index 136b47fd7a..28635082bc 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt @@ -6,7 +6,7 @@ import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationChecker -import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationResult +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceSetSummary import hu.bme.mit.theta.analysis.expr.ExprAction import hu.bme.mit.theta.analysis.expr.ExprState import hu.bme.mit.theta.analysis.expr.StmtAction @@ -15,7 +15,7 @@ class XstsTracegenConfig private constructor( private val checker: TraceGenerationChecker, private val prec: P ) { - fun check(): SafetyResult, EmptyCex> { + fun check(): SafetyResult, EmptyCex> { return checker.check(prec) } 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 07660c81d4..3e221d7e8b 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 @@ -16,6 +16,7 @@ package hu.bme.mit.theta.xsts.cli +import com.github.ajalt.clikt.parameters.options.default import com.github.ajalt.clikt.parameters.options.option import com.github.ajalt.clikt.parameters.types.file import com.google.common.base.Stopwatch @@ -26,8 +27,10 @@ import hu.bme.mit.theta.analysis.EmptyCex import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.analysis.State import hu.bme.mit.theta.analysis.algorithm.SafetyResult -import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceGenerationResult +import hu.bme.mit.theta.analysis.algorithm.tracegeneration.TraceSetSummary +import hu.bme.mit.theta.analysis.utils.TraceSummaryVisualizer import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter import hu.bme.mit.theta.solver.SolverManager import hu.bme.mit.theta.solver.z3.Z3SolverFactory import hu.bme.mit.theta.xsts.analysis.tracegeneration.XstsTracegenBuilder @@ -43,14 +46,16 @@ class XstsCliTracegen : XstsCliBaseCommand( help = "Trace generation (instead of verification). Property and input options will be ignored" ) { val traceDir: File? by option( - help = "Directory the traces should be written into. If not specified, traces are written into model directory." - ).file(mustExist = true, canBeFile = false) + help = "Directory the traces should be written into. If not specified, output is written into model-directory/traces." + ).file(mustExist = true, canBeFile = false) // use the non-null value in traceDirPath! - private fun printResult(status: SafetyResult, EmptyCex>, totalTimeMs: Long) { - logger.write(Logger.Level.RESULT, "Successfully generated ${status.asSafe().witness.traces.size} traces in ${totalTimeMs}ms") + private fun printResult(status: SafetyResult, EmptyCex>, totalTimeMs: Long, traceDirPath : File) { + logger.write(Logger.Level.RESULT, "Successfully generated ${status.asSafe().witness.sourceTraces.size} traces in ${totalTimeMs}ms") // TODO print coverage (full or not)? - logger.write(Logger.Level.VERBOSE, "Trace Metadata:") - logger.write(Logger.Level.VERBOSE, status.asSafe().witness.metadata.toString()) + val graph = TraceSummaryVisualizer.visualize(status.asSafe().witness) + val visFile = traceDirPath.absolutePath + File.separator + inputOptions.model.name + ".trace-summary.png" + GraphvizWriter.getInstance().writeFileAutoConvert(graph, visFile) + logger.write(Logger.Level.VERBOSE, "Trace Summary was visualized in ${visFile}:") } override fun run() { @@ -63,16 +68,18 @@ class XstsCliTracegen : XstsCliBaseCommand( } private fun doRun() { + val traceDirPath : File = if(traceDir == null) { + File(inputOptions.model.parent+File.separator+"traces") + } else { traceDir!! } + registerSolverManagers() val solverFactory = SolverManager.resolveSolverFactory(solver) val modelFile = inputOptions.model - val tracePath = modelFile.parent + File.separator + "traces" - val traceDir = File(tracePath) - if (traceDir.exists()) { - MoreFiles.deleteRecursively(traceDir.toPath(), RecursiveDeleteOption.ALLOW_INSECURE) + if (traceDirPath.exists()) { + MoreFiles.deleteRecursively(traceDirPath.toPath(), RecursiveDeleteOption.ALLOW_INSECURE) } - traceDir.mkdir() + traceDirPath.mkdir() val propStream = ByteArrayInputStream( ("prop {\n" + @@ -89,7 +96,7 @@ class XstsCliTracegen : XstsCliBaseCommand( // TODO concretization, writing into file sw.stop() - printResult(result, sw.elapsed(TimeUnit.MILLISECONDS)) + printResult(result, sw.elapsed(TimeUnit.MILLISECONDS), traceDirPath) } } \ No newline at end of file