EmergenTheta Update

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.7.0"
+    version = "6.8.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt

@@ -22,11 +22,22 @@ import hu.bme.mit.theta.cfa.CFA
 import hu.bme.mit.theta.core.decl.Decls
 import hu.bme.mit.theta.core.model.Valuation
 import hu.bme.mit.theta.core.stmt.*
+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.abstracttype.AbstractExprs.Neq
 import hu.bme.mit.theta.core.type.booltype.BoolExprs.And
-import hu.bme.mit.theta.core.type.inttype.IntExprs.*
+import hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool
+import hu.bme.mit.theta.core.type.booltype.BoolType
+import hu.bme.mit.theta.core.type.bvtype.BvType
+import hu.bme.mit.theta.core.type.fptype.FpExprs.*
+import hu.bme.mit.theta.core.type.fptype.FpType
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr
+import hu.bme.mit.theta.core.type.inttype.IntType
+import hu.bme.mit.theta.core.utils.BvUtils
 import hu.bme.mit.theta.core.utils.StmtUtils
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
+import java.math.BigInteger
 import java.util.*
 
 fun CFA.toMonolithicExpr(): MonolithicExpr {
@@ -36,7 +47,11 @@ fun CFA.toMonolithicExpr(): MonolithicExpr {
   for ((i, x) in this.locs.withIndex()) {
     map[x] = i
   }
-  val locVar = Decls.Var("__loc__", Int())
+  val locVar =
+    Decls.Var(
+      "__loc__",
+      Int(),
+    ) // TODO: add edge var as well, to avoid parallel edges causing problems
   val tranList =
     this.edges
       .map { e ->
@@ -49,15 +64,40 @@ fun CFA.toMonolithicExpr(): MonolithicExpr {
         )
       }
       .toList()
+
+  val defaultValues =
+    this.vars
+      .map {
+        when (it.type) {
+          is IntType -> Eq(it.ref, Int(0))
+          is BoolType -> Eq(it.ref, Bool(false))
+          is BvType ->
+            Eq(
+              it.ref,
+              BvUtils.bigIntegerToNeutralBvLitExpr(BigInteger.ZERO, (it.type as BvType).size),
+            )
+          is FpType -> FpAssign(it.ref as Expr<FpType>, NaN(it.type as FpType))
+          else -> throw IllegalArgumentException("Unsupported type")
+        }
+      }
+      .toList()
+      .let { And(it) }
+
   val trans = NonDetStmt.of(tranList)
   val transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0))
   val transExpr = And(transUnfold.exprs)
-  val initExpr = Eq(locVar.ref, Int(map[this.initLoc]!!))
+  val initExpr = And(Eq(locVar.ref, Int(map[this.initLoc]!!)), defaultValues)
   val propExpr = Neq(locVar.ref, Int(map[this.errorLoc.orElseThrow()]!!))
 
   val offsetIndex = transUnfold.indexing
 
-  return MonolithicExpr(initExpr, transExpr, propExpr, offsetIndex)
+  return MonolithicExpr(
+    initExpr,
+    transExpr,
+    propExpr,
+    offsetIndex,
+    vars = this.vars.toList() + listOf(locVar),
+  )
 }
 
 fun CFA.valToAction(val1: Valuation, val2: Valuation): CfaAction {

subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaMddCheckerTest.java

@@ -0,0 +1,127 @@
+/*
+ *  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.cfa.analysis;
+
+import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Domain.*;
+import static hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement.*;
+
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex;
+import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker;
+import hu.bme.mit.theta.analysis.algorithm.mdd.MddProof;
+import hu.bme.mit.theta.analysis.expr.ExprAction;
+import hu.bme.mit.theta.cfa.CFA;
+import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
+import hu.bme.mit.theta.common.OsHelper;
+import hu.bme.mit.theta.common.logging.ConsoleLogger;
+import hu.bme.mit.theta.common.logging.Logger;
+import hu.bme.mit.theta.common.logging.NullLogger;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
+import hu.bme.mit.theta.solver.SolverFactory;
+import hu.bme.mit.theta.solver.SolverManager;
+import hu.bme.mit.theta.solver.SolverPool;
+import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
+import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager;
+import java.io.FileInputStream;
+import java.util.Arrays;
+import java.util.Collection;
+import org.junit.Assert;
+import org.junit.Assume;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+@RunWith(value = Parameterized.class)
+public class CfaMddCheckerTest {
+
+    @Parameterized.Parameter(value = 0)
+    public String filePath;
+
+    @Parameterized.Parameter(value = 1)
+    public boolean isSafe;
+
+    @Parameterized.Parameters(name = "{index}: {0}, {1}")
+    public static Collection<Object[]> data() {
+        return Arrays.asList(
+                new Object[][] {
+                    {"src/test/resources/arithmetic-bool00.cfa", false},
+                    {"src/test/resources/arithmetic-bool01.cfa", false},
+                    {"src/test/resources/arithmetic-bool10.cfa", false},
+                    {"src/test/resources/arithmetic-bool11.cfa", false},
+                    {"src/test/resources/arithmetic-mod.cfa", true},
+                    {"src/test/resources/counter5_true.cfa", true},
+                    {"src/test/resources/counter_bv_true.cfa", true},
+                    {"src/test/resources/counter_bv_false.cfa", false},
+                    {"src/test/resources/ifelse.cfa", false},
+                });
+    }
+
+    @Test
+    public void test() throws Exception {
+        final Logger logger = new ConsoleLogger(Logger.Level.SUBSTEP);
+
+        SolverManager.registerSolverManager(Z3SolverManager.create());
+        if (OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) {
+            SolverManager.registerSolverManager(
+                    SmtLibSolverManager.create(SmtLibSolverManager.HOME, NullLogger.getInstance()));
+        }
+
+        final SolverFactory solverFactory;
+        try {
+            solverFactory = SolverManager.resolveSolverFactory("Z3");
+        } catch (Exception e) {
+            Assume.assumeNoException(e);
+            return;
+        }
+
+        try {
+            CFA cfa = CfaDslManager.createCfa(new FileInputStream(filePath));
+            var monolithicExpr = CfaToMonolithicExprKt.toMonolithicExpr(cfa);
+
+            final SafetyResult<MddProof, MddCex> status;
+            try (var solverPool = new SolverPool(solverFactory)) {
+                final MddChecker<ExprAction> checker =
+                        MddChecker.create(
+                                monolithicExpr.getInitExpr(),
+                                VarIndexingFactory.indexing(0),
+                                new ExprAction() {
+                                    @Override
+                                    public Expr<BoolType> toExpr() {
+                                        return monolithicExpr.getTransExpr();
+                                    }
+
+                                    @Override
+                                    public VarIndexing nextIndexing() {
+                                        return VarIndexingFactory.indexing(1);
+                                    }
+                                },
+                                monolithicExpr.getPropExpr(),
+                                monolithicExpr.getVars(),
+                                solverPool,
+                                logger,
+                                MddChecker.IterationStrategy.GSAT);
+                status = checker.check(null);
+            }
+
+            Assert.assertEquals(isSafe, status.isSafe());
+        } finally {
+            SolverManager.closeAll();
+        }
+    }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/AbstractMonolithicExpr.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 hu.bme.mit.theta.analysis.algorithm.bounded
+
+import hu.bme.mit.theta.analysis.pred.PredPrec
+import hu.bme.mit.theta.analysis.pred.PredState
+import hu.bme.mit.theta.core.decl.Decl
+import hu.bme.mit.theta.core.decl.Decls
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.model.Valuation
+import hu.bme.mit.theta.core.type.Expr
+import hu.bme.mit.theta.core.type.anytype.Exprs
+import hu.bme.mit.theta.core.type.booltype.BoolExprs
+import hu.bme.mit.theta.core.type.booltype.BoolLitExpr
+import hu.bme.mit.theta.core.type.booltype.BoolType
+import hu.bme.mit.theta.core.type.booltype.IffExpr
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And
+import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not
+import hu.bme.mit.theta.core.utils.ExprUtils
+import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
+import java.util.HashMap
+
+fun MonolithicExpr.createAbstract(prec: PredPrec): MonolithicExpr {
+  // TODO: handle initOffsetIndex in abstract initExpr
+  val lambdaList = ArrayList<IffExpr>()
+  val lambdaPrimeList = ArrayList<IffExpr>()
+  val activationLiterals = ArrayList<VarDecl<*>>()
+  val literalToPred = HashMap<Decl<*>, Expr<BoolType>>()
+
+  prec.preds.forEachIndexed { index, expr ->
+    run {
+      val v = Decls.Var("v$index", BoolType.getInstance())
+      activationLiterals.add(v)
+      literalToPred[v] = expr
+      lambdaList.add(IffExpr.of(v.ref, expr))
+      lambdaPrimeList.add(
+        BoolExprs.Iff(Exprs.Prime(v.ref), ExprUtils.applyPrimes(expr, this.transOffsetIndex))
+      )
+    }
+  }
+
+  var indexingBuilder = VarIndexingFactory.indexingBuilder(1)
+  this.vars
+    .filter { it !in ctrlVars }
+    .forEach { decl ->
+      repeat(transOffsetIndex.get(decl)) { indexingBuilder = indexingBuilder.inc(decl) }
+    }
+
+  return MonolithicExpr(
+    initExpr = And(And(lambdaList), initExpr),
+    transExpr = And(And(lambdaList), And(lambdaPrimeList), transExpr),
+    propExpr = Not(And(And(lambdaList), Not(propExpr))),
+    transOffsetIndex = indexingBuilder.build(),
+    initOffsetIndex = VarIndexingFactory.indexing(0),
+    vars = activationLiterals + ctrlVars,
+    valToState = { valuation: Valuation ->
+      PredState.of(
+        valuation
+          .toMap()
+          .entries
+          .stream()
+          .filter { it.key !in ctrlVars }
+          .map {
+            when ((it.value as BoolLitExpr).value) {
+              true -> literalToPred[it.key]
+              false -> Not(literalToPred[it.key])
+            }
+          }
+          .toList()
+      )
+    },
+    biValToAction = this.biValToAction,
+    ctrlVars = ctrlVars,
+  )
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt

@@ -76,7 +76,7 @@ constructor(
   private val logger: Logger,
 ) : SafetyChecker<EmptyProof, Trace<S, A>, UnitPrec> {
 
-  private val vars = monolithicExpr.vars()
+  private val vars = monolithicExpr.vars
   private val unfoldedInitExpr =
     PathUtils.unfold(monolithicExpr.initExpr, VarIndexingFactory.indexing(0))
   private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/MonolithicExpr.kt

@@ -13,25 +13,36 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
-
 package hu.bme.mit.theta.analysis.algorithm.bounded
 
+import hu.bme.mit.theta.analysis.expl.ExplState
+import hu.bme.mit.theta.analysis.expr.ExprAction
+import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.core.model.Valuation
 import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.utils.ExprUtils.getVars
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
 
-data class MonolithicExpr(
-    val initExpr: Expr<BoolType>,
-    val transExpr: Expr<BoolType>,
-    val propExpr: Expr<BoolType>,
-    val transOffsetIndex: VarIndexing = VarIndexingFactory.indexing(1),
-    val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0)
-) {
+data class MonolithicExpr
+@JvmOverloads
+constructor(
+  val initExpr: Expr<BoolType>,
+  val transExpr: Expr<BoolType>,
+  val propExpr: Expr<BoolType>,
+  val transOffsetIndex: VarIndexing = VarIndexingFactory.indexing(1),
+  val initOffsetIndex: VarIndexing = VarIndexingFactory.indexing(0),
+  val vars: List<VarDecl<*>> =
+    (getVars(initExpr) union getVars(transExpr) union getVars(propExpr)).toList(),
+  val valToState: (Valuation) -> ExprState = ExplState::of,
+  val biValToAction: (Valuation, Valuation) -> ExprAction = { _: Valuation, _: Valuation ->
+    object : ExprAction {
+      override fun toExpr(): Expr<BoolType> = transExpr
 
-    fun vars(): Collection<VarDecl<*>> {
-        return getVars(initExpr) union getVars(transExpr) union getVars(propExpr)
+      override fun nextIndexing(): VarIndexing = transOffsetIndex
     }
-}
+  },
+  val ctrlVars: Collection<VarDecl<*>> = listOf(),
+)