From 0dc81f0c51716c2151e2b2395eed57cc04b2343a Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 30 Jul 2024 15:58:26 +0200 Subject: [PATCH] Add valToState and biValToAction for XSTS --- .../src/main/kotlin/XstsToMonolithicExpr.kt | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt index fbc9a65c39..b9b7fe3bd5 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/XstsToMonolithicExpr.kt @@ -15,11 +15,15 @@ */ import hu.bme.mit.theta.analysis.algorithm.bounded.MonolithicExpr +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.core.model.Valuation import hu.bme.mit.theta.core.stmt.Stmts; import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And import hu.bme.mit.theta.core.utils.StmtUtils; import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory; import hu.bme.mit.theta.xsts.XSTS; +import hu.bme.mit.theta.xsts.analysis.XstsAction +import hu.bme.mit.theta.xsts.analysis.XstsState fun XSTS.toMonolithicExpr(): MonolithicExpr { @@ -34,3 +38,17 @@ fun XSTS.toMonolithicExpr(): MonolithicExpr { return MonolithicExpr(initExpr, transExpr, propExpr, transOffsetIndex, initOffsetIndex) } + +fun XSTS.valToAction(val1: Valuation, val2: Valuation): XstsAction { + return XstsAction.create( + Stmts.SequenceStmt(listOf(this.env, this.tran)) + ) +} + +fun XSTS.valToState(val1: Valuation): XstsState { + return XstsState.of( + ExplState.of(val1), + false, + true + ) +} \ No newline at end of file