diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt index 38cd7085da..562dd1e800 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt +++ b/subprojects/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/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt index 81fe818a3a..b384f1bc25 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt +++ b/subprojects/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, XcfaAction> /** * Backward transitions in the transition system (a transition of a loop). */ - private val backwardTransitions: MutableSet = mutableSetOf() + protected val backwardTransitions: MutableSet = mutableSetOf() init { collectBackwardTransitions() @@ -312,7 +312,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, 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, 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 index 5c6f56c56c..db7c2e1392 100644 --- 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) { 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) { // 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))