apply witness removed unnecessary edges

ftsrg · Feb 23, 2025 · b5b5aca · b5b5aca
1 parent f944598
commit b5b5aca
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 13 deletions.
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -50,8 +50,7 @@ import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts
 import hu.bme.mit.theta.xcfa.cli.checkers.getChecker
 import hu.bme.mit.theta.xcfa.cli.params.*
 import hu.bme.mit.theta.xcfa.cli.utils.*
-import hu.bme.mit.theta.xcfa.cli.witnesstransformation.ApplyWitnessPass
-import hu.bme.mit.theta.xcfa.cli.witnesstransformation.NontermValidationPasses
+import hu.bme.mit.theta.xcfa.cli.witnesstransformation.ApplyWitnessPasses
 import hu.bme.mit.theta.xcfa.cli.witnesstransformation.XcfaTraceConcretizer
 import hu.bme.mit.theta.xcfa.getFlatLabels
 import hu.bme.mit.theta.xcfa.model.XCFA
@@ -174,7 +173,7 @@ fun frontend(
 
   val xcfa = getXcfa(config, parseContext, logger, uniqueLogger)
 
-  xcfa.optimizeFurther(NontermValidationPasses(parseContext, logger))
+  xcfa.optimizeFurther(ApplyWitnessPasses(parseContext, logger))
 
   val mcm =
     if (config.inputConfig.catFile != null) {

diff --git a/...cfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesstransformation/ApplyWitnessPass.kt b/...cfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/witnesstransformation/ApplyWitnessPass.kt
@@ -90,29 +90,76 @@ class ApplyWitnessPass(parseContext: ParseContext) : ProcedurePass {
     val allWaypoints = cycleWaypoints + followWaypoints
 
     // collect edges corresponding to recurrence location, cycle and follow waypoints
-    val edgesToKeep = mutableSetOf<XcfaEdge>()
+    val edgesOfWaypoints = mutableSetOf<XcfaEdge>()
     for (wayPoint in allWaypoints) {
       println("witness wp: ${wayPoint.location.line}, ${wayPoint.location.column}")
       for (edge in builder.getEdges()) {
         val edgeMetadata = (edge.metadata as? CMetaData)
         if (edgeMetadata == null) {
-          edgesToKeep.add(edge) // if no metadata, keep it ?
+          edgesOfWaypoints.add(edge) // if no metadata, keep it ?
         }
         if (edgeMetadata != null && edgeMetadata.lineNumberStart == wayPoint.location.line) {
-          if (edgeMetadata.colNumberStart!=null && edgeMetadata.colNumberStart!!+1 == wayPoint.location.column) edgesToKeep.add(edge)
+          if (edgeMetadata.colNumberStart!=null && edgeMetadata.colNumberStart!!+1 == wayPoint.location.column) edgesOfWaypoints.add(edge)
         }
         if (edgeMetadata != null && edgeMetadata.lineNumberStop == wayPoint.location.line) {
-          if (edgeMetadata.colNumberStop!=null && edgeMetadata.colNumberStop!!+1 == wayPoint.location.column) edgesToKeep.add(edge)
+          if (edgeMetadata.colNumberStop!=null && edgeMetadata.colNumberStop!!+1 == wayPoint.location.column) edgesOfWaypoints.add(edge)
         }
       }
     }
 
-    val edgesToDelete = builder.getEdges().filter { edge -> edge !in edgesToKeep }.toSet()
+    // all edges, from which the waypoint edges are not reachable, should be removed
+    val edgesToKeep = mutableSetOf<XcfaEdge>()
+    val dist = floydWarshall(builder.getEdges())
+    for (edgeToKeep in edgesOfWaypoints) {
+      for (edge in builder.getEdges()) {
+        if (dist[edge to edgeToKeep] != -1) {
+          edgesToKeep.add(edge)
+        }
+      }
+    }
+    edgesToKeep.addAll(edgesOfWaypoints)
+
+    val edgesToDelete = builder.getEdges().filter { edge -> edge !in edgesOfWaypoints }.toMutableSet()
 
     for(edge in edgesToDelete) {
       builder.removeEdge(edge)
     }
 
     return builder
   }
+
+  private val inf = -1
+
+  fun floydWarshall(edges: Set<XcfaEdge>): Map<Pair<XcfaEdge, XcfaEdge>, Int> {
+    // Initialize distance map for edges
+    val dist = mutableMapOf<Pair<XcfaEdge, XcfaEdge>, Int>()
+
+    for (edge1 in edges) {
+      for (edge2 in edges) {
+        dist[edge1 to edge2] = if (edge1 == edge2) 0 else inf
+      }
+    }
+
+    // Set initial distances based on connectivity
+    for (edge1 in edges) {
+      for (edge2 in edges) {
+        if (edge1.target == edge2.source) {  // Can transition from edge1 to edge2
+          dist[edge1 to edge2] = 1  // Assuming unit weight
+        }
+      }
+    }
+
+    // Floyd-Warshall Algorithm for edge connectivity
+    for (k in edges) {
+      for (i in edges) {
+        for (j in edges) {
+          if (dist[i to k]!! != inf && dist[k to j]!! != inf) {
+            dist[i to j] = minOf(dist[i to j]!!, dist[i to k]!! + dist[k to j]!!)
+          }
+        }
+      }
+    }
+
+    return dist
+  }
 }
diff --git a/...transformation/NontermValidationPasses.kt → ...tnesstransformation/ApplyWitnessPasses.kt b/...transformation/NontermValidationPasses.kt → ...tnesstransformation/ApplyWitnessPasses.kt
@@ -18,17 +18,17 @@ package hu.bme.mit.theta.xcfa.cli.witnesstransformation
 
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.frontend.ParseContext
-import hu.bme.mit.theta.xcfa.passes.DeterministicPass
-import hu.bme.mit.theta.xcfa.passes.LbePass
-import hu.bme.mit.theta.xcfa.passes.NormalizePass
-import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager
+import hu.bme.mit.theta.xcfa.passes.*
 
-class NontermValidationPasses(
+class ApplyWitnessPasses(
   parseContext: ParseContext,
   uniqueWarningLogger: Logger,
 ) :
   ProcedurePassManager(
     listOf(
+      NormalizePass(), // needed after lbe, TODO
+      DeterministicPass(), // needed after lbe, TODO
+      EliminateSelfLoops(),
       ApplyWitnessPass(parseContext),
       LbePass(parseContext),
       NormalizePass(), // needed after lbe, TODO