.cexs can exported, but todos for tracegen with abstraction still pre…

…sent

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()
 

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
         }
     }
 

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]!!
     }
 }

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!")

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)

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
             )
         }

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>) {