diff --git a/stars-core/src/main/kotlin/tools/aqua/stars/core/metric/metrics/postEvaluation/MissedPredicateCombinationsPerTSCMetric.kt b/stars-core/src/main/kotlin/tools/aqua/stars/core/metric/metrics/postEvaluation/MissedPredicateCombinationsPerTSCMetric.kt index a1858c57..238957b9 100644 --- a/stars-core/src/main/kotlin/tools/aqua/stars/core/metric/metrics/postEvaluation/MissedPredicateCombinationsPerTSCMetric.kt +++ b/stars-core/src/main/kotlin/tools/aqua/stars/core/metric/metrics/postEvaluation/MissedPredicateCombinationsPerTSCMetric.kt @@ -131,17 +131,18 @@ class MissedPredicateCombinationsPerTSCMetric< // Create set for storage of all combinations val predicateCombinations = mutableSetOf() 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 index 0bac345f..c98d0fda 100644 --- 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,7 +48,6 @@ class TSCInstanceNode< val monitorResults: Map = emptyMap(), val value: Any = Unit ) { - /** Edges of this [TSCInstanceNode]. */ val edges: MutableList> = mutableListOf() @@ -56,6 +55,49 @@ class TSCInstanceNode< fun getAllEdges(): List> = 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, + currentNodeEdge: TSCInstanceEdge? = null + ): List> = + 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 = this + ): List> = + listOf( + TSCInstanceNode( + currentNode.tscNode, + currentNode.label, + currentNode.monitorResults, + currentNode.value)) + + if (currentNode.edges.isNotEmpty()) { + currentNode.edges.flatMap { edge -> + traverse(edge.destination).map { child -> + TSCInstanceNode( + currentNode.tscNode, + currentNode.label, + currentNode.monitorResults, + currentNode.value) + .apply { this.edges += TSCInstanceEdge(child, edge.tscEdge) } + } + } + } else { + emptyList() + } + /** * Validates own (and recursively all children's) successor constraints imposed by the * [TSCNode] 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()