Using labels instead of edges for variable ordering

ftsrg · Nov 11, 2024 · 37b4d14 · 37b4d14
1 parent c498938
commit 37b4d14
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/...ects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt b/...ects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToMddChecker.kt
@@ -31,6 +31,7 @@ import hu.bme.mit.theta.solver.SolverPool
 import hu.bme.mit.theta.xcfa.analysis.*
 import hu.bme.mit.theta.xcfa.cli.params.*
 import hu.bme.mit.theta.xcfa.cli.utils.getSolver
+import hu.bme.mit.theta.xcfa.getFlatLabels
 import hu.bme.mit.theta.xcfa.model.XCFA
 
 fun getMddChecker(
@@ -63,8 +64,10 @@ fun getMddChecker(
     }
   val safetyProperty = monolithicExpr.propExpr
   val stmts =
-    xcfa.procedures.flatMap { it.edges.map { xcfaEdge -> xcfaEdge.label.toStmt() } }.toSet()
-  val variableOrder = orderVarsFromRandomStartingPoints(monolithicExpr.vars, stmts)
+    xcfa.procedures
+      .flatMap { it.edges.flatMap { xcfaEdge -> xcfaEdge.getFlatLabels().map { it.toStmt() } } }
+      .toSet()
+  val variableOrder = orderVarsFromRandomStartingPoints(monolithicExpr.vars, stmts, 20)
   val solverPool = SolverPool(refinementSolverFactory)
   val iterationStrategy = mddConfig.iterationStrategy