Fix missing missedPredicateCombinations

tudo-aqua · Oct 25, 2024 · bb14e75 · bb14e75
1 parent 1baa145
commit bb14e75
Show file tree

Hide file tree

Showing 2 changed files with 57 additions and 17 deletions.
diff --git a/.../aqua/stars/core/metric/metrics/postEvaluation/MissedPredicateCombinationsPerTSCMetric.kt b/.../aqua/stars/core/metric/metrics/postEvaluation/MissedPredicateCombinationsPerTSCMetric.kt
@@ -131,17 +131,18 @@ class MissedPredicateCombinationsPerTSCMetric<
     // Create set for storage of all combinations
     val predicateCombinations = mutableSetOf<PredicateCombination>()
     tscInstances.forEach { t ->
-      // Get all TSCEdges that are possible for the current TSCInstance, excluding TSCAlwaysEdges,
-      // as they do not
-      // represent a predicate
-      val allEdgesInValidInstances = t.getAllEdges().filter { it.condition != CONST_TRUE }
+      // Get all traversals that are possible for the current TSCInstance, excluding TSCAlwaysEdges,
+      // as they do not represent a predicate
+      val predicateTraversals =
+          t.traverse()
+              .filter { it.getLeafNodeEdges(it).any { it.tscEdge.condition != CONST_TRUE } }
+              .map { it.toString() }
       // Combine all TSCEdges with each other
-      allEdgesInValidInstances.forEach { edge1 ->
-        allEdgesInValidInstances
-            .filter { it != edge1 }
-            .forEach { edge2 ->
-              predicateCombinations +=
-                  PredicateCombination(edge1.destination.label, edge2.destination.label)
+      predicateTraversals.forEach { predicatePath1 ->
+        predicateTraversals
+            .filter { it != predicatePath1 }
+            .forEach { predicatePath2 ->
+              predicateCombinations += PredicateCombination(predicatePath1, predicatePath2)
             }
       }
     }

diff --git a/stars-core/src/main/kotlin/tools/aqua/stars/core/tsc/instance/TSCInstanceNode.kt b/stars-core/src/main/kotlin/tools/aqua/stars/core/tsc/instance/TSCInstanceNode.kt
@@ -48,14 +48,56 @@ class TSCInstanceNode<
     val monitorResults: Map<String, Boolean> = emptyMap(),
     val value: Any = Unit
 ) {
-
   /** Edges of this [TSCInstanceNode]. */
   val edges: MutableList<TSCInstanceEdge<E, T, S, U, D>> = mutableListOf()
 
   /** Returns all edges. */
   fun getAllEdges(): List<TSCEdge<E, T, S, U, D>> =
       edges.map { it.tscEdge } + edges.flatMap { it.destination.getAllEdges() }
 
+  /** Returns a [List] of all [TSCInstanceNode]s that are leaf nodes in the given [currentNode]. */
+  fun getLeafNodeEdges(
+      currentNode: TSCInstanceNode<E, T, S, U, D>,
+      currentNodeEdge: TSCInstanceEdge<E, T, S, U, D>? = null
+  ): List<TSCInstanceEdge<E, T, S, U, D>> =
+      if (currentNodeEdge == null && currentNode.edges.isEmpty()) {
+        listOf()
+      } else if (currentNodeEdge != null && currentNode.edges.isEmpty()) {
+        listOf(currentNodeEdge)
+      } else {
+        currentNode.edges.flatMap { edge ->
+          edge.destination.getLeafNodeEdges(edge.destination, edge)
+        }
+      }
+
+  /**
+   * Returns a [List] of [TSCInstanceNode]s. Each [TSCInstanceNode] represents one traversal of the
+   * tree.
+   */
+  fun traverse(
+      currentNode: TSCInstanceNode<E, T, S, U, D> = this
+  ): List<TSCInstanceNode<E, T, S, U, D>> =
+      listOf(
+          TSCInstanceNode<E, T, S, U, D>(
+              currentNode.tscNode,
+              currentNode.label,
+              currentNode.monitorResults,
+              currentNode.value)) +
+          if (currentNode.edges.isNotEmpty()) {
+            currentNode.edges.flatMap { edge ->
+              traverse(edge.destination).map { child ->
+                TSCInstanceNode<E, T, S, U, D>(
+                        currentNode.tscNode,
+                        currentNode.label,
+                        currentNode.monitorResults,
+                        currentNode.value)
+                    .apply { this.edges += TSCInstanceEdge<E, T, S, U, D>(child, edge.tscEdge) }
+              }
+            }
+          } else {
+            emptyList()
+          }
+
   /**
    * Validates own (and recursively all children's) successor constraints imposed by the
    * [TSCNode<E,T,S>] types the instances were built from (e.g. exactly one for 'TSCXorNode' or
@@ -123,12 +165,9 @@ class TSCInstanceNode<
       StringBuilder()
           .apply {
             append(if (value is Unit) "\n" else "($value)\n")
-
-            edges.forEach { instanceEdge ->
-              append("  ".repeat(depth))
-              append("--> $label")
-              append(instanceEdge.destination.toString(depth + 1))
-            }
+            append("  ".repeat(depth))
+            append("--> $label")
+            edges.forEach { instanceEdge -> append(instanceEdge.destination.toString(depth + 1)) }
           }
           .toString()