ftsrg · mondokm · Jan 23, 2025 · Nov 1, 2024 · Nov 1, 2024 · Dec 14, 2024
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.8.6"
+    version = "6.9.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties
@@ -1,5 +1,5 @@
 #
-#  Copyright 2024 Budapest University of Technology and Economics
+#  Copyright 2025 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.
@@ -17,7 +17,7 @@
 javaVersion=17
 kotlinVersion=1.9.25
 shadowVersion=7.1.2
-antlrVersion=4.9.2
+antlrVersion=4.12.0
 guavaVersion=31.1-jre
 jcommanderVersion=1.72
 z3Version=4.5.0
@@ -41,4 +41,5 @@ javasmtVersion=4.1.1
 sosylabVersion=0.3000-569-g89796f98
 cliktVersion=4.4.0
 spotlessVersion=6.25.0
-kamlVersion=0.59.0
+kamlVersion=0.59.0
+nuprocessVersion=2.0.6
diff --git a/buildSrc/settings.gradle.kts b/buildSrc/settings.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.
@@ -81,4 +81,6 @@ object Deps {
     val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"
 
     val kaml = "com.charleskorn.kaml:kaml:${Versions.kaml}"
+
+    val nuprocess = "com.zaxxer:nuprocess:${Versions.nuprocess}"
 }
diff --git a/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts b/buildSrc/src/main/kotlin/antlr-grammar.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/cli-tool.gradle.kts b/buildSrc/src/main/kotlin/cli-tool.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/jacoco-common.gradle.kts b/buildSrc/src/main/kotlin/jacoco-common.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/java-common.gradle.kts b/buildSrc/src/main/kotlin/java-common.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/kaml-serialization.gradle.kts b/buildSrc/src/main/kotlin/kaml-serialization.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.
@@ -17,7 +17,7 @@
 import gradle.kotlin.dsl.accessors._07de9d51edfbede3e6fa517ade9dcf20.implementation
 
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/kotlin-common.gradle.kts b/buildSrc/src/main/kotlin/kotlin-common.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/maven-artifact.gradle.kts b/buildSrc/src/main/kotlin/maven-artifact.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/buildSrc/src/main/kotlin/tool-common.gradle.kts b/buildSrc/src/main/kotlin/tool-common.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/gradle/shared-with-buildSrc/mirrors.gradle.kts b/gradle/shared-with-buildSrc/mirrors.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/lib/jhoafparser-1.1.1.jar b/lib/jhoafparser-1.1.1.jar
diff --git a/scripts/complex.kts b/scripts/complex.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/scripts/simple.kts b/scripts/simple.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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,6 +21,8 @@ include(
     "common/core",
     "common/grammar",
     "common/multi-tests",
+    "common/ltl",
+    "common/ltl-cli",
 
     "frontends/c-frontend",
     "frontends/petrinet-frontend/petrinet-model",

diff --git a/subprojects/cfa/cfa-analysis/build.gradle.kts b/subprojects/cfa/cfa-analysis/build.gradle.kts
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.

diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.
@@ -15,19 +15,18 @@
  */
 package hu.bme.mit.theta.cfa.analysis;
 
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import hu.bme.mit.theta.analysis.expr.StmtAction;
 import hu.bme.mit.theta.cfa.CFA.Edge;
 import hu.bme.mit.theta.cfa.CFA.Loc;
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.core.stmt.Stmt;
-
 import java.util.Collections;
 import java.util.List;
 import java.util.stream.Collectors;
 
-import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkNotNull;
-
 public final class CfaAction extends StmtAction {
 
     private final List<Edge> edges;
@@ -39,8 +38,9 @@ private CfaAction(final Loc source, final Loc target, final List<Edge> edges) {
         this.source = checkNotNull(source);
         this.target = checkNotNull(target);
         this.edges = Collections.unmodifiableList(checkNotNull(edges));
-        this.stmts = Collections.unmodifiableList(
-                edges.stream().map(Edge::getStmt).collect(Collectors.toList()));
+        this.stmts =
+                Collections.unmodifiableList(
+                        edges.stream().map(Edge::getStmt).collect(Collectors.toList()));
     }
 
     public static CfaAction create(final Edge edge) {

diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAnalysis.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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,8 +18,8 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import hu.bme.mit.theta.analysis.Analysis;
-import hu.bme.mit.theta.analysis.PartialOrd;
 import hu.bme.mit.theta.analysis.InitFunc;
+import hu.bme.mit.theta.analysis.PartialOrd;
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.TransFunc;
 import hu.bme.mit.theta.analysis.expr.ExprState;
@@ -32,17 +32,17 @@ public final class CfaAnalysis<S extends ExprState, P extends Prec>
     private final InitFunc<CfaState<S>, CfaPrec<P>> initFunc;
     private final TransFunc<CfaState<S>, CfaAction, CfaPrec<P>> transFunc;
 
-    private CfaAnalysis(final Loc initLoc,
-                        final Analysis<S, ? super CfaAction, ? super P> analysis) {
+    private CfaAnalysis(
+            final Loc initLoc, final Analysis<S, ? super CfaAction, ? super P> analysis) {
         checkNotNull(initLoc);
         checkNotNull(analysis);
         partialOrd = CfaOrd.create(analysis.getPartialOrd());
         initFunc = CfaInitFunc.create(initLoc, analysis.getInitFunc());
         transFunc = CfaTransFunc.create(analysis.getTransFunc());
     }
 
-    public static <S extends ExprState, P extends Prec> CfaAnalysis<S, P> create(final Loc initLoc,
-                                                                                 final Analysis<S, ? super CfaAction, ? super P> analysis) {
+    public static <S extends ExprState, P extends Prec> CfaAnalysis<S, P> create(
+            final Loc initLoc, final Analysis<S, ? super CfaAction, ? super P> analysis) {
         return new CfaAnalysis<>(initLoc, analysis);
     }
 
@@ -60,5 +60,4 @@ public InitFunc<CfaState<S>, CfaPrec<P>> getInitFunc() {
     public TransFunc<CfaState<S>, CfaAction, CfaPrec<P>> getTransFunc() {
         return transFunc;
     }
-
 }
diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitFunc.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.
@@ -15,18 +15,17 @@
  */
 package hu.bme.mit.theta.cfa.analysis;
 
+import static com.google.common.base.Preconditions.checkNotNull;
+
 import hu.bme.mit.theta.analysis.InitFunc;
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.expr.ExprState;
 import hu.bme.mit.theta.cfa.CFA.Loc;
-
 import java.util.ArrayList;
 import java.util.Collection;
 
-import static com.google.common.base.Preconditions.checkNotNull;
-
-public final class CfaInitFunc<S extends ExprState, P extends Prec> implements
-        InitFunc<CfaState<S>, CfaPrec<P>> {
+public final class CfaInitFunc<S extends ExprState, P extends Prec>
+        implements InitFunc<CfaState<S>, CfaPrec<P>> {
 
     private final Loc initLoc;
     private final InitFunc<S, ? super P> initFunc;
@@ -36,8 +35,8 @@ private CfaInitFunc(final Loc initLoc, final InitFunc<S, ? super P> initFunc) {
         this.initFunc = checkNotNull(initFunc);
     }
 
-    public static <S extends ExprState, P extends Prec> CfaInitFunc<S, P> create(final Loc initLoc,
-                                                                                 final InitFunc<S, ? super P> initFunc) {
+    public static <S extends ExprState, P extends Prec> CfaInitFunc<S, P> create(
+            final Loc initLoc, final InitFunc<S, ? super P> initFunc) {
         return new CfaInitFunc<>(initLoc, initFunc);
     }
 
@@ -54,5 +53,4 @@ public Collection<CfaState<S>> getInitStates(final CfaPrec<P> prec) {
         }
         return initStates;
     }
-
 }
diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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,20 +20,17 @@
 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.core.stmt.AssumeStmt;
 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;
-
-import hu.bme.mit.theta.common.container.Containers;
-
 import java.util.Map;
 import java.util.Set;
 
 public final class CfaInitPrecs {
 
-    private CfaInitPrecs() {
-    }
+    private CfaInitPrecs() {}
 
     public static LocalCfaPrec<PredPrec> collectAssumesLocal(CFA cfa) {
         Map<CFA.Loc, PredPrec> precs = Containers.createMap();

diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaOrd.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.
@@ -34,8 +34,7 @@ public static <S extends ExprState> CfaOrd<S> create(final PartialOrd<S> partial
 
     @Override
     public boolean isLeq(final CfaState<S> state1, final CfaState<S> state2) {
-        return state1.getLoc().equals(state2.getLoc()) && partialOrd.isLeq(state1.getState(),
-                state2.getState());
+        return state1.getLoc().equals(state2.getLoc())
+                && partialOrd.isLeq(state1.getState(), state2.getState());
     }
-
 }
diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaPrec.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2025 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.