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 a92db7f766..938ae566f7 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
@@ -7,7 +7,7 @@ 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.summary.TraceGenerationResult
-import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.TraceGenerationSummaryBuilder
+import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractSummaryBuilder
 import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary
 import hu.bme.mit.theta.common.logging.Logger
 import java.util.function.Consumer
@@ -60,7 +60,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
             }.toList())
 
         assert(!getFullTraces)
-        val summaryBuilder = TraceGenerationSummaryBuilder<S, A>()
+        val summaryBuilder = AbstractSummaryBuilder<S, A>()
         argTraces.forEach { trace -> summaryBuilder.addTrace(trace) }
         val traceSetSummary = summaryBuilder.build()
 
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt
index 78746d9f11..13a5200383 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt
@@ -18,14 +18,13 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary
 
 import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.analysis.Action
-import hu.bme.mit.theta.analysis.PartialOrd
 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
 
-class TraceGenerationSummaryBuilder<S : State, A : Action> {
+class AbstractSummaryBuilder<S : State, A : Action> {
     val argTraces: MutableList<ArgTrace<S, A>> = mutableListOf()
 
     fun addTrace(trace: ArgTrace<S, A>) {
@@ -72,9 +71,9 @@ class TraceGenerationSummaryBuilder<S : State, A : Action> {
 
         // create summary nodes
 
-        val argNodeSummaryNodeMap = mutableMapOf<ArgNode<S, A>, SummaryNode<S, A>>()
+        val argNodeSummaryNodeMap = mutableMapOf<ArgNode<S, A>, AbstractSummaryNode<S, A>>()
         for (nodeGroup in nodeGroups) {
-            val summaryNode = SummaryNode.create(nodeGroup)
+            val summaryNode = AbstractSummaryNode.create(nodeGroup)
             for(node in nodeGroup) {
                 argNodeSummaryNodeMap[node] = summaryNode
             }
@@ -84,20 +83,20 @@ class TraceGenerationSummaryBuilder<S : State, A : Action> {
         checkState(initSummaryNodes.size==1, "Initial arg node must be in exactly 1 summary node!")
         val initNode = initSummaryNodes.get(0)
 
-        val summaryEdges = mutableSetOf<SummaryEdge<S, A>>()
+        val abstractSummaryEdges = mutableSetOf<AbstractSummaryEdge<S, A>>()
         // save edges as well, so we can easily connect edge sources and targets
         for(summaryNode in summaryNodes) {
             for(argNode in summaryNode.argNodes) {
                 for(edge in argNode.outEdges) {
                     if(edge.target in argNodes) {
                         // summary edge adds itself to source and target as well
-                        summaryEdges.add(SummaryEdge.create(edge, summaryNode, argNodeSummaryNodeMap[edge.target]!!))
+                        abstractSummaryEdges.add(AbstractSummaryEdge.create(edge, summaryNode, argNodeSummaryNodeMap[edge.target]!!))
                     }
                 }
             }
         }
 
-        return AbstractTraceSummary(argTraces, summaryEdges, summaryNodes, initNode)
+        return AbstractTraceSummary(argTraces, abstractSummaryEdges, summaryNodes, initNode)
     }
 }
 
@@ -108,28 +107,28 @@ class TraceGenerationSummaryBuilder<S : State, A : Action> {
  */
 data class AbstractTraceSummary<S : State, A : Action> (
     val sourceTraces : Collection<ArgTrace<S, A>>,
-    val summaryEdges : Collection<SummaryEdge<S, A>>,
-    val summaryNodes : Collection<SummaryNode<S, A>>,
-    val initNode : SummaryNode<S, A>
+    val abstractSummaryEdges : Collection<AbstractSummaryEdge<S, A>>,
+    val summaryNodes : Collection<AbstractSummaryNode<S, A>>,
+    val initNode : AbstractSummaryNode<S, A>
     ) : Witness {
 }
 
 /**
  * Groups arg nodes based on coverages, but also stores the traces they appear in, coverage relations and arg nodes
  */
-class SummaryNode<S : State, A: Action> private constructor (val nodeSummaryId: Long,
+class AbstractSummaryNode<S : State, A: Action> private constructor (val id: Long,
                                                              val argNodes: Set<ArgNode<S, A>>,
                                                              val leastOverApproximatedNode : ArgNode<S, A>,
                                                              val mostOverApproximatedNode : ArgNode<S, A>,
                                                             ) {
     // not immutable for edges, as both source and target has to exist when creating edge :c
-    var inEdges : MutableSet<SummaryEdge<S, A>> = mutableSetOf()
-    var outEdges : MutableSet<SummaryEdge<S, A>> = mutableSetOf()
+    var inEdges : MutableSet<AbstractSummaryEdge<S, A>> = mutableSetOf()
+    var outEdges : MutableSet<AbstractSummaryEdge<S, A>> = mutableSetOf()
 
     companion object {
         var counter : Long = 0
 
-        fun <S : State, A : Action> create(argNodes: MutableSet<ArgNode<S, A>>) : SummaryNode<S, A> {
+        fun <S : State, A : Action> create(argNodes: MutableSet<ArgNode<S, A>>) : AbstractSummaryNode<S, A> {
             // all of the nodes should be in some kind of coverage relationship with each other, otherwise, split this summary node
             for(node in argNodes) {
                 for(node2 in argNodes) {
@@ -172,7 +171,7 @@ class SummaryNode<S : State, A: Action> private constructor (val nodeSummaryId:
                 }
             }
 
-            return SummaryNode(counter++, argNodes, leastOverApproximatedNode, mostOverApproximatedNode)
+            return AbstractSummaryNode(counter++, argNodes, leastOverApproximatedNode, mostOverApproximatedNode)
         }
     }
 
@@ -197,27 +196,27 @@ class SummaryNode<S : State, A: Action> private constructor (val nodeSummaryId:
         return getLabel()
     }
 
-    fun addOutEdge(summaryEdge: SummaryEdge<S, A>) {
-        outEdges.add(summaryEdge)
+    fun addOutEdge(abstractSummaryEdge: AbstractSummaryEdge<S, A>) {
+        outEdges.add(abstractSummaryEdge)
     }
 
-    fun addInEdge(summaryEdge: SummaryEdge<S, A>) {
-        inEdges.add(summaryEdge)
+    fun addInEdge(abstractSummaryEdge: AbstractSummaryEdge<S, A>) {
+        inEdges.add(abstractSummaryEdge)
     }
 }
 
-class SummaryEdge<S: State, A: Action> private constructor (
+class AbstractSummaryEdge<S: State, A: Action> private constructor (
     val argEdge: ArgEdge<S, A>,
-    val source: SummaryNode<S, A>,
-    val target: SummaryNode<S, A>,
+    val source: AbstractSummaryNode<S, A>,
+    val target: AbstractSummaryNode<S, A>,
     val action: A = argEdge.action,
 ) {
     companion object {
-        fun <S: State, A: Action> create(argEdge: ArgEdge<S, A>, source : SummaryNode<S, A>, target : SummaryNode<S, A>) : SummaryEdge<S, A> {
-            val summaryEdge = SummaryEdge(argEdge, source, target)
-            source.addOutEdge(summaryEdge)
-            target.addInEdge(summaryEdge)
-            return summaryEdge
+        fun <S: State, A: Action> create(argEdge: ArgEdge<S, A>, source : AbstractSummaryNode<S, A>, target : AbstractSummaryNode<S, A>) : AbstractSummaryEdge<S, A> {
+            val abstractSummaryEdge = AbstractSummaryEdge(argEdge, source, target)
+            source.addOutEdge(abstractSummaryEdge)
+            target.addInEdge(abstractSummaryEdge)
+            return abstractSummaryEdge
         }
     }
 
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt
index c0b97d4824..eb5b8995a2 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt
@@ -20,55 +20,13 @@ import hu.bme.mit.theta.analysis.Action
 import hu.bme.mit.theta.analysis.State
 import hu.bme.mit.theta.core.model.Valuation
 
-class ConcreteSummaryBuilder<S: State, A: Action> {
-    fun build(
-        valuations: MutableMap<SummaryNode<out S, out A>, Valuation>,
-        summary: AbstractTraceSummary<out S, out A>
-    ): ConcreteSummary<Valuation, A> {
-        // TODO check that every node has a valuation?
-        // TODO make valuation into a template type?
-
-        // create nodes (states/valuations)
-        val concreteNodeMap: MutableMap<SummaryNode<out S, out A>, ConcreteSummaryNode<Valuation, A>> = mutableMapOf()
-        for(node in summary.summaryNodes) {
-            concreteNodeMap[node] = ConcreteSummaryNode<Valuation, A>(valuations[node]!!)
-        }
-
-        // create edges (actions)
-        val edges: MutableSet<ConcreteSummaryEdge<Valuation, A>> = mutableSetOf()
-        for((summaryNode, concreteNode) in concreteNodeMap) {
-            for(summaryEdge in summaryNode.outEdges) {
-                edges.add(ConcreteSummaryEdge.create(summaryEdge.action, concreteNode, concreteNodeMap[summaryEdge.target]!!))
-            }
-        }
-
-        // create concrete summary
-        return ConcreteSummary(concreteNodeMap.values.toSet(), edges)
-    }
-}
-
-data class ConcreteSummary<S, A>(val nodes: Set<ConcreteSummaryNode<S, A>>, val edges: Set<ConcreteSummaryEdge<S, A>>)
-
-class ConcreteSummaryNode<S, A>(val state: S) {
-    val inEdges : MutableSet<ConcreteSummaryEdge<S,A>> = mutableSetOf()
-    val outEdges : MutableSet<ConcreteSummaryEdge<S,A>> = mutableSetOf()
-    
-    fun addInEdge(edge: ConcreteSummaryEdge<S, A>) {
-        inEdges.add(edge)
-    }
-
-    fun addOutEdge(edge: ConcreteSummaryEdge<S, A>) {
-        outEdges.add(edge)
-    }
-}
-
-class ConcreteSummaryEdge<S, A> private constructor(val action : A, val source: ConcreteSummaryNode<S, A>, val target: ConcreteSummaryNode<S, A>) {
-    companion object {
-        fun <S, A> create(action: A, source: ConcreteSummaryNode<S, A>, target: ConcreteSummaryNode<S, A>) : ConcreteSummaryEdge<S, A> {
-            val edge = ConcreteSummaryEdge<S, A>(action, source, target)
-            source.addOutEdge(edge)
-            target.addInEdge(edge)
-            return edge
-        }
+class ConcreteSummary<S : State, A: Action>(
+    val valuationMap: MutableMap<AbstractSummaryNode<out S, out A>, Valuation>,
+    val summary: AbstractTraceSummary<out S, out A>
+) {
+    // TODO check that every node has a valuation?
+
+    fun getValuation(node: AbstractSummaryNode<S, A>): Valuation {
+        return valuationMap[node]!!
     }
 }
\ No newline at end of file
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt
index c06377ae1f..e43fd0c150 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt
@@ -49,11 +49,11 @@ class ExprSummaryFwBinItpChecker private constructor(
      * and map of the updated indexings
      */
     fun addNodeToSolver(
-        currentNode: SummaryNode<out ExprState, out ExprAction>,
+        currentNode: AbstractSummaryNode<out ExprState, out ExprAction>,
         A: ItpMarker,
-        indexingMap: MutableMap<SummaryNode<out ExprState, out ExprAction>, VarIndexing>,
-    ) : Pair<Optional<SummaryEdge<out ExprState, out ExprAction>>, MutableMap<SummaryNode<out ExprState, out ExprAction>, VarIndexing>> {
-        var currentIndexingMap : MutableMap<SummaryNode<out ExprState, out ExprAction>, VarIndexing> = indexingMap
+        indexingMap: Map<AbstractSummaryNode<out ExprState, out ExprAction>, VarIndexing>,
+    ) : Pair<Optional<AbstractSummaryEdge<out ExprState, out ExprAction>>, MutableMap<AbstractSummaryNode<out ExprState, out ExprAction>, VarIndexing>> {
+        var currentIndexingMap : MutableMap<AbstractSummaryNode<out ExprState, out ExprAction>, VarIndexing> = indexingMap.toMutableMap()
 
         for (edge in currentNode.outEdges) {
             solver.push()
@@ -104,7 +104,7 @@ class ExprSummaryFwBinItpChecker private constructor(
         Preconditions.checkNotNull(summary)
         val summaryNodeCount = summary.summaryNodes.size
 
-        val indexingMap : MutableMap<SummaryNode<out ExprState, out ExprAction>, VarIndexing> = mutableMapOf()
+        val indexingMap : MutableMap<AbstractSummaryNode<out ExprState, out ExprAction>, VarIndexing> = mutableMapOf()
         indexingMap[summary.initNode] = VarIndexingFactory.indexing(0)
 
         solver.push()
@@ -126,13 +126,12 @@ class ExprSummaryFwBinItpChecker private constructor(
         // concretizable case: we don't have a target, thus we don't even need B in this case
         val status = if (concretizable) {
             val model = solver.model
-            val valuations = mutableMapOf<SummaryNode<out ExprState, out ExprAction>, Valuation>()
+            val valuations = mutableMapOf<AbstractSummaryNode<out ExprState, out ExprAction>, Valuation>()
             for ((node, indexing) in updatedIndexingMap.entries) {
                 valuations[node] = PathUtils.extractValuation(model, indexing)
             }
 
-            val builder = ConcreteSummaryBuilder<ExprState, ExprAction>()
-            val concreteSummary = builder.build(valuations, summary)
+            val concreteSummary = ConcreteSummary(valuations, summary)
             FeasibleExprSummaryStatus(concreteSummary)
         } else {
             checkState(result.first.isPresent, "If summary not concretizable, border edge must be present!")
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt
index dbbef7efe9..b97e4639c2 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt
@@ -24,7 +24,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolType
 
 abstract class ExprSummaryStatus(val feasible : Boolean)
 
-class FeasibleExprSummaryStatus<S : Valuation, A : Action>(val summary : ConcreteSummary<S,A>)
+class FeasibleExprSummaryStatus<S : State, A : Action>(val summary : ConcreteSummary<S,A>)
     : ExprSummaryStatus(true)
 
 class InfeasibleExprSummaryStatus(val itp : Expr<BoolType>) : ExprSummaryStatus(false)
\ No newline at end of file
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt
index 40893facf3..999d40b83e 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt
@@ -53,18 +53,18 @@ object AbstractTraceSummaryVisualizer {
                 .fillColor(fillColor).lineColor(lineColor)
                 .lineStyle(lineStyle).build()
 
-            graph.addNode(stateNodeSummary.nodeSummaryId.toString(), nAttribute)
+            graph.addNode(stateNodeSummary.id.toString(), nAttribute)
         }
 
-        for(summaryEdge in abstractTraceSummary.summaryEdges) {
+        for(summaryEdge in abstractTraceSummary.abstractSummaryEdges) {
             val eAttribute = EdgeAttributes.builder()
                 .label(summaryEdge.getLabel())
                 .color(lineColor)
                 .lineStyle(lineStyle).build()
 
             graph.addEdge(
-                summaryEdge.source.nodeSummaryId.toString(),
-                summaryEdge.target.nodeSummaryId.toString(),
+                summaryEdge.source.id.toString(),
+                summaryEdge.target.id.toString(),
                 eAttribute
             )
         }
diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/TraceGenerationXstsSummaryConcretizerUtil.kt b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/TraceGenerationXstsSummaryConcretizerUtil.kt
index efc63e5eec..6c70c305fb 100644
--- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/TraceGenerationXstsSummaryConcretizerUtil.kt
+++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/TraceGenerationXstsSummaryConcretizerUtil.kt
@@ -1,10 +1,9 @@
 package hu.bme.mit.theta.xsts.analysis.concretizer
 
+import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.analysis.Trace
-import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary
-import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.ExprSummaryStatus
+import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.*
 import hu.bme.mit.theta.analysis.expl.ExplState
-import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.expr.refinement.ExprSummaryFwBinItpChecker
 import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation
 import hu.bme.mit.theta.common.Tuple2
@@ -24,15 +23,29 @@ object TraceGenerationXstsSummaryConcretizerUtil {
         private set
     private var foundInfeasible = false
 
-    fun concretizeSummary(
-        summary: AbstractTraceSummary<XstsState<ExprState>, XstsAction>, solverFactory: SolverFactory, xsts: XSTS
-    ): ExprSummaryStatus {
+    fun concretize(
+        summary: AbstractTraceSummary<XstsState<*>, XstsAction>, solverFactory: SolverFactory, xsts: XSTS
+    ): Map<AbstractSummaryNode<out XstsState<*>, out XstsAction>, XstsState<ExplState>> {
         val varFilter = VarFilter.of(xsts)
         val checker: ExprSummaryFwBinItpChecker = ExprSummaryFwBinItpChecker.create(
             xsts.initFormula, solverFactory.createItpSolver()
         )
+        val status = checker.check(summary)
 
-        return checker.check(summary)
+        checkState(status.feasible, "Summary could not be concretized")
+
+        val concreteSummary = (status as FeasibleExprSummaryStatus<XstsState<*>, XstsAction>).summary
+
+        val xstsStateMap : MutableMap<AbstractSummaryNode<out XstsState<*>, out XstsAction>, XstsState<ExplState>> = mutableMapOf()
+        for ((abstractNode, valuation) in concreteSummary.valuationMap) {
+            xstsStateMap[abstractNode] = XstsState.of<ExplState>(
+                ExplState.of(varFilter.filter(valuation)),
+                abstractNode.getStates().iterator().next().lastActionWasEnv(),
+                abstractNode.getStates().iterator().next().isInitialized()
+            )
+        }
+
+        return xstsStateMap
     }
 
     private fun addToReport(refutation: ItpRefutation, abstractTrace: Trace<XstsState<ExplState>, XstsAction>) {
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 94bf223eaf..954cf1ca54 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
@@ -22,11 +22,10 @@ import com.google.common.base.Stopwatch
 import com.google.common.io.MoreFiles
 import com.google.common.io.RecursiveDeleteOption
 import hu.bme.mit.theta.analysis.*
-import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.AbstractTraceSummary
-import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.ExprSummaryStatus
-import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.InfeasibleExprSummaryStatus
-import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.*
+import hu.bme.mit.theta.analysis.expl.ExplState
 import hu.bme.mit.theta.analysis.utils.AbstractTraceSummaryVisualizer
+import hu.bme.mit.theta.common.Utils
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter
 import hu.bme.mit.theta.solver.SolverManager
@@ -51,25 +50,43 @@ class XstsCliTracegen : XstsCliBaseCommand(
         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 toCexs(summaryStateMap: Map<AbstractSummaryNode<out XstsState<*>, out XstsAction>, XstsState<ExplState>>): String {
+        val sb = Utils.lispStringBuilder(javaClass.simpleName).body()
+
+        for((node, state) in summaryStateMap) {
+            sb.add(Utils.lispStringBuilder("${node.id}: ${XstsState::class.java.simpleName}")
+                .add(if (state.isInitialized) "post_init" else "pre_init")
+                .add(if (state.lastActionWasEnv()) "last_env" else "last_internal").body()
+                .add(state.state.toString()))
+        }
+
+        for(node in summaryStateMap.keys) {
+            for(outEdge in node.outEdges) {
+                sb.add("${node.id} -> ${outEdge.target.id}")
+            }
+        }
+
+        return sb.toString()
+    }
+
     private fun printResult(
-        concretizationResult: ExprSummaryStatus, abstractSummary: AbstractTraceSummary<out State, out Action>, totalTimeMs: Long, traceDirPath: File) {
+        concretizationResult: Map<AbstractSummaryNode<out XstsState<*>, out XstsAction>, XstsState<ExplState>>, abstractSummary: AbstractTraceSummary<out State, out Action>, totalTimeMs: Long, traceDirPath: File) {
         logger.write(Logger.Level.RESULT, "Successfully generated a summary of ${abstractSummary.sourceTraces.size} traces in ${totalTimeMs}ms\n")
         // TODO print coverage (full or not)?
 
         val graph = AbstractTraceSummaryVisualizer.visualize(abstractSummary)
         val visFile = traceDirPath.absolutePath + File.separator + inputOptions.model.name + ".abstract-trace-summary.png"
         GraphvizWriter.getInstance().writeFileAutoConvert(graph, visFile)
-        logger.write(Logger.Level.VERBOSE, "Abstract trace summary was visualized in ${visFile}")
-
-        if(concretizationResult.feasible) {
-            logger.write(Logger.Level.RESULT, "Abstract trace summary successfully concretized\n")
-            val concreteSummaryFile = traceDirPath.absolutePath + File.separator + inputOptions.model.name + ".cexs"
-            TODO("write to file")
-            logger.write(Logger.Level.VERBOSE, "Concrete trace summary exported to ${concreteSummaryFile}")
-        } else {
-            logger.write(Logger.Level.RESULT, "Abstract trace summary was infeasible, could not be concretized\n")
-            logger.write(Logger.Level.RESULT, "Interpolant: ${(concretizationResult as InfeasibleExprSummaryStatus).itp}\n")
+        logger.write(Logger.Level.SUBSTEP, "Abstract trace summary was visualized in ${visFile}")
+
+        val concreteSummaryFile = traceDirPath.absolutePath + File.separator + inputOptions.model.name + ".cexs"
+
+        val cexsString = toCexs(concretizationResult)
+        PrintWriter(File(concreteSummaryFile)).use { printWriter ->
+            printWriter.write(cexsString)
         }
+
+        logger.write(Logger.Level.SUBSTEP, "Concrete trace summary exported to ${concreteSummaryFile}")
     }
 
     override fun run() {
@@ -109,8 +126,8 @@ class XstsCliTracegen : XstsCliBaseCommand(
         val result = checker.check()
 
         // TODO concretization, writing into file
-        val concretizationResult = TraceGenerationXstsSummaryConcretizerUtil.concretizeSummary(
-            result.summary as AbstractTraceSummary<XstsState<ExprState>, XstsAction>, Z3LegacySolverFactory.getInstance(), xsts
+        val concretizationResult = TraceGenerationXstsSummaryConcretizerUtil.concretize(
+            result.summary as AbstractTraceSummary<XstsState<*>, XstsAction>, Z3LegacySolverFactory.getInstance(), xsts
         )
 
         sw.stop()