MDD look-ahead optimizations

.github/actions/benchexec-test/action.yml

@@ -50,7 +50,7 @@ runs:
         cat "$XML"
 
         folder=$(dirname $(find . -name "theta.jar" | head -n1))
-        benchexec "$XML" -n 2 --no-container --tool-directory "$folder"
+        benchexec "$XML" -n 2 --tool-directory "$folder"
     - name: Upload results
       uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
       with:

.github/actions/zenodo-release/action.yml

@@ -3,6 +3,8 @@ description: 'Create release and deploy to zenodo'
 inputs:
     tool:
         required: true
+    artifact:
+        required: true
     prevrecord:
         required: true
     token:
@@ -15,7 +17,7 @@ runs:
         fetch-depth: 0
     - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v3.0.2
       with:
-        name: ${{inputs.tool}}
+        name: ${{inputs.artifact}}
         path: upload/
 
     - name: Set up Python

.github/workflows/linux-build-test-deploy.yml

@@ -253,25 +253,29 @@ jobs:
     runs-on: ubuntu-24.04
     strategy:
       matrix:
-        tool: [Theta, EmergenTheta, Thorn, ThetaCHC]
         include:
-          - tool: Theta-svcomp
+          - tool: Theta
+            artifact: Theta-svcomp
             record: 14194483
-          - tool: EmergenTheta-svcomp
+          - tool: EmergenTheta
+            artifact: EmergenTheta-svcomp
             record: 15536866
-          - tool: Thorn-svcomp
+          - tool: Thorn
+            artifact: Thorn-svcomp
             record: 14194485
-          - tool: Theta-chccomp
+          - tool: ThetaCHC
+            artifact: Theta-chccomp
             record: 15537027
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
       - name: Create zenodo release and deploy tools
         uses: ./.github/actions/zenodo-release
         with:
-          tool: ${{matrix.tool}}
-          prevrecord: ${{matrix.record}}
-          token: ${{secrets.zenodo_token}}
+          tool: ${{ matrix.tool }}
+          artifact: ${{ matrix.artifact }}
+          prevrecord: ${{ matrix.record }}
+          token: ${{ secrets.zenodo_token }}
 
   deploy-maven:
     needs: test-linux

build.gradle.kts

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

buildSrc/gradle.properties

@@ -39,6 +39,7 @@ spotlessVersion=8.1.0
 nuprocessVersion=3.0.0
 eldaricaVersion=2.2
 hawtjniVersion=1.18
+fastutilVersion=8.5.15
 sonarqubeVersion=7.1.0.6387
 javadocVersion=9.1.0
 

buildSrc/src/main/kotlin/Deps.kt

@@ -107,5 +107,6 @@ object Deps {
 
     val nuprocess = "com.zaxxer:nuprocess:${Versions.nuprocess}"
 
-  val hawtjni = "org.fusesource.hawtjni:hawtjni-runtime:${Versions.hawtjni}"
+    val hawtjni = "org.fusesource.hawtjni:hawtjni-runtime:${Versions.hawtjni}"
+    val fastutil = "it.unimi.dsi:fastutil:${Versions.fastutil}"
 }

buildSrc/src/main/kotlin/antlr-grammar.gradle.kts

@@ -41,3 +41,11 @@ tasks {
         arguments.addAll(listOf("-package", packageName, "-Werror", "-visitor"))
     }
 }
+
+pluginManager.withPlugin("com.diffplug.spotless") {
+    configure<com.diffplug.gradle.spotless.SpotlessExtension> {
+        java {
+            targetExclude("**/build/generated-src/**/*.java")
+        }
+    }
+}

buildSrc/src/main/kotlin/java-common.gradle.kts

@@ -112,7 +112,7 @@ spotless {
     java {
         importOrder("java|javax", "hu.bme.", "")
         removeUnusedImports()
-        googleJavaFormat("1.25.2").aosp().reflowLongStrings()
+        googleJavaFormat("1.35.0").aosp().reflowLongStrings()
         formatAnnotations()
     }
     kotlin {

settings.gradle.kts

@@ -28,6 +28,7 @@ include(
     "frontends/petrinet-model",
     "frontends/petrinet-analysis",
     "frontends/petrinet-xsts",
+    "frontends/dve-frontend",
     "frontends/chc-frontend",
     "frontends/llvm",
 

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -20,7 +20,7 @@
 import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrec;
 import hu.bme.mit.theta.cfa.analysis.prec.LocalCfaPrec;
 import hu.bme.mit.theta.common.Utils;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import hu.bme.mit.theta.core.stmt.AssumeStmt;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
@@ -33,9 +33,9 @@ public final class CfaInitPrecs {
     private CfaInitPrecs() {}
 
     public static LocalCfaPrec<PredPrec> collectAssumesLocal(CFA cfa) {
-        Map<CFA.Loc, PredPrec> precs = Containers.createMap();
+        Map<CFA.Loc, PredPrec> precs = CollectionUtil.createMap();
         for (CFA.Loc l : cfa.getLocs()) {
-            Set<Expr<BoolType>> exprs = Containers.createSet();
+            Set<Expr<BoolType>> exprs = CollectionUtil.createSet();
             for (CFA.Edge e : l.getInEdges()) {
                 CFA.Edge running = e;
                 while (running != null) {
@@ -56,7 +56,7 @@ public static LocalCfaPrec<PredPrec> collectAssumesLocal(CFA cfa) {
     }
 
     public static GlobalCfaPrec<PredPrec> collectAssumesGlobal(CFA cfa) {
-        Set<Expr<BoolType>> assumes = Containers.createSet();
+        Set<Expr<BoolType>> assumes = CollectionUtil.createSet();
         for (CFA.Edge e : cfa.getEdges()) {
             if (e.getStmt() instanceof AssumeStmt) {
                 AssumeStmt assumeStmt = (AssumeStmt) e.getStmt();

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -24,7 +24,7 @@
 import hu.bme.mit.theta.cfa.CFA;
 import hu.bme.mit.theta.cfa.CFA.Edge;
 import hu.bme.mit.theta.cfa.CFA.Loc;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
@@ -82,7 +82,7 @@ private int getDistanceToError(final Loc loc) {
 
     static Map<Loc, Integer> calculateDistancesToError(final CFA cfa, final Loc errLoc) {
         List<Loc> queue = new LinkedList<>();
-        final Map<Loc, Integer> distancesToError = Containers.createMap();
+        final Map<Loc, Integer> distancesToError = CollectionUtil.createMap();
         queue.add(errLoc);
         distancesToError.put(errLoc, 0);
         int distance = 1;

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -21,7 +21,7 @@
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode;
 import hu.bme.mit.theta.analysis.reachedset.ReachedSet;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
@@ -38,7 +38,7 @@ public final class ImpactReachedSet<S extends State, A extends Action, K>
 
     private ImpactReachedSet(final Function<? super S, ? extends K> partitioning) {
         this.partitioning = checkNotNull(partitioning);
-        partitions = Containers.createMap();
+        partitions = CollectionUtil.createMap();
     }
 
     public static <S extends State, A extends Action, K> ImpactReachedSet<S, A, K> create(

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -18,7 +18,7 @@
 import hu.bme.mit.theta.cfa.CFA.Loc;
 import hu.bme.mit.theta.cfa.analysis.CfaAction;
 import hu.bme.mit.theta.cfa.analysis.CfaState;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import java.util.Collection;
 import java.util.Map;
 
@@ -33,7 +33,7 @@ public final class CfaCachedLts implements CfaLts {
 
     public CfaCachedLts(final CfaLts lts) {
         this.lts = lts;
-        this.actionCache = Containers.createMap();
+        this.actionCache = CollectionUtil.createMap();
     }
 
     @Override

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -25,7 +25,7 @@
 import hu.bme.mit.theta.cfa.analysis.CfaPrec;
 import hu.bme.mit.theta.common.LispStringBuilder;
 import hu.bme.mit.theta.common.Utils;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import java.util.Collection;
 import java.util.Collections;
@@ -85,7 +85,7 @@ public P getPrec(final Loc loc) {
     public LocalCfaPrec<P> refine(final Map<Loc, P> refinedPrecs) {
         checkNotNull(refinedPrecs);
 
-        final Map<Loc, P> refinedMapping = Containers.createMap(this.mapping);
+        final Map<Loc, P> refinedMapping = CollectionUtil.createMap(this.mapping);
 
         for (final Entry<Loc, P> entry : refinedPrecs.entrySet()) {
             final Loc loc = entry.getKey();

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -28,7 +28,7 @@
 import hu.bme.mit.theta.cfa.CFA.Loc;
 import hu.bme.mit.theta.cfa.analysis.CfaPrec;
 import hu.bme.mit.theta.cfa.analysis.CfaState;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import java.util.Map;
 
 public final class LocalCfaPrecRefiner<
@@ -60,7 +60,7 @@ public CfaPrec<P> refine(
         // joining them to the old precision of the location
 
         final LocalCfaPrec<P> genPrec = (LocalCfaPrec<P>) prec;
-        final Map<Loc, P> runningPrecs = Containers.createMap();
+        final Map<Loc, P> runningPrecs = CollectionUtil.createMap();
         for (final CfaState<S> state : trace.getStates()) {
             runningPrecs.put(state.getLoc(), genPrec.getPrec(state.getLoc()));
         }

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -22,7 +22,7 @@
 import hu.bme.mit.theta.cfa.CFA.Loc;
 import hu.bme.mit.theta.cfa.analysis.CfaAction;
 import hu.bme.mit.theta.cfa.analysis.CfaState;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import hu.bme.mit.theta.common.table.TableWriter;
 import hu.bme.mit.theta.common.visualization.*;
 import hu.bme.mit.theta.common.visualization.Shape;
@@ -51,7 +51,7 @@ private CfaVisualizer() {}
 
     public static Graph visualize(final CFA cfa) {
         final Graph graph = new Graph(CFA_ID, CFA_LABEL);
-        final Map<Loc, String> ids = Containers.createMap();
+        final Map<Loc, String> ids = CollectionUtil.createMap();
         addVars(graph, cfa);
         for (final Loc loc : cfa.getLocs()) {
             addLocation(graph, cfa, loc, ids);

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

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -22,7 +22,7 @@
 import hu.bme.mit.theta.cfa.analysis.lts.CfaLts;
 import hu.bme.mit.theta.cfa.analysis.lts.CfaSbeLts;
 import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import java.io.FileInputStream;
@@ -46,7 +46,7 @@ private CFA.Loc getLocByName(String name) {
     }
 
     private Set<String> getNextLocs(CfaLts lts, String loc) {
-        Set<String> locs = Containers.createSet();
+        Set<String> locs = CollectionUtil.createSet();
         SS ss = new SS();
         for (var act : lts.getEnabledActionsFor(CfaState.of(getLocByName(loc), ss))) {
             locs.add(act.getTarget().getName());

subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaMetrics.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -16,7 +16,7 @@
 package hu.bme.mit.theta.cfa.cli;
 
 import hu.bme.mit.theta.cfa.CFA;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.core.stmt.AssignStmt;
 import hu.bme.mit.theta.core.stmt.AssumeStmt;
@@ -72,7 +72,7 @@ public static void printMetrics(Logger logger, CFA cfa) {
     }
 
     public static int getCfaComponents(final CFA cfa) {
-        final Set<CFA.Loc> visited = Containers.createSet();
+        final Set<CFA.Loc> visited = CollectionUtil.createSet();
         int components = 0;
 
         for (final CFA.Loc loc : cfa.getLocs()) {

subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2025 Budapest University of Technology and Economics
+ *  Copyright 2026 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.
@@ -22,7 +22,7 @@
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import hu.bme.mit.theta.common.Utils;
-import hu.bme.mit.theta.common.container.Containers;
+import hu.bme.mit.theta.common.collection.CollectionUtil;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.stmt.Stmt;
 import hu.bme.mit.theta.core.utils.StmtUtils;
@@ -53,7 +53,7 @@ private CFA(final Builder builder) {
                 edges.stream()
                         .flatMap(e -> StmtUtils.getVars(e.getStmt()).stream())
                         .collect(toImmutableSet());
-        Set<String> varNames = Containers.createSet();
+        Set<String> varNames = CollectionUtil.createSet();
         for (var v : vars) {
             checkArgument(
                     !varNames.contains(v.getName()),
@@ -203,10 +203,10 @@ public static final class Builder {
         private static int UNNAMED_LOC_LABEL = 0;
 
         private Builder() {
-            locs = Containers.createSet();
-            locNames = Containers.createSet();
+            locs = CollectionUtil.createSet();
+            locNames = CollectionUtil.createSet();
             edges = new LinkedList<>();
-            acceptingEdges = Containers.createSet();
+            acceptingEdges = CollectionUtil.createSet();
             built = false;
         }