From de0cfd6930ab4d3cb522d22f08dc00d0deaba6a1 Mon Sep 17 00:00:00 2001 From: RipplB Date: Mon, 4 Mar 2024 15:08:37 +0100 Subject: [PATCH] Tests for multi --- settings.gradle.kts | 1 + .../theta/analysis/multi/MultiAnalysisTest.kt | 148 +++++++++++++++ .../common/multi-tests/build.gradle.kts | 30 +++ .../kotlin/multi/MultiAlternating3Test.kt | 96 ++++++++++ .../test/kotlin/multi/MultiAlternatingTest.kt | 172 ++++++++++++++++++ .../MultiNondetDiningPhilosophersTest.kt | 123 +++++++++++++ .../test/kotlin/multi/MultiSelfProductTest.kt | 88 +++++++++ .../src/test/resources/cfa/doubler.cfa | 7 + .../src/test/resources/cfa/philosopher1.cfa | 67 +++++++ .../src/test/resources/cfa/philosopher2.cfa | 53 ++++++ .../src/test/resources/cfa/philosopher3.cfa | 53 ++++++ .../src/test/resources/cfa/philosopher4.cfa | 53 ++++++ .../src/test/resources/xsts/incr_double.xsts | 11 ++ .../src/test/resources/xsts/incrementor.xsts | 11 ++ .../src/test/resources/xsts/xneq12.prop | 1 + .../src/test/resources/xsts/xneq32.prop | 1 + .../src/test/resources/xsts/xneq7.prop | 1 + 17 files changed, 916 insertions(+) create mode 100644 subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiAnalysisTest.kt create mode 100644 subprojects/common/multi-tests/build.gradle.kts create mode 100644 subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternating3Test.kt create mode 100644 subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt create mode 100644 subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt create mode 100644 subprojects/common/multi-tests/src/test/kotlin/multi/MultiSelfProductTest.kt create mode 100644 subprojects/common/multi-tests/src/test/resources/cfa/doubler.cfa create mode 100644 subprojects/common/multi-tests/src/test/resources/cfa/philosopher1.cfa create mode 100644 subprojects/common/multi-tests/src/test/resources/cfa/philosopher2.cfa create mode 100644 subprojects/common/multi-tests/src/test/resources/cfa/philosopher3.cfa create mode 100644 subprojects/common/multi-tests/src/test/resources/cfa/philosopher4.cfa create mode 100644 subprojects/common/multi-tests/src/test/resources/xsts/incr_double.xsts create mode 100644 subprojects/common/multi-tests/src/test/resources/xsts/incrementor.xsts create mode 100644 subprojects/common/multi-tests/src/test/resources/xsts/xneq12.prop create mode 100644 subprojects/common/multi-tests/src/test/resources/xsts/xneq32.prop create mode 100644 subprojects/common/multi-tests/src/test/resources/xsts/xneq7.prop diff --git a/settings.gradle.kts b/settings.gradle.kts index e13aec1d4a..91b45a0f0e 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -20,6 +20,7 @@ include( "common/common", "common/core", "common/grammar", + "common/multi-tests", "frontends/c-frontend", "frontends/chc-frontend", diff --git a/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiAnalysisTest.kt b/subprojects/common/analysis/src/test/kotlin/hu/bme/mit/theta/analysis/multi/MultiAnalysisTest.kt new file mode 100644 index 0000000000..18e5f6697a --- /dev/null +++ b/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? = True() + + override fun isBottom(): Boolean = false + + } + + class NumberedAction() : StmtAction() { + + override fun getStmts(): List? { + return listOf(SkipStmt.getInstance()) + } + + } + + class NumberedAnalysis : Analysis { + + override fun getPartialOrd(): PartialOrd? = + object : PartialOrd { + override fun isLeq( + state1: NumberedState?, + state2: NumberedState? + ): Boolean = state1!!.num <= state2!!.num + + } + + override fun getInitFunc(): InitFunc? = + object : InitFunc { + override fun getInitStates( + prec: UnitPrec? + ): Collection? = listOf(NumberedState(0)) + + } + + override fun getTransFunc(): TransFunc? = + object : TransFunc { + override fun getSuccStates( + state: NumberedState?, + action: NumberedAction?, + prec: UnitPrec? + ): Collection? = listOf(NumberedState(state!!.num + 1)) + + } + + } + + class NumberedLTS : LTS { + + override fun getEnabledActionsFor( + state: NumberedState? + ): Collection? = listOf(NumberedAction()) + + } + + @Test + fun test() { + + val side: MultiAnalysisSide = + MultiAnalysisSide( + NumberedAnalysis(), + object : InitFunc { + override fun getInitStates( + prec: UnitPrec? + ): Collection? = 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( + { ms: ExprMultiState -> if (ms.sourceSide == MultiSide.RIGHT || ms.leftState.num % 2 == 1) MultiSide.LEFT else MultiSide.RIGHT }, + object : InitFunc { + override fun getInitStates( + prec: UnitPrec? + ): Collection? = 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)) + + } + + +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/build.gradle.kts b/subprojects/common/multi-tests/build.gradle.kts new file mode 100644 index 0000000000..0eb6b08b2b --- /dev/null +++ b/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")) +} diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternating3Test.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternating3Test.kt new file mode 100644 index 0000000000..68e6ed2688 --- /dev/null +++ b/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) + + } +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt new file mode 100644 index 0000000000..e325f3a933 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiAlternatingTest.kt @@ -0,0 +1,172 @@ +/* + * 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.expr.ExprStatePredicate +import hu.bme.mit.theta.analysis.multi.MultiStatePredicate +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +import hu.bme.mit.theta.analysis.multi.builder.stmt.StmtMultiBuilder +import hu.bme.mit.theta.analysis.multi.config.StmtMultiConfigBuilder +import hu.bme.mit.theta.analysis.pred.ExprSplitters +import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec +import hu.bme.mit.theta.analysis.pred.PredPrec +import hu.bme.mit.theta.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.CfaPrec +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.copyWithReplacingVars +import hu.bme.mit.theta.cfa.dsl.CfaDslManager +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.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import java.io.FileInputStream +import java.io.IOException +import java.io.SequenceInputStream + +class MultiAlternatingTest { + + val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP) + val solver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + + @Test + fun testExplPrec() { + var xsts: XSTS + try { + SequenceInputStream( + FileInputStream("src/test/resources/xsts/incrementor.xsts"), + FileInputStream("src/test/resources/xsts/xneq7.prop") + ).use { inputStream -> + xsts = XstsDslManager.createXsts(inputStream) + } + } catch (e: IOException) { + throw RuntimeException(e) + } + + val xstsConfigBuilder = XstsConfigBuilder( + XstsConfigBuilder.Domain.EXPL, + XstsConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + Z3LegacySolverFactory.getInstance() + ) + val xstsExplBuilder = xstsConfigBuilder.ExplStrategy(xsts) + + val variables = xsts.vars + + var originalCfa: CFA + FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> + originalCfa = CfaDslManager.createCfa(inputStream) + } + val cfa = originalCfa.copyWithReplacingVars(variables.associateBy { it.name }) + val cfaConfigBuilder = CfaConfigBuilder( + CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance() + ) + cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfaExplBuilder = cfaConfigBuilder.ExplStrategy(cfa) + + val dataAnalysis = xstsExplBuilder.dataAnalysis + val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), cfa.initLoc) + val dataInitPrec = ExplPrec.of(variables) + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + val product = StmtMultiBuilder(cfaExplBuilder.multiSide, cfaExplBuilder.lts).addRightSide( + xstsExplBuilder.multiSide, xstsExplBuilder.lts + ).build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val prop = Not(xsts.prop) + val dataPredicate = ExplStatePredicate(prop, solver) + val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( + product, prop, + MultiStatePredicate(dataPredicate), + cfaRefToPrec, ItpRefToExplPrec(), ItpRefToExplPrec(), cfaInitPrec, + dataInitPrec, dataInitPrec, Z3LegacySolverFactory.getInstance(), logger + ) + val result = multiConfigBuilder.build().check() + + assertTrue(result.isUnsafe) + assertEquals(8, result.asUnsafe().trace.length()) + } + + @Test + fun testPredPrec() { + var xsts: XSTS + try { + SequenceInputStream( + FileInputStream("src/test/resources/xsts/incrementor.xsts"), + FileInputStream("src/test/resources/xsts/xneq7.prop") + ).use { inputStream -> + xsts = XstsDslManager.createXsts(inputStream) + } + } catch (e: IOException) { + throw RuntimeException(e) + } + + val xstsConfigBuilder = XstsConfigBuilder( + XstsConfigBuilder.Domain.PRED_BOOL, + XstsConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance(), + Z3LegacySolverFactory.getInstance() + ) + val xstsPredBuilder = xstsConfigBuilder.PredStrategy(xsts) + val dataAnalysis = xstsPredBuilder.dataAnalysis + + var cfa: CFA + FileInputStream("src/test/resources/cfa/doubler.cfa").use { inputStream -> + cfa = CfaDslManager.createCfa(inputStream) + } + cfa = cfa.copyWithReplacingVars(xsts.vars.associateBy { it.name }) + val cfaConfigBuilder = CfaConfigBuilder( + CfaConfigBuilder.Domain.PRED_BOOL, + CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance() + ) + cfaConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfaPredBuilder = cfaConfigBuilder.PredStrategy(cfa) + val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToPredPrec(ExprSplitters.atoms()), cfa.initLoc) + val dataInitPrec = PredPrec.of() + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + + val product = StmtMultiBuilder(cfaPredBuilder.multiSide, cfaPredBuilder.lts) + .addRightSide(xstsPredBuilder.multiSide, xstsPredBuilder.lts) + .build( + NextSideFunctions.Alternating(), + dataAnalysis.initFunc + ) + val prop = Not(xsts.prop) + val dataPredicate = ExprStatePredicate(prop, solver) + + val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( + product, prop, + MultiStatePredicate(dataPredicate), + cfaRefToPrec, ItpRefToPredPrec(ExprSplitters.atoms()), ItpRefToPredPrec(ExprSplitters.atoms()), cfaInitPrec, + dataInitPrec, dataInitPrec, Z3LegacySolverFactory.getInstance(), logger + ) + val result = multiConfigBuilder.build().check() + + assertTrue(result.isUnsafe) + } + +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt new file mode 100644 index 0000000000..99ec3898bd --- /dev/null +++ b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt @@ -0,0 +1,123 @@ +/* + * 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.ExplInitFunc +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.cfa.CFA +import hu.bme.mit.theta.cfa.analysis.CfaPrec +import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder +import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec +import hu.bme.mit.theta.cfa.analysis.prec.RefutationToGlobalCfaPrec +import hu.bme.mit.theta.cfa.copyWithReplacingVars +import hu.bme.mit.theta.cfa.dsl.CfaDslManager +import hu.bme.mit.theta.common.logging.ConsoleLogger +import hu.bme.mit.theta.common.logging.Logger +import hu.bme.mit.theta.core.type.Expr +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq +import hu.bme.mit.theta.core.type.booltype.BoolExprs.* +import hu.bme.mit.theta.core.type.booltype.BoolType +import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory +import org.junit.Test +import org.junit.jupiter.api.Assertions +import java.io.FileInputStream + +class MultiNondetDiningPhilosophersTest { + + val logger: Logger = ConsoleLogger(Logger.Level.SUBSTEP) + val solver: Solver = Z3LegacySolverFactory.getInstance().createSolver() + + @Test + fun test() { + var phil1cfa: CFA + FileInputStream("src/test/resources/cfa/philosopher1.cfa").use { inputStream -> + phil1cfa = CfaDslManager.createCfa(inputStream) + } + var phil2rawCfa: CFA + FileInputStream("src/test/resources/cfa/philosopher2.cfa").use { inputStream -> + phil2rawCfa = CfaDslManager.createCfa(inputStream) + } + var phil3rawCfa: CFA + FileInputStream("src/test/resources/cfa/philosopher3.cfa").use { inputStream -> + phil3rawCfa = CfaDslManager.createCfa(inputStream) + } + var phil4rawCfa: CFA + FileInputStream("src/test/resources/cfa/philosopher4.cfa").use { inputStream -> + phil4rawCfa = CfaDslManager.createCfa(inputStream) + } + val variables = phil1cfa.vars + val phil2cfa = phil2rawCfa.copyWithReplacingVars(variables.associateBy { it.name }) + val phil3cfa = phil3rawCfa.copyWithReplacingVars(variables.associateBy { it.name }) + val phil4cfa = phil4rawCfa.copyWithReplacingVars(variables.associateBy { it.name }) + + val cfa1ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance()) + cfa1ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfa1ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil1cfa) + val cfa2ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance()) + cfa2ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfa2ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil2cfa) + val cfa3ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance()) + cfa3ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfa3ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil3cfa) + val cfa4ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP, + Z3LegacySolverFactory.getInstance()) + cfa4ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE) + val cfa4ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil4cfa) + + val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), phil1cfa.initLoc) + val dataInitPrec = ExplPrec.of(variables) + val cfaInitPrec: CfaPrec = GlobalCfaPrec.create(dataInitPrec) + + var initExpr: Expr = True() + variables.filter { it.name.contains("inited") }.forEach { initExpr = Eq(it.ref, False()) } + + val product1 = StmtMultiBuilder(cfa1ExplBuilder.multiSide, cfa1ExplBuilder.lts) + .addRightSide(cfa2ExplBuilder.multiSide, cfa2ExplBuilder.lts) + .build(NextSideFunctions.Nondet(), ExplInitFunc.create(solver, initExpr)) + val product2 = StmtMultiBuilder(cfa3ExplBuilder.multiSide, cfa3ExplBuilder.lts) + .addRightSide(cfa4ExplBuilder.multiSide, cfa4ExplBuilder.lts) + .build(NextSideFunctions.Nondet(), ExplInitFunc.create(solver, initExpr)) + val totalProduct = StmtMultiBuilder(product1.side, product1.lts) + .addRightSide(product2.side, product2.lts) + .build(NextSideFunctions.Nondet(), ExplInitFunc.create(solver, initExpr)) + + var prop: Expr = True() + variables.forEach { prop = And(prop, Eq(it.ref, True())) } + val dataPredicate = ExplStatePredicate(prop, solver) + val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder(totalProduct, prop, + MultiStatePredicate(dataPredicate), + RefToMultiPrec(cfaRefToPrec, cfaRefToPrec, ItpRefToExplPrec()), + RefToMultiPrec(cfaRefToPrec, cfaRefToPrec, ItpRefToExplPrec()), ItpRefToExplPrec(), + MultiPrec(cfaInitPrec, cfaInitPrec, dataInitPrec), + MultiPrec(cfaInitPrec, cfaInitPrec, dataInitPrec), dataInitPrec, Z3LegacySolverFactory.getInstance(), logger) + val result = multiConfigBuilder.build().check() + + Assertions.assertTrue(result.isUnsafe) + } +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiSelfProductTest.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiSelfProductTest.kt new file mode 100644 index 0000000000..5355c57c31 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiSelfProductTest.kt @@ -0,0 +1,88 @@ +/* + * 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.MultiStatePredicate +import hu.bme.mit.theta.analysis.multi.NextSideFunctions +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 MultiSelfProductTest { + + 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/xneq12.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 dataAnalysis = xstsExplBuilder1.dataAnalysis + val dataInitPrec = ExplPrec.of(variables) + + val product = StmtMultiBuilder(xstsExplBuilder1.multiSide, xstsExplBuilder1.lts) + .addRightSide(xstsExplBuilder2.multiSide, xstsExplBuilder2.lts) + .build(NextSideFunctions.Alternating(), dataAnalysis.initFunc) + val prop = Not(xsts.prop) + val dataPredicate = ExplStatePredicate(prop, solver) + val multiConfigBuilder = StmtMultiConfigBuilder.ItpStmtMultiConfigBuilder( + product, prop, + MultiStatePredicate(dataPredicate), + ItpRefToExplPrec(), ItpRefToExplPrec(), ItpRefToExplPrec(), dataInitPrec, + dataInitPrec, dataInitPrec, Z3LegacySolverFactory.getInstance(), logger + ) + val result = multiConfigBuilder.build().check() + + assertTrue(result.isUnsafe) + + } +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/cfa/doubler.cfa b/subprojects/common/multi-tests/src/test/resources/cfa/doubler.cfa new file mode 100644 index 0000000000..1e5e98828a --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/cfa/doubler.cfa @@ -0,0 +1,7 @@ +main process cfa { + var x : int + + init loc L1 + + L1 -> L1 { x := 2 * x } +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/cfa/philosopher1.cfa b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher1.cfa new file mode 100644 index 0000000000..a7e33ad577 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher1.cfa @@ -0,0 +1,67 @@ +main process cfa { + + var fork1 : bool + var fork2 : bool + var fork3 : bool + var fork4 : bool + + var think1 : bool + var think2 : bool + var think3 : bool + var think4 : bool + + var inited : bool + + init loc I + loc Think + loc LFork + loc RFork + loc Eat + + I -> Think { + think1 := true + think2 := true + think3 := true + think4 := true + fork1 := false + fork2 := false + fork3 := false + fork4 := false + inited := true + } + + + Think -> Think + LFork -> LFork + RFork -> RFork + Eat -> Eat + + Think -> LFork { + assume not fork1 + fork1 := true + } + + Think -> RFork { + assume not fork2 + fork2 := true + } + + RFork -> Eat { + assume not fork1 + think1 := false + fork1 := true + } + + LFork -> Eat { + assume not fork2 + think1 := false + fork2 := true + } + + Eat -> Think { + fork1 := false + fork2 := false + think1 := true + } + +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/cfa/philosopher2.cfa b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher2.cfa new file mode 100644 index 0000000000..7c390f4ba2 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher2.cfa @@ -0,0 +1,53 @@ +main process cfa { + + var fork2 : bool + var fork3 : bool + + var think2 : bool + + var inited : bool + + init loc I + loc Think + loc LFork + loc RFork + loc Eat + + I -> Think { + assume inited + } + + Think -> Think + LFork -> LFork + RFork -> RFork + Eat -> Eat + + Think -> LFork { + assume not fork2 + fork2 := true + } + + Think -> RFork { + assume not fork3 + fork3 := true + } + + RFork -> Eat { + assume not fork2 + think2 := false + fork2 := true + } + + LFork -> Eat { + assume not fork3 + think2 := false + fork3 := true + } + + Eat -> Eat { + fork2 := false + fork3 := false + think2 := true + } + +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/cfa/philosopher3.cfa b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher3.cfa new file mode 100644 index 0000000000..13c111289b --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher3.cfa @@ -0,0 +1,53 @@ +main process cfa { + + var fork3 : bool + var fork4 : bool + + var think3 : bool + + var inited : bool + + init loc I + loc Think + loc LFork + loc RFork + loc Eat + + I -> Think { + assume inited + } + + Think -> Think + LFork -> LFork + RFork -> RFork + Eat -> Eat + + Think -> LFork { + assume not fork3 + fork3 := true + } + + Think -> RFork { + assume not fork4 + fork4 := true + } + + RFork -> Eat { + assume not fork3 + think3 := false + fork3 := true + } + + LFork -> Eat { + assume not fork4 + think3 := false + fork4 := true + } + + Eat -> Eat { + fork3 := false + fork4 := false + think3 := true + } + +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/cfa/philosopher4.cfa b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher4.cfa new file mode 100644 index 0000000000..3806da4040 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/cfa/philosopher4.cfa @@ -0,0 +1,53 @@ +main process cfa { + + var fork1 : bool + var fork4 : bool + + var think4 : bool + + var inited : bool + + init loc I + loc Think + loc LFork + loc RFork + loc Eat + + I -> Think { + assume inited + } + + Think -> Think + LFork -> LFork + RFork -> RFork + Eat -> Eat + + Think -> LFork { + assume not fork4 + fork4 := true + } + + Think -> RFork { + assume not fork1 + fork1 := true + } + + RFork -> Eat { + assume not fork4 + think4 := false + fork4 := true + } + + LFork -> Eat { + assume not fork1 + think4 := false + fork1 := true + } + + Eat -> Eat { + fork4 := false + fork1 := false + think4 := true + } + +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/xsts/incr_double.xsts b/subprojects/common/multi-tests/src/test/resources/xsts/incr_double.xsts new file mode 100644 index 0000000000..2268da2ee4 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/xsts/incr_double.xsts @@ -0,0 +1,11 @@ +var x: integer = 1 + +trans { + x:=2*x; +} + +init {} + +env { + x:=x+1; +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/xsts/incrementor.xsts b/subprojects/common/multi-tests/src/test/resources/xsts/incrementor.xsts new file mode 100644 index 0000000000..f52a929c24 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/xsts/incrementor.xsts @@ -0,0 +1,11 @@ +var x: integer = 0 + +trans { + x:=x+1; +} + +init {} + +env { + x:=x+1; +} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/xsts/xneq12.prop b/subprojects/common/multi-tests/src/test/resources/xsts/xneq12.prop new file mode 100644 index 0000000000..4d8ca27e4b --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/xsts/xneq12.prop @@ -0,0 +1 @@ +prop {x!=12} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/xsts/xneq32.prop b/subprojects/common/multi-tests/src/test/resources/xsts/xneq32.prop new file mode 100644 index 0000000000..57df1fd44d --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/xsts/xneq32.prop @@ -0,0 +1 @@ +prop {x!=32} \ No newline at end of file diff --git a/subprojects/common/multi-tests/src/test/resources/xsts/xneq7.prop b/subprojects/common/multi-tests/src/test/resources/xsts/xneq7.prop new file mode 100644 index 0000000000..1bbf116861 --- /dev/null +++ b/subprojects/common/multi-tests/src/test/resources/xsts/xneq7.prop @@ -0,0 +1 @@ +prop {x!=7} \ No newline at end of file