xcfa refactor merge

ftsrg · Oct 21, 2023 · 6d33a5a · 6d33a5a
1 parent 6f34fe0
commit 6d33a5a
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt b/...s/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt
@@ -20,8 +20,8 @@ class XcfaAasporCoiLts(
         simpleXcfaLts = coiLTS
     }
 
-    override fun getTransitionOf(action: XcfaAction): XcfaEdge =
-        super.getTransitionOf(action.transFuncVersion ?: action)
+    override fun getEdgeOf(action: XcfaAction): XcfaEdge =
+        super.getEdgeOf(action.transFuncVersion ?: action)
 
     override fun isBackwardAction(action: XcfaAction): Boolean =
         backwardTransitions.any { it.source == action.edge.source && it.target == action.edge.target }

diff --git a/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt b/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt
@@ -64,7 +64,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
     /**
      * Backward transitions in the transition system (a transition of a loop).
      */
-    private val backwardTransitions: MutableSet<XcfaEdge> = mutableSetOf()
+    protected val backwardTransitions: MutableSet<XcfaEdge> = mutableSetOf()
 
     init {
         collectBackwardTransitions()
@@ -312,7 +312,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
      * @param action the action whose edge is to be returned
      * @return the edge of the action
      */
-    protected fun getEdgeOf(action: XcfaAction) = action.edge
+    protected open fun getEdgeOf(action: XcfaAction) = action.edge
 
     /**
      * Returns the outgoing edges of the target of the given edge.
@@ -338,7 +338,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
      * @param action the action to be classified as backward action or non-backward action
      * @return true, if the action is a backward action
      */
-    protected fun isBackwardAction(action: XcfaAction): Boolean = backwardTransitions.contains(getEdgeOf(action))
+    protected open fun isBackwardAction(action: XcfaAction): Boolean = backwardTransitions.contains(getEdgeOf(action))
 
     /**
      * Collects backward edges of the given XCFA.

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
@@ -175,7 +175,6 @@ class XcfaCli(private val args: Array<String>) {
         val gsonForOutput = getGson()
         val logger = ConsoleLogger(logLevel)
         val explicitProperty: ErrorDetection = getExplicitProperty()
-        registerAllSolverManagers(solverHome, logger)
 
         // propagating input variables
         LbePass.level = lbeLevel
@@ -207,6 +206,7 @@ class XcfaCli(private val args: Array<String>) {
         // verification
         stopwatch.reset().start()
         logger.write(Logger.Level.INFO, "Starting verification of ${xcfa.name} using $backend")
+        registerAllSolverManagers(solverHome, logger)
         val config = parseConfigFromCli()
         if (strategy != Strategy.PORTFOLIO && printConfigFile != null) {
             printConfigFile!!.writeText(gsonForOutput.toJson(config))