From 6d33a5af5bf8bd707b8273846fdac3577fa270cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Sat, 21 Oct 2023 11:39:54 +0200 Subject: [PATCH] xcfa refactor merge --- .../hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt | 4 ++-- .../java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt | 6 +++--- .../src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) 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))