draft for rewriting a non-timed xta to xcfa

ftsrg · Nov 28, 2024 · 4120e8c · 4120e8c
1 parent bd69e1c
commit 4120e8c
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 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
@@ -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
@@ -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()
   }