diff --git a/.github/workflows/linux-build-test-deploy.yml b/.github/workflows/linux-build-test-deploy.yml
index 1ff709451b..b4de982086 100644
--- a/.github/workflows/linux-build-test-deploy.yml
+++ b/.github/workflows/linux-build-test-deploy.yml
@@ -165,6 +165,9 @@ jobs:
dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli", "theta-xcfa-cli"]
runs-on: ubuntu-latest
steps:
+ - name: Set java home to java 17
+ run: |
+ echo "JAVA_HOME=$(echo $JAVA_HOME_17_X64)" >> $GITHUB_ENV
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Version
diff --git a/.gitignore b/.gitignore
index 7fa1e2dabb..e68c7c1070 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,9 +13,16 @@ dest/
.classpath
# Intellij
-.idea/
+.idea/**
*.iml
*.iws
+# useful exclusions
+!.idea/copyright
+!.idea/copyright/bme_apache2.xml
+!.idea/copyright/profiles_settings.xml
+!.idea/codeStyles
+!.idea/codeStyles/codeStyleConfig.xml
+!.idea/codeStyles/Project.xml
# Other
wdl-output.json
diff --git a/.idea/codeStyles/Project.xml b/.idea/codeStyles/Project.xml
new file mode 100644
index 0000000000..a522151798
--- /dev/null
+++ b/.idea/codeStyles/Project.xml
@@ -0,0 +1,78 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/codeStyles/codeStyleConfig.xml b/.idea/codeStyles/codeStyleConfig.xml
new file mode 100644
index 0000000000..79ee123c2b
--- /dev/null
+++ b/.idea/codeStyles/codeStyleConfig.xml
@@ -0,0 +1,5 @@
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/copyright/bme_apache2.xml b/.idea/copyright/bme_apache2.xml
new file mode 100644
index 0000000000..97178a1877
--- /dev/null
+++ b/.idea/copyright/bme_apache2.xml
@@ -0,0 +1,6 @@
+
+
+
+
+
+
\ No newline at end of file
diff --git a/.idea/copyright/profiles_settings.xml b/.idea/copyright/profiles_settings.xml
new file mode 100644
index 0000000000..978f7b5fe9
--- /dev/null
+++ b/.idea/copyright/profiles_settings.xml
@@ -0,0 +1,3 @@
+
+
+
\ No newline at end of file
diff --git a/build.gradle.kts b/build.gradle.kts
index 235741e9d6..84584f9864 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -28,7 +28,7 @@ buildscript {
allprojects {
group = "hu.bme.mit.theta"
- version = "6.2.0"
+ version = "6.2.1"
apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
}
@@ -39,7 +39,7 @@ sonar {
property("sonar.organization", "ftsrg-github")
property("sonar.host.url", "https://sonarcloud.io")
property("sonar.coverage.jacoco.xmlReportPaths",
- "${project.buildDir}/reports/jacoco/jacocoRootReport/jacocoRootReport.xml")
+ "${project.layout.buildDirectory.asFile.get()}/reports/jacoco/jacocoRootReport/jacocoRootReport.xml")
}
}
@@ -51,9 +51,9 @@ tasks {
description = "Generates merged code coverage report for all test tasks."
reports {
- html.isEnabled = false
- xml.isEnabled = true
- csv.isEnabled = false
+ html.required.set(false)
+ xml.required.set(true)
+ csv.required.set(false)
}
val reportTasks = subprojects.mapNotNull { subproject ->
diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts
index 36b1f85544..093b423f12 100644
--- a/buildSrc/build.gradle.kts
+++ b/buildSrc/build.gradle.kts
@@ -13,7 +13,6 @@
* See the License for the specific language governing permissions and
* limitations under the License.
*/
-import org.jetbrains.kotlin.gradle.plugin.KotlinSourceSet
import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
plugins {
@@ -29,10 +28,6 @@ repositories {
apply(from = rootDir.resolve("../gradle/shared-with-buildSrc/mirrors.gradle.kts"))
-kotlinDslPluginOptions {
- experimentalWarning.set(false)
-}
-
val kotlinVersion: String by project
val shadowVersion: String by project
@@ -60,30 +55,29 @@ configurations.all {
}
val versionsClassName = "Versions"
-val generatedVersionsKotlinSrcDir = buildDir.resolve("generated-sources/versions/kotlin")
+val generatedVersionsKotlinSrcDir = layout.buildDirectory.dir("generated-sources/versions/kotlin").get().asFile
val generatedVersionsFile = generatedVersionsKotlinSrcDir.resolve("$versionsClassName.kt")
sourceSets {
named("main") {
- withConvention(KotlinSourceSet::class) {
- kotlin.srcDir(generatedVersionsKotlinSrcDir)
- }
+ kotlin.srcDir(generatedVersionsKotlinSrcDir)
}
}
+
fun generateVersionsSource(): String {
val text = StringBuilder()
- text.appendln("object $versionsClassName {")
+ text.appendLine("object $versionsClassName {")
for (property in project.properties) {
if (property.key.endsWith("Version")) {
val keyWithoutVersion = property.key.substringBefore("Version")
- text.appendln(" const val `$keyWithoutVersion` = \"${property.value}\"")
+ text.appendLine(" const val `$keyWithoutVersion` = \"${property.value}\"")
}
}
- text.appendln("}")
+ text.appendLine("}")
return text.toString()
}
diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties
index 499eb7e837..ecd967b559 100644
--- a/buildSrc/gradle.properties
+++ b/buildSrc/gradle.properties
@@ -15,7 +15,7 @@
#
javaVersion=17
-kotlinVersion=1.7.10
+kotlinVersion=1.9.25
shadowVersion=7.1.2
antlrVersion=4.9.2
guavaVersion=31.1-jre
@@ -24,7 +24,8 @@ z3Version=4.5.0
junitVersion=5.9.3
junit4Version=4.12
jacocoVersion=0.8.8
-mockitoVersion=2.2.11
+mockitoVersion=5.12.0
+mockitoKotlinVersion=5.4.0
pnmlFrameworkVersion=2.2.12
emfCommonVersion=2.10.1
emfCodegenVersion=2.10.0
diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt
index ab28cb0deb..652a9f0678 100644
--- a/buildSrc/src/main/kotlin/Deps.kt
+++ b/buildSrc/src/main/kotlin/Deps.kt
@@ -68,6 +68,8 @@ object Deps {
object Mockito {
val core = "org.mockito:mockito-core:${Versions.mockito}"
+ val extension = "org.mockito:mockito-junit-jupiter:${Versions.mockito}"
+ val kotlin = "org.mockito.kotlin:mockito-kotlin:${Versions.mockitoKotlin}"
}
object Kotlin {
diff --git a/buildSrc/src/main/kotlin/jacoco-common.gradle.kts b/buildSrc/src/main/kotlin/jacoco-common.gradle.kts
index 74e95ad419..4f8c7b9522 100644
--- a/buildSrc/src/main/kotlin/jacoco-common.gradle.kts
+++ b/buildSrc/src/main/kotlin/jacoco-common.gradle.kts
@@ -19,8 +19,8 @@ extensions.configure {
toolVersion = Versions.jacoco
}
-tasks.withType(JacocoReport::class.java).all {
+tasks.withType().configureEach {
reports {
- xml.isEnabled = true
+ xml.required.set(true)
}
-}
\ No newline at end of file
+}
diff --git a/buildSrc/src/main/kotlin/java-common.gradle.kts b/buildSrc/src/main/kotlin/java-common.gradle.kts
index 4981d2394a..48a37e8235 100644
--- a/buildSrc/src/main/kotlin/java-common.gradle.kts
+++ b/buildSrc/src/main/kotlin/java-common.gradle.kts
@@ -13,9 +13,11 @@
* See the License for the specific language governing permissions and
* limitations under the License.
*/
-apply()
-apply(plugin = "jacoco-common")
-apply(plugin = "maven-artifact")
+plugins {
+ java
+ id("jacoco-common")
+ id("maven-publish") // The correct plugin id for maven-related tasks
+}
dependencies {
val implementation: Configuration by configurations
@@ -33,6 +35,7 @@ dependencies {
testImplementation(Deps.junit5param)
testImplementation(Deps.junit5engine)
testImplementation(Deps.Mockito.core)
+ testImplementation(Deps.Mockito.extension)
}
tasks {
diff --git a/buildSrc/src/main/kotlin/kotlin-common.gradle.kts b/buildSrc/src/main/kotlin/kotlin-common.gradle.kts
index cf53f36826..59eef2f722 100644
--- a/buildSrc/src/main/kotlin/kotlin-common.gradle.kts
+++ b/buildSrc/src/main/kotlin/kotlin-common.gradle.kts
@@ -13,15 +13,17 @@
* See the License for the specific language governing permissions and
* limitations under the License.
*/
-import org.jetbrains.kotlin.gradle.plugin.KotlinPlatformJvmPlugin
import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
apply(plugin = "java-common")
-apply()
+plugins {
+ kotlin("jvm")
+}
dependencies {
val implementation: Configuration by configurations
implementation(Deps.Kotlin.stdlib)
implementation(Deps.Kotlin.reflect)
+ implementation(Deps.Mockito.kotlin)
}
tasks {
withType() {
diff --git a/buildSrc/src/main/kotlin/tool-common.gradle.kts b/buildSrc/src/main/kotlin/tool-common.gradle.kts
index 26413cc5ce..9e666b2a0c 100644
--- a/buildSrc/src/main/kotlin/tool-common.gradle.kts
+++ b/buildSrc/src/main/kotlin/tool-common.gradle.kts
@@ -34,6 +34,7 @@ tasks {
tasks.withType() {
manifest {
- attributes["Implementation-Version"] = version
+ attributes["Implementation-Version"] = archiveVersion
}
+ isZip64 = true
}
diff --git a/doc/Coding-conventions.md b/doc/Coding-conventions.md
index 39955229e6..5d534a1d70 100644
--- a/doc/Coding-conventions.md
+++ b/doc/Coding-conventions.md
@@ -7,7 +7,7 @@ We mainly follow the standard Java coding conventions and most of the convention
## Naming and formatting
-* **DO** use the generally accepted naming and source code formatting conventions of Java (Item 56 of [1], Chapter 1 of [5]). If you are developing in IntelliJ Idea you can import our commonly used formatting profile (see [Development.md](Development.md) for more information).
+* **DO** use the generally accepted naming and source code formatting conventions of Java (Item 56 of [1], Chapter 1 of [5]). If you are developing in IntelliJ Idea the built in formatting by the project can be used (see [Development.md](Development.md) for more information).
* **DO** start project names with the prefix `hu.bme.mit.theta`.
* **DO** use CamelCase for class names containing subsequent capital letters, except when the whole name is a sequence of capital letters. Examples: `CFA`, `CfaEdge`, `OsHelper`.
* **CONSIDER** using abbreviations for well known and common names. Examples: `Expression` -> `Expr`, `Statement` -> `Stmt`, `Counterexample` -> `Cex`.
diff --git a/doc/Development.md b/doc/Development.md
index 22f5243124..33b20f1891 100644
--- a/doc/Development.md
+++ b/doc/Development.md
@@ -19,8 +19,7 @@ We usually develop on separate branches and increment the version number just be
As the main repository is read-only, we suggest you to create your own [fork](https://help.github.com/articles/fork-a-repo/). Within your fork, we also recommend to create new _branches_ for your development. This enables us later on to easily integrate your work into the main repository by using [pull requests](https://help.github.com/articles/about-pull-requests/).
-As the framework is under development, we suggest you to [sync your fork](https://help.github.com/articles/syncing-a-fork/) often and merge the master branch into your development branch(es).
-If you are confident that only you are working on your branch, you can also [rebase instead of merge](https://www.atlassian.com/git/tutorials/merging-vs-rebasing), but be careful.
+As the framework is under development, we suggest you to [sync your fork](https://help.github.com/articles/syncing-a-fork/) often and rebase your development branch(es) onto the master branch.
## Building
@@ -30,7 +29,7 @@ See [Build.md](Build.md).
- Theta can be imported into [IntelliJ IDEA](https://www.jetbrains.com/idea/) as an existing Gradle project by selecting the _build.gradle.kts_ file in the root of the repository.
- If you want to build the whole project (and not just run a single test for example), make sure to run the _build task of the whole project_. This can be done by opening the Gradle tab, and then selecting _theta / theta / Tasks / build / build_, right clicking and selecting _Run_.
-- [Import](https://www.jetbrains.com/help/idea/copying-code-style-settings.html) _doc/ThetaIntelliJCodeStyle.xml_ as a code style scheme for Java so that your formatting settings are consistent with the rest of the project.
+- Code styling and copyright noticing should be automatically set up for the ones accepted by the Github CI. It is not recommended to change them.
## Coding conventions
diff --git a/doc/ThetaIntelliJCodeStyle.xml b/doc/ThetaIntelliJCodeStyle.xml
deleted file mode 100644
index c34ed46965..0000000000
--- a/doc/ThetaIntelliJCodeStyle.xml
+++ /dev/null
@@ -1,110 +0,0 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
index aa991fceae..19cfad969b 100644
--- a/gradle/wrapper/gradle-wrapper.properties
+++ b/gradle/wrapper/gradle-wrapper.properties
@@ -1,5 +1,5 @@
distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-7.4.2-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.9-bin.zip
zipStoreBase=GRADLE_USER_HOME
zipStorePath=wrapper/dists
diff --git a/subprojects/cfa/cfa-cli/build.gradle.kts b/subprojects/cfa/cfa-cli/build.gradle.kts
index d3f5e363cb..bb62725072 100644
--- a/subprojects/cfa/cfa-cli/build.gradle.kts
+++ b/subprojects/cfa/cfa-cli/build.gradle.kts
@@ -30,5 +30,5 @@ dependencies {
}
application {
- mainClassName = "hu.bme.mit.theta.cfa.cli.CfaCli"
+ mainClass.set("hu.bme.mit.theta.cfa.cli.CfaCli")
}
diff --git a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt
index 3234b6a198..ce30555dea 100644
--- a/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt
+++ b/subprojects/common/multi-tests/src/test/kotlin/multi/MultiNondetDiningPhilosophersTest.kt
@@ -75,19 +75,19 @@ class MultiNondetDiningPhilosophersTest {
val cfa1ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP,
Z3LegacySolverFactory.getInstance())
- cfa1ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE)
+ cfa1ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE)
val cfa1ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil1cfa)
val cfa2ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP,
Z3LegacySolverFactory.getInstance())
- cfa2ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE)
+ cfa2ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE)
val cfa2ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil2cfa)
val cfa3ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP,
Z3LegacySolverFactory.getInstance())
- cfa3ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE)
+ cfa3ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE)
val cfa3ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil3cfa)
val cfa4ConfigBuilder = CfaConfigBuilder(CfaConfigBuilder.Domain.EXPL, CfaConfigBuilder.Refinement.SEQ_ITP,
Z3LegacySolverFactory.getInstance())
- cfa4ConfigBuilder.encoding(CfaConfigBuilder.Encoding.SBE)
+ cfa4ConfigBuilder.encoding(CfaConfigBuilder.Encoding.LBE)
val cfa4ExplBuilder = cfa1ConfigBuilder.ExplStrategy(phil4cfa)
val cfaRefToPrec = RefutationToGlobalCfaPrec(ItpRefToExplPrec(), phil1cfa.initLoc)
diff --git a/subprojects/solver/solver-smtlib-cli/build.gradle.kts b/subprojects/solver/solver-smtlib-cli/build.gradle.kts
index a7a8734efd..95cbb948f4 100644
--- a/subprojects/solver/solver-smtlib-cli/build.gradle.kts
+++ b/subprojects/solver/solver-smtlib-cli/build.gradle.kts
@@ -25,5 +25,5 @@ dependencies {
}
application {
- mainClassName = "hu.bme.mit.theta.solver.smtlib.cli.SmtLibCli"
+ mainClass.set("hu.bme.mit.theta.solver.smtlib.cli.SmtLibCli")
}
diff --git a/subprojects/sts/sts-cli/build.gradle.kts b/subprojects/sts/sts-cli/build.gradle.kts
index 66685b6eb5..cb1eedf2e2 100644
--- a/subprojects/sts/sts-cli/build.gradle.kts
+++ b/subprojects/sts/sts-cli/build.gradle.kts
@@ -29,5 +29,5 @@ dependencies {
}
application {
- mainClassName = "hu.bme.mit.theta.sts.cli.StsCli"
+ mainClass.set("hu.bme.mit.theta.sts.cli.StsCli")
}
diff --git a/subprojects/xcfa/xcfa-cli/build.gradle.kts b/subprojects/xcfa/xcfa-cli/build.gradle.kts
index dc92ba6f04..f695b775af 100644
--- a/subprojects/xcfa/xcfa-cli/build.gradle.kts
+++ b/subprojects/xcfa/xcfa-cli/build.gradle.kts
@@ -48,6 +48,6 @@ dependencies {
}
application {
- mainClassName = "hu.bme.mit.theta.xcfa.cli.XcfaCli"
+ mainClass.set("hu.bme.mit.theta.xcfa.cli.XcfaCli")
}
diff --git a/subprojects/xsts/xsts-cli/build.gradle.kts b/subprojects/xsts/xsts-cli/build.gradle.kts
index f73e672db1..1016451f40 100644
--- a/subprojects/xsts/xsts-cli/build.gradle.kts
+++ b/subprojects/xsts/xsts-cli/build.gradle.kts
@@ -33,5 +33,5 @@ dependencies {
}
application {
- mainClassName = "hu.bme.mit.theta.xsts.cli.XstsCli"
+ mainClass.set("hu.bme.mit.theta.xsts.cli.XstsCli")
}
diff --git a/subprojects/xta/xta-cli/build.gradle.kts b/subprojects/xta/xta-cli/build.gradle.kts
index 8c5551b6d9..5e0a67ed33 100644
--- a/subprojects/xta/xta-cli/build.gradle.kts
+++ b/subprojects/xta/xta-cli/build.gradle.kts
@@ -29,5 +29,5 @@ dependencies {
}
application {
- mainClassName = "hu.bme.mit.theta.xta.cli.XtaCli"
+ mainClass.set("hu.bme.mit.theta.xta.cli.XtaCli")
}