Add variable swapping algorithms

Create extension functions for Xsts and CFA which create a copy of a
model by replacing the variables in the parameter.

subprojects/cfa/cfa/build.gradle.kts

@@ -16,6 +16,7 @@
 plugins {
     id("java-common")
     id("antlr-grammar")
+    id("kotlin-common")
 }
 
 dependencies {

subprojects/cfa/cfa/src/main/kotlin/hu/bme/mit/theta/cfa/CFAVarChanger.kt

@@ -0,0 +1,41 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.cfa
+
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.utils.changeVars
+
+/**
+ * Extension function for CFA. Creates a new CFA which looks exactly the same, but any variable whose name is present in
+ * the parameter gets replaced to the associated instance.
+ */
+fun CFA.copyWithReplacingVars(variableMapping: Map<String, VarDecl<*>>): CFA {
+    val builder = CFA.builder()
+    val locationMap: Map<String, CFA.Loc> = locs.associate { it.name to builder.createLoc(it.name) }
+    builder.initLoc = locationMap[initLoc.name]
+    if (errorLoc.isPresent)
+        builder.errorLoc = locationMap[errorLoc.get().name]
+    if (finalLoc.isPresent)
+        builder.finalLoc = locationMap[finalLoc.get().name]
+    edges.forEach {
+        builder.createEdge(
+            locationMap[it.source.name], locationMap[it.target.name],
+            it.stmt.changeVars(variableMapping)
+        )
+    }
+    return builder.build()
+}

subprojects/cfa/cfa/src/test/kotlin/hu/bme/mit/theta/cfa/CFAVarChangerUnitTest.kt

@@ -0,0 +1,40 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.cfa
+
+import hu.bme.mit.theta.cfa.dsl.CfaDslManager
+import hu.bme.mit.theta.core.decl.Decls
+import hu.bme.mit.theta.core.type.inttype.IntType
+import org.junit.jupiter.api.Test
+import java.io.FileInputStream
+
+class CFAVarChangerUnitTest {
+
+    @Test
+    fun `single variable changing`() {
+        var origCfa: CFA
+        FileInputStream("src/test/resources/counter5_true.cfa").use { inputStream ->
+            origCfa = CfaDslManager.createCfa(inputStream)
+        }
+        val newVar = Decls.Var("x", IntType.getInstance())
+        val newCfa = origCfa.copyWithReplacingVars(listOf(newVar).associateBy { it.name })
+
+        assert(!newCfa.vars.any {
+            origCfa.vars.contains(it)
+        })
+        assert(origCfa.vars.iterator().next() != newCfa.vars.iterator().next())
+    }
+}

subprojects/common/core/build.gradle.kts

@@ -17,6 +17,7 @@ plugins {
     id("java-common")
     id("antlr-grammar")
     id("java-test-fixtures")
+    id("kotlin-common")
 }
 
 dependencies {

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/StmtUtils.java

@@ -20,7 +20,9 @@
 import hu.bme.mit.theta.core.stmt.Stmt;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 
 /**
@@ -78,4 +80,10 @@ public static StmtUnfoldResult toExpr(final List<? extends Stmt> stmts,
         return StmtToExprTransformer.toExpr(stmts, indexing);
     }
 
+    public static Stmt changeVars(final Stmt stmt, final Iterable<VarDecl<?>> varDecls) {
+        final Map<String, VarDecl<?>> map = new HashMap<>();
+        varDecls.forEach(varDecl -> map.put(varDecl.getName(), varDecl));
+        return VarChangerUtilsKt.changeVars(stmt, map);
+    }
+
 }

subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt

@@ -0,0 +1,66 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.core.utils
+
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.stmt.*
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.Type
+import hu.bme.mit.theta.core.type.anytype.RefExpr
+import hu.bme.mit.theta.core.utils.TypeUtils.cast
+
+fun Stmt.changeVars(variableMapping: Map<String, VarDecl<*>>): Stmt {
+    return when (this) {
+        is AssignStmt<*> -> AssignStmt.of(
+            cast(varDecl.changeVars(variableMapping), varDecl.type),
+            cast(expr.changeVars(variableMapping), varDecl.type)
+        )
+
+        is HavocStmt<*> -> HavocStmt.of(varDecl.changeVars(variableMapping))
+        is AssumeStmt -> AssumeStmt.of(cond.changeVars(variableMapping))
+        is SequenceStmt -> SequenceStmt.of(stmts.map { it.changeVars(variableMapping) })
+        is SkipStmt -> this
+        is NonDetStmt -> NonDetStmt.of(stmts.map { it.changeVars(variableMapping) })
+        is LoopStmt -> LoopStmt.of(
+            stmt.changeVars(variableMapping), loopVariable.changeVars(variableMapping),
+            from.changeVars(variableMapping), to.changeVars(variableMapping)
+        )
+
+        is IfStmt -> IfStmt.of(
+            cond.changeVars(variableMapping), then.changeVars(variableMapping),
+            elze.changeVars(variableMapping)
+        )
+
+        else -> TODO("Not yet implemented")
+    }
+}
+
+fun <T : Type> Expr<T>.changeVars(variableMapping: Map<String, VarDecl<*>>): Expr<T> =
+    if (this is RefExpr<T>) {
+        when (this.decl) {
+            is VarDecl<T> -> (this.decl as VarDecl<T>).changeVars(variableMapping).ref
+            else -> this
+        }
+    } else this.withOps(this.ops.map { it.changeVars(variableMapping) })
+
+@SuppressWarnings("kotlin:S6530")
+fun <T : Type> VarDecl<T>.changeVars(variableMapping: Map<String, VarDecl<*>>): VarDecl<T> {
+    val swap = variableMapping[this.name] ?: return this
+    if (swap.type != this.type)
+        throw RuntimeException("Can't change variable to different type")
+    return swap as VarDecl<T>
+}

subprojects/xsts/xsts/build.gradle.kts

@@ -16,6 +16,7 @@
 plugins {
     id("java-common")
     id("antlr-grammar")
+    id("kotlin-common")
 }
 
 dependencies {

subprojects/xsts/xsts/src/main/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChanger.kt

@@ -0,0 +1,33 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.xsts.utils
+
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.stmt.NonDetStmt
+import hu.bme.mit.theta.core.utils.changeVars
+import hu.bme.mit.theta.xsts.XSTS
+
+fun XSTS.copyWithReplacingVars(variableMapping: Map<String, VarDecl<*>>): XSTS {
+    val newVarToType = varToType.toMutableMap()
+    variableMapping.forEach { (name, varDecl) -> newVarToType[varDecl] = varToType[vars.find { it.name == name }] }
+    val matchingCtrlVarNames = ctrlVars.filter { variableMapping.containsKey(it.name) }.map { it.name }
+    val newCtrlVars = ctrlVars.filter { it.name !in variableMapping }
+        .toSet() + variableMapping.filter { it.key in matchingCtrlVarNames }.values.toSet()
+    return XSTS(newVarToType, newCtrlVars, init.changeVars(variableMapping) as NonDetStmt,
+        tran.changeVars(variableMapping) as NonDetStmt, env.changeVars(variableMapping) as NonDetStmt,
+        initFormula.changeVars(variableMapping), prop.changeVars(variableMapping))
+}

subprojects/xsts/xsts/src/test/kotlin/hu/bme/mit/theta/xsts/utils/XSTSVarChangerUnitTest.kt

@@ -0,0 +1,56 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xsts.utils
+
+import hu.bme.mit.theta.core.decl.Decls
+import hu.bme.mit.theta.core.type.inttype.IntType
+import hu.bme.mit.theta.core.utils.StmtUtils
+import hu.bme.mit.theta.xsts.XSTS
+import hu.bme.mit.theta.xsts.dsl.XstsDslManager
+import org.junit.jupiter.api.Test
+import java.io.FileInputStream
+
+class XSTSVarChangerUnitTest {
+
+    @Test
+    fun `xsts variable changing`() {
+        var origXsts: XSTS
+        FileInputStream("src/test/resources/incrementors.xsts").use { inputStream ->
+            origXsts = XstsDslManager.createXsts(inputStream)
+        }
+        val newX = Decls.Var("x", IntType.getInstance())
+        val newY = Decls.Var("y", IntType.getInstance())
+        val newXsts = origXsts.copyWithReplacingVars(
+            listOf(newX, newY)
+                .associateBy { it.name }
+        )
+
+        val origVars = setOf(
+            StmtUtils.getVars(origXsts.init),
+            StmtUtils.getVars(origXsts.tran),
+            StmtUtils.getVars(origXsts.env)
+        )
+        val newVars = setOf(
+            StmtUtils.getVars(newXsts.init),
+            StmtUtils.getVars(newXsts.tran),
+            StmtUtils.getVars(newXsts.env)
+        )
+
+        assert(!newVars.any {
+            origVars.contains(it)
+        })
+    }
+}

subprojects/xsts/xsts/src/test/resources/incrementors.xsts

@@ -0,0 +1,16 @@
+var x: integer = 0
+ctrl var y: integer
+
+trans {
+    x:=x+1;
+}
+
+init {
+    y:=0;
+}
+
+env {
+    x:=x+1;
+}
+
+prop {true}