Tests for multi

settings.gradle.kts

@@ -20,6 +20,7 @@ include(
     "common/common",
     "common/core",
     "common/grammar",
+    "common/multi-tests",
 
     "frontends/c-frontend",
     "frontends/chc-frontend",

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

@@ -0,0 +1,148 @@
+/*
+ * 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.Analysis
+import hu.bme.mit.theta.analysis.InitFunc
+import hu.bme.mit.theta.analysis.LTS
+import hu.bme.mit.theta.analysis.PartialOrd
+import hu.bme.mit.theta.analysis.TransFunc
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.analysis.expr.StmtAction
+import hu.bme.mit.theta.analysis.multi.builder.stmt.StmtMultiBuilder
+import hu.bme.mit.theta.analysis.multi.stmt.ExprMultiState
+import hu.bme.mit.theta.analysis.unit.UnitPrec
+import hu.bme.mit.theta.analysis.unit.UnitState
+import hu.bme.mit.theta.core.stmt.SkipStmt
+import hu.bme.mit.theta.core.stmt.Stmt
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.True
+import hu.bme.mit.theta.core.type.booltype.BoolType
+import org.junit.jupiter.api.Test
+
+
+class MultiAnalysisTest {
+
+    val multiUnitPrec = MultiPrec(UnitPrec.getInstance(), UnitPrec.getInstance(), UnitPrec.getInstance())
+
+    class NumberedState(val num: Int) : ExprState {
+
+        override fun toExpr(): Expr<BoolType?>? = True()
+
+        override fun isBottom(): Boolean = false
+
+    }
+
+    class NumberedAction() : StmtAction() {
+
+        override fun getStmts(): List<Stmt?>? {
+            return listOf(SkipStmt.getInstance())
+        }
+
+    }
+
+    class NumberedAnalysis : Analysis<NumberedState, NumberedAction, UnitPrec> {
+
+        override fun getPartialOrd(): PartialOrd<NumberedState>? =
+            object : PartialOrd<NumberedState> {
+                override fun isLeq(
+                    state1: NumberedState?,
+                    state2: NumberedState?
+                ): Boolean = state1!!.num <= state2!!.num
+
+            }
+
+        override fun getInitFunc(): InitFunc<NumberedState?, UnitPrec?>? =
+            object : InitFunc<NumberedState?, UnitPrec?> {
+                override fun getInitStates(
+                    prec: UnitPrec?
+                ): Collection<NumberedState?>? = listOf<NumberedState>(NumberedState(0))
+
+            }
+
+        override fun getTransFunc(): TransFunc<NumberedState?, NumberedAction?, UnitPrec?>? =
+            object : TransFunc<NumberedState?, NumberedAction?, UnitPrec?> {
+                override fun getSuccStates(
+                    state: NumberedState?,
+                    action: NumberedAction?,
+                    prec: UnitPrec?
+                ): Collection<NumberedState?>? = listOf(NumberedState(state!!.num + 1))
+
+            }
+
+    }
+
+    class NumberedLTS : LTS<NumberedState, NumberedAction> {
+
+        override fun getEnabledActionsFor(
+            state: NumberedState?
+        ): Collection<NumberedAction?>? = listOf(NumberedAction())
+
+    }
+
+    @Test
+    fun test() {
+
+        val side: MultiAnalysisSide<NumberedState, UnitState, NumberedState, NumberedAction, UnitPrec, UnitPrec> =
+            MultiAnalysisSide(
+                NumberedAnalysis(),
+                object : InitFunc<NumberedState, UnitPrec> {
+                    override fun getInitStates(
+                        prec: UnitPrec?
+                    ): Collection<NumberedState?>? = listOf(NumberedState(0))
+                },
+                { c: NumberedState, _: UnitState -> c },
+                { c: NumberedState -> c },
+                { c: NumberedState -> UnitState.getInstance() },
+                { p: UnitPrec -> p }
+            )
+
+        val builderResult = StmtMultiBuilder(side, NumberedLTS())
+            .addRightSide(side, NumberedLTS())
+            .build<UnitPrec>(
+                { ms: ExprMultiState<NumberedState, NumberedState, UnitState> -> if (ms.sourceSide == MultiSide.RIGHT || ms.leftState.num % 2 == 1) MultiSide.LEFT else MultiSide.RIGHT },
+                object : InitFunc<UnitState, UnitPrec> {
+                    override fun getInitStates(
+                        prec: UnitPrec?
+                    ): Collection<UnitState?>? = listOf(UnitState.getInstance())
+                }
+            )
+
+        val multiAnalysis = builderResult.side.analysis
+        val initStates = multiAnalysis.initFunc.getInitStates(multiUnitPrec)
+        val initState = initStates.single()
+
+        assert(initStates.size == 1)
+        assert(initState.leftState.num == 0 && initState.rightState.num == 0)
+
+        var action = builderResult.lts.getEnabledActionsFor(initState).single()
+
+        val succ1State = multiAnalysis.transFunc.getSuccStates(initState, action, multiUnitPrec).single()
+        assert(succ1State.leftState.num == 0 && succ1State.rightState.num == 1)
+        action = builderResult.lts.getEnabledActionsFor(succ1State).single()
+
+        val succ2State = multiAnalysis.transFunc.getSuccStates(succ1State, action, multiUnitPrec).single()
+        assert(succ2State.leftState.num == 1 && succ2State.rightState.num == 1)
+        action = builderResult.lts.getEnabledActionsFor(succ2State).single()
+
+        val succ3State = multiAnalysis.transFunc.getSuccStates(succ2State, action, multiUnitPrec).single()
+        assert(succ3State.leftState.num == 2 && succ3State.rightState.num == 1)
+
+        assert(multiAnalysis.partialOrd.isLeq(succ2State, succ3State))
+
+    }
+
+
+}

subprojects/common/multi-tests/build.gradle.kts

@@ -0,0 +1,30 @@
+/*
+ *  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.
+ */
+plugins {
+    id("kotlin-common")
+}
+
+dependencies {
+    testImplementation(project(":theta-common"))
+    testImplementation(project(":theta-analysis"))
+    testImplementation(project(":theta-core"))
+    testImplementation(project(":theta-solver"))
+    testImplementation(project(":theta-solver-z3-legacy"))
+    testImplementation(project(":theta-cfa"))
+    testImplementation(project(":theta-cfa-analysis"))
+    testImplementation(project(":theta-xsts"))
+    testImplementation(project(":theta-xsts-analysis"))
+}

subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternating3Test.kt

@@ -0,0 +1,96 @@
+/*
+ *  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 multi
+
+import hu.bme.mit.theta.analysis.expl.ExplPrec
+import hu.bme.mit.theta.analysis.expl.ExplStatePredicate
+import hu.bme.mit.theta.analysis.expl.ItpRefToExplPrec
+import hu.bme.mit.theta.analysis.multi.MultiPrec
+import hu.bme.mit.theta.analysis.multi.MultiStatePredicate
+import hu.bme.mit.theta.analysis.multi.NextSideFunctions
+import hu.bme.mit.theta.analysis.multi.RefToMultiPrec
+import hu.bme.mit.theta.analysis.multi.builder.stmt.StmtMultiBuilder
+import hu.bme.mit.theta.analysis.multi.config.StmtMultiConfigBuilder
+import hu.bme.mit.theta.common.logging.ConsoleLogger
+import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.Not
+import hu.bme.mit.theta.solver.Solver
+import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory
+import hu.bme.mit.theta.xsts.XSTS
+import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder
+import hu.bme.mit.theta.xsts.dsl.XstsDslManager
+import org.junit.Test
+import org.junit.jupiter.api.Assertions.assertTrue
+import java.io.FileInputStream
+import java.io.IOException
+import java.io.SequenceInputStream
+
+class MultiAlternating3Test {
+
+    val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP)
+    val solver: Solver = Z3LegacySolverFactory.getInstance().createSolver()
+
+    @Test
+    fun test() {
+        var xsts: XSTS
+        try {
+            SequenceInputStream(
+                FileInputStream("src/test/resources/xsts/incr_double.xsts"),
+                FileInputStream("src/test/resources/xsts/xneq32.prop")
+            ).use { inputStream ->
+                xsts = XstsDslManager.createXsts(inputStream)
+            }
+        } catch (e: IOException) {
+            throw RuntimeException(e)
+        }
+        val variables = xsts.vars
+
+        val xstsConfigBuilder = XstsConfigBuilder(
+            XstsConfigBuilder.Domain.EXPL,
+            XstsConfigBuilder.Refinement.SEQ_ITP,
+            Z3LegacySolverFactory.getInstance(),
+            Z3LegacySolverFactory.getInstance()
+        )
+        val xstsExplBuilder1 = xstsConfigBuilder.ExplStrategy(xsts)
+        val xstsExplBuilder2 = xstsConfigBuilder.ExplStrategy(xsts)
+        val xstsExplBuilder3 = xstsConfigBuilder.ExplStrategy(xsts)
+
+        val dataAnalysis = xstsExplBuilder1.dataAnalysis
+        val dataInitPrec = ExplPrec.of(variables)
+
+        val doubleProduct = StmtMultiBuilder(xstsExplBuilder1.multiSide, xstsExplBuilder1.lts)
+            .addRightSide(xstsExplBuilder2.multiSide, xstsExplBuilder2.lts)
+            .build(NextSideFunctions.Alternating(), dataAnalysis.initFunc)
+        val tripeProduct = StmtMultiBuilder(xstsExplBuilder3.multiSide, xstsExplBuilder3.lts)
+            .addRightSide(doubleProduct.side, doubleProduct.lts)
+            .build(NextSideFunctions.Alternating3(), dataAnalysis.initFunc)
+        val prop = Not(xsts.prop)
+        val dataPredicate = ExplStatePredicate(prop, solver)
+        val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder(
+            tripeProduct, prop,
+            MultiStatePredicate(dataPredicate),
+            ItpRefToExplPrec(), RefToMultiPrec(ItpRefToExplPrec(), ItpRefToExplPrec(), ItpRefToExplPrec()),
+            ItpRefToExplPrec(), dataInitPrec,
+            MultiPrec(dataInitPrec, dataInitPrec, dataInitPrec), dataInitPrec, Z3LegacySolverFactory.getInstance(),
+            logger
+        )
+        val result = multiConfigBuilder.build().check()
+
+        assertTrue(result.isUnsafe)
+
+    }
+}