basic trace summary and visualization added

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt

@@ -15,7 +15,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
     private val logger: Logger,
     private val abstractor: Abstractor<S, A, P>,
     private val getFullTraces : Boolean,
-) : SafetyChecker<TraceGenerationResult<S, A>, EmptyCex, P> { // TODO refactor templates?
+) : SafetyChecker<TraceSetSummary<S, A>, EmptyCex, P> { // TODO refactor templates?
     private var traces: List<Trace<S, A>> = ArrayList()
 
     companion object {
@@ -28,7 +28,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
         }
     }
 
-    override fun check(prec: P): SafetyResult<TraceGenerationResult<S, A>, EmptyCex> {
+    override fun check(prec: P): SafetyResult<TraceSetSummary<S, A>, 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<S : State, A : Action, P : Prec?>(
         assert(!getFullTraces)
         val metadataBuilder = TraceGenerationSummaryBuilder<S, A>()
         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<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))
+        return SafetyResult.safe(traceSetSummary)
     }
 
     private fun filterEndNodes(

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<S : State, A : Action> {
+class TraceGenerationSummaryBuilder<S : State, A : Action> {
     val argTraces: MutableList<ArgTrace<S, A>> = mutableListOf()
 
     fun addTrace(trace: ArgTrace<S, A>) {
@@ -37,40 +40,64 @@ sealed class TraceGenerationSummaryBuilder<S : State, A : Action> {
                     }
                 ).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<NodeSummary<S, A>>()
+        val summaryNodes = mutableSetOf<SummaryNode<S, A>>()
         for (nodeGroup in nodeGroups) {
-            nodeSummaries.add(NodeSummary.create(nodeGroup))
+            summaryNodes.add(SummaryNode.create(nodeGroup))
         }
 
-        return TraceSetSummary<S, A>(argTraces, nodeSummaries)
+        // save edges as well, so we can easily connect edge sources and targets
+        val summaryEdges = mutableSetOf<SummaryEdge<S, A>>()
+
+        val inEdgeMap = mutableMapOf<ArgEdge<S, A>, SummaryNode<S, A>>()
+        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<S : State, A : Action> 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<S : State, A : Action> (
     val sourceTraces : Collection<ArgTrace<S, A>>,
-    val stateSummaries : Collection<NodeSummary<S, A>>,
-    ) {
-
-    override fun toString(): String {
-        TODO()
-    }
+    val summaryNodes : Collection<SummaryNode<S, A>>,
+    val summaryEdges : Collection<SummaryEdge<S, A>>
+    ) : Witness {
 }
 
 /**
  * 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>>) {
+class SummaryNode<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> {
+        fun <S : State, A : Action> create(argNodes: MutableSet<ArgNode<S, A>>) : SummaryNode<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) {
@@ -82,16 +109,18 @@ class NodeSummary<S : State, A: Action> private constructor (val nodeSummaryId:
                 }
             }
 
-            return NodeSummary(counter++, argNodes)
+            return SummaryNode(counter++, argNodes)
         }
     }
 
-    fun getOutEdges() {
-        TODO()
+    fun getOutEdges(): Set<ArgEdge<S, A>> {
+        return argNodes.map { node -> node.outEdges.toList() }.flatten().toSet()
     }
 
-    fun getInEdges() {
-        TODO()
+    fun getInEdges() : Set<ArgEdge<S, A>> {
+        return argNodes
+            .filter { node -> node.inEdge.isPresent }
+            .map { node -> node.inEdge.get() }.toSet()
     }
 
     fun getLabel() : String {
@@ -110,4 +139,14 @@ class NodeSummary<S : State, A: Action> private constructor (val nodeSummaryId:
     override fun toString(): String {
         return getLabel()
     }
+}
+
+data class SummaryEdge<S : State, A: Action>(
+    val argEdge: ArgEdge<S, A>,
+    val source: SummaryNode<S, A>,
+    val target: SummaryNode<S, A>
+) {
+    fun getLabel() : String {
+        return argEdge.action.toString()
+    }
 }

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<S: State, A: Action> (
-    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<S, A>,
-        traceSummaryId : String = "trace_summary",
-        traceSummaryLabel : String = "Trace Summary",
-        ) {
-        val traces = traceGenerationResult.traces
+    fun <S: State, A: Action> visualize(
+        traceSetSummary: TraceSetSummary<S, A>,
+        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
     }
 }

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<S : State, A : Action, P : Prec?> private constructor(
     private val checker: TraceGenerationChecker<S, A, P>,
     private val prec: P
 ) {
-    fun check(): SafetyResult<TraceGenerationResult<S, A>, EmptyCex> {
+    fun check(): SafetyResult<TraceSetSummary<S, A>, EmptyCex> {
         return checker.check(prec)
     }
 

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<out TraceGenerationResult<out State, out Action>, EmptyCex>, totalTimeMs: Long) {
-        logger.write(Logger.Level.RESULT, "Successfully generated ${status.asSafe().witness.traces.size} traces in ${totalTimeMs}ms")
+    private fun printResult(status: SafetyResult<out TraceSetSummary<out State, out Action>, 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)
     }
 
 }