Spor as an xcfa specific algorithm - refactor

ftsrg · Oct 11, 2023 · fdc40cf · fdc40cf
2 parents 5532f72 + 68ade94
commit fdc40cf
Show file tree

Hide file tree

Showing 3 changed files with 215 additions and 293 deletions.
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SporLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SporLts.java
diff --git a/...ects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt b/...ects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt
@@ -23,15 +23,11 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.model.XCFA
 
-class XcfaAasporLts(xcfa: XCFA,
-    private val ignoredVarRegistry: MutableMap<Decl<out Type>, MutableSet<ExprState>>) :
+class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<out Type>, MutableSet<ExprState>>) :
     XcfaSporLts(xcfa) {
 
-    override fun <P : Prec> getEnabledActionsFor(
-        state: XcfaState<*>,
-        exploredActions: Collection<XcfaAction>,
-        prec: P
-    ): Set<XcfaAction> {
+    override fun <P : Prec> getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection<XcfaAction>,
+        prec: P): Set<XcfaAction> {
         // Collecting enabled actions
         val allEnabledActions = getAllEnabledActionsFor(state)
 
@@ -121,8 +117,8 @@ class XcfaAasporLts(xcfa: XCFA,
             return true
         }
         val usedByPersistentSetAction = getCachedUsedSharedObjects(
-            getTransitionOf(persistentSetAction))
-        val influencedSharedObjects = getInfluencedSharedObjects(getTransitionOf(action))
+            getEdgeOf(persistentSetAction))
+        val influencedSharedObjects = getInfluencedSharedObjects(getEdgeOf(action))
         for (varDecl in influencedSharedObjects) {
             if (usedByPersistentSetAction.contains(varDecl)) {
                 if (varDecl !in prec.usedVars) {