Add valToState and biValToAction for XSTS

ftsrg · Jul 30, 2024 · 0dc81f0 · 0dc81f0
1 parent 221cf4a
commit 0dc81f0
Showing 1 changed file with 18 additions and 0 deletions.
diff --git 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<ExplState> {
+    return XstsState.of(
+        ExplState.of(val1),
+        false,
+        true
+    )
+}