From 4120e8c0701cd6ae05a1fafe38f96a845face1b2 Mon Sep 17 00:00:00 2001
From: Daniel Szekeres <szekeresdani@gmail.com>
Date: Thu, 28 Nov 2024 15:21:21 +0100
Subject: [PATCH] draft for rewriting a non-timed xta to xcfa

---
 .../java/hu/bme/mit/theta/xcfa/model/Dsl.kt   | 32 ++++++++++++++++---
 .../hu/bme/mit/theta/xcfa/model/XcfaLabel.kt  |  2 +-
 2 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Dsl.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Dsl.kt
index 90e05c8a19..ca55d4d35f 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Dsl.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Dsl.kt
@@ -24,7 +24,14 @@ import hu.bme.mit.theta.core.stmt.Stmts.*
 import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.LitExpr
 import hu.bme.mit.theta.core.type.Type
+import hu.bme.mit.theta.core.type.booltype.BoolExprs
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool
+import hu.bme.mit.theta.core.type.booltype.BoolLitExpr
 import hu.bme.mit.theta.core.type.booltype.BoolType
+import hu.bme.mit.theta.core.type.inttype.IntExprs
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
+import hu.bme.mit.theta.core.type.inttype.IntLitExpr
+import hu.bme.mit.theta.core.type.inttype.IntType
 import hu.bme.mit.theta.grammar.dsl.SimpleScope
 import hu.bme.mit.theta.grammar.dsl.expr.ExpressionWrapper
 import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager
@@ -36,17 +43,26 @@ class VarContext(val builder: XcfaBuilder, private val local: Boolean) {
 
   infix fun String.type(type: Type): Pair<String, Type> = Pair(this, type)
 
-  infix fun Pair<String, Type>.init(initValue: String): VarDecl<Type> {
+  infix fun Pair<String, Type>.init(initValue: String): VarDecl<Type> =
+    init(ExpressionWrapper(SimpleScope(SymbolTable()), initValue).instantiate(Env()) as LitExpr<*>)
+
+  infix fun Pair<String, Type>.init(initValue: LitExpr<*>): VarDecl<Type> {
     val varDecl = Var(first, second)
     builder.addVar(
       XcfaGlobalVar(
         varDecl,
-        ExpressionWrapper(SimpleScope(SymbolTable()), initValue).instantiate(Env()) as LitExpr<*>,
+        initValue,
         local,
       )
     )
     return varDecl
   }
+
+  fun bool(name: String, initValue: BoolLitExpr) =
+    (name type Bool() init initValue) as VarDecl<BoolType>
+
+  fun int(name: String, initValue: IntLitExpr) =
+    (name type Int() init initValue) as VarDecl<IntType>
 }
 
 fun XcfaProcedureBuilder.lookup(name: String): VarDecl<out Type> =
@@ -105,6 +121,12 @@ class XcfaProcedureBuilderContext(val builder: XcfaProcedureBuilder) {
     return v
   }
 
+  fun bool(name: String) =
+    (name type Bool()) as VarDecl<BoolType>
+
+  fun int(name: String) =
+    (name type Int()) as VarDecl<IntType>
+
   infix fun VarDecl<Type>.direction(direction: ParamDirection): VarDecl<Type> {
     builder.addParam(this, direction)
     return this
@@ -292,8 +314,10 @@ class XcfaProcedureBuilderContext(val builder: XcfaProcedureBuilder) {
   }
 
   infix fun String.to(to: String): (lambda: SequenceLabelContext.() -> SequenceLabel) -> XcfaEdge {
-    val loc1 = locationLut.getOrElse(this) { XcfaLocation(this, metadata = EmptyMetaData) }
-    locationLut.putIfAbsent(this, loc1)
+    val startName = this@XcfaProcedureBuilderContext.builder.name + this
+    val to = this@XcfaProcedureBuilderContext.builder.name + to
+    val loc1 = locationLut.getOrElse(startName) { XcfaLocation(this, metadata = EmptyMetaData) }
+    locationLut.putIfAbsent(startName, loc1)
     builder.addLoc(loc1)
     val loc2 = locationLut.getOrElse(to) { XcfaLocation(to, metadata = EmptyMetaData) }
     locationLut.putIfAbsent(to, loc2)
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt
index 4e6a2251e0..8e8c01f999 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt
@@ -220,7 +220,7 @@ constructor(val labels: List<XcfaLabel>, override val metadata: MetaData = Empty
   }
 
   override fun toString(): String {
-    val sj = StringJoiner(",", "[", "]")
+    val sj = StringJoiner(",\\n", "[", "]")
     labels.forEach { sj.add(it.toString()) }
     return sj.toString()
   }