Models26 finalization

.github/workflows/build.yml

@@ -19,42 +19,22 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-#          - macos-13
+          - windows-latest
+          - macos-latest
     runs-on: ${{ matrix.os }}
     steps:
-#    - name: Setup Docker on MacOS
-#      uses: douglascamata/setup-docker-macos-action@v1-alpha
-#      if: ${{ matrix.os == 'macos-13' }}
-    - name: Test Docker
-      run: docker run hello-world
-    - name: Checkout code
-      uses: actions/checkout@v6
-    - name: Set up JDK
-      uses: actions/setup-java@v5
-      with:
-        java-version: 25
-        distribution: adopt
-    - name: Setup Gradle
-      uses: gradle/actions/setup-gradle@v5
-    - name: Setup Node
-      uses: actions/setup-node@v6
-      with:
-        node-version: 22
-        cache: 'npm'
-        cache-dependency-path: 'subprojects/semantifyr-vscode/package-lock.json'
-    - name: Gradle build
-      run: ./gradlew build
-    - name: Bundle Extension
-      run: ./gradlew bundleExtension
-    - name: Upload Artifacts
-      if: ${{ matrix.os == 'ubuntu-latest' }}
-      uses: actions/upload-artifact@v7
-      with:
-        path: |
-          **/build/vscode/
-          **/build/distributions/
-          **/build/reports/
-          **/build/test-results/
+      - name: Checkout code
+        uses: actions/checkout@v6
+      - name: Set up JDK
+        uses: actions/setup-java@v5
+        with:
+          java-version: 25
+          distribution: adopt
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v5
+      - name: Gradle build
+        shell: bash
+        run: ./gradlew build
 
   reuse-check:
     name: REUSE Compliance Check

CONTRIBUTORS.md

@@ -11,6 +11,6 @@
 **Project leader** Vince, Molnár <molnar.vince@vik.bme.hu>
 
 Contributors (in alphabetical order):
- 
- - Ármin, Zavada <zavadaarmin@edu.bme.hu>
- - Marussy, Kristóf <marussy@mit.bme.hu>
+
+- Ármin, Zavada <zavadaarmin@edu.bme.hu>
+- Marussy, Kristóf <marussy@mit.bme.hu>

README.md

@@ -14,9 +14,11 @@ A framework to support the declarative definition of engineering model semantics
 
 Use Java 25 for building.
 
-Run `gradlew build` to assemble the whole project, and execute all automated test, including regression testing and formal verifications. The required environment (e.g., Theta binaries) is automatically constructed by Gradle. Tests should run in a few minutes.
+Run `gradlew build` to assemble and test the project, including regression testing and formal verifications. The required environment (e.g., Theta binaries) is automatically constructed by Gradle. Tests should run in 10-20 minutes.
 
-To execute all tests (even extremely slow, several days long tests!), run `gradlew allTests`.
+To execute slow verification cases (the longest may take ~1 hour), run `gradlew testSlowVerificationCases`.
+
+Or run `gradlew allTests` for all tests.
 
 NOTE: Verification tests use Docker to run Theta. To run the build locally, ensure you have docker installed!
 

buildSrc/src/main/kotlin/hu/bme/mit/semantifyr/gradle/conventions/application.gradle.kts

@@ -11,10 +11,6 @@ plugins {
     application
 }
 
-tasks.startScripts {
-    classpath = files("%APP_HOME%/lib/*")
-}
-
 val distributionOutput by configurations.creating {
     isCanBeConsumed = true
     isCanBeResolved = false

buildSrc/src/main/kotlin/hu/bme/mit/semantifyr/gradle/conventions/jvm.gradle.kts

@@ -8,7 +8,6 @@ package hu.bme.mit.semantifyr.gradle.conventions
 
 import org.gradle.accessors.dm.LibrariesForLibs
 import org.gradle.api.tasks.testing.logging.TestExceptionFormat
-import org.gradle.kotlin.dsl.registering
 
 plugins {
     `java-library`
@@ -39,8 +38,12 @@ java.toolchain {
 }
 
 tasks {
+    // TODO: refactor tests to use test suites
     test {
         useJUnitPlatform {
+            // we should use source sets instead
+            excludeTags("benchmark")
+            excludeTags("verification")
             excludeTags("slow")
         }
 
@@ -52,17 +55,8 @@ tasks {
         finalizedBy(tasks.jacocoTestReport)
     }
 
-    val allTests by tasks.registering(Test::class) {
-        useJUnitPlatform()
-
-        minHeapSize = "512m"
-        maxHeapSize = "4G"
-        testLogging.showStandardStreams = true
-
-        finalizedBy(tasks.jacocoTestReport)
-    }
-
     jacocoTestReport {
         inputs.files(test.get().outputs)
+        executionData(test.get())
     }
 }

buildSrc/src/main/kotlin/hu/bme/mit/semantifyr/gradle/conventions/theta.gradle.kts

@@ -0,0 +1,113 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.gradle.conventions
+
+import org.gradle.api.tasks.testing.logging.TestExceptionFormat
+
+plugins {
+    id("hu.bme.mit.semantifyr.gradle.conventions.jvm")
+}
+
+val thetaClasspath by configurations.creating {
+    isCanBeConsumed = false
+    isCanBeResolved = true
+}
+
+dependencies {
+    thetaClasspath(project(":theta-wrapper", configuration = "thetaOutput"))
+}
+
+/*
+ * Simple Build service that acts as a lock or throttling device preventing parallel execution
+ */
+abstract class VerificationTestService : BuildService<BuildServiceParameters.None>
+
+val verificationTestServiceName = "verificationTestService"
+val verificationTestServiceProvider = gradle.sharedServices.registerIfAbsent(verificationTestServiceName, VerificationTestService::class) {
+    // only allow at most 1 verification task per Gradle build
+    maxParallelUsages.set(1)
+}
+
+tasks {
+    val testVerificationCases by tasks.registering(Test::class) {
+        inputs.files(thetaClasspath)
+
+        group = "verification"
+
+        useJUnitPlatform {
+            // we should use source sets instead
+            excludeTags("benchmark")
+            includeTags("verification")
+            excludeTags("slow")
+        }
+
+        testClassesDirs = sourceSets.test.get().output.classesDirs
+        classpath = sourceSets.test.get().runtimeClasspath
+
+        usesService(verificationTestServiceProvider)
+
+        minHeapSize = "512m"
+        maxHeapSize = "4G"
+        testLogging.showStandardStreams = true
+        testLogging.exceptionFormat = TestExceptionFormat.FULL
+
+        maxParallelForks = 1
+
+        val thetaCliPath = project(":theta-wrapper").layout.buildDirectory.dir("theta-xsts-cli").get().asFile.absolutePath
+        val existingPath = environment["PATH"] ?: System.getenv("PATH") ?: ""
+        environment("PATH", "$thetaCliPath${File.pathSeparator}$existingPath")
+
+        shouldRunAfter(test)
+        finalizedBy(jacocoTestReport)
+    }
+
+    val testSlowVerificationCases by tasks.registering(Test::class) {
+        inputs.files(thetaClasspath)
+
+        group = "verification"
+
+        useJUnitPlatform {
+            // we should use source sets instead
+            excludeTags("benchmark")
+//            includeTags("verification")
+            includeTags("slow")
+        }
+
+        testClassesDirs = sourceSets.test.get().output.classesDirs
+        classpath = sourceSets.test.get().runtimeClasspath
+
+        usesService(verificationTestServiceProvider)
+
+        minHeapSize = "512m"
+        maxHeapSize = "4G"
+        testLogging.showStandardStreams = true
+        testLogging.exceptionFormat = TestExceptionFormat.FULL
+
+        val thetaCliPath = project(":theta-wrapper").layout.buildDirectory.dir("theta-xsts-cli").get().asFile.absolutePath
+        val existingPath = environment["PATH"] ?: System.getenv("PATH") ?: ""
+        environment("PATH", "$thetaCliPath${File.pathSeparator}$existingPath")
+
+        maxParallelForks = 1
+    }
+
+    val allTests by tasks.registering(DefaultTask::class) {
+        group = "verification"
+
+        dependsOn(test)
+        dependsOn(testVerificationCases)
+        dependsOn(testSlowVerificationCases)
+    }
+
+    jacocoTestReport {
+        inputs.files(testVerificationCases.get().outputs)
+        executionData(testVerificationCases.get())
+    }
+
+    check {
+        inputs.files(testVerificationCases.get().outputs)
+    }
+}

buildSrc/src/main/kotlin/hu/bme/mit/semantifyr/gradle/xtext.gradle.kts

@@ -7,7 +7,6 @@
 package hu.bme.mit.semantifyr.gradle
 
 import org.gradle.accessors.dm.LibrariesForLibs
-import org.gradle.kotlin.dsl.the
 
 plugins {
     id("hu.bme.mit.semantifyr.gradle.mwe2")
@@ -66,7 +65,7 @@ val generateXtextLanguage by tasks.registering(JavaExec::class) {
     outputs.dir(extension.testFixtureGenPath)
     outputs.dir(extension.ideOutput)
 
-    args(extension.mweFile.asFile.get(), "-p", "rootPath=/$projectDir/..")
+    args(extension.mweFile.get(), "-p", "rootPath=/$projectDir/..")
 }
 
 artifacts {
@@ -99,7 +98,7 @@ tasks {
 interface XtextPluginConfiguration {
     val genPath: DirectoryProperty
     val testFixtureGenPath: DirectoryProperty
-    val mweFile: RegularFileProperty
-    val xtextFile: RegularFileProperty
+    val mweFile: Property<String>
+    val xtextFile: Property<String>
     val ideOutput: DirectoryProperty
 }

gradle.properties

@@ -7,4 +7,5 @@ org.gradle.jvmargs=-Xmx2048M
 org.gradle.cache=true
 org.gradle.configuration-cache=true
 org.gradle.parallel=true
-thetaVersion=6.5.2
+thetaXstsCliVersion=6.27.14
+version=0.1.0

gradle/libs.versions.toml

@@ -6,7 +6,6 @@
 ecore = "2.41.0"
 junit = "6.0.3"
 assertj = "3.27.7"
-junitplatform = "6.0.3"
 mockito = "5.21.0"
 mwe2 = "2.25.0"
 slf4j = "2.0.17"
@@ -20,11 +19,12 @@ viatra = "2.9.1"
 dockerJava = "3.7.0"
 guice = "7.0.0"
 node = "7.1.0"
+bmuschkoDocker = "9.4.0"
 
 [libraries]
 ecore = { group = "org.eclipse.emf", name = "org.eclipse.emf.ecore", version.ref = "ecore" }
 ecore-codegen = { group = "org.eclipse.emf", name = "org.eclipse.emf.codegen.ecore", version.ref = "ecore" }
-junit-platform-launcher = { group = "org.junit.platform", name = "junit-platform-launcher", version.ref = "junitplatform" }
+junit-platform-launcher = { group = "org.junit.platform", name = "junit-platform-launcher", version.ref = "junit" }
 junit-api = { group = "org.junit.jupiter", name = "junit-jupiter-api", version.ref = "junit" }
 junit-engine = { group = "org.junit.jupiter", name = "junit-jupiter-engine", version.ref = "junit" }
 junit-params = { group = "org.junit.jupiter", name = "junit-jupiter-params", version.ref = "junit" }
@@ -52,10 +52,11 @@ viatra-query-runtime = { group = "org.eclipse.viatra", name = "viatra-query-runt
 viatra-transformation-runtime = { group = "org.eclipse.viatra", name = "viatra-transformation-runtime", version.ref = "viatra" }
 guice = { group = "com.google.inject", name = "guice", version.ref = "guice" }
 guice-extensions-assistedinject = { group = "com.google.inject.extensions", name = "guice-assistedinject", version.ref = "guice" }
-docker-java-core = { group = "com.github.docker-java" , name = "docker-java-core", version.ref = "dockerJava" }
-docker-java-transport = { group = "com.github.docker-java" , name = "docker-java-transport-httpclient5", version.ref = "dockerJava" }
+docker-java-core = { group = "com.github.docker-java", name = "docker-java-core", version.ref = "dockerJava" }
+docker-java-transport = { group = "com.github.docker-java", name = "docker-java-transport-httpclient5", version.ref = "dockerJava" }
 
 [plugins]
 kotlin-jvm = { id = "org.jetbrains.kotlin.jvm", version.ref = "kotlin" }
 kotlin-serialization = { id = "org.jetbrains.kotlin.plugin.serialization", version.ref = "kotlin" }
 gradle-node = { id = "com.github.node-gradle.node", version.ref = "node" }
+bmuschko-docker = { id = "com.bmuschko.docker-remote-api", version.ref = "bmuschkoDocker" }

settings.gradle.kts

@@ -31,4 +31,5 @@ fun includeDirectory(dirPath: String) {
 }
 
 includeDirectory("subprojects/frontends/gamma")
+includeDirectory("subprojects/frontends/sysmlv2")
 includeDirectory("subprojects/backends/theta")

subprojects/backends/theta/cex.lang.ide/src/main/resources/log4j2.properties

@@ -0,0 +1,14 @@
+#
+# SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+#
+# SPDX-License-Identifier: EPL-2.0
+#
+
+rootLogger.level=WARN
+rootLogger.appenderRef.file.ref=FileAppender
+
+appender.file.name=FileAppender
+appender.file.type=File
+appender.file.fileName=cex.lsp.log
+appender.file.layout.type=PatternLayout
+appender.file.layout.pattern=%p\t%d{ISO8601}\t%r\t%c\t[%t]\t%m%n

subprojects/backends/theta/cex.lang/build.gradle.kts

@@ -9,6 +9,6 @@ plugins {
 }
 
 xtext {
-    mweFile = layout.projectDirectory.file("src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2")
-    xtextFile = layout.projectDirectory.file("src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext")
+    mweFile = "src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2"
+    xtextFile = "src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext"
 }

subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexStandaloneSetup.java

@@ -9,7 +9,7 @@
  */
 public class CexStandaloneSetup extends CexStandaloneSetupGenerated {
 
-	public static void doSetup() {
-		new CexStandaloneSetup().createInjectorAndDoEMFRegistration();
-	}
+    public static void doSetup() {
+        new CexStandaloneSetup().createInjectorAndDoEMFRegistration();
+    }
 }

subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/validation/CexValidator.java

@@ -10,7 +10,7 @@
  * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#validation
  */
 public class CexValidator extends AbstractCexValidator {
-	
+
 //	public static final String INVALID_NAME = "invalidName";
 //
 //	@Check
@@ -21,5 +21,5 @@ public class CexValidator extends AbstractCexValidator {
 //					INVALID_NAME);
 //		}
 //	}
-	
+
 }