Added cfa->xcfa via xcfa-cli --input-type CFA

subprojects/xcfa/xcfa-cli/build.gradle.kts

@@ -42,6 +42,7 @@ dependencies {
     implementation(project(":theta-litmus2xcfa"))
     implementation(project(":theta-graph-solver"))
     implementation(project(":theta-cat"))
+    implementation(project(":theta-cfa"))
     implementation(files(rootDir.resolve(Deps.z3legacy)))
     implementation("com.zaxxer:nuprocess:2.0.5")
     implementation("org.jetbrains.kotlin:kotlin-scripting-jsr223:${Versions.kotlin}")

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt

@@ -60,6 +60,7 @@ enum class InputType {
   DSL,
   CHC,
   LITMUS,
+  CFA,
 }
 
 enum class Backend {

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt

@@ -139,6 +139,7 @@ data class FrontendConfig<T : SpecFrontendConfig>(
         InputType.JSON -> null
         InputType.DSL -> null
         InputType.LITMUS -> null
+        InputType.CFA -> null
         InputType.CHC -> CHCFrontendConfig() as T
       }
   }

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt

@@ -16,6 +16,8 @@
 package hu.bme.mit.theta.xcfa.cli.utils
 
 import hu.bme.mit.theta.c2xcfa.getXcfaFromC
+import hu.bme.mit.theta.cfa.CFA
+import hu.bme.mit.theta.cfa.dsl.CfaDslManager
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.frontend.ParseContext
 import hu.bme.mit.theta.frontend.chc.ChcFrontend
@@ -29,13 +31,15 @@ import hu.bme.mit.theta.xcfa.cli.params.CHCFrontendConfig
 import hu.bme.mit.theta.xcfa.cli.params.ExitCodes
 import hu.bme.mit.theta.xcfa.cli.params.InputType
 import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig
-import hu.bme.mit.theta.xcfa.model.XCFA
+import hu.bme.mit.theta.xcfa.model.*
 import hu.bme.mit.theta.xcfa.passes.ChcPasses
+import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager
 import java.io.File
 import java.io.FileInputStream
 import java.io.FileReader
 import javax.script.ScriptEngine
 import javax.script.ScriptEngineManager
+import kotlin.jvm.optionals.getOrNull
 import kotlin.system.exitProcess
 import org.antlr.v4.runtime.CharStreams
 
@@ -81,6 +85,16 @@ fun getXcfa(
         val kotlinEngine: ScriptEngine = ScriptEngineManager().getEngineByExtension("kts")
         kotlinEngine.eval(FileReader(config.inputConfig.input!!)) as XCFA
       }
+
+      InputType.CFA -> {
+        FileInputStream(config.inputConfig.input!!).use { inputStream ->
+          try {
+            return CfaDslManager.createCfa(inputStream).toXcfa()
+          } catch (ex: java.lang.Exception) {
+            throw java.lang.Exception("Could not parse CFA: " + ex.message, ex)
+          }
+        }
+      }
     }
   } catch (e: Exception) {
     if (config.debugConfig.stacktrace) e.printStackTrace()
@@ -90,6 +104,43 @@ fun getXcfa(
     exitProcess(ExitCodes.FRONTEND_FAILED.code)
   }
 
+private fun CFA.toXcfa(): XCFA {
+  val xcfaBuilder = XcfaBuilder("chc")
+  val builder = XcfaProcedureBuilder("main", ProcedurePassManager())
+  this.vars.forEach(builder::addVar)
+
+  builder.createInitLoc()
+  builder.createErrorLoc()
+  builder.createFinalLoc()
+
+  val initLocation = builder.initLoc
+  val errorLocation = builder.errorLoc.get()
+  val finalLocation = builder.finalLoc.get()
+
+  val locs =
+    locs.associateWith {
+      when {
+        this.initLoc == it -> initLocation
+        this.finalLoc.getOrNull() == it -> finalLocation
+        this.errorLoc.getOrNull() == it -> errorLocation
+        else -> XcfaLocation(it.name, metadata = EmptyMetaData).also { builder.addLoc(it) }
+      }
+    }
+  edges.forEach {
+    XcfaEdge(
+        locs[it.source]!!,
+        locs[it.target]!!,
+        StmtLabel(stmt = it.stmt, metadata = EmptyMetaData),
+        metadata = EmptyMetaData,
+      )
+      .apply { builder.addEdge(this) }
+  }
+
+  xcfaBuilder.addProcedure(builder)
+  xcfaBuilder.addEntryPoint(builder, ArrayList())
+  return xcfaBuilder.build()
+}
+
 private fun parseC(
   input: File,
   explicitProperty: ErrorDetection,