From 6fd2d6dea1ca7278a2fa52cc882a5692350ef7f1 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sun, 3 Nov 2024 23:21:12 +0100 Subject: [PATCH] fixed parsing of labels --- .../hu/bme/mit/theta/xcfa/model/XcfaLabel.kt | 365 +++++++++--------- .../hu/bme/mit/theta/xcfa/gson/GsonTest.kt | 28 ++ 2 files changed, 216 insertions(+), 177 deletions(-) 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 93f636b306..4e6a2251e0 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 @@ -13,7 +13,6 @@ * See the License for the specific language governing permissions and * limitations under the License. */ - package hu.bme.mit.theta.xcfa.model import hu.bme.mit.theta.common.dsl.Env @@ -30,242 +29,254 @@ import java.util.* sealed class XcfaLabel(open val metadata: MetaData) { - open fun toStmt(): Stmt = Skip() + open fun toStmt(): Stmt = Skip() } -data class InvokeLabel @JvmOverloads constructor( - val name: String, - val params: List>, - override val metadata: MetaData, - val tempLookup: Map, VarDecl<*>> = emptyMap() +data class InvokeLabel +@JvmOverloads +constructor( + val name: String, + val params: List>, + override val metadata: MetaData, + val tempLookup: Map, VarDecl<*>> = emptyMap(), ) : XcfaLabel(metadata) { - override fun toString(): String { - val sj = StringJoiner(", ", "(", ")") - params.forEach { sj.add(it.toString()) } - return "$name$sj" - } - - companion object { - - fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { - val (name, params) = Regex("([^\\(]*)\\((.*)\\)").matchEntire(s)!!.destructured - return InvokeLabel(name, - params.split(",").map { ExpressionWrapper(scope, it).instantiate(env) }, - metadata = metadata) - } + override fun toString(): String { + val sj = StringJoiner(", ", "(", ")") + params.forEach { sj.add(it.toString()) } + return "$name$sj" + } + + companion object { + + fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { + val (name, params) = Regex("^([^(]*)\\((.*)\\)$").matchEntire(s)!!.destructured + return InvokeLabel( + name, + params.split(",").map { ExpressionWrapper(scope, it).instantiate(env) }, + metadata = metadata, + ) } + } } data class ReturnLabel(val enclosedLabel: XcfaLabel) : - XcfaLabel(metadata = enclosedLabel.metadata) { + XcfaLabel(metadata = enclosedLabel.metadata) { - override fun toStmt(): Stmt { - return enclosedLabel.toStmt() - } + override fun toStmt(): Stmt { + return enclosedLabel.toStmt() + } - override fun toString(): String { - return "Return ($enclosedLabel)" - } + override fun toString(): String { + return "Return ($enclosedLabel)" + } } data class StartLabel( - val name: String, - val params: List>, - val pidVar: VarDecl<*>, - override val metadata: MetaData, - val tempLookup: Map, VarDecl<*>> = emptyMap() + val name: String, + val params: List>, + val pidVar: VarDecl<*>, + override val metadata: MetaData, + val tempLookup: Map, VarDecl<*>> = emptyMap(), ) : XcfaLabel(metadata = metadata) { - override fun toString(): String { - val sj = StringJoiner(", ", "(", ")") - params.forEach { sj.add(it.toString()) } - return "$pidVar = start $name$sj" - } - - companion object { - - fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { - val (pidVarName, pidVarType, name, params) = Regex( - "\\(var (.*) (.*)\\) = start (.*)\\((.*)\\)").matchEntire(s)!!.destructured - val pidVar = env.eval(scope.resolve(pidVarName).orElseThrow()) as VarDecl<*> - return StartLabel(name, - params.split(",").map { ExpressionWrapper(scope, it).instantiate(env) }, pidVar, - metadata = metadata) - } + override fun toString(): String { + val sj = StringJoiner(", ", "(", ")") + params.forEach { sj.add(it.toString()) } + return "$pidVar = start $name$sj" + } + + companion object { + + fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { + val (pidVarName, pidVarType, name, params) = + Regex("^\\(var (.*) (.*)\\) = start ([^(]*)\\((.*)\\)$").matchEntire(s)!!.destructured + val pidVar = env.eval(scope.resolve(pidVarName).orElseThrow()) as VarDecl<*> + return StartLabel( + name, + params.split(",").map { ExpressionWrapper(scope, it).instantiate(env) }, + pidVar, + metadata = metadata, + ) } + } } -data class JoinLabel( - val pidVar: VarDecl<*>, - override val metadata: MetaData -) : XcfaLabel(metadata = metadata) { +data class JoinLabel(val pidVar: VarDecl<*>, override val metadata: MetaData) : + XcfaLabel(metadata = metadata) { - override fun toString(): String { - return "join $pidVar" - } + override fun toString(): String { + return "join $pidVar" + } - companion object { + companion object { - fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { - val (pidVarName, pidVarType) = Regex("join \\(var (.*) (.*)\\)").matchEntire( - s)!!.destructured - val pidVar = env.eval(scope.resolve(pidVarName).orElseThrow()) as VarDecl<*> - return JoinLabel(pidVar, metadata = metadata) - } + fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { + val (pidVarName, pidVarType) = + Regex("^join \\(var (.*) (.*)\\)$").matchEntire(s)!!.destructured + val pidVar = env.eval(scope.resolve(pidVarName).orElseThrow()) as VarDecl<*> + return JoinLabel(pidVar, metadata = metadata) } + } } enum class ChoiceType { - NONE, - MAIN_PATH, - ALTERNATIVE_PATH + NONE, + MAIN_PATH, + ALTERNATIVE_PATH, } -data class StmtLabel @JvmOverloads constructor( - val stmt: Stmt, - val choiceType: ChoiceType = ChoiceType.NONE, - override val metadata: MetaData = EmptyMetaData +data class StmtLabel +@JvmOverloads +constructor( + val stmt: Stmt, + val choiceType: ChoiceType = ChoiceType.NONE, + override val metadata: MetaData = EmptyMetaData, ) : XcfaLabel(metadata = metadata) { - init { - check( - stmt !is NonDetStmt && stmt !is SequenceStmt) { "NonDetStmt and SequenceStmt are not supported in XCFA. Use the corresponding labels instead." } - } - - override fun toStmt(): Stmt = stmt - override fun toString(): String { - if (choiceType != ChoiceType.NONE) - return "($stmt)[choiceType=$choiceType]" - else - return stmt.toString() + init { + check(stmt !is NonDetStmt && stmt !is SequenceStmt) { + "NonDetStmt and SequenceStmt are not supported in XCFA. Use the corresponding labels instead." } - - companion object { - - fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { - val matchResult = Regex("\\((.*)\\)\\[choiceType=(.*)]").matchEntire(s) - if (matchResult != null) { - val (stmt, choiceTypeStr) = matchResult.destructured - return StmtLabel(StatementWrapper(stmt, scope).instantiate(env), - choiceType = ChoiceType.valueOf(choiceTypeStr), metadata = metadata) - } else { - return StmtLabel(StatementWrapper(s, scope).instantiate(env), - choiceType = ChoiceType.NONE, metadata = metadata) - } - } + } + + override fun toStmt(): Stmt = stmt + + override fun toString(): String { + if (choiceType != ChoiceType.NONE) return "($stmt)[choiceType=$choiceType]" + else return stmt.toString() + } + + companion object { + + fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { + val matchResult = Regex("^\\((.*)\\)\\[choiceType=(.*)]$").matchEntire(s) + if (matchResult != null) { + val (stmt, choiceTypeStr) = matchResult.destructured + return StmtLabel( + StatementWrapper(stmt, scope).instantiate(env), + choiceType = ChoiceType.valueOf(choiceTypeStr), + metadata = metadata, + ) + } else { + return StmtLabel( + StatementWrapper(s, scope).instantiate(env), + choiceType = ChoiceType.NONE, + metadata = metadata, + ) + } } + } } data class ReadLabel( - val local: VarDecl<*>, - val global: VarDecl<*>, - val labels: Set, - override val metadata: MetaData + val local: VarDecl<*>, + val global: VarDecl<*>, + val labels: Set, + override val metadata: MetaData, ) : XcfaLabel(metadata = metadata) { - override fun toString(): String { - return "R[$local <- $global] @$labels" - } + override fun toString(): String { + return "R[$local <- $global] @$labels" + } } -data class WriteLabel constructor( - val local: VarDecl<*>, - val global: VarDecl<*>, - val labels: Set, - override val metadata: MetaData +data class WriteLabel +constructor( + val local: VarDecl<*>, + val global: VarDecl<*>, + val labels: Set, + override val metadata: MetaData, ) : XcfaLabel(metadata = metadata) { - override fun toString(): String { - return "W[$global <- $local] @$labels" - } + override fun toString(): String { + return "W[$global <- $local] @$labels" + } } -data class FenceLabel( - val labels: Set, - override val metadata: MetaData = EmptyMetaData -) : XcfaLabel(metadata = metadata) { +data class FenceLabel(val labels: Set, override val metadata: MetaData = EmptyMetaData) : + XcfaLabel(metadata = metadata) { - override fun toString(): String { - return "F[${labels.joinToString(";")}]" - } + override fun toString(): String { + return "F[${labels.joinToString(";")}]" + } - companion object { + companion object { - fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { - val (labelList) = Regex("F\\[(.*)]").matchEntire(s)!!.destructured - return FenceLabel(labelList.split(";").toSet(), metadata = metadata) - } + fun fromString(s: String, scope: Scope, env: Env, metadata: MetaData): XcfaLabel { + val (labelList) = Regex("^F\\[(.*)]$").matchEntire(s)!!.destructured + return FenceLabel(labelList.split(";").toSet(), metadata = metadata) } + } } -data class SequenceLabel @JvmOverloads constructor( - val labels: List, - override val metadata: MetaData = EmptyMetaData -) : XcfaLabel(metadata = metadata) { +data class SequenceLabel +@JvmOverloads +constructor(val labels: List, override val metadata: MetaData = EmptyMetaData) : + XcfaLabel(metadata = metadata) { - override fun toStmt(): Stmt { - return SequenceStmt(labels.map { it.toStmt() }) - } + override fun toStmt(): Stmt { + return SequenceStmt(labels.map { it.toStmt() }) + } - override fun toString(): String { - val sj = StringJoiner(",", "[", "]") - labels.forEach { sj.add(it.toString()) } - return sj.toString() - } + override fun toString(): String { + val sj = StringJoiner(",", "[", "]") + labels.forEach { sj.add(it.toString()) } + return sj.toString() + } } -data class NondetLabel @JvmOverloads constructor( - val labels: Set, - override val metadata: MetaData = EmptyMetaData -) : XcfaLabel(metadata = metadata) { +data class NondetLabel +@JvmOverloads +constructor(val labels: Set, override val metadata: MetaData = EmptyMetaData) : + XcfaLabel(metadata = metadata) { - override fun toStmt(): Stmt { - return NonDetStmt(labels.map { it.toStmt() }) - } + override fun toStmt(): Stmt { + return NonDetStmt(labels.map { it.toStmt() }) + } - override fun toString(): String { - return "NonDet($labels)" - } + override fun toString(): String { + return "NonDet($labels)" + } } object NopLabel : XcfaLabel(metadata = EmptyMetaData) { - override fun toStmt(): Stmt { - return Skip() - } + override fun toStmt(): Stmt { + return Skip() + } - override fun toString(): String { - return "Nop" - } + override fun toString(): String { + return "Nop" + } } fun getTempLookup(label: XcfaLabel): Map, VarDecl<*>> { - return when (label) { - is InvokeLabel -> { - label.tempLookup - } - - is StartLabel -> { - label.tempLookup - } - - is SequenceLabel -> { - val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() - for (sublabel in label.labels) { - lookup.putAll(getTempLookup(sublabel)) - } - lookup - } - - is NondetLabel -> { - val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() - for (sublabel in label.labels) { - lookup.putAll(getTempLookup(sublabel)) - } - lookup - } - - else -> emptyMap() + return when (label) { + is InvokeLabel -> { + label.tempLookup } -} \ No newline at end of file + + is StartLabel -> { + label.tempLookup + } + + is SequenceLabel -> { + val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() + for (sublabel in label.labels) { + lookup.putAll(getTempLookup(sublabel)) + } + lookup + } + + is NondetLabel -> { + val lookup: MutableMap, VarDecl<*>> = LinkedHashMap() + for (sublabel in label.labels) { + lookup.putAll(getTempLookup(sublabel)) + } + lookup + } + + else -> emptyMap() + } +} diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt index 161f8a4f1a..23235c44a1 100644 --- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt +++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/gson/GsonTest.kt @@ -106,6 +106,34 @@ class GsonTest { assertEquals(xcfaSource, output) } + @Test + fun testAsyncRoundtrip() { + val xcfaSource = + xcfa("example") { + global { + "x" type Int() init "0" + "thr1" type Int() init "0" + } + procedure("main") { (init to final) { "thr1".start("proc1", "(mod x 0)") } } + procedure("proc1") { (init to final) { assume("true") } } + } + + val symbolTable = XcfaScope(SymbolTable()) + val x_symbol = NamedSymbol("x") + val thr1_symbol = NamedSymbol("thr1") + symbolTable.add(x_symbol) + symbolTable.add(thr1_symbol) + val env = Env() + env.define(x_symbol, xcfaSource.vars.find { it.wrappedVar.name == "x" }!!.wrappedVar) + env.define(thr1_symbol, xcfaSource.vars.find { it.wrappedVar.name == "thr1" }!!.wrappedVar) + val gson = getGson(symbolTable, env, true) + + val output = gson.fromJson(gson.toJson(xcfaSource), XCFA::class.java) + println(xcfaSource) + println(output) + assertEquals(xcfaSource, output) + } + @Test fun testParseContextRoundTrip() { val parseContext = ParseContext()