#18 Implemented CEX Witness serialization

.github/workflows/build.yml

@@ -30,7 +30,7 @@ jobs:
     - name: Set up JDK
       uses: actions/setup-java@v4
       with:
-        java-version: 17
+        java-version: 21
         distribution: adopt
     - name: Setup Gradle
       uses: gradle/actions/setup-gradle@v4

.github/workflows/dependency.yml

@@ -16,7 +16,7 @@ jobs:
       - uses: actions/setup-java@v4
         with:
           distribution: temurin
-          java-version: 17
+          java-version: 21
 
       - name: Generate and submit dependency graph
         uses: gradle/actions/dependency-submission@v4

README.md

@@ -10,7 +10,7 @@ A framework to support the declarative definition of engineering model semantics
 
 ## Build
 
-Use Java 17 for building.
+Use Java 21 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.
 

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

@@ -32,7 +32,7 @@ dependencies {
 }
 
 java.toolchain {
-    languageVersion.set(JavaLanguageVersion.of(17))
+    languageVersion.set(JavaLanguageVersion.of(21))
 }
 
 tasks {

settings.gradle.kts

@@ -10,6 +10,8 @@ include(
     "semantifyr",
     "xsts.lang",
     "xsts.lang.ide",
+    "cex.lang",
+    "cex.lang.ide",
     "oxsts.model",
     "oxsts.lang",
     "oxsts.lang.ide",

subprojects/cex.lang.ide/.gitignore

@@ -0,0 +1,6 @@
+# SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+#
+# SPDX-License-Identifier: EPL-2.0
+
+/src/main/xtext-gen/
+!.gitignore

subprojects/cex.lang.ide/build.gradle.kts

@@ -0,0 +1,56 @@
+/*
+ * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+plugins {
+    id("hu.bme.mit.semantifyr.gradle.xtext-generated")
+    id("hu.bme.mit.semantifyr.gradle.conventions.application")
+}
+
+val ideGeneratedClasspath by configurations.creating {
+    isCanBeConsumed = false
+    isCanBeResolved = true
+}
+
+dependencies {
+    api(project(":cex.lang"))
+
+    implementation(libs.xtext.ide)
+    runtimeOnly(libs.slf4j.log4j)
+
+    ideGeneratedClasspath(project(":cex.lang", configuration = "ideGeneratedOutput"))
+}
+
+val distributionOutput by configurations.creating {
+    isCanBeConsumed = true
+    isCanBeResolved = false
+}
+
+artifacts {
+    add(distributionOutput.name, layout.buildDirectory.dir("install")) {
+        builtBy(tasks.installDist)
+    }
+}
+
+val cloneIdeGenerated by tasks.registering(Sync::class) {
+    inputs.files(ideGeneratedClasspath)
+
+    from(ideGeneratedClasspath.asFileTree)
+    into("src/main/xtext-gen")
+}
+
+listOf("compileJava", "processResources").forEach { task ->
+    tasks.named(task) {
+        inputs.files(cloneIdeGenerated.get().outputs)
+    }
+}
+
+tasks.clean {
+    delete("src/main/xtext-gen")
+}
+
+application {
+    mainClass = "hu.bme.mit.semantifyr.cex.lang.ide.CexIdeSetup"
+}

subprojects/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeModule.java

@@ -0,0 +1,14 @@
+/*
+ * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.cex.lang.ide;
+
+/**
+ * Use this class to register ide components.
+ */
+public class CexIdeModule extends AbstractCexIdeModule {
+
+}

subprojects/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeSetup.java

@@ -0,0 +1,42 @@
+/*
+ * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.cex.lang.ide;
+
+import com.google.inject.Guice;
+import com.google.inject.Injector;
+import hu.bme.mit.semantifyr.cex.lang.CexRuntimeModule;
+import hu.bme.mit.semantifyr.cex.lang.CexStandaloneSetup;
+import org.eclipse.lsp4j.jsonrpc.Launcher;
+import org.eclipse.lsp4j.services.LanguageClient;
+import org.eclipse.xtext.ide.server.LanguageServerImpl;
+import org.eclipse.xtext.ide.server.ServerModule;
+import org.eclipse.xtext.util.Modules2;
+
+import java.util.concurrent.ExecutionException;
+
+/**
+ * Initialization support for running Xtext languages as language servers.
+ */
+public class CexIdeSetup extends CexStandaloneSetup {
+
+	@Override
+	public Injector createInjector() {
+		return Guice.createInjector(Modules2.mixin(new CexRuntimeModule(), new CexIdeModule()));
+	}
+
+    public static void main(String[] args) throws InterruptedException, ExecutionException {
+        CexIdeSetup.doSetup();
+
+        Injector injector = Guice.createInjector(new ServerModule());
+        LanguageServerImpl languageServer = injector.getInstance(LanguageServerImpl.class);
+
+        Launcher<LanguageClient> launcher = Launcher.createLauncher(languageServer, LanguageClient.class, System.in, System.out);
+        languageServer.connect(launcher.getRemoteProxy());
+        launcher.startListening().get();
+    }
+
+}

subprojects/cex.lang.ide/src/main/resources/plugin.properties

@@ -0,0 +1,5 @@
+# SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+#
+# SPDX-License-Identifier: EPL-2.0
+
+_UI_DiagnosticRoot_diagnostic=Specified, so the LSP server functions correctly

subprojects/cex.lang/.gitignore

@@ -0,0 +1,7 @@
+# SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+#
+# SPDX-License-Identifier: EPL-2.0
+
+model/
+/src/main/xtext-gen/
+/src/testFixtures/xtext-gen/

subprojects/cex.lang/build.gradle.kts

@@ -0,0 +1,65 @@
+/*
+ * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+plugins {
+    id("hu.bme.mit.semantifyr.gradle.xtext-generated")
+}
+
+dependencies {
+    implementation(platform(libs.xtext.bom))
+    implementation(libs.xtext.core)
+    implementation(libs.xtext.xbase)
+
+    testFixturesApi(libs.xtext.testing)
+
+    mwe2(libs.xtext.generator)
+    mwe2(libs.xtext.generator.antlr)
+}
+
+val generateXtextLanguage by tasks.registering(JavaExec::class) {
+    mainClass.set("org.eclipse.emf.mwe2.launch.runtime.Mwe2Launcher")
+    classpath(configurations.mwe2)
+
+    inputs.file("src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2")
+    inputs.file("src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext")
+
+    outputs.dir("src/main/xtext-gen")
+    outputs.dir("src/testFixtures/xtext-gen")
+    outputs.dir(layout.buildDirectory.dir("generated/sources/xtext/ide"))
+
+    args("src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2", "-p", "rootPath=/$projectDir/..")
+}
+
+val ideGeneratedOutput by configurations.creating {
+    isCanBeConsumed = true
+    isCanBeResolved = false
+}
+
+artifacts {
+    add(ideGeneratedOutput.name, layout.buildDirectory.dir("generated/sources/xtext/ide")) {
+        builtBy(generateXtextLanguage)
+    }
+}
+
+tasks {
+    jar {
+        from(sourceSets.main.map { it.allSource }) {
+            include("**/*.xtext")
+        }
+    }
+
+    listOf("compileJava", "processResources", "compileTestJava", "compileTestFixturesJava", "processTestFixturesResources").forEach { task ->
+        named(task) {
+            inputs.files(generateXtextLanguage.get().outputs)
+        }
+    }
+
+    clean {
+        delete("src/main/xtext-gen")
+        delete("src/test/java")
+        delete("src/testFixtures/xtext-gen")
+    }
+}

subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext

@@ -0,0 +1,73 @@
+/*
+ * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+grammar hu.bme.mit.semantifyr.cex.lang.Cex with org.eclipse.xtext.common.Terminals
+
+generate cex "http://www.bme.hu/mit/2024/cex"
+
+import "http://www.eclipse.org/emf/2002/Ecore" as Ecore
+
+Cex:
+	"(" ("XstsStateSequence" | "XstsCliTracegen")
+	    (states += XstsState)*
+
+	    (edges += StateEdge)*
+	")"
+;
+
+StateEdge:
+    from=[XstsState] "->" to=[XstsState]
+;
+
+XstsState:
+    "(" (name=ID ":")? "XstsState" (preInit?="pre_init")? (postInit?="post_init")? (lastEnv?="last_env")? (lastInternal?="last_internal")?
+        state = State
+    ")"
+;
+
+State:
+    ExplState
+;
+
+ExplState:
+    "(" "ExplState"
+        (variableStates += ExplVariableState)*
+    ")"
+;
+
+ExplVariableState:
+    "("
+        variable=ID value=ExplVariableValue
+    ")"
+;
+
+ExplVariableValue:
+    LiteralInteger
+    | LiteralBoolean
+    | LiteralEnum
+;
+
+LiteralEnum:
+    type=ID "." value=ID
+;
+
+LiteralBoolean:
+	value = BooleanValue
+;
+
+LiteralInteger:
+	value = SignedInt
+;
+
+BooleanValue returns Ecore::EBoolean:
+	'true' | 'false'
+;
+
+SignedInt returns Ecore::EInt:
+    ('-')? INT
+;
+
+terminal ID: '^'?('a'..'z'|'A'..'Z'|'_'|'$') ('a'..'z'|'A'..'Z'|'_'|'0'..'9'|'$')*;

subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexRuntimeModule.java

@@ -0,0 +1,11 @@
+/*
+ * generated by Xtext 2.36.0
+ */
+package hu.bme.mit.semantifyr.cex.lang;
+
+
+/**
+ * Use this class to register components to be used at runtime / without the Equinox extension registry.
+ */
+public class CexRuntimeModule extends AbstractCexRuntimeModule {
+}

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

@@ -0,0 +1,15 @@
+/*
+ * generated by Xtext 2.36.0
+ */
+package hu.bme.mit.semantifyr.cex.lang;
+
+
+/**
+ * Initialization support for running Xtext languages without Equinox extension registry.
+ */
+public class CexStandaloneSetup extends CexStandaloneSetupGenerated {
+
+	public static void doSetup() {
+		new CexStandaloneSetup().createInjectorAndDoEMFRegistration();
+	}
+}