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..b9ae631f31 --- /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(initState, succ3State)) + + } + + +} \ No newline at end of file