Kotlinizing

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

@@ -21,8 +21,7 @@ import hu.bme.mit.theta.core.utils.changeVars
 
 fun CFA.copyWithReplacingVars(variableMapping: Map<String, VarDecl<*>>): CFA {
     val builder = CFA.builder()
-    val locationMap: Map<String, CFA.Loc> = mutableMapOf(
-        *(locs.map { Pair(it.name, builder.createLoc(it.name)) }.toTypedArray()))
+    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]

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiStatePredicate.java

@@ -0,0 +1,34 @@
+/*
+ *  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.analysis.multi;
+
+import hu.bme.mit.theta.analysis.State;
+
+import java.util.function.Predicate;
+
+public class MultiStatePredicate<LState extends State, RState extends State, DataState extends State> implements Predicate<MultiState<LState, RState, DataState>> {
+
+    private final Predicate<DataState> dataStatePredicate;
+
+    public MultiStatePredicate(Predicate<DataState> dataStatePredicate) {
+        this.dataStatePredicate = dataStatePredicate;
+    }
+
+    @Override
+    public boolean test(MultiState<LState, RState, DataState> multiState) {
+        return dataStatePredicate.test(multiState.getDataState());
+    }
+}

subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiOfTwoTest.kt

@@ -95,7 +95,7 @@ class MultiOfTwoTest {
         FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream ->
             originalCfa = CfaDslManager.createCfa(inputStream)
         }
-        val cfa = originalCfa.copyWithReplacingVars(mapOf(*(variables.map { Pair(it.name, it) }.toTypedArray())))
+        val cfa = originalCfa.copyWithReplacingVars(variables.associateBy { it.name })
         val dataAnalysis = xstsExplBuilder.dataAnalysis
         val cfaAnalysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis)
         val cfaLts: CfaLts = CfaSbeLts.getInstance()
@@ -126,7 +126,7 @@ class MultiOfTwoTest {
                 { llts, cls, rlts, crs, dns -> StmtMultiLts.of(llts, cls, rlts, crs, dns) })
         val prop = Not(xsts.prop)
         val dataPredicate = ExplStatePredicate(prop, solver)
-        val argBuilder = ArgBuilder.create(product.lts, product.analysis) { s -> dataPredicate.test(s.dataState) }
+        val argBuilder = ArgBuilder.create(product.lts, product.analysis, MultiStatePredicate(dataPredicate))
         val abstractor = BasicAbstractor.builder(argBuilder).build()
         val traceChecker = ExprTraceSeqItpChecker.create(True(), prop, itpSolver)
         val precRefiner =
@@ -168,6 +168,7 @@ class MultiOfTwoTest {
         FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream ->
             cfa = CfaDslManager.createCfa(inputStream)
         }
+        cfa = cfa.copyWithReplacingVars(xsts.vars.associateBy { it.name })
         val cfaAnalysis = CfaAnalysis.create(cfa.initLoc, dataAnalysis)
         val cfaLts: CfaLts = CfaSbeLts.getInstance()
         val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc)

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

@@ -20,7 +20,10 @@
 import hu.bme.mit.theta.core.stmt.Stmt;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 
+import java.util.Collection;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 
 /**
@@ -78,4 +81,10 @@ public static StmtUnfoldResult toExpr(final List<? extends Stmt> stmts,
         return StmtToExprTransformer.toExpr(stmts, indexing);
     }
 
+    public static Stmt changeVars(final Stmt stmt, final Collection<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/StmtUtils.kt → subprojects/common/core/src/main/kotlin/hu/bme/mit/theta/core/utils/VarChangerUtils.kt

@@ -33,6 +33,12 @@ fun Stmt.changeVars(variableMapping: Map<String, VarDecl<*>>): Stmt {
         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")
     }
 }

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

@@ -22,9 +22,12 @@ 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 = mutableMapOf(*(varToType.map { Pair(it.key, it.value) }.toTypedArray()))
+    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 = setOf(*(ctrlVars.filter { !variableMapping.containsKey(it.name) }.toTypedArray()), *(variableMapping.filter { it.key in matchingCtrlVarNames }.values.toTypedArray()))
-    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))
+    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))
 }