Merge branch 'master' into fix-ref

.gitignore

@@ -35,3 +35,4 @@ xcfa.dot
 xcfa.json
 *.plantuml
 xcfa-*.smt2
+witness.yml

build.gradle.kts

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

buildSrc/build.gradle.kts

@@ -38,6 +38,7 @@ fun gradlePlugin(id: String, version: String): String = "$id:$id.gradle.plugin:$
 dependencies {
     compileOnly(gradleKotlinDsl())
     implementation(kotlin("gradle-plugin", kotlinVersion))
+    implementation(kotlin("serialization", kotlinVersion))
     implementation(gradlePlugin("com.github.johnrengelman.shadow", shadowVersion))
     implementation(gradlePlugin("com.diffplug.spotless", spotlessVersion))
 }

buildSrc/gradle.properties

@@ -40,4 +40,5 @@ gsonVersion=2.9.1
 javasmtVersion=4.1.1
 sosylabVersion=0.3000-569-g89796f98
 cliktVersion=4.4.0
-spotlessVersion=6.25.0
+spotlessVersion=6.25.0
+kamlVersion=0.59.0

buildSrc/src/main/kotlin/Deps.kt

@@ -79,4 +79,6 @@ object Deps {
     }
 
     val clikt = "com.github.ajalt.clikt:clikt:${Versions.clikt}"
+
+    val kaml = "com.charleskorn.kaml:kaml:${Versions.kaml}"
 }

buildSrc/src/main/kotlin/kaml-serialization.gradle.kts

@@ -0,0 +1,41 @@
+/*
+ *  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.
+ */
+
+import gradle.kotlin.dsl.accessors._07de9d51edfbede3e6fa517ade9dcf20.implementation
+
+/*
+ *  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.
+ */
+
+apply(plugin = "kotlin-common")
+plugins {
+    kotlin("plugin.serialization")
+}
+dependencies {
+    implementation(Deps.kaml)
+}

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

@@ -17,60 +17,65 @@
 
 import static org.junit.Assert.assertTrue;
 
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.IOException;
-
 import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
-import hu.bme.mit.theta.analysis.pred.PredState;
-import hu.bme.mit.theta.cfa.analysis.CfaAction;
-import hu.bme.mit.theta.cfa.analysis.CfaState;
-import hu.bme.mit.theta.solver.Solver;
-import org.junit.Test;
-
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgChecker;
 import hu.bme.mit.theta.analysis.expr.ExprAction;
 import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.pred.PredState;
 import hu.bme.mit.theta.analysis.unit.UnitPrec;
 import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
 import hu.bme.mit.theta.cfa.CFA;
+import hu.bme.mit.theta.cfa.analysis.CfaAction;
+import hu.bme.mit.theta.cfa.analysis.CfaState;
 import hu.bme.mit.theta.cfa.analysis.lts.CfaLbeLts;
 import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
 import hu.bme.mit.theta.solver.ItpSolver;
+import hu.bme.mit.theta.solver.Solver;
 import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory;
+import java.io.FileInputStream;
+import java.io.FileNotFoundException;
+import java.io.IOException;
+import org.junit.Test;
 
 public final class CfaPredImpactCheckerTest {
 
     @Test
     public void test() throws FileNotFoundException, IOException {
         // Arrange
-        final CFA cfa = CfaDslManager.createCfa(
-                new FileInputStream("src/test/resources/counter5_true.cfa"));
+        final CFA cfa =
+                CfaDslManager.createCfa(
+                        new FileInputStream("src/test/resources/counter5_true.cfa"));
 
         final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver();
         final ItpSolver refinementSolver = Z3LegacySolverFactory.getInstance().createItpSolver();
 
-        final PredImpactChecker checker = PredImpactChecker.create(
-                CfaLbeLts.of(cfa.getErrorLoc().get()), cfa.getInitLoc(),
-                l -> l.equals(cfa.getErrorLoc().get()), abstractionSolver, refinementSolver);
+        final PredImpactChecker checker =
+                PredImpactChecker.create(
+                        CfaLbeLts.of(cfa.getErrorLoc().get()),
+                        cfa.getInitLoc(),
+                        l -> l.equals(cfa.getErrorLoc().get()),
+                        abstractionSolver,
+                        refinementSolver);
 
         // Act
-        final SafetyResult<ARG<CfaState<PredState>, CfaAction>, Trace<CfaState<PredState>, CfaAction>> status = checker.check(
-                UnitPrec.getInstance());
+        final SafetyResult<
+                        ARG<CfaState<PredState>, CfaAction>, Trace<CfaState<PredState>, CfaAction>>
+                status = checker.check(UnitPrec.getInstance());
 
         // Assert
         assertTrue(status.isSafe());
 
-        final ARG<? extends ExprState, ? extends ExprAction> arg = status.getWitness();
+        final ARG<? extends ExprState, ? extends ExprAction> arg = status.getProof();
         arg.minimize();
 
         final ArgChecker argChecker = ArgChecker.create(abstractionSolver);
         assertTrue(argChecker.isWellLabeled(arg));
 
         System.out.println(
-                GraphvizWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg)));
+                GraphvizWriter.getInstance()
+                        .writeString(ArgVisualizer.getDefault().visualize(arg)));
     }
-}
+}