summary concretization and least/most over approx arg node wip

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

@@ -3,10 +3,12 @@ package hu.bme.mit.theta.analysis.algorithm.tracegeneration
 import com.google.common.base.Preconditions
 import hu.bme.mit.theta.analysis.*
 import hu.bme.mit.theta.analysis.algorithm.*
-import hu.bme.mit.theta.analysis.algorithm.SafetyResult
 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.AbstractTraceSummary
 import hu.bme.mit.theta.common.logging.Logger
 import java.util.function.Consumer
 import kotlin.collections.ArrayList
@@ -15,7 +17,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
     private val logger: Logger,
     private val abstractor: Abstractor<S, A, P>,
     private val getFullTraces : Boolean,
-) : Checker<TraceSetSummary<S, A>, P> {
+) : Checker<AbstractTraceSummary<S, A>, P> {
     private var traces: List<Trace<S, A>> = ArrayList()
 
     companion object {
@@ -28,7 +30,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
         }
     }
 
-    override fun check(prec: P): SafetyResult<TraceSetSummary<S, A>, EmptyCex> {
+    override fun check(prec: P): TraceGenerationResult<AbstractTraceSummary<S, A>, S, A> {
         logger.write(Logger.Level.SUBSTEP, "Printing prec for trace generation...\n" + System.lineSeparator())
         logger.write(Logger.Level.SUBSTEP, prec.toString())
 
@@ -37,17 +39,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
 
         logger.write(Logger.Level.SUBSTEP, "ARG done, fetching traces...\n")
 
-        /*
-        logger.write(Logger.Level.SUBSTEP, "Printing ARG to file..." + System.lineSeparator())
-        val g: Graph = ArgVisualizer.getDefault().visualize(arg)
-        try {
-            FileWriter("arg.txt").use { fw ->
-                fw.write(GraphvizWriter.getInstance().writeString(g))
-            }
-        } catch (e: IOException) {
-            throw java.lang.RuntimeException(e)
-        }
-        */
+        // TODO remove xsts specific parts
 
         // bad node: XSTS specific thing, that the last state (last_env nodes) doubles up and the leaf is covered by the
         // last_env before which is superfluous.
@@ -67,31 +59,23 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
                 )
             }.toList())
 
-        // TODO does not work with full traces (see below - modification should be done to arg traces?)
         assert(!getFullTraces)
-        val metadataBuilder = TraceGenerationSummaryBuilder<S, A>()
-        argTraces.forEach { trace -> metadataBuilder.addTrace(trace) }
-        val traceSetSummary = metadataBuilder.build()
+        val summaryBuilder = TraceGenerationSummaryBuilder<S, A>()
+        argTraces.forEach { trace -> summaryBuilder.addTrace(trace) }
+        val traceSetSummary = summaryBuilder.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
-        traces = if (getFullTraces) {
-            // TODO might get stuck on an infinite loop!!
-            logger.write(Logger.Level.SUBSTEP, "Generating full traces....\n")
-            modifyToFullTraces(filteredEndNodes, argTraces)
-        } else {
-            ArrayList(argTraces.stream().map { obj: ArgTrace<S, A> -> obj.toTrace() }
+        traces = ArrayList(argTraces.stream().map { obj: ArgTrace<S, A> -> obj.toTrace() }
                 .toList())
-        }
 
         Preconditions.checkState(
             traces.isNotEmpty(),
             "Generated 0 traces, configuration should probably be adjusted"
         )
         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(traceSetSummary)
+        return TraceGenerationResult(traceSetSummary)
     }
 
     private fun filterEndNodes(
@@ -154,6 +138,7 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
         return coveredEndNodes
     }
 
+/*
     private fun modifyToFullTraces(
         filteredEndNodes: List<ArgNode<S, A>>,
         argTraces: List<ArgTrace<S, A>>
@@ -220,15 +205,18 @@ class TraceGenerationChecker<S : State, A : Action, P : Prec?>(
         }
 
         // adding traces that did not have to be lengthened to the resulting state-action trace list
-        /*
+        */
+/*
         for (ArgTrace<S, A> argTrace : argTraces) {
             if(!crossCoveredEndNodes.contains(argTrace.node(argTrace.nodes().size()-1))) {
                 result.add(argTrace.toTrace());
             }
         }
-        */
+        *//*
+
         return result
     }
+*/
 
     // created for traces that are stored as a list (they are not concatenated yet)
     private fun getLastNode(traceList: List<AdvancedArgTrace<S, A>>): ArgNode<S, A> {

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

@@ -1,3 +1,19 @@
+/*
+ *  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;

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceSetSummary.kt → subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt

@@ -1,4 +1,20 @@
-package hu.bme.mit.theta.analysis.algorithm.tracegeneration
+/*
+ *  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.summary
 
 import com.google.common.base.Preconditions.checkState
 import hu.bme.mit.theta.analysis.Action
@@ -7,16 +23,20 @@ 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
 
 class TraceGenerationSummaryBuilder<S : State, A : Action> {
     val argTraces: MutableList<ArgTrace<S, A>> = mutableListOf()
 
     fun addTrace(trace: ArgTrace<S, A>) {
+        if(argTraces.isNotEmpty()) {
+            checkState(argTraces.get(0).node(0)==trace.node(0), "All traces in summary must start with the same node!")
+        }
         argTraces.add(trace)
     }
 
-    fun build(): TraceSetSummary<S, A> {
+    fun build(): AbstractTraceSummary<S, A> {
+        checkState(argTraces.isNotEmpty(), "Summary must have at least one trace in it!")
+
         val argNodes: Set<ArgNode<S, A>> = argTraces.map { trace -> trace.nodes() }.flatten().toSet()
 
         // grouping nodes covering each other for state summaries
@@ -49,11 +69,14 @@ class TraceGenerationSummaryBuilder<S : State, A : Action> {
             }
         }
 
-        // create state summaries
+        // create summary nodes
         val summaryNodes = mutableSetOf<SummaryNode<S, A>>()
         for (nodeGroup in nodeGroups) {
             summaryNodes.add(SummaryNode.create(nodeGroup))
         }
+        val initSummaryNodes = summaryNodes.filter { summaryNode -> argTraces.get(0).node(0) in summaryNode.argNodes }
+        checkState(initSummaryNodes.size==1, "Initial arg node must be in exactly 1 summary node!")
+        val initNode = initSummaryNodes.get(0)
 
         // save edges as well, so we can easily connect edge sources and targets
         val summaryEdges = mutableSetOf<SummaryEdge<S, A>>()
@@ -74,7 +97,7 @@ class TraceGenerationSummaryBuilder<S : State, A : Action> {
                 }
             }
         }
-        return TraceSetSummary(argTraces, summaryNodes, summaryEdges)
+        return AbstractTraceSummary(argTraces, summaryNodes, summaryEdges, initNode)
     }
 }
 
@@ -83,10 +106,11 @@ class TraceGenerationSummaryBuilder<S : State, A : Action> {
  * 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> (
+data class AbstractTraceSummary<S : State, A : Action> (
     val sourceTraces : Collection<ArgTrace<S, A>>,
     val summaryNodes : Collection<SummaryNode<S, A>>,
-    val summaryEdges : Collection<SummaryEdge<S, A>>
+    val summaryEdges : Collection<SummaryEdge<S, A>>,
+    val initNode : SummaryNode<S, A>
     ) : Witness {
 }
 
@@ -99,16 +123,35 @@ class SummaryNode<S : State, A: Action> private constructor (val nodeSummaryId:
 
         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) {
-                    checkState(
-                        (node == node2) ||
-                        (node.coveringNode.isPresent() && node.coveringNode.get() == node2) ||
-                        (node.coveredNodes.anyMatch { n -> n==node2 })
-                    )
+            var leastOverApproximatedNode : ArgNode<S, A>
+            var mostOverApproximatedNode : ArgNode<S, A>
+
+            val notCoveringNodes = argNodes.filter { argNode -> argNode.coveredNodes.count() == 0L }
+            for(node in notCoveringNodes) {
+                for(node2 in notCoveringNodes) {
+                    TODO() // see comment below - we want to find least over-approximated node
+                }
+            }
+
+            /*
+            public boolean mayCover(final ArgNode<S, A> node) {
+                if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) {
+                    return ancestors().noneMatch(n -> n.equals(node) || n.isSubsumed());
+                } else {
+                    return false;
+                }
+            }
+
+            public boolean mayCoverStandard(final ArgNode<S, A> node) {
+                if (arg.getPartialOrd().isLeq(node.getState(), this.getState())) {
+                    return !(this.equals(node) || this.isSubsumed()); // no need to check ancestors in CEGAR
+                } else {
+                    return false;
                 }
             }
 
+            * */
+
             return SummaryNode(counter++, argNodes)
         }
     }
@@ -123,6 +166,10 @@ class SummaryNode<S : State, A: Action> private constructor (val nodeSummaryId:
             .map { node -> node.inEdge.get() }.toSet()
     }
 
+    fun getStates() : Set<S> {
+        return argNodes.map { argNode -> argNode.state }.toSet()
+    }
+
     fun getLabel() : String {
         val sb = StringBuilder()