= emptyList(),
+ val logFile: File? = null,
+ val errorFile: File? = null,
+)
+
+class SpinReplaySpecification(
+ val workingDirectory: File,
+ val modelFileName: String,
+ val logFile: File,
+ val errorFile: File? = null,
+)
+
+interface SpinExecutor : BackendExecutor {
+ suspend fun execute(specification: SpinExecutionSpecification): SpinExecutionResult
+
+ suspend fun replayTrail(specification: SpinReplaySpecification): SpinExecutionResult
+
+ companion object {
+ fun shell(): SpinExecutor {
+ return ShellBasedSpinExecutor()
+ }
+
+ fun autoDetect(): SpinExecutor {
+ return shell()
+ }
+ }
+}
diff --git a/subprojects/backends/spin/spin-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/spin/execution/ShellBasedSpinExecutor.kt b/subprojects/backends/spin/spin-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/spin/execution/ShellBasedSpinExecutor.kt
new file mode 100644
index 00000000..6712a205
--- /dev/null
+++ b/subprojects/backends/spin/spin-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/spin/execution/ShellBasedSpinExecutor.kt
@@ -0,0 +1,41 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.spin.execution
+
+import hu.bme.mit.semantifyr.backend.execution.ShellBasedBackendExecutor
+import hu.bme.mit.semantifyr.backends.spin.SpinExecutionResult
+import hu.bme.mit.semantifyr.backends.spin.SpinExecutionSpecification
+import hu.bme.mit.semantifyr.backends.spin.SpinExecutor
+import hu.bme.mit.semantifyr.backends.spin.SpinReplaySpecification
+
+class ShellBasedSpinExecutor :
+ ShellBasedBackendExecutor(),
+ SpinExecutor {
+ override val binaryName = "spin"
+
+ override suspend fun execute(specification: SpinExecutionSpecification): SpinExecutionResult {
+ val args = listOf("-search") + specification.extraArguments + listOf(specification.modelFileName)
+ val exitCode = runProcess(
+ args = args,
+ workingDirectory = specification.workingDirectory,
+ logFile = specification.logFile,
+ errorFile = specification.errorFile,
+ )
+ return SpinExecutionResult(exitCode)
+ }
+
+ override suspend fun replayTrail(specification: SpinReplaySpecification): SpinExecutionResult {
+ val args = listOf("-t", "-p", "-g", specification.modelFileName)
+ val exitCode = runProcess(
+ args = args,
+ workingDirectory = specification.workingDirectory,
+ logFile = specification.logFile,
+ errorFile = specification.errorFile,
+ )
+ return SpinExecutionResult(exitCode)
+ }
+}
diff --git a/subprojects/backends/theta/cex.lang.ide/.gitignore b/subprojects/backends/theta/cex.lang.ide/.gitignore
deleted file mode 100644
index ae7eb7e8..00000000
--- a/subprojects/backends/theta/cex.lang.ide/.gitignore
+++ /dev/null
@@ -1,6 +0,0 @@
-# SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
-#
-# SPDX-License-Identifier: EPL-2.0
-
-/src/main/xtext-gen/
-!.gitignore
diff --git a/subprojects/backends/theta/cex.lang.ide/build.gradle.kts b/subprojects/backends/theta/cex.lang.ide/build.gradle.kts
deleted file mode 100644
index d210b1c3..00000000
--- a/subprojects/backends/theta/cex.lang.ide/build.gradle.kts
+++ /dev/null
@@ -1,50 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-plugins {
- id("hu.bme.mit.semantifyr.gradle.conventions.application")
-}
-
-val ideGeneratedClasspath by configurations.creating {
- isCanBeConsumed = false
- isCanBeResolved = true
-}
-
-dependencies {
- api(project(":cex.lang"))
-
- api(libs.xtext.ide)
- runtimeOnly(libs.slf4j.log4j)
-
- ideGeneratedClasspath(project(":cex.lang", configuration = "ideGeneratedOutput"))
-}
-
-sourceSets {
- main {
- java.srcDir("src/main/xtext-gen")
- }
-}
-
-tasks {
- val cloneIdeGenerated by registering(Sync::class) {
- inputs.files(ideGeneratedClasspath)
-
- from(ideGeneratedClasspath.asFileTree)
- into("src/main/xtext-gen")
- }
-
- compileJava {
- inputs.files(cloneIdeGenerated.get().outputs)
- }
-
- clean {
- delete("src/main/xtext-gen")
- }
-}
-
-application {
- mainClass = "hu.bme.mit.semantifyr.cex.lang.ide.CexIdeSetup"
-}
diff --git a/subprojects/backends/theta/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeModule.java b/subprojects/backends/theta/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeModule.java
deleted file mode 100644
index 38d9a5b2..00000000
--- a/subprojects/backends/theta/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeModule.java
+++ /dev/null
@@ -1,14 +0,0 @@
-/*
- * 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 {
-
-}
diff --git a/subprojects/backends/theta/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeSetup.java b/subprojects/backends/theta/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeSetup.java
deleted file mode 100644
index 0cc265f1..00000000
--- a/subprojects/backends/theta/cex.lang.ide/src/main/java/hu/bme/mit/semantifyr/cex/lang/ide/CexIdeSetup.java
+++ /dev/null
@@ -1,77 +0,0 @@
-/*
- * 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.io.IOException;
-import java.net.ServerSocket;
-import java.nio.file.Files;
-import java.nio.file.Path;
-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 ServerModule(), new CexRuntimeModule(), new CexIdeModule()));
- }
-
- public static void main(String[] args) throws InterruptedException, ExecutionException, IOException {
- Files.deleteIfExists(Path.of("cex.lsp.log"));
-
- if (args.length == 2) {
- if (args[0].equals("--network")) {
- int port = Integer.parseInt(args[1]);
- runOnPort(port);
- return;
- }
- }
-
- runOnStdIo();
- }
-
- private static void runOnStdIo() throws ExecutionException, InterruptedException {
- Injector injector = new CexIdeSetup().createInjectorAndDoEMFRegistration();
- var languageServer = injector.getInstance(LanguageServerImpl.class);
-
- var launcher = Launcher.createLauncher(languageServer, LanguageClient.class, System.in, System.out);
- languageServer.connect(launcher.getRemoteProxy());
- launcher.startListening().get();
- }
-
- private static void runOnPort(int port) throws IOException, ExecutionException, InterruptedException {
- var injector = new CexIdeSetup().createInjectorAndDoEMFRegistration();
- var languageServer = injector.getInstance(LanguageServerImpl.class);
-
- try (var serverSocket = new ServerSocket(port)) {
- System.out.println("LSP server listening on port " + port);
- try (var clientSocket = serverSocket.accept()) {
- System.out.println("Client connected from " + clientSocket.getRemoteSocketAddress());
-
- var in = clientSocket.getInputStream();
- var out = clientSocket.getOutputStream();
-
- var launcher = Launcher.createLauncher(languageServer, LanguageClient.class, in, out);
- languageServer.connect(launcher.getRemoteProxy());
- launcher.startListening().get();
- }
- }
- }
-
-}
diff --git a/subprojects/backends/theta/cex.lang.ide/src/main/resources/log4j.properties b/subprojects/backends/theta/cex.lang.ide/src/main/resources/log4j.properties
deleted file mode 100644
index 39447047..00000000
--- a/subprojects/backends/theta/cex.lang.ide/src/main/resources/log4j.properties
+++ /dev/null
@@ -1,12 +0,0 @@
-#
-# SPDX-FileCopyrightText: 2025 The Semantifyr Authors
-#
-# SPDX-License-Identifier: EPL-2.0
-#
-
-log4j.rootLogger=WARNING,fout
-
-log4j.appender.fout=org.apache.log4j.FileAppender
-log4j.appender.fout.File=cex.lsp.log
-log4j.appender.fout.layout=org.apache.log4j.PatternLayout
-log4j.appender.fout.layout.ConversionPattern=%p\t%d{ISO8601}\t%r\t%c\t[%t]\t%m%n
diff --git a/subprojects/backends/theta/cex.lang.ide/src/main/resources/log4j2.properties b/subprojects/backends/theta/cex.lang.ide/src/main/resources/log4j2.properties
deleted file mode 100644
index faaa8cd9..00000000
--- a/subprojects/backends/theta/cex.lang.ide/src/main/resources/log4j2.properties
+++ /dev/null
@@ -1,14 +0,0 @@
-#
-# 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
diff --git a/subprojects/backends/theta/cex.lang.ide/src/main/resources/plugin.properties b/subprojects/backends/theta/cex.lang.ide/src/main/resources/plugin.properties
deleted file mode 100644
index c0f26175..00000000
--- a/subprojects/backends/theta/cex.lang.ide/src/main/resources/plugin.properties
+++ /dev/null
@@ -1,5 +0,0 @@
-# SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
-#
-# SPDX-License-Identifier: EPL-2.0
-
-_UI_DiagnosticRoot_diagnostic=Specified, so the LSP server functions correctly
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexRuntimeModule.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexRuntimeModule.java
index 678b89e0..c045ea7e 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexRuntimeModule.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexRuntimeModule.java
@@ -3,9 +3,8 @@
*/
package hu.bme.mit.semantifyr.cex.lang;
-
/**
- * Use this class to register components to be used at runtime / without the Equinox extension registry.
+ * Use this class to register components to be used at runtime / without the Equinox extension
+ * registry.
*/
-public class CexRuntimeModule extends AbstractCexRuntimeModule {
-}
+public class CexRuntimeModule extends AbstractCexRuntimeModule {}
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexStandaloneSetup.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexStandaloneSetup.java
index 46d8f542..e94a8647 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexStandaloneSetup.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/CexStandaloneSetup.java
@@ -3,10 +3,7 @@
*/
package hu.bme.mit.semantifyr.cex.lang;
-
-/**
- * Initialization support for running Xtext languages without Equinox extension registry.
- */
+/** Initialization support for running Xtext languages without Equinox extension registry. */
public class CexStandaloneSetup extends CexStandaloneSetupGenerated {
public static void doSetup() {
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2 b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2
index 51e3d2e6..25239e85 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2
@@ -21,16 +21,11 @@ Workflow {
src = null
}
runtimeTest = {
- enabled = true
+ enabled = false
// Only generate the xtext-gen files and leave the rest of the project alone
root = null
srcGen = '${rootPath}/cex.lang/src/testFixtures/xtext-gen'
}
- genericIde = {
- enabled = true
- root = null
- srcGen = "${rootPath}/cex.lang/build/generated/sources/xtext/ide"
- }
mavenLayout = true
}
code = {
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/formatting2/CexFormatter.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/formatting2/CexFormatter.java
index 572563c2..1b7f45ed 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/formatting2/CexFormatter.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/formatting2/CexFormatter.java
@@ -5,6 +5,4 @@
import org.eclipse.xtext.formatting2.AbstractJavaFormatter;
-public class CexFormatter extends AbstractJavaFormatter {
-
-}
+public class CexFormatter extends AbstractJavaFormatter {}
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/scoping/CexScopeProvider.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/scoping/CexScopeProvider.java
index cd4c8dd7..b9c01b1f 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/scoping/CexScopeProvider.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/scoping/CexScopeProvider.java
@@ -3,13 +3,10 @@
*/
package hu.bme.mit.semantifyr.cex.lang.scoping;
-
/**
* This class contains custom scoping description.
- *
- * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping
- * on how and when to use it.
+ *
+ * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#scoping on how and
+ * when to use it.
*/
-public class CexScopeProvider extends AbstractCexScopeProvider {
-
-}
+public class CexScopeProvider extends AbstractCexScopeProvider {}
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSemanticSequencer.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSemanticSequencer.java
index 79f3d40f..978f99cf 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSemanticSequencer.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSemanticSequencer.java
@@ -3,6 +3,4 @@
*/
package hu.bme.mit.semantifyr.cex.lang.serializer;
-
-public class CexSemanticSequencer extends AbstractCexSemanticSequencer {
-}
+public class CexSemanticSequencer extends AbstractCexSemanticSequencer {}
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSyntacticSequencer.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSyntacticSequencer.java
index 3626d236..4ac3d3c7 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSyntacticSequencer.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/serializer/CexSyntacticSequencer.java
@@ -3,6 +3,4 @@
*/
package hu.bme.mit.semantifyr.cex.lang.serializer;
-
-public class CexSyntacticSequencer extends AbstractCexSyntacticSequencer {
-}
+public class CexSyntacticSequencer extends AbstractCexSyntacticSequencer {}
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/utils/CexExpressionVisitor.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/utils/CexExpressionVisitor.java
index e264f920..4c7f4dbe 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/utils/CexExpressionVisitor.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/utils/CexExpressionVisitor.java
@@ -30,7 +30,8 @@ protected T visit(LiteralExpression expression) {
}
protected abstract T visit(LiteralInteger expression);
+
protected abstract T visit(LiteralBoolean expression);
- protected abstract T visit(LiteralEnum expression);
+ protected abstract T visit(LiteralEnum expression);
}
diff --git a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/validation/CexValidator.java b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/validation/CexValidator.java
index dc30b827..d93c02b5 100644
--- a/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/validation/CexValidator.java
+++ b/subprojects/backends/theta/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/validation/CexValidator.java
@@ -3,23 +3,22 @@
*/
package hu.bme.mit.semantifyr.cex.lang.validation;
-
/**
- * This class contains custom validation rules.
+ * This class contains custom validation rules.
*
- * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#validation
+ *
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
-// public void checkGreetingStartsWithCapital(Greeting greeting) {
-// if (!Character.isUpperCase(greeting.getName().charAt(0))) {
-// warning("Name should start with a capital",
-// CexPackage.Literals.GREETING__NAME,
-// INVALID_NAME);
-// }
-// }
+ // public static final String INVALID_NAME = "invalidName";
+ //
+ // @Check
+ // public void checkGreetingStartsWithCapital(Greeting greeting) {
+ // if (!Character.isUpperCase(greeting.getName().charAt(0))) {
+ // warning("Name should start with a capital",
+ // CexPackage.Literals.GREETING__NAME,
+ // INVALID_NAME);
+ // }
+ // }
}
diff --git a/subprojects/backends/theta/theta-backend/build.gradle.kts b/subprojects/backends/theta/theta-backend/build.gradle.kts
new file mode 100644
index 00000000..f7b8b7db
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/build.gradle.kts
@@ -0,0 +1,23 @@
+/*
+ * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+plugins {
+ id("hu.bme.mit.semantifyr.gradle.conventions.backend")
+ kotlin("jvm")
+ kotlin("plugin.serialization")
+}
+
+dependencies {
+ api(project(":backend"))
+ api(project(":xsts.lang"))
+ api(project(":theta-executor"))
+ api(libs.guice.extensions.assistedinject)
+
+ implementation(project(":logging"))
+ implementation(libs.kotlinx.serialization.json)
+
+ testImplementation(testFixtures(project(":backend")))
+}
diff --git a/subprojects/backends/theta/theta-backend/src/integrationTest/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaSemanticConformanceTest.kt b/subprojects/backends/theta/theta-backend/src/integrationTest/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaSemanticConformanceTest.kt
new file mode 100644
index 00000000..3902957b
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/integrationTest/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaSemanticConformanceTest.kt
@@ -0,0 +1,61 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta
+
+import hu.bme.mit.semantifyr.backends.theta.execution.ShellBasedThetaXstsExecutor
+import hu.bme.mit.semantifyr.oxsts.lang.OxstsStandaloneSetup
+import hu.bme.mit.semantifyr.portfolios.Portfolios
+import hu.bme.mit.semantifyr.verifier.SemantifyrVerifierTestHelper
+import hu.bme.mit.semantifyr.verifier.VerificationCase
+import hu.bme.mit.semantifyr.verifier.portfolio.SingleBackendPortfolio
+import org.junit.jupiter.api.Assumptions
+import org.junit.jupiter.api.BeforeAll
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.Arguments
+import org.junit.jupiter.params.provider.MethodSource
+import kotlin.io.path.Path
+
+class ThetaSemanticConformanceTest {
+
+ companion object {
+
+ private val injector = OxstsStandaloneSetup().createInjectorAndDoEMFRegistration()
+ private val helper = injector.getInstance(SemantifyrVerifierTestHelper::class.java)
+
+ private val context by lazy {
+ helper.semantifyrLoader.startContext()
+ .loadModels(Path("build/test-models/semantic"))
+ .buildAndResolve()
+ }
+
+ @JvmStatic
+ @BeforeAll
+ fun assumeThetaAvailable() {
+ Assumptions.assumeTrue(
+ ShellBasedThetaXstsExecutor().isAvailable(),
+ "theta-xsts-cli not on PATH - skipping Theta conformance tests",
+ )
+ }
+
+ @JvmStatic
+ fun `OXSTS Semantic Test Suite Passes`(): List {
+ return helper.collectVerificationCasesAsArguments(context)
+ }
+ }
+
+ @ParameterizedTest
+ @MethodSource
+ suspend fun `OXSTS Semantic Test Suite Passes`(verificationCase: VerificationCase) {
+ helper.checkTestModel(
+ context,
+ verificationCase,
+ verificationPortfolio = SingleBackendPortfolio(ThetaBackend(), ThetaConfig.CegarExplPredCombined),
+ outputDirectory = SemantifyrVerifierTestHelper.testArtifactRoot(ThetaSemanticConformanceTest::class.java),
+ validationPortfolio = Portfolios.AllAgree,
+ )
+ }
+}
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaBackend.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaBackend.kt
new file mode 100644
index 00000000..91609429
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaBackend.kt
@@ -0,0 +1,163 @@
+/*
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta
+
+import com.google.inject.AbstractModule
+import com.google.inject.Injector
+import com.google.inject.assistedinject.Assisted
+import com.google.inject.assistedinject.AssistedInject
+import com.google.inject.assistedinject.FactoryModuleBuilder
+import hu.bme.mit.semantifyr.backend.BackendVerificationRequest
+import hu.bme.mit.semantifyr.backend.BackendVerificationResult
+import hu.bme.mit.semantifyr.backend.VerificationBackend
+import hu.bme.mit.semantifyr.backend.VerificationContext
+import hu.bme.mit.semantifyr.backend.VerificationVerdict
+import hu.bme.mit.semantifyr.backend.execution.ExecutionEnvironment
+import hu.bme.mit.semantifyr.backend.scopes.VerificationScope
+import hu.bme.mit.semantifyr.backend.scopes.VerificationScoped
+import hu.bme.mit.semantifyr.backend.scopes.withVerificationScope
+import hu.bme.mit.semantifyr.backend.witness.InlinedWitness
+import hu.bme.mit.semantifyr.backends.theta.artifacts.ThetaArtifactManager
+import hu.bme.mit.semantifyr.backends.theta.backannotation.CexReader
+import hu.bme.mit.semantifyr.backends.theta.backannotation.CexWitnessTransformer
+import hu.bme.mit.semantifyr.backends.theta.backannotation.InlinedWitnessTransformer
+import hu.bme.mit.semantifyr.backends.theta.backannotation.XstsWitnessTransformer
+import hu.bme.mit.semantifyr.backends.theta.transformation.xsts.ThetaModelTransformer
+import hu.bme.mit.semantifyr.logging.debug
+import hu.bme.mit.semantifyr.logging.info
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.AG
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.EF
+import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
+import java.nio.file.Path
+
+class ThetaBackend : VerificationBackend() {
+
+ override val id = "theta"
+ override val executorKey = ThetaExecutorKey
+
+ override suspend fun verify(
+ parentInjector: Injector,
+ config: ThetaConfig,
+ request: BackendVerificationRequest,
+ environment: ExecutionEnvironment,
+ ): BackendVerificationResult {
+ val executor = environment[ThetaExecutorKey]
+ logger.info { "[theta:${config.id}] dispatching via ${executor::class.simpleName}" }
+ val injector = parentInjector.createChildInjector(ThetaBackendModule())
+ return withVerificationScope {
+ val factory = injector.getInstance(ThetaVerificationContext.Factory::class.java)
+ val context = factory.create(config, executor, request)
+ context.execute()
+ }
+ }
+}
+
+class ThetaBackendModule : AbstractModule() {
+ override fun configure() {
+ bindScope(VerificationScoped::class.java, VerificationScope)
+ install(FactoryModuleBuilder().build(ThetaVerificationContext.Factory::class.java))
+
+ super.configure()
+ }
+}
+
+class ThetaVerificationContext @AssistedInject constructor(
+ @param:Assisted private val config: ThetaConfig,
+ @param:Assisted override val executor: ThetaXstsExecutor,
+ @Assisted request: BackendVerificationRequest,
+ private val thetaModelTransformer: ThetaModelTransformer,
+ private val cexReader: CexReader,
+ private val cexWitnessTransformer: CexWitnessTransformer,
+ private val xstsWitnessTransformer: XstsWitnessTransformer,
+ private val inlinedWitnessTransformer: InlinedWitnessTransformer,
+) : VerificationContext(
+ backendId = "theta:${config.id}",
+ request = request,
+) {
+
+ private val artifactManager = ThetaArtifactManager(request.artifactOutputPath)
+
+ override suspend fun prepare(): XstsModel {
+ logger.info { "[$backendId] transforming InlinedOxsts -> XSTS" }
+ val xsts = thetaModelTransformer.transform(request.inlinedOxsts, artifactManager.xstsUri)
+
+ val resourceSet = request.inlinedOxsts.eResource().resourceSet
+ resourceSet.getResource(artifactManager.xstsUri, false)?.delete(emptyMap())
+ val resource = resourceSet.createResource(artifactManager.xstsUri)
+ resource.contents += xsts
+ xsts.eResource().save(emptyMap())
+
+ return xsts
+ }
+
+ override suspend fun run(artifacts: XstsModel): ThetaVerdict? {
+ val workingDir = artifactManager.xstsFile.parentFile
+ val cexRelPath = artifactManager.cexFile.relativeTo(workingDir).path
+ val command = config.parameters.split(" ") + listOf("--model", artifactManager.xstsFile.name, "--cexfile", cexRelPath)
+
+ val spec = ThetaExecutionSpecification(
+ workingDirectory = workingDir,
+ command = command,
+ logFile = artifactManager.logFile,
+ errorFile = artifactManager.errorFile,
+ )
+
+ logger.debug { "[$backendId] invoking Theta: ${config.parameters}" }
+ val result = executor.execute(spec)
+
+ if (result.exitCode != 0) {
+ error("Theta execution failed with exit code ${result.exitCode}")
+ }
+
+ return spec.logFile?.takeIf { it.exists() }?.useLines { lines ->
+ lines.firstNotNullOfOrNull(::detectSafety)
+ }
+ }
+
+ override fun interpret(rawVerdict: ThetaVerdict?, artifacts: XstsModel): VerificationVerdict {
+ val property = request.inlinedOxsts.property.expression
+ return when {
+ property is AG && rawVerdict == ThetaVerdict.Unsafe -> VerificationVerdict.Failed
+ property is EF && rawVerdict == ThetaVerdict.Safe -> VerificationVerdict.Failed
+ rawVerdict == ThetaVerdict.Safe || rawVerdict == ThetaVerdict.Unsafe -> VerificationVerdict.Passed
+ else -> VerificationVerdict.Inconclusive
+ }
+ }
+
+ override suspend fun buildWitness(rawVerdict: ThetaVerdict?, artifacts: XstsModel): InlinedWitness? {
+ if (!artifactManager.cexFile.exists()) {
+ return null
+ }
+ return buildInlinedWitness(artifacts, artifactManager.cexFile.toPath())
+ }
+
+ private fun buildInlinedWitness(xsts: XstsModel, cexPath: Path): InlinedWitness {
+ logger.info { "[$backendId] building inlined-oxsts witness from CEX" }
+ val cexModel = cexReader.loadCexModel(cexPath)
+ val cexWitness = cexWitnessTransformer.transform(cexModel)
+ val xstsWitness = xstsWitnessTransformer.transform(xsts, cexWitness)
+ return inlinedWitnessTransformer.transform(request.inlinedOxsts, xstsWitness)
+ }
+
+ private fun detectSafety(line: String): ThetaVerdict? {
+ return when {
+ line.contains("SafetyResult Unsafe") -> ThetaVerdict.Unsafe
+ line.contains("SafetyResult Safe") -> ThetaVerdict.Safe
+ else -> null
+ }
+ }
+
+ enum class ThetaVerdict { Safe, Unsafe }
+
+ interface Factory {
+ fun create(
+ config: ThetaConfig,
+ executor: ThetaXstsExecutor,
+ request: BackendVerificationRequest,
+ ): ThetaVerificationContext
+ }
+}
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaConfig.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaConfig.kt
new file mode 100644
index 00000000..66095cc1
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaConfig.kt
@@ -0,0 +1,55 @@
+/*
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta
+
+import hu.bme.mit.semantifyr.backend.BackendConfig
+
+data class ThetaConfig(
+ override val id: String,
+ val parameters: String,
+) : BackendConfig {
+ companion object {
+ val CegarExpl = ThetaConfig(
+ id = "cegar-expl",
+ parameters = "CEGAR --domain EXPL --flatten-depth 0 --refinement SEQ_ITP --maxenum 250 --initprec CTRL --stacktrace",
+ )
+ val CegarExplPredCombined = ThetaConfig(
+ id = "cegar-expl-pred-combined",
+ parameters = "CEGAR --domain EXPL_PRED_COMBINED --flatten-depth 0 --autoexpl NEWOPERANDS --initprec CTRL --stacktrace",
+ )
+ val CegarPredCart = ThetaConfig(
+ id = "cegar-pred-cart",
+ parameters = "CEGAR --domain PRED_CART --flatten-depth 0 --refinement SEQ_ITP --stacktrace",
+ )
+ val BoundedKInduction = ThetaConfig(
+ id = "bounded-kinduction",
+ parameters = "BOUNDED --flatten-depth 0 --variant KINDUCTION --stacktrace",
+ )
+ val BoundedBmc = ThetaConfig(
+ id = "bounded-bmc",
+ parameters = "BOUNDED --flatten-depth 0 --variant BMC --stacktrace",
+ )
+ val BoundedImc = ThetaConfig(
+ id = "bounded-imc",
+ parameters = "BOUNDED --flatten-depth 0 --variant IMC --stacktrace",
+ )
+ val Ic3 = ThetaConfig(
+ id = "ic3",
+ parameters = "IC3 --flatten-depth 0 --stacktrace",
+ )
+
+ val Builtin: List = listOf(
+ CegarExpl,
+ CegarExplPredCombined,
+ CegarPredCart,
+ BoundedKInduction,
+ BoundedBmc,
+ BoundedImc,
+ Ic3,
+ )
+ }
+}
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/artifacts/ThetaArtifactManager.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/artifacts/ThetaArtifactManager.kt
new file mode 100644
index 00000000..595ce6e2
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/artifacts/ThetaArtifactManager.kt
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.artifacts
+
+import org.eclipse.emf.common.util.URI
+import java.io.File
+import java.nio.file.Path
+
+class ThetaArtifactManager(
+ private val rootDirectory: Path,
+) {
+
+ val xstsFile: File
+ get() = rootDirectory.resolve("inlined.xsts").toFile()
+
+ val xstsUri: URI
+ get() = URI.createFileURI(xstsFile.absolutePath)
+
+ val cexFile: File
+ get() = rootDirectory.resolve("out.cex").toFile()
+
+ val logFile: File
+ get() = rootDirectory.resolve("theta.out").toFile()
+
+ val errorFile: File
+ get() = rootDirectory.resolve("theta.err").toFile()
+}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/xsts/CexExpressionToXstsExpressionTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexExpressionToXstsExpressionTransformer.kt
similarity index 93%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/xsts/CexExpressionToXstsExpressionTransformer.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexExpressionToXstsExpressionTransformer.kt
index 08171b15..db8a98b6 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/xsts/CexExpressionToXstsExpressionTransformer.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexExpressionToXstsExpressionTransformer.kt
@@ -1,10 +1,10 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.xsts
+package hu.bme.mit.semantifyr.backends.theta.backannotation
import hu.bme.mit.semantifyr.cex.lang.cex.ArithmeticUnaryOperator
import hu.bme.mit.semantifyr.cex.lang.cex.LiteralBoolean
@@ -17,7 +17,7 @@ import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsFactory
import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
class CexExpressionToXstsExpressionTransformer(
- val xstsModel: XstsModel
+ val xstsModel: XstsModel,
) : CexExpressionVisitor() {
fun transform(expression: hu.bme.mit.semantifyr.cex.lang.cex.Expression): Expression {
@@ -68,5 +68,4 @@ class CexExpressionToXstsExpressionTransformer(
it.element = enumLiteral
}
}
-
}
diff --git a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/utils/CexReader.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexReader.kt
similarity index 65%
rename from subprojects/backends/theta/theta-wrapper/src/main/kotlin/utils/CexReader.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexReader.kt
index 9b7c6e33..0020fbd3 100644
--- a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/utils/CexReader.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexReader.kt
@@ -1,11 +1,12 @@
/*
- * SPDX-FileCopyrightText: 2023-2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.wrapper.utils
+package hu.bme.mit.semantifyr.backends.theta.backannotation
+import hu.bme.mit.semantifyr.backend.scopes.VerificationScoped
import hu.bme.mit.semantifyr.cex.lang.CexStandaloneSetup
import hu.bme.mit.semantifyr.cex.lang.cex.CexModel
import org.eclipse.emf.common.util.URI
@@ -15,10 +16,15 @@ import org.eclipse.xtext.resource.XtextResourceSet
import java.nio.file.Path
import kotlin.io.path.absolutePathString
+@VerificationScoped
class CexReader {
- private val cexInjector = CexStandaloneSetup().createInjectorAndDoEMFRegistration()
- private val resourceSetProvider = cexInjector.getProvider(XtextResourceSet::class.java)
+ private val cexInjector by lazy {
+ CexStandaloneSetup().createInjectorAndDoEMFRegistration()
+ }
+ private val resourceSetProvider by lazy {
+ cexInjector.getProvider(XtextResourceSet::class.java)
+ }
private fun loadFile(resourceSet: ResourceSet, path: Path): Resource {
return resourceSet.getResource(URI.createFileURI(path.absolutePathString()), true)
@@ -29,5 +35,4 @@ class CexReader {
val resource = loadFile(resourceSet, model)
return resource.contents.single() as CexModel
}
-
}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/cex/CexAssumptionWitness.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexWitness.kt
similarity index 58%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/cex/CexAssumptionWitness.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexWitness.kt
index 1cf4ba31..dcb85e03 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/cex/CexAssumptionWitness.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/CexWitness.kt
@@ -1,52 +1,51 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.cex
+package hu.bme.mit.semantifyr.backends.theta.backannotation
import hu.bme.mit.semantifyr.cex.lang.cex.CexModel
import hu.bme.mit.semantifyr.cex.lang.cex.ExplStateValue
import hu.bme.mit.semantifyr.cex.lang.cex.ExplVariableValue
import hu.bme.mit.semantifyr.cex.lang.cex.Expression
import hu.bme.mit.semantifyr.cex.lang.cex.XstsState
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.AssumptionWitness
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.AssumptionWitnessState
-class CexAssumptionWitnessStateVariableValue(
+class CexWitnessStateVariableValue(
val variableName: String,
val value: Expression,
)
-private fun ExplVariableValue.toCexVariable(): CexAssumptionWitnessStateVariableValue {
- return CexAssumptionWitnessStateVariableValue(
+private fun ExplVariableValue.toCexVariable(): CexWitnessStateVariableValue {
+ return CexWitnessStateVariableValue(
variable,
value,
)
}
-class CexAssumptionWitnessState(
-// id: String,
- val variableValues: List
-) : AssumptionWitnessState()
+class CexWitnessState(
+ val variableValues: List,
+)
-private fun XstsState.toCexState(): CexAssumptionWitnessState {
+private fun XstsState.toCexState(): CexWitnessState {
val state = stateValue
require(state is ExplStateValue)
- return CexAssumptionWitnessState(
- state.variableValues.map { it.toCexVariable() },
+ return CexWitnessState(
+ state.variableValues.map {
+ it.toCexVariable()
+ },
)
}
-class CexAssumptionWitness(
- override val initialState: CexAssumptionWitnessState,
- override val initializedState: CexAssumptionWitnessState?,
- override val transitionStates: List,
- override val nextStateMap: Map>,
-) : AssumptionWitness()
+class CexWitness(
+ val initialState: CexWitnessState,
+ val initializedState: CexWitnessState?,
+ val transitionStates: List,
+ val nextStateMap: Map>,
+)
private val XstsState.isTran
get() = isPostInit && isLastInternal
@@ -55,9 +54,9 @@ private val XstsState.isInitial
private val XstsState.isInitialized
get() = isPostInit && isLastInternal
-class CexAssumptionWitnessTransformer {
+class CexWitnessTransformer {
- fun transform(cexModel: CexModel): CexAssumptionWitness {
+ fun transform(cexModel: CexModel): CexWitness {
val initialState = cexModel.states.first()
val initializedState = cexModel.states.getOrNull(1)
val states = cexModel.states.drop(2).filter {
@@ -87,12 +86,11 @@ class CexAssumptionWitnessTransformer {
}
}
- return CexAssumptionWitness(
+ return CexWitness(
initialCexState,
initializedCexState,
cexStates,
nextStateMap,
)
}
-
}
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/InlinedWitnessTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/InlinedWitnessTransformer.kt
new file mode 100644
index 00000000..fd900dad
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/InlinedWitnessTransformer.kt
@@ -0,0 +1,77 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.backannotation
+
+import com.google.inject.Inject
+import hu.bme.mit.semantifyr.backend.witness.InlinedWitness
+import hu.bme.mit.semantifyr.backend.witness.WitnessState
+import hu.bme.mit.semantifyr.backend.witness.WitnessStateValue
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlinedOxsts
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.VariableDeclaration
+
+class InlinedWitnessTransformer @Inject constructor(
+ private val xstsExpressionToOxstsExpressionTransformer: XstsExpressionToOxstsExpressionTransformer,
+) {
+
+ private inner class TransformerContext(val inlinedOxsts: InlinedOxsts) {
+ val mappings = mutableMapOf()
+ val variablesByName: Map = inlinedOxsts.variables.associateBy {
+ it.name
+ }
+
+ fun transform(xstsAssumptionWitnessState: XstsWitnessState) = mappings.getOrPut(xstsAssumptionWitnessState) {
+ val stateVariableValues = xstsAssumptionWitnessState.variableValues
+
+ WitnessState(
+ transformStateValues(stateVariableValues),
+ )
+ }
+
+ private fun transformStateValues(stateVariableValues: List): List {
+ return stateVariableValues.map {
+ transform(it)
+ }
+ }
+
+ private fun transform(variableValue: XstsWitnessStateVariableValue): WitnessStateValue {
+ return WitnessStateValue(
+ resolveOxstsVariable(variableValue.variableDeclaration.name),
+ xstsExpressionToOxstsExpressionTransformer.transform(variableValue.value),
+ )
+ }
+
+ private fun resolveOxstsVariable(variableName: String): VariableDeclaration {
+ return variablesByName[variableName]
+ ?: error("Variable with name $variableName not found!")
+ }
+ }
+
+ fun transform(inlinedOxsts: InlinedOxsts, xstsAssumptionWitness: XstsWitness): InlinedWitness {
+ val context = TransformerContext(inlinedOxsts)
+
+ val initialState = context.transform(xstsAssumptionWitness.initialState)
+ val initializedState = if (xstsAssumptionWitness.initializedState != null) {
+ context.transform(xstsAssumptionWitness.initializedState)
+ } else {
+ null
+ }
+ val transitionStates = xstsAssumptionWitness.transitionStates.map {
+ context.transform(it)
+ }
+ val nextStateMap = xstsAssumptionWitness.nextStateMap.map {
+ context.transform(it.key) to it.value.map { context.transform(it) }
+ }.toMap()
+
+ return InlinedWitness(
+ initialState,
+ initializedState,
+ transitionStates,
+ nextStateMap,
+ inlinedOxsts,
+ )
+ }
+}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/oxsts/XstsExpressionToOxstsExpressionTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/XstsExpressionToOxstsExpressionTransformer.kt
similarity index 74%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/oxsts/XstsExpressionToOxstsExpressionTransformer.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/XstsExpressionToOxstsExpressionTransformer.kt
index 0e42ab01..1e2c84c3 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/oxsts/XstsExpressionToOxstsExpressionTransformer.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/backannotation/XstsExpressionToOxstsExpressionTransformer.kt
@@ -1,15 +1,15 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.inlinedoxsts
+package hu.bme.mit.semantifyr.backends.theta.backannotation
import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts.OxstsDomainTransformer
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
-import hu.bme.mit.semantifyr.semantics.utils.OxstsFactory
+import hu.bme.mit.semantifyr.backends.theta.transformation.xsts.ThetaDomainTransformer
+import hu.bme.mit.semantifyr.compiler.pipeline.utils.OxstsFactory
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.Expression
import hu.bme.mit.semantifyr.xsts.lang.utils.XstsExpressionVisitor
import hu.bme.mit.semantifyr.xsts.lang.xsts.ArithmeticBinaryOperator
import hu.bme.mit.semantifyr.xsts.lang.xsts.ArithmeticOp
@@ -22,7 +22,6 @@ import hu.bme.mit.semantifyr.xsts.lang.xsts.ConcreteLiteralArray
import hu.bme.mit.semantifyr.xsts.lang.xsts.DefaultLiteralArray
import hu.bme.mit.semantifyr.xsts.lang.xsts.ElementReferenceExpression
import hu.bme.mit.semantifyr.xsts.lang.xsts.EnumLiteral
-import hu.bme.mit.semantifyr.xsts.lang.xsts.Expression
import hu.bme.mit.semantifyr.xsts.lang.xsts.IfThenElseExpression
import hu.bme.mit.semantifyr.xsts.lang.xsts.IntegerType
import hu.bme.mit.semantifyr.xsts.lang.xsts.LiteralBoolean
@@ -32,13 +31,11 @@ import hu.bme.mit.semantifyr.xsts.lang.xsts.ReadIndexingSuffixExpression
import hu.bme.mit.semantifyr.xsts.lang.xsts.UnaryOp
import hu.bme.mit.semantifyr.xsts.lang.xsts.WriteIndexingSuffixExpression
-@CompilationScoped
-class XstsExpressionToOxstsExpressionTransformer : XstsExpressionVisitor() {
+class XstsExpressionToOxstsExpressionTransformer @Inject constructor(
+ private val thetaDomainTransformer: ThetaDomainTransformer,
+) : XstsExpressionVisitor() {
- @Inject
- private lateinit var oxstsExpressionTransformer: OxstsDomainTransformer
-
- fun transform(expression: Expression): hu.bme.mit.semantifyr.oxsts.model.oxsts.Expression {
+ fun transform(expression: hu.bme.mit.semantifyr.xsts.lang.xsts.Expression): Expression {
return visit(expression)
}
@@ -81,7 +78,7 @@ class XstsExpressionToOxstsExpressionTransformer : XstsExpressionVisitor,
+)
+
+class XstsWitness(
+ val initialState: XstsWitnessState,
+ val initializedState: XstsWitnessState?,
+ val transitionStates: List,
+ val nextStateMap: Map>,
+ val xstsModel: XstsModel,
+) {
+ fun getNextStates(state: XstsWitnessState): List {
+ return nextStateMap[state] ?: emptyList()
+ }
+}
+
+class XstsWitnessTransformer {
+
+ private class TransformerContext(val xstsModel: XstsModel) {
+ val cexExpressionToXstsExpressionTransformer = CexExpressionToXstsExpressionTransformer(xstsModel)
+
+ val mappings = mutableMapOf()
+
+ fun transform(cexAssumptionWitnessState: CexWitnessState) = mappings.getOrPut(cexAssumptionWitnessState) {
+ XstsWitnessState(
+ cexAssumptionWitnessState.variableValues.filterNot {
+ LocalVarNames.isLocalVar(it.variableName)
+ }.map {
+ transform(it)
+ },
+ )
+ }
+
+ private fun transform(variableValue: CexWitnessStateVariableValue): XstsWitnessStateVariableValue {
+ val variable = xstsModel.variableDeclarations.firstOrNull {
+ it.name == variableValue.variableName
+ }
+ check(variable != null) {
+ "Variable with name ${variableValue.variableName} not found!"
+ }
+
+ return XstsWitnessStateVariableValue(
+ variable,
+ cexExpressionToXstsExpressionTransformer.transform(variableValue.value),
+ )
+ }
+ }
+
+ fun transform(xstsModel: XstsModel, cexAssumptionWitness: CexWitness): XstsWitness {
+ val context = TransformerContext(xstsModel)
+
+ val initialState = context.transform(cexAssumptionWitness.initialState)
+ val initializedState = if (cexAssumptionWitness.initializedState != null) {
+ context.transform(cexAssumptionWitness.initializedState)
+ } else {
+ null
+ }
+ val transitionStates = cexAssumptionWitness.transitionStates.map {
+ context.transform(it)
+ }
+ val nextStateMap = cexAssumptionWitness.nextStateMap.map {
+ context.transform(it.key) to it.value.map { context.transform(it) }
+ }.toMap()
+
+ return XstsWitness(
+ initialState,
+ initializedState,
+ transitionStates,
+ nextStateMap,
+ xstsModel,
+ )
+ }
+}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsDomainTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaDomainTransformer.kt
similarity index 82%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsDomainTransformer.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaDomainTransformer.kt
index f3da17de..03d47275 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsDomainTransformer.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaDomainTransformer.kt
@@ -1,27 +1,27 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
import com.google.inject.Inject
+import hu.bme.mit.semantifyr.backend.scopes.VerificationScoped
import hu.bme.mit.semantifyr.oxsts.lang.library.builtin.BuiltinSymbolResolver
import hu.bme.mit.semantifyr.oxsts.model.oxsts.DataTypeDeclaration
import hu.bme.mit.semantifyr.oxsts.model.oxsts.EnumDeclaration
import hu.bme.mit.semantifyr.oxsts.model.oxsts.EnumLiteral
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
+import hu.bme.mit.semantifyr.xsts.lang.xsts.Type
-typealias XstsType = hu.bme.mit.semantifyr.xsts.lang.xsts.Type
+typealias XstsType = Type
private typealias XstsEnumDeclaration = hu.bme.mit.semantifyr.xsts.lang.xsts.EnumDeclaration
private typealias XstsEnumLiteral = hu.bme.mit.semantifyr.xsts.lang.xsts.EnumLiteral
-@CompilationScoped
-class OxstsDomainTransformer {
-
- @Inject
- private lateinit var builtinSymbolResolver: BuiltinSymbolResolver
+@VerificationScoped
+class ThetaDomainTransformer @Inject constructor(
+ private val builtinSymbolResolver: BuiltinSymbolResolver,
+) {
private val enumDeclarationMap = mutableMapOf()
private val enumLiteralMap = mutableMapOf()
@@ -59,5 +59,4 @@ class OxstsDomainTransformer {
value == enumLiteral
}?.key ?: error("Corresponding enum literal was not transformed!")
}
-
}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsExpressionTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaExpressionTransformer.kt
similarity index 73%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsExpressionTransformer.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaExpressionTransformer.kt
index 6ff04adb..b18772bf 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsExpressionTransformer.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaExpressionTransformer.kt
@@ -1,21 +1,20 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
import com.google.inject.Inject
-import hu.bme.mit.semantifyr.oxsts.lang.utils.ExpressionVisitor
+import hu.bme.mit.semantifyr.backend.BackendUnsupportedException
+import hu.bme.mit.semantifyr.backend.transformation.BackendExpressionVisitor
import hu.bme.mit.semantifyr.oxsts.model.oxsts.AG
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ArithmeticBinaryOperator
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ArithmeticOp
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ArithmeticUnaryOperator
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.ArrayLiteral
import hu.bme.mit.semantifyr.oxsts.model.oxsts.BooleanOp
import hu.bme.mit.semantifyr.oxsts.model.oxsts.BooleanOperator
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.CallSuffixExpression
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ComparisonOp
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ComparisonOperator
import hu.bme.mit.semantifyr.oxsts.model.oxsts.EF
@@ -23,35 +22,29 @@ import hu.bme.mit.semantifyr.oxsts.model.oxsts.Element
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ElementReference
import hu.bme.mit.semantifyr.oxsts.model.oxsts.EnumLiteral
import hu.bme.mit.semantifyr.oxsts.model.oxsts.Expression
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.IfThenElse
import hu.bme.mit.semantifyr.oxsts.model.oxsts.IndexingSuffixExpression
import hu.bme.mit.semantifyr.oxsts.model.oxsts.LiteralBoolean
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.LiteralInfinity
import hu.bme.mit.semantifyr.oxsts.model.oxsts.LiteralInteger
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.LiteralNothing
import hu.bme.mit.semantifyr.oxsts.model.oxsts.LiteralReal
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.LiteralString
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.NavigationSuffixExpression
import hu.bme.mit.semantifyr.oxsts.model.oxsts.NegationOperator
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.RangeExpression
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.SelfReference
import hu.bme.mit.semantifyr.oxsts.model.oxsts.UnaryOp
import hu.bme.mit.semantifyr.oxsts.model.oxsts.VariableDeclaration
+import hu.bme.mit.semantifyr.xsts.lang.xsts.ElementReferenceExpression
+import org.eclipse.emf.ecore.EObject
-private typealias XstsElement = org.eclipse.emf.ecore.EObject
+private typealias XstsElement = EObject
private typealias XstsComparisonOp = hu.bme.mit.semantifyr.xsts.lang.xsts.ComparisonOp
private typealias XstsBooleanOp = hu.bme.mit.semantifyr.xsts.lang.xsts.BooleanOp
private typealias XstsUnaryOp = hu.bme.mit.semantifyr.xsts.lang.xsts.UnaryOp
private typealias XstsArithmeticOp = hu.bme.mit.semantifyr.xsts.lang.xsts.ArithmeticOp
private typealias XstsExpression = hu.bme.mit.semantifyr.xsts.lang.xsts.Expression
-private typealias XstsElementReferenceExpression = hu.bme.mit.semantifyr.xsts.lang.xsts.ElementReferenceExpression
+private typealias XstsElementReferenceExpression = ElementReferenceExpression
-class OxstsExpressionTransformer : ExpressionVisitor() {
-
- @Inject
- private lateinit var oxstsVariableTransformer: OxstsVariableTransformer
-
- @Inject
- private lateinit var oxstsDomainTransformer: OxstsDomainTransformer
+class ThetaExpressionTransformer @Inject constructor(
+ private val thetaVariableTransformer: ThetaVariableTransformer,
+ private val thetaDomainTransformer: ThetaDomainTransformer,
+) : BackendExpressionVisitor() {
fun transform(expression: Expression): XstsExpression {
return visit(expression)
@@ -102,10 +95,6 @@ class OxstsExpressionTransformer : ExpressionVisitor() {
}
}
- override fun visit(expression: RangeExpression): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
override fun visit(expression: ComparisonOperator): XstsExpression {
return XstsFactory.createComparisonOperator().also {
it.left = transform(expression.left)
@@ -157,16 +146,8 @@ class OxstsExpressionTransformer : ExpressionVisitor() {
}
}
- override fun visit(expression: ArrayLiteral): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
- override fun visit(expression: LiteralInfinity): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
override fun visit(expression: LiteralReal): XstsExpression {
- error("No equivalent in XSTS!")
+ throw BackendUnsupportedException("Theta does not support real literals")
}
override fun visit(expression: LiteralInteger): XstsExpression {
@@ -175,20 +156,12 @@ class OxstsExpressionTransformer : ExpressionVisitor() {
}
}
- override fun visit(expression: LiteralString): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
override fun visit(expression: LiteralBoolean): XstsExpression {
return XstsFactory.createLiteralBoolean().also {
it.isValue = expression.isValue
}
}
- override fun visit(expression: LiteralNothing): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
override fun visit(expression: ElementReference): XstsExpression {
return XstsFactory.createElementReferenceExpression().also {
it.element = demandTransformElement(expression.element)
@@ -197,24 +170,12 @@ class OxstsExpressionTransformer : ExpressionVisitor() {
private fun demandTransformElement(element: Element): XstsElement {
return when (element) {
- is VariableDeclaration -> oxstsVariableTransformer.transform(element)
- is EnumLiteral -> oxstsDomainTransformer.transform(element)
+ is VariableDeclaration -> thetaVariableTransformer.transform(element)
+ is EnumLiteral -> thetaDomainTransformer.transform(element)
else -> error("Unexpected kind of element: $element")
}
}
- override fun visit(expression: SelfReference): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
- override fun visit(expression: NavigationSuffixExpression): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
- override fun visit(expression: CallSuffixExpression): XstsExpression {
- error("No equivalent in XSTS!")
- }
-
override fun visit(expression: IndexingSuffixExpression): XstsExpression {
return XstsFactory.createReadIndexingSuffixExpression().also {
it.primary = transformReference(expression.primary)
@@ -222,4 +183,11 @@ class OxstsExpressionTransformer : ExpressionVisitor() {
}
}
+ override fun visit(expression: IfThenElse): XstsExpression {
+ return XstsFactory.createIfThenElseExpression().also {
+ it.guard = transform(expression.guard)
+ it.then = transform(expression.then)
+ it.`else` = transform(expression.`else`)
+ }
+ }
}
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaModelTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaModelTransformer.kt
new file mode 100644
index 00000000..99497d24
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaModelTransformer.kt
@@ -0,0 +1,59 @@
+/*
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
+
+import com.google.inject.Inject
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.EnumDeclaration
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlinedOxsts
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.TransitionDeclaration
+import hu.bme.mit.semantifyr.xsts.lang.xsts.SequenceOperation
+import hu.bme.mit.semantifyr.xsts.lang.xsts.Transition
+import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
+import org.eclipse.emf.common.util.URI
+
+private typealias XstsTransition = Transition
+private typealias XstsSequenceOperation = SequenceOperation
+
+class ThetaModelTransformer @Inject constructor(
+ private val thetaOperationTransformer: ThetaOperationTransformer,
+ private val thetaPropertyTransformer: ThetaPropertyTransformer,
+ private val thetaDomainTransformer: ThetaDomainTransformer,
+ private val thetaVariableTransformer: ThetaVariableTransformer,
+ private val xstsModelCreator: XstsModelCreator,
+) {
+
+ fun transform(inlinedOxsts: InlinedOxsts, xstsUri: URI): XstsModel {
+ val xsts = xstsModelCreator.createEmptyXsts(xstsUri)
+
+ for (variableDeclaration in inlinedOxsts.variables) {
+ xsts.variableDeclarations += thetaVariableTransformer.transformTopLevel(variableDeclaration)
+ }
+
+ xsts.env = XstsFactory.createTransition().also {
+ it.branches += XstsFactory.createSequenceOperation()
+ }
+ xsts.tran = transform(inlinedOxsts.mainTransition)
+ xsts.init = transform(inlinedOxsts.initTransition)
+ xsts.property = thetaPropertyTransformer.transform(inlinedOxsts.property)
+
+ xsts.enumDeclarations += inlinedOxsts.variables.asSequence().map {
+ it.typeSpecification.domain
+ }.filterIsInstance().map {
+ thetaDomainTransformer.transform(it)
+ }.distinct()
+
+ return xsts
+ }
+
+ private fun transform(transitionDeclaration: TransitionDeclaration): XstsTransition {
+ return XstsFactory.createTransition().also {
+ for (branch in transitionDeclaration.branches) {
+ it.branches += thetaOperationTransformer.transform(branch) as XstsSequenceOperation
+ }
+ }
+ }
+}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsOperationTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaOperationTransformer.kt
similarity index 57%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsOperationTransformer.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaOperationTransformer.kt
index e5ab534c..c45c3cf1 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsOperationTransformer.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaOperationTransformer.kt
@@ -1,41 +1,30 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
import com.google.inject.Inject
-import hu.bme.mit.semantifyr.oxsts.lang.utils.OperationVisitor
+import hu.bme.mit.semantifyr.backend.transformation.BackendOperationVisitor
import hu.bme.mit.semantifyr.oxsts.model.oxsts.AssignmentOperation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.AssumptionOperation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ChoiceOperation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.ForOperation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.HavocOperation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.IfOperation
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlineCall
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlineChoiceFor
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlineIfOperation
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlineSeqFor
import hu.bme.mit.semantifyr.oxsts.model.oxsts.LocalVarDeclarationOperation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.Operation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.RangeExpression
import hu.bme.mit.semantifyr.oxsts.model.oxsts.SequenceOperation
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.TraceOperation
typealias XstsOperation = hu.bme.mit.semantifyr.xsts.lang.xsts.Operation
-class OxstsOperationTransformer : OperationVisitor() {
-
- @Inject
- private lateinit var oxstsExpressionTransformer: OxstsExpressionTransformer
-
- @Inject
- private lateinit var oxstsVariableTransformer: OxstsVariableTransformer
-
- @Inject
- private lateinit var traceOperationTransformer: TraceOperationTransformer
+class ThetaOperationTransformer @Inject constructor(
+ private val thetaExpressionTransformer: ThetaExpressionTransformer,
+ private val thetaVariableTransformer: ThetaVariableTransformer,
+) : BackendOperationVisitor() {
fun transform(operation: Operation): XstsOperation {
return visit(operation)
@@ -58,17 +47,17 @@ class OxstsOperationTransformer : OperationVisitor() {
}
override fun visit(operation: LocalVarDeclarationOperation): XstsOperation {
- return oxstsVariableTransformer.transformLocalVar(operation)
+ return thetaVariableTransformer.transformLocalVar(operation)
}
override fun visit(operation: ForOperation): XstsOperation {
return XstsFactory.createForOperation().also {
- it.loopVar = oxstsVariableTransformer.transform(operation.loopVariable)
+ it.loopVar = thetaVariableTransformer.transform(operation.loopVariable)
val range = operation.rangeExpression
if (range is RangeExpression) {
// TODO: handle inclusive-exclusive!
- it.from = oxstsExpressionTransformer.transform(range.left)
- it.to = oxstsExpressionTransformer.transform(range.right)
+ it.from = thetaExpressionTransformer.transform(range.left)
+ it.to = thetaExpressionTransformer.transform(range.right)
}
it.body = transform(operation.body)
}
@@ -76,9 +65,8 @@ class OxstsOperationTransformer : OperationVisitor() {
override fun visit(operation: IfOperation): XstsOperation {
return XstsFactory.createIfOperation().also {
- it.guard = oxstsExpressionTransformer.transform(operation.guard)
+ it.guard = thetaExpressionTransformer.transform(operation.guard)
it.body = transform(operation.body)
-
if (operation.`else` != null) {
it.`else` = transform(operation.`else`)
}
@@ -87,41 +75,20 @@ class OxstsOperationTransformer : OperationVisitor() {
override fun visit(operation: HavocOperation): XstsOperation {
return XstsFactory.createHavocOperation().also {
- it.reference = oxstsExpressionTransformer.transformReference(operation.reference)
+ it.reference = thetaExpressionTransformer.transformReference(operation.reference)
}
}
override fun visit(operation: AssumptionOperation): XstsOperation {
return XstsFactory.createAssumptionOperation().also {
- it.expression = oxstsExpressionTransformer.transform(operation.expression)
+ it.expression = thetaExpressionTransformer.transform(operation.expression)
}
}
override fun visit(operation: AssignmentOperation): XstsOperation {
return XstsFactory.createAssignmentOperation().also {
- it.reference = oxstsExpressionTransformer.transformReference(operation.reference)
- it.expression = oxstsExpressionTransformer.transform(operation.expression)
+ it.reference = thetaExpressionTransformer.transformReference(operation.reference)
+ it.expression = thetaExpressionTransformer.transform(operation.expression)
}
}
-
- override fun visit(operation: TraceOperation): XstsOperation {
- return traceOperationTransformer.transformTraceOperation(operation)
- }
-
- override fun visit(operation: InlineCall): XstsOperation {
- error("No equivalent in XSTS!")
- }
-
- override fun visit(operation: InlineIfOperation): XstsOperation {
- error("No equivalent in XSTS!")
- }
-
- override fun visit(operation: InlineSeqFor): XstsOperation {
- error("No equivalent in XSTS!")
- }
-
- override fun visit(operation: InlineChoiceFor): XstsOperation {
- error("No equivalent in XSTS!")
- }
-
}
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaPropertyTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaPropertyTransformer.kt
new file mode 100644
index 00000000..f8e3598e
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaPropertyTransformer.kt
@@ -0,0 +1,24 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
+
+import com.google.inject.Inject
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.PropertyDeclaration
+import hu.bme.mit.semantifyr.xsts.lang.xsts.Property
+
+private typealias XstsProperty = Property
+
+class ThetaPropertyTransformer @Inject constructor(
+ private val thetaExpressionTransformer: ThetaExpressionTransformer,
+) {
+
+ fun transform(propertyDeclaration: PropertyDeclaration): XstsProperty {
+ return XstsFactory.createProperty().also {
+ it.invariant = thetaExpressionTransformer.transform(propertyDeclaration.expression)
+ }
+ }
+}
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaTypeReferenceTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaTypeReferenceTransformer.kt
new file mode 100644
index 00000000..d83cf1b4
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaTypeReferenceTransformer.kt
@@ -0,0 +1,37 @@
+/*
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
+
+import com.google.inject.Inject
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.DataTypeDeclaration
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.DomainDeclaration
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.EnumDeclaration
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.Multiplicity
+
+class ThetaTypeReferenceTransformer @Inject constructor(
+ private val thetaDomainTransformer: ThetaDomainTransformer,
+) {
+
+ fun transform(domainDeclaration: DomainDeclaration, multiplicity: Multiplicity?): XstsType {
+ val xstsType = when (domainDeclaration) {
+ is EnumDeclaration -> XstsFactory.createEnumType().also {
+ it.enumDeclaration = thetaDomainTransformer.transform(domainDeclaration)
+ }
+ is DataTypeDeclaration -> thetaDomainTransformer.transform(domainDeclaration)
+ else -> error("Unexpected variable type: $domainDeclaration")
+ }
+
+ if (multiplicity == null) {
+ return xstsType
+ }
+
+ return XstsFactory.createArrayType().also {
+ it.indexType = XstsFactory.createIntegerType()
+ it.elementType = xstsType
+ }
+ }
+}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsVariableTransformer.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaVariableTransformer.kt
similarity index 66%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsVariableTransformer.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaVariableTransformer.kt
index 6b22c0a5..5aa8c18b 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsVariableTransformer.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaVariableTransformer.kt
@@ -1,32 +1,35 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
import com.google.inject.Inject
+import com.google.inject.Provider
+import hu.bme.mit.semantifyr.backend.scopes.VerificationScoped
import hu.bme.mit.semantifyr.oxsts.lang.library.builtin.BuiltinAnnotationHandler
import hu.bme.mit.semantifyr.oxsts.model.oxsts.LocalVarDeclarationOperation
import hu.bme.mit.semantifyr.oxsts.model.oxsts.VariableDeclaration
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
+import hu.bme.mit.semantifyr.xsts.lang.xsts.LocalVarDeclOperation
+import hu.bme.mit.semantifyr.xsts.lang.xsts.TopLevelVariableDeclaration
private typealias XstsVariableDeclaration = hu.bme.mit.semantifyr.xsts.lang.xsts.VariableDeclaration
-typealias XstsTopLevelVariableDeclaration = hu.bme.mit.semantifyr.xsts.lang.xsts.TopLevelVariableDeclaration
-private typealias XstsLocalVarDeclarationOperation = hu.bme.mit.semantifyr.xsts.lang.xsts.LocalVarDeclOperation
-
-@CompilationScoped
-class OxstsVariableTransformer {
-
- @Inject
- private lateinit var oxstsExpressionTransformer: OxstsExpressionTransformer
-
- @Inject
- private lateinit var oxstsTypeReferenceTransformer: OxstsTypeReferenceTransformer
-
- @Inject
- private lateinit var builtinAnnotationHandler: BuiltinAnnotationHandler
+typealias XstsTopLevelVariableDeclaration = TopLevelVariableDeclaration
+private typealias XstsLocalVarDeclarationOperation = LocalVarDeclOperation
+
+@VerificationScoped
+class ThetaVariableTransformer @Inject constructor(
+ private val thetaTypeReferenceTransformer: ThetaTypeReferenceTransformer,
+ private val builtinAnnotationHandler: BuiltinAnnotationHandler,
+ private val thetaExpressionTransformerProvider: Provider,
+) {
+
+ // resolve dependency cycle
+ private val thetaExpressionTransformer by lazy {
+ thetaExpressionTransformerProvider.get()
+ }
private val topVariableMap = mutableMapOf()
private val localVariableMap = mutableMapOf()
@@ -66,11 +69,10 @@ class OxstsVariableTransformer {
variable.name = variableDeclaration.name
val type = variableDeclaration.typeSpecification.domain
- variable.type = oxstsTypeReferenceTransformer.transform(type, variableDeclaration.typeSpecification?.multiplicity)
+ variable.type = thetaTypeReferenceTransformer.transform(type, variableDeclaration.typeSpecification?.multiplicity)
if (variableDeclaration.expression != null) {
- variable.expression = oxstsExpressionTransformer.transform(variableDeclaration.expression)
+ variable.expression = thetaExpressionTransformer.transform(variableDeclaration.expression)
}
}
-
}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/XstsFactory.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/XstsFactory.kt
similarity index 53%
rename from subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/XstsFactory.kt
rename to subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/XstsFactory.kt
index 49a5d297..f03d04a8 100644
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/XstsFactory.kt
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/XstsFactory.kt
@@ -1,10 +1,10 @@
/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
*
* SPDX-License-Identifier: EPL-2.0
*/
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
import hu.bme.mit.semantifyr.xsts.lang.xsts.impl.XstsFactoryImpl
diff --git a/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/XstsModelCreator.kt b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/XstsModelCreator.kt
new file mode 100644
index 00000000..01d5294d
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/XstsModelCreator.kt
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
+
+import hu.bme.mit.semantifyr.backend.scopes.VerificationScoped
+import hu.bme.mit.semantifyr.xsts.lang.XstsStandaloneSetup
+import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
+import org.eclipse.emf.common.util.URI
+import org.eclipse.xtext.resource.XtextResourceSet
+
+@VerificationScoped
+class XstsModelCreator {
+
+ private val xstsInjector by lazy {
+ XstsStandaloneSetup().createInjectorAndDoEMFRegistration()
+ }
+
+ private val resourceSetProvider by lazy {
+ xstsInjector.getProvider(XtextResourceSet::class.java)
+ }
+
+ fun createEmptyXsts(xstsUri: URI): XstsModel {
+ val resourceSet = resourceSetProvider.get()
+ val resource = resourceSet.createResource(xstsUri)
+
+ val xstsModel = XstsFactory.createXstsModel()
+ resource.contents += xstsModel
+
+ return xstsModel
+ }
+
+}
diff --git a/subprojects/backends/theta/theta-backend/src/test/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaModelTransformerTest.kt b/subprojects/backends/theta/theta-backend/src/test/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaModelTransformerTest.kt
new file mode 100644
index 00000000..ebdda5dc
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/test/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaModelTransformerTest.kt
@@ -0,0 +1,149 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
+
+import hu.bme.mit.semantifyr.xsts.lang.xsts.AssignmentOperation
+import hu.bme.mit.semantifyr.xsts.lang.xsts.BooleanType
+import hu.bme.mit.semantifyr.xsts.lang.xsts.ChoiceOperation
+import hu.bme.mit.semantifyr.xsts.lang.xsts.IntegerType
+import hu.bme.mit.semantifyr.xsts.lang.xsts.NegationOperator
+import hu.bme.mit.semantifyr.xsts.lang.xsts.SequenceOperation
+import org.assertj.core.api.Assertions.assertThat
+import org.junit.jupiter.api.Test
+
+class ThetaModelTransformerTest : ThetaTransformationTestBase() {
+
+ @Test
+ suspend fun `int variable produces a TopLevelVariableDeclaration with IntegerType`() {
+ withTransformer {
+ val xsts = it.transform(
+ parse(
+ """
+ inlined oxsts of semantifyr::Anything
+ var x : int := 0
+ init { }
+ tran { }
+ prop { AG true }
+ """,
+ ),
+ testXstsUri,
+ )
+
+ assertThat(xsts.variableDeclarations).hasSize(1)
+ val variable = xsts.variableDeclarations.single()
+ assertThat(variable.name).isEqualTo("x")
+ assertThat(variable.type).isInstanceOf(IntegerType::class.java)
+ }
+ }
+
+ @Test
+ suspend fun `boolean variable produces BooleanType`() {
+ withTransformer {
+ val xsts = it.transform(
+ parse(
+ """
+ inlined oxsts of semantifyr::Anything
+ var b : bool := false
+ init { }
+ tran { }
+ prop { AG true }
+ """,
+ ),
+ testXstsUri,
+ )
+
+ assertThat(xsts.variableDeclarations.single().type).isInstanceOf(BooleanType::class.java)
+ }
+ }
+
+ @Test
+ suspend fun `assignment in tran appears as an AssignmentOperation in tran branches`() {
+ withTransformer {
+ val xsts = it.transform(
+ parse(
+ """
+ inlined oxsts of semantifyr::Anything
+ var x : int := 0
+ init { }
+ tran { x := x + 1 }
+ prop { AG true }
+ """,
+ ),
+ testXstsUri,
+ )
+
+ val tranBranches = xsts.tran.branches
+ assertThat(tranBranches).hasSize(1)
+ val branchSteps = (tranBranches.single() as SequenceOperation).steps
+ assertThat(branchSteps).hasSize(1)
+ assertThat(branchSteps.single()).isInstanceOf(AssignmentOperation::class.java)
+ }
+ }
+
+ @Test
+ suspend fun `choice in tran produces a ChoiceOperation with two branches`() {
+ withTransformer {
+ val xsts = it.transform(
+ parse(
+ """
+ inlined oxsts of semantifyr::Anything
+ var x : int := 0
+ init { }
+ tran { choice { x := 1 } or { x := 2 } }
+ prop { AG true }
+ """,
+ ),
+ testXstsUri,
+ )
+
+ val tranBranch = xsts.tran.branches.single() as SequenceOperation
+ val first = tranBranch.steps.single()
+ assertThat(first).isInstanceOf(ChoiceOperation::class.java)
+ assertThat((first as ChoiceOperation).branches).hasSize(2)
+ }
+ }
+
+ @Test
+ suspend fun `AG property maps to an invariant equal to its body (no negation)`() {
+ withTransformer {
+ val xsts = it.transform(
+ parse(
+ """
+ inlined oxsts of semantifyr::Anything
+ var x : int := 0
+ init { }
+ tran { }
+ prop { AG (x == 5) }
+ """,
+ ),
+ testXstsUri,
+ )
+
+ assertThat(xsts.property.invariant).isNotInstanceOf(NegationOperator::class.java)
+ }
+ }
+
+ @Test
+ suspend fun `EF property maps to a NegationOperator over the body`() {
+ withTransformer {
+ val xsts = it.transform(
+ parse(
+ """
+ inlined oxsts of semantifyr::Anything
+ var x : int := 0
+ init { }
+ tran { }
+ prop { EF (x == 5) }
+ """,
+ ),
+ testXstsUri,
+ )
+
+ assertThat(xsts.property.invariant).isInstanceOf(NegationOperator::class.java)
+ }
+ }
+}
diff --git a/subprojects/backends/theta/theta-backend/src/test/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaTransformationTestBase.kt b/subprojects/backends/theta/theta-backend/src/test/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaTransformationTestBase.kt
new file mode 100644
index 00000000..ab26411c
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/test/kotlin/hu/bme/mit/semantifyr/backends/theta/transformation/xsts/ThetaTransformationTestBase.kt
@@ -0,0 +1,45 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.transformation.xsts
+
+import com.google.inject.Inject
+import com.google.inject.Injector
+import hu.bme.mit.semantifyr.backend.scopes.withVerificationScope
+import hu.bme.mit.semantifyr.backends.theta.ThetaBackendModule
+import hu.bme.mit.semantifyr.oxsts.lang.tests.InjectWithOxsts
+import hu.bme.mit.semantifyr.oxsts.lang.tests.utils.InlinedOxstsParseHelper
+import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlinedOxsts
+import org.eclipse.emf.common.util.URI
+import java.io.File
+
+@InjectWithOxsts
+abstract class ThetaTransformationTestBase {
+
+ @Inject
+ protected lateinit var inlinedOxstsParseHelper: InlinedOxstsParseHelper
+
+ @Inject
+ protected lateinit var oxstsInjector: Injector
+
+ private val childInjector by lazy {
+ oxstsInjector.createChildInjector(ThetaBackendModule())
+ }
+
+ protected val testXstsUri: URI by lazy {
+ URI.createFileURI(File("build/test-tmp/model.xsts").absolutePath)
+ }
+
+ protected fun parse(source: String): InlinedOxsts {
+ return inlinedOxstsParseHelper.parse(source.trimIndent())
+ }
+
+ protected suspend fun withTransformer(block: suspend (ThetaModelTransformer) -> T): T {
+ return withVerificationScope {
+ block(childInjector.getInstance(ThetaModelTransformer::class.java))
+ }
+ }
+}
diff --git a/subprojects/backends/theta/theta-backend/src/verificationTest/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaVerificationTests.kt b/subprojects/backends/theta/theta-backend/src/verificationTest/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaVerificationTests.kt
new file mode 100644
index 00000000..f8ea9f6d
--- /dev/null
+++ b/subprojects/backends/theta/theta-backend/src/verificationTest/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaVerificationTests.kt
@@ -0,0 +1,62 @@
+/*
+ * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta
+
+import hu.bme.mit.semantifyr.backends.theta.execution.ShellBasedThetaXstsExecutor
+import hu.bme.mit.semantifyr.oxsts.lang.OxstsStandaloneSetup
+import hu.bme.mit.semantifyr.oxsts.lang.tests.InjectWithOxsts
+import hu.bme.mit.semantifyr.verifier.SemantifyrVerifierTestHelper
+import hu.bme.mit.semantifyr.verifier.VerificationCase
+import hu.bme.mit.semantifyr.verifier.portfolio.SingleBackendPortfolio
+import org.junit.jupiter.api.Assumptions
+import org.junit.jupiter.api.BeforeAll
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.Arguments
+import org.junit.jupiter.params.provider.MethodSource
+import kotlin.io.path.Path
+
+@InjectWithOxsts
+class ThetaVerificationTests {
+
+ companion object {
+
+ private val injector = OxstsStandaloneSetup().createInjectorAndDoEMFRegistration()
+ private val helper = injector.getInstance(SemantifyrVerifierTestHelper::class.java)
+
+ private val context by lazy {
+ helper.semantifyrLoader
+ .startContext()
+ .loadModels(Path("build/test-models/simple"))
+ .buildAndResolve()
+ }
+
+ @JvmStatic
+ @BeforeAll
+ fun assumeThetaAvailable() {
+ Assumptions.assumeTrue(
+ ShellBasedThetaXstsExecutor().isAvailable(),
+ "theta-xsts-cli not on PATH - skipping Theta backend tests",
+ )
+ }
+
+ @JvmStatic
+ fun `OXSTS Simple Test Suite Passes`(): List {
+ return helper.collectVerificationCasesAsArguments(context)
+ }
+ }
+
+ @ParameterizedTest
+ @MethodSource
+ suspend fun `OXSTS Simple Test Suite Passes`(verificationCase: VerificationCase) {
+ helper.checkTestModel(
+ context,
+ verificationCase,
+ verificationPortfolio = SingleBackendPortfolio(ThetaBackend(), ThetaConfig.CegarExplPredCombined),
+ outputDirectory = SemantifyrVerifierTestHelper.testArtifactRoot(ThetaVerificationTests::class.java),
+ )
+ }
+}
diff --git a/subprojects/backends/theta/theta-wrapper/build.gradle.kts b/subprojects/backends/theta/theta-executor/build.gradle.kts
similarity index 95%
rename from subprojects/backends/theta/theta-wrapper/build.gradle.kts
rename to subprojects/backends/theta/theta-executor/build.gradle.kts
index d6e6d6df..c8ca040a 100644
--- a/subprojects/backends/theta/theta-wrapper/build.gradle.kts
+++ b/subprojects/backends/theta/theta-executor/build.gradle.kts
@@ -27,7 +27,6 @@ val nativeExt = when (currentOs) {
}
repositories {
- mavenCentral()
exclusiveContent {
forRepository {
ivy {
@@ -81,13 +80,15 @@ val thetaOutput by configurations.creating {
dependencies {
api(project(":cex.lang"))
+ api(project(":backend"))
api(libs.guice)
+ implementation(project(":logging"))
implementation(libs.kotlinx.coroutines.core)
implementation(libs.docker.java.core)
implementation(libs.docker.java.transport)
- thetaCliJarClasspath("hu.bme.mit.ftsrg.theta:theta-xsts-cli:${thetaXstsCliVersion}@jar")
+ thetaCliJarClasspath("hu.bme.mit.ftsrg.theta:theta-xsts-cli:$thetaXstsCliVersion@jar")
// Z3 — available on all platforms and architectures
thetaNativeLibs("org.sosy-lab:javasmt-solver-z3:4.14.0:libz3-$currentArch@$nativeExt")
@@ -100,6 +101,7 @@ dependencies {
thetaNativeLibs("org.sosy-lab:javasmt-solver-bitwuzla:0.7.0-13.1-g595512ae:libbitwuzlaj-x64@so")
thetaNativeLibs("org.sosy-lab:javasmt-solver-opensmt:2.9.0-gef441e1c:libopensmtj-x64@so")
}
+
"windows" if currentArch == "x64" -> {
thetaNativeLibs("org.sosy-lab:javasmt-solver-mathsat5:5.6.11-sosy1:mathsat5j-x64@dll")
thetaNativeLibs("org.sosy-lab:javasmt-solver-mathsat5:5.6.11-sosy1:mathsat-x64@dll")
@@ -110,8 +112,8 @@ dependencies {
}
// Z3 legacy — a custom Z3 4.5.0 fork with renamed library symbols, committed to the theta repo
- thetaZ3LegacyLibs("hu.bme.mit.ftsrg.theta.lib:libz3legacy:${thetaXstsCliVersion}@$nativeExt")
- thetaZ3LegacyLibs("hu.bme.mit.ftsrg.theta.lib:libz3javalegacy:${thetaXstsCliVersion}@$nativeExt")
+ thetaZ3LegacyLibs("hu.bme.mit.ftsrg.theta.lib:libz3legacy:$thetaXstsCliVersion@$nativeExt")
+ thetaZ3LegacyLibs("hu.bme.mit.ftsrg.theta.lib:libz3javalegacy:$thetaXstsCliVersion@$nativeExt")
}
val prepareThetaXstsCli by tasks.registering(Sync::class) {
diff --git a/subprojects/backends/theta/theta-wrapper/scripts/theta-xsts-cli b/subprojects/backends/theta/theta-executor/scripts/theta-xsts-cli
similarity index 100%
rename from subprojects/backends/theta/theta-wrapper/scripts/theta-xsts-cli
rename to subprojects/backends/theta/theta-executor/scripts/theta-xsts-cli
diff --git a/subprojects/backends/theta/theta-wrapper/scripts/theta-xsts-cli.cmd b/subprojects/backends/theta/theta-executor/scripts/theta-xsts-cli.cmd
similarity index 100%
rename from subprojects/backends/theta/theta-wrapper/scripts/theta-xsts-cli.cmd
rename to subprojects/backends/theta/theta-executor/scripts/theta-xsts-cli.cmd
diff --git a/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaXstsExecutor.kt b/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaXstsExecutor.kt
new file mode 100644
index 00000000..c6e0fe09
--- /dev/null
+++ b/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/ThetaXstsExecutor.kt
@@ -0,0 +1,70 @@
+/*
+ * SPDX-FileCopyrightText: 2023-2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta
+
+import hu.bme.mit.semantifyr.backend.execution.BackendExecutor
+import hu.bme.mit.semantifyr.backend.execution.ExecutorKey
+import hu.bme.mit.semantifyr.backends.theta.execution.DockerBasedThetaXstsExecutor
+import hu.bme.mit.semantifyr.backends.theta.execution.ShellBasedThetaXstsExecutor
+import hu.bme.mit.semantifyr.logging.debug
+import hu.bme.mit.semantifyr.logging.loggerFactory
+import java.io.File
+
+const val THETA_DEFAULT_IMAGE = "ftsrg/theta-xsts-cli:6.28.1"
+
+@JvmField
+val ThetaExecutorKey = ExecutorKey(
+ name = "theta",
+ unavailableHints = listOf(
+ "Install theta-xsts-cli and ensure it is on PATH (preferred).",
+ "Alternatively, install Docker so the bundled image $THETA_DEFAULT_IMAGE can be pulled.",
+ ),
+) {
+ ThetaXstsExecutor.autoDetect()
+}
+
+class ThetaExecutionResult(
+ val exitCode: Int,
+)
+
+class ThetaExecutionSpecification(
+ val workingDirectory: File,
+ val command: List,
+ val logFile: File? = null,
+ val errorFile: File? = null,
+)
+
+interface ThetaXstsExecutor : BackendExecutor {
+ suspend fun execute(thetaExecutionSpecification: ThetaExecutionSpecification): ThetaExecutionResult
+
+ companion object {
+ private val logger by loggerFactory()
+
+ fun shell(): ThetaXstsExecutor {
+ return ShellBasedThetaXstsExecutor()
+ }
+
+ fun docker(image: String = THETA_DEFAULT_IMAGE): ThetaXstsExecutor {
+ return DockerBasedThetaXstsExecutor(image)
+ }
+
+ fun autoDetect(image: String = THETA_DEFAULT_IMAGE): ThetaXstsExecutor {
+ logger.debug { "Auto-detecting Theta executor" }
+ val shell = shell()
+ if (shell.isAvailable()) {
+ logger.debug { "Theta auto-detect: shell available" }
+ return shell
+ }
+ logger.debug { "Theta auto-detect: shell unavailable, falling back to Docker image $image" }
+ val docker = docker(image)
+ check(docker.isAvailable()) {
+ "Could not find any working Theta XSTS executor (tried shell and docker $image)."
+ }
+ return docker
+ }
+ }
+}
diff --git a/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/execution/DockerBasedThetaXstsExecutor.kt b/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/execution/DockerBasedThetaXstsExecutor.kt
new file mode 100644
index 00000000..523c6dea
--- /dev/null
+++ b/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/execution/DockerBasedThetaXstsExecutor.kt
@@ -0,0 +1,50 @@
+/*
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.execution
+
+import com.github.dockerjava.api.command.CreateContainerResponse
+import com.github.dockerjava.api.model.Bind
+import com.github.dockerjava.api.model.HostConfig
+import com.github.dockerjava.api.model.Volume
+import hu.bme.mit.semantifyr.backend.execution.DockerBasedBackendExecutor
+import hu.bme.mit.semantifyr.backends.theta.THETA_DEFAULT_IMAGE
+import hu.bme.mit.semantifyr.backends.theta.ThetaExecutionResult
+import hu.bme.mit.semantifyr.backends.theta.ThetaExecutionSpecification
+import hu.bme.mit.semantifyr.backends.theta.ThetaXstsExecutor
+import hu.bme.mit.semantifyr.logging.debug
+import hu.bme.mit.semantifyr.logging.info
+
+class DockerBasedThetaXstsExecutor(
+ image: String = THETA_DEFAULT_IMAGE,
+) : DockerBasedBackendExecutor(image),
+ ThetaXstsExecutor {
+
+ override suspend fun execute(thetaExecutionSpecification: ThetaExecutionSpecification): ThetaExecutionResult {
+ val container = createContainer(thetaExecutionSpecification)
+ logger.info { "Starting Docker container for image $image in ${thetaExecutionSpecification.workingDirectory.absolutePath}" }
+ logger.debug { "Docker container id ${container.id}, command: ${thetaExecutionSpecification.command.joinToString(" ")}" }
+
+ val result = runContainer(container, thetaExecutionSpecification.logFile, thetaExecutionSpecification.errorFile)
+
+ logger.info { "Docker container exited with status ${result.statusCode}" }
+ return ThetaExecutionResult(result.statusCode)
+ }
+
+ private fun createContainer(spec: ThetaExecutionSpecification): CreateContainerResponse {
+ val hostConfig = HostConfig
+ .newHostConfig()
+ .withBinds(Bind(spec.workingDirectory.absolutePath, Volume("/host/working_directory")))
+
+ return dockerClient
+ .createContainerCmd(image)
+ .withHostConfig(hostConfig)
+ .withWorkingDir("/host/working_directory")
+ .withCmd(spec.command)
+ .withEntrypoint("java", "-jar", "/theta-xsts-cli.jar")
+ .exec()
+ }
+}
diff --git a/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/execution/ShellBasedThetaXstsExecutor.kt b/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/execution/ShellBasedThetaXstsExecutor.kt
new file mode 100644
index 00000000..71feb4b4
--- /dev/null
+++ b/subprojects/backends/theta/theta-executor/src/main/kotlin/hu/bme/mit/semantifyr/backends/theta/execution/ShellBasedThetaXstsExecutor.kt
@@ -0,0 +1,33 @@
+/*
+ * SPDX-FileCopyrightText: 2025-2026 The Semantifyr Authors
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+package hu.bme.mit.semantifyr.backends.theta.execution
+
+import hu.bme.mit.semantifyr.backend.execution.ShellBasedBackendExecutor
+import hu.bme.mit.semantifyr.backends.theta.ThetaExecutionResult
+import hu.bme.mit.semantifyr.backends.theta.ThetaExecutionSpecification
+import hu.bme.mit.semantifyr.backends.theta.ThetaXstsExecutor
+
+class ShellBasedThetaXstsExecutor :
+ ShellBasedBackendExecutor(),
+ ThetaXstsExecutor {
+
+ override val binaryName: String = "theta-xsts-cli"
+
+ override fun isAvailable(): Boolean {
+ return probeAvailability(probeArgs = listOf("--version"))
+ }
+
+ override suspend fun execute(thetaExecutionSpecification: ThetaExecutionSpecification): ThetaExecutionResult {
+ val exitCode = runProcess(
+ args = thetaExecutionSpecification.command,
+ workingDirectory = thetaExecutionSpecification.workingDirectory,
+ logFile = thetaExecutionSpecification.logFile,
+ errorFile = thetaExecutionSpecification.errorFile,
+ )
+ return ThetaExecutionResult(exitCode)
+ }
+}
diff --git a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/DockerBasedThetaXstsExecutor.kt b/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/DockerBasedThetaXstsExecutor.kt
deleted file mode 100644
index f67aac03..00000000
--- a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/DockerBasedThetaXstsExecutor.kt
+++ /dev/null
@@ -1,129 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.wrapper.execution
-
-import com.github.dockerjava.api.command.CreateContainerResponse
-import com.github.dockerjava.api.exception.NotFoundException
-import com.github.dockerjava.api.model.Bind
-import com.github.dockerjava.api.model.HostConfig
-import com.github.dockerjava.api.model.Volume
-import com.github.dockerjava.api.model.WaitResponse
-import com.github.dockerjava.core.DefaultDockerClientConfig
-import com.github.dockerjava.core.DockerClientImpl
-import com.github.dockerjava.httpclient5.ApacheDockerHttpClient
-import kotlinx.coroutines.Dispatchers
-import kotlinx.coroutines.NonCancellable
-import kotlinx.coroutines.coroutineScope
-import kotlinx.coroutines.withContext
-
-class DockerBasedThetaXstsExecutor : ThetaXstsExecutor() {
-
- private val imageName = "ftsrg/theta-xsts-cli"
- private val version = "6.27.17"
- private val dockerClient by lazy {
- try {
- val config = DefaultDockerClientConfig.createDefaultConfigBuilder().build()
- val httpClient = ApacheDockerHttpClient.Builder()
- .dockerHost(config.dockerHost)
- .sslConfig(config.sslConfig).build()
- DockerClientImpl.getInstance(config, httpClient)
- } catch (_: Exception) {
- null
- }
- }
-
- override fun initialize() {
- val imageId = "$imageName:$version"
- try {
- dockerClient!!.inspectImageCmd(imageId).exec()
- } catch (e: NotFoundException) {
- dockerClient!!.pullImageCmd(imageName).withTag(version).start().awaitCompletion()
- }
- }
-
- override fun check(): Boolean {
- return try {
- // try to initialize, if success we have docker :)
- initialize()
- true
- } catch (_: Exception) {
- false
- }
- }
-
- override suspend fun execute(thetaExecutionSpecification: ThetaExecutionSpecification) = coroutineScope {
- val container = createContainer(thetaExecutionSpecification)
-
- val result = try {
- runContainer(thetaExecutionSpecification, container)
- } finally {
- withContext(NonCancellable) {
- stopContainer(container)
- saveContainerLogs(thetaExecutionSpecification, container)
- destroyContainer(container)
- }
- }
-
- // TODO: handle theta errors if any
-
- ThetaExecutionResult(result.statusCode)
- }
-
- private fun createContainer(thetaExecutionSpecification: ThetaExecutionSpecification): CreateContainerResponse {
- val hostConfig = HostConfig.newHostConfig()
- .withBinds(Bind(thetaExecutionSpecification.workingDirectory.absolutePath, Volume("/host/working_directory")))
-
- val container = dockerClient!!.createContainerCmd("$imageName:$version")
- .withHostConfig(hostConfig)
- .withWorkingDir("/host/working_directory")
- .withCmd(thetaExecutionSpecification.command)
- .withEntrypoint("java", "-jar", "/theta-xsts-cli.jar")
- .exec()
-
- return container
- }
-
- private suspend fun runContainer(thetaExecutionSpecification: ThetaExecutionSpecification, container: CreateContainerResponse): WaitResponse {
- dockerClient!!.startContainerCmd(container.id).exec()
-
- return withTimeout(thetaExecutionSpecification) {
- runAsync(Dispatchers.IO) {
- dockerClient!!.waitContainerCmd(container.id).exec(it)
- }
- }
- }
-
- private fun stopContainer(container: CreateContainerResponse) {
- try {
- dockerClient!!.stopContainerCmd(container.id).exec()
- } catch (_: Exception) {
- // swallow exceptions
- }
- }
-
- private suspend fun saveContainerLogs(thetaExecutionSpecification: ThetaExecutionSpecification, container: CreateContainerResponse) = withContext(Dispatchers.IO) {
- try {
- dockerClient!!.logContainerCmd(container.id)
- .withStdOut(true)
- .withStdErr(true)
- .withTailAll()
- .exec(StreamLoggerCallback(thetaExecutionSpecification.logStream, thetaExecutionSpecification.errorStream))
- .await()
- } catch (t: Throwable) {
- // swallow exceptions
- }
- }
-
- private fun destroyContainer(container: CreateContainerResponse) {
- try {
- dockerClient!!.removeContainerCmd(container.id).withForce(true).exec()
- } catch (_: Exception) {
- // swallow exceptions
- }
- }
-
-}
diff --git a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ShellBasedThetaXstsExecutor.kt b/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ShellBasedThetaXstsExecutor.kt
deleted file mode 100644
index 9e6524fe..00000000
--- a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ShellBasedThetaXstsExecutor.kt
+++ /dev/null
@@ -1,103 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.wrapper.execution
-
-import hu.bme.mit.semantifyr.backends.theta.wrapper.utils.destroyTree
-import kotlinx.coroutines.CoroutineScope
-import kotlinx.coroutines.Dispatchers
-import kotlinx.coroutines.NonCancellable
-import kotlinx.coroutines.cancelAndJoin
-import kotlinx.coroutines.coroutineScope
-import kotlinx.coroutines.launch
-import kotlinx.coroutines.runInterruptible
-import kotlinx.coroutines.withContext
-import java.io.InputStream
-import java.io.OutputStream
-
-class ShellBasedThetaXstsExecutor : ThetaXstsExecutor() {
-
- private val isWindows = System.getProperty("os.name").lowercase().contains("windows")
-
- override fun check(): Boolean {
- return try {
- thetaProcessBuilder("--version").start().waitFor() == 0
- } catch (e: Exception) {
- false
- }
- }
-
- fun CoroutineScope.startReaderJob(inputStream: InputStream, outputStream: OutputStream) = launch(Dispatchers.IO) {
- val writer = outputStream.bufferedWriter()
- try {
- runInterruptible {
- inputStream.bufferedReader().lineSequence().forEach {
- writer.appendLine(it)
- }
- }
- } catch (_: Exception) {
- // swallow IO and cancellation exceptions
- } finally {
- writer.flush()
- }
- }
-
- override suspend fun execute(thetaExecutionSpecification: ThetaExecutionSpecification) = coroutineScope {
- val process = createProcessBuilder(thetaExecutionSpecification).start()
-
- val stdoutJob = startReaderJob(process.inputStream, thetaExecutionSpecification.logStream)
- val stderrJob = startReaderJob(process.errorStream, thetaExecutionSpecification.errorStream)
-
- try {
- withTimeout(thetaExecutionSpecification) {
- runInterruptible(Dispatchers.IO) {
- process.waitFor()
- }
- }
- } finally {
- withContext(NonCancellable) {
- process.destroyTree()
- process.waitFor()
- stdoutJob.cancelAndJoin()
- stderrJob.cancelAndJoin()
- }
- }
-
- // TODO: handle theta errors if any
-
- ThetaExecutionResult(process.exitValue())
- }
-
- private fun createProcessBuilder(thetaExecutionSpecification: ThetaExecutionSpecification): ProcessBuilder {
- return thetaProcessBuilder(thetaExecutionSpecification.command)
- .directory(thetaExecutionSpecification.workingDirectory)
- }
-
- private fun thetaProcessBuilder(vararg args: String): ProcessBuilder {
- val args = thetaCmd(args.toList())
-
- return ProcessBuilder(args)
- .redirectOutput(ProcessBuilder.Redirect.PIPE)
- .redirectError(ProcessBuilder.Redirect.PIPE)
- }
-
- private fun thetaProcessBuilder(args: List): ProcessBuilder {
- val args = thetaCmd(args)
-
- return ProcessBuilder(args)
- .redirectOutput(ProcessBuilder.Redirect.PIPE)
- .redirectError(ProcessBuilder.Redirect.PIPE)
- }
-
- private fun thetaCmd(args: List): List {
- return if (isWindows) {
- listOf("cmd", "/c", "theta-xsts-cli") + args
- } else {
- listOf("theta-xsts-cli") + args
- }
- }
-
-}
diff --git a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ThetaXstsExecutor.kt b/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ThetaXstsExecutor.kt
deleted file mode 100644
index 8169c442..00000000
--- a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ThetaXstsExecutor.kt
+++ /dev/null
@@ -1,43 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023-2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.wrapper.execution
-
-import kotlinx.coroutines.withTimeout
-import org.apache.commons.io.output.NullOutputStream
-import java.io.File
-import java.io.OutputStream
-import kotlin.time.Duration
-
-class ThetaExecutionResult(
- val exitCode: Int,
-)
-
-class ThetaExecutionSpecification(
- val workingDirectory: File,
- val command: List,
- val logStream: OutputStream = NullOutputStream.INSTANCE,
- val errorStream: OutputStream = NullOutputStream.INSTANCE,
- val timeout: Duration,
-)
-
-abstract class ThetaXstsExecutor {
-
- abstract fun check(): Boolean
-
- open fun initialize() {
-
- }
-
- abstract suspend fun execute(thetaExecutionSpecification: ThetaExecutionSpecification): ThetaExecutionResult
-
- protected suspend inline fun withTimeout(thetaExecutionSpecification: ThetaExecutionSpecification, crossinline block: suspend () -> T): T {
- return withTimeout(thetaExecutionSpecification.timeout) {
- block()
- }
- }
-
-}
diff --git a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ThetaXstsExecutorProvider.kt b/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ThetaXstsExecutorProvider.kt
deleted file mode 100644
index 0b1a2d1d..00000000
--- a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/execution/ThetaXstsExecutorProvider.kt
+++ /dev/null
@@ -1,44 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.wrapper.execution
-
-import com.google.inject.Inject
-
-class ThetaXstsExecutorProvider {
-
- @Inject
- private lateinit var dockerBasedThetaXstsExecutor: DockerBasedThetaXstsExecutor
-
- @Inject
- private lateinit var shellBasedThetaXstsExecutor: ShellBasedThetaXstsExecutor
-
- private var resolvedExecutor: ThetaXstsExecutor? = null
-
- fun getExecutor(): ThetaXstsExecutor {
- if (resolvedExecutor == null) {
- resolvedExecutor = resolveExecutor()
-
- resolvedExecutor!!.initialize()
- }
-
- return resolvedExecutor!!
- }
-
- private fun resolveExecutor(): ThetaXstsExecutor {
- if (shellBasedThetaXstsExecutor.check()) {
- return shellBasedThetaXstsExecutor
- }
-
- // docker-based executor.check is still unreliable... FIXME
- if (dockerBasedThetaXstsExecutor.check()) {
- return dockerBasedThetaXstsExecutor
- }
-
- throw IllegalStateException("Could not find any working Theta Xsts executor.")
- }
-
-}
diff --git a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/utils/ProcessUtils.kt b/subprojects/backends/theta/theta-wrapper/src/main/kotlin/utils/ProcessUtils.kt
deleted file mode 100644
index 440f293f..00000000
--- a/subprojects/backends/theta/theta-wrapper/src/main/kotlin/utils/ProcessUtils.kt
+++ /dev/null
@@ -1,29 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.wrapper.utils
-
-fun Process.destroyTree() {
- val handle = toHandle()
- val descendants = handle.descendants()
-
- for (descendant in descendants) {
- descendant.destroy()
- }
-
- handle.destroy()
-}
-
-fun Process.destroyTreeForcibly() {
- val handle = toHandle()
- val descendants = handle.descendants()
-
- for (descendant in descendants) {
- descendant.destroyForcibly()
- }
-
- handle.destroyForcibly()
-}
diff --git a/subprojects/backends/theta/xsts-verifier/build.gradle.kts b/subprojects/backends/theta/xsts-verifier/build.gradle.kts
deleted file mode 100644
index 073702d5..00000000
--- a/subprojects/backends/theta/xsts-verifier/build.gradle.kts
+++ /dev/null
@@ -1,29 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-plugins {
- id("hu.bme.mit.semantifyr.gradle.conventions.jvm")
- id("hu.bme.mit.semantifyr.gradle.conventions.theta")
- kotlin("jvm")
- kotlin("plugin.serialization")
-}
-
-repositories {
- mavenCentral()
-}
-
-dependencies {
- api(project(":semantics"))
- api(project(":xsts.lang"))
- api(project(":theta-wrapper"))
-
- implementation(libs.kotlinx.serialization.json)
-
- testRuntimeOnly(libs.slf4j.log4j)
-
- testFixturesApi(project(":semantics"))
- testFixturesApi(testFixtures(project(":semantics")))
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/ThetaArtifactManager.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/ThetaArtifactManager.kt
deleted file mode 100644
index fef6f459..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/ThetaArtifactManager.kt
+++ /dev/null
@@ -1,68 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.execution.ThetaVerificationSpecification
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
-import hu.bme.mit.semantifyr.semantics.transformation.serializer.ArtifactManager
-import hu.bme.mit.semantifyr.semantics.verification.VerificationCaseRunResult
-import hu.bme.mit.semantifyr.semantics.verification.VerificationTimeMetrics
-import kotlinx.serialization.Serializable
-import kotlinx.serialization.json.Json
-import kotlinx.serialization.json.encodeToStream
-import org.eclipse.emf.common.util.URI
-import java.io.File
-
-@Serializable
-data class VerificationPortfolioResult(
- val winningSpecification: ThetaVerificationSpecification,
- val allArguments: List,
-)
-
-@CompilationScoped
-class ThetaArtifactManager {
-
- @Inject
- private lateinit var artifactManager: ArtifactManager
-
- val xstsFile: File
- get() = artifactManager.resolve("inlined.xsts")
-
- val xstsUri: URI
- get() = URI.createFileURI(xstsFile.absolutePath)
-
- fun serialize(result: VerificationCaseRunResult) {
- val file = artifactManager.resolve("report.json")
- file.parentFile.mkdirs()
-
- val json = Json {
- prettyPrint = true
- prettyPrintIndent = " "
- explicitNulls = false
- }
-
- file.outputStream().buffered().use {
- json.encodeToStream(result, it)
- }
- }
-
- fun serialize(data: VerificationPortfolioResult) {
- val file = artifactManager.resolve("portfolio.json")
- file.parentFile.mkdirs()
-
- val json = Json {
- prettyPrint = true
- prettyPrintIndent = " "
- }
-
- file.outputStream().buffered().use {
- json.encodeToStream(data, it)
- }
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/ThetaVerifier.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/ThetaVerifier.kt
deleted file mode 100644
index 06edb3ea..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/ThetaVerifier.kt
+++ /dev/null
@@ -1,198 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.cex.CexAssumptionWitnessTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.oxsts.InlinedOxstsAssumptionWitnessTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.xsts.XstsAssumptionWitnessTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.execution.ThetaPortfolioRunner
-import hu.bme.mit.semantifyr.backends.theta.verification.execution.ThetaSafeVerificationResult
-import hu.bme.mit.semantifyr.backends.theta.verification.execution.ThetaUnsafeVerificationResult
-import hu.bme.mit.semantifyr.backends.theta.verification.execution.ThetaVerificationResult
-import hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts.OxstsTransformer
-import hu.bme.mit.semantifyr.backends.theta.wrapper.utils.CexReader
-import hu.bme.mit.semantifyr.oxsts.lang.naming.OxstsQualifiedNameProvider
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.AG
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.ClassDeclaration
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.EF
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlinedOxsts
-import hu.bme.mit.semantifyr.semantics.transformation.ProgressContext
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
-import hu.bme.mit.semantifyr.semantics.transformation.serializer.ArtifactManager
-import hu.bme.mit.semantifyr.semantics.utils.loggerFactory
-import hu.bme.mit.semantifyr.semantics.verification.AbstractOxstsVerifier
-import hu.bme.mit.semantifyr.semantics.verification.VerificationCaseRunResult
-import hu.bme.mit.semantifyr.semantics.verification.VerificationMetaData
-import hu.bme.mit.semantifyr.semantics.verification.VerificationResult
-import hu.bme.mit.semantifyr.semantics.verification.VerificationTimeMetrics
-import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
-import java.io.File
-import kotlin.io.path.Path
-import kotlin.time.Clock
-import kotlin.time.Duration
-import kotlin.time.TimeSource.Monotonic.markNow
-import kotlin.time.measureTime
-import kotlin.time.measureTimedValue
-
-@CompilationScoped
-open class ThetaVerifier : AbstractOxstsVerifier() {
-
- val logger by loggerFactory()
-
- @Inject
- private lateinit var oxstsTransformer: OxstsTransformer
-
- @Inject
- private lateinit var oxstsQualifiedNameProvider: OxstsQualifiedNameProvider
-
- @Inject
- private lateinit var cexReader: CexReader
-
- @Inject
- private lateinit var cexAssumptionWitnessTransformer: CexAssumptionWitnessTransformer
-
- @Inject
- private lateinit var xstsAssumptionWitnessTransformer: XstsAssumptionWitnessTransformer
-
- @Inject
- private lateinit var inlinedOxstsAssumptionWitnessTransformer: InlinedOxstsAssumptionWitnessTransformer
-
- @Inject
- private lateinit var thetaPortfolioRunner: ThetaPortfolioRunner
-
- @Inject
- private lateinit var artifactManager: ArtifactManager
-
- @Inject
- private lateinit var thetaArtifactManager: ThetaArtifactManager
-
- protected fun transformToXsts(progressContext: ProgressContext, inlinedOxsts: InlinedOxsts): XstsModel {
- return oxstsTransformer.transform(inlinedOxsts, progressContext)
- }
-
- protected fun verifyXsts(
- progressContext: ProgressContext,
- xstsModel: XstsModel,
- timeout: Duration
- ): ThetaVerificationResult {
- xstsModel.eResource().save(emptyMap())
-
- val workingDirectory = thetaArtifactManager.xstsFile.parent
- val name = thetaArtifactManager.xstsFile.nameWithoutExtension
-
- return thetaPortfolioRunner.run(workingDirectory, name, progressContext, timeout)
- }
-
- override fun verify(
- progressContext: ProgressContext,
- classDeclaration: ClassDeclaration,
- timeout: Duration
- ): VerificationCaseRunResult {
- // TODO: the artifact manager should be created with this base path already initialized -> see scope helper
- val filePath = File(classDeclaration.eResource().uri.toFileString())
- val parentPath = filePath.parentFile
- val outPath = parentPath.resolve("out")
- val basePath = outPath.resolve(filePath.nameWithoutExtension + File.separator + classDeclaration.name)
- artifactManager.initialize(basePath)
-
-
- val (result, duration) = measureTimedValue {
- doRunVerification(progressContext, classDeclaration, timeout)
- }
-
- thetaArtifactManager.serialize(result)
-
- return result
- }
-
- private fun doRunVerification(
- progressContext: ProgressContext,
- classDeclaration: ClassDeclaration,
- timeout: Duration
- ): VerificationCaseRunResult {
- val verificationTimeMetrics = VerificationTimeMetrics()
-
- val startedAt = Clock.System.now()
- val mark = markNow()
-
- val verificationMetaData = VerificationMetaData(
- oxstsQualifiedNameProvider.getFullyQualifiedNameString(classDeclaration),
- classDeclaration.eResource().uri.toFileString(),
- startedAt,
- timeout,
- )
-
- logger.info("Inlining class")
- progressContext.reportProgress("Inlining class")
- val (inlinedOxsts, inliningDuration) = measureTimedValue {
- inlineClass(progressContext, classDeclaration)
- }
- verificationTimeMetrics.inliningDuration = inliningDuration
- logger.info("Inlining took: $inliningDuration")
-
- progressContext.checkIsCancelled()
- logger.info("Transforming to Xsts")
- progressContext.reportProgress("Transforming to Xsts")
- val (xstsModel, xstsDuration) = measureTimedValue {
- transformToXsts(progressContext, inlinedOxsts)
- }
- verificationTimeMetrics.xstsTransformationDuration = xstsDuration
- logger.info("Xsts transformation took: $xstsDuration")
-
- val result = try {
- // Because of the Temporal bubbling optimizations these are the only options
- val property = inlinedOxsts.property.expression
-
- progressContext.checkIsCancelled()
- logger.info("Running verification")
- progressContext.reportProgress("Running verification")
- val (result, verifyDuration) = measureTimedValue {
- verifyXsts(progressContext, xstsModel, timeout)
- }
- verificationTimeMetrics.verificationDuration = verifyDuration
- logger.info("Verification took: $verifyDuration")
-
- if (result.hasWitness) {
- logger.info("Creating witness")
- progressContext.reportProgress("Creating witness")
- val backAnnotationDuration = measureTime {
- val cexPath = Path(result.runtimeDetails.workingDirectory, result.runtimeDetails.cexPath)
- val cexModel = cexReader.loadCexModel(cexPath)
- val cexWitness = cexAssumptionWitnessTransformer.transform(cexModel)
- val xstsWitness = xstsAssumptionWitnessTransformer.transform(xstsModel, cexWitness)
- val inlinedOxstsWitness = inlinedOxstsAssumptionWitnessTransformer.transform(inlinedOxsts, xstsWitness)
- backAnnotateWitness(inlinedOxstsWitness)
- }
- verificationTimeMetrics.backAnnotationDuration = backAnnotationDuration
- logger.info("Back annotation took: $backAnnotationDuration")
- }
-
- when (property) {
- is AG if result is ThetaUnsafeVerificationResult -> {
- VerificationCaseRunResult(VerificationResult.Failed, verificationTimeMetrics, verificationMetaData, "Expected Safe result, got Unsafe instead!")
- }
- is EF if result is ThetaSafeVerificationResult -> {
- VerificationCaseRunResult(VerificationResult.Failed, verificationTimeMetrics, verificationMetaData, "Expected Unsafe result, got Safe instead!")
- }
- else -> {
- VerificationCaseRunResult(VerificationResult.Passed, verificationTimeMetrics, verificationMetaData)
- }
- }
- } catch (e: Exception) {
- logger.error("Exception during verification: ", e)
- VerificationCaseRunResult(VerificationResult.Errored, verificationTimeMetrics, verificationMetaData, e.message)
- }
-
- verificationTimeMetrics.totalDuration = mark.elapsedNow()
-
- logger.info("Result is ${result.result} - ${result.message ?: "No message"}")
-
- return result
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/ThetaSummaryGenerator.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/ThetaSummaryGenerator.kt
deleted file mode 100644
index 390a5e9c..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/ThetaSummaryGenerator.kt
+++ /dev/null
@@ -1,149 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.backannotation
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.cex.CexAssumptionWitnessTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.oxsts.InlinedOxstsAssumptionWitnessTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.xsts.XstsAssumptionWitnessTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts.OxstsTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.utils.ensureExistsOutputStream
-import hu.bme.mit.semantifyr.backends.theta.wrapper.execution.ThetaExecutionSpecification
-import hu.bme.mit.semantifyr.backends.theta.wrapper.execution.ThetaXstsExecutorProvider
-import hu.bme.mit.semantifyr.backends.theta.wrapper.utils.CexReader
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.ClassDeclaration
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlinedOxsts
-import hu.bme.mit.semantifyr.semantics.transformation.OxstsClassInliner
-import hu.bme.mit.semantifyr.semantics.transformation.ProgressContext
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.AssumptionWitnessBackAnnotator
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.OxstsClassAssumptionWitnessTransformer
-import hu.bme.mit.semantifyr.semantics.verification.VerificationDispatcher
-import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
-import org.eclipse.emf.common.util.URI
-import java.io.File
-import kotlin.io.path.pathString
-import kotlin.time.DurationUnit
-import kotlin.time.toDuration
-
-class ThetaSummaryGenerator {
-
- @Inject
- private lateinit var oxstsClassInliner: OxstsClassInliner
-
- @Inject
- private lateinit var assumptionWitnessBackAnnotator: AssumptionWitnessBackAnnotator
-
- @Inject
- private lateinit var oxstsClassAssumptionWitnessTransformer: OxstsClassAssumptionWitnessTransformer
-
- @Inject
- private lateinit var oxstsTransformer: OxstsTransformer
-
- @Inject
- private lateinit var thetaXstsExecutorProvider: ThetaXstsExecutorProvider
-
- @Inject
- private lateinit var verificationDispatcher: VerificationDispatcher
-
- @Inject
- private lateinit var cexReader: CexReader
-
- @Inject
- private lateinit var cexAssumptionWitnessTransformer: CexAssumptionWitnessTransformer
-
- @Inject
- private lateinit var xstsAssumptionWitnessTransformer: XstsAssumptionWitnessTransformer
-
- @Inject
- private lateinit var inlinedOxstsAssumptionWitnessTransformer: InlinedOxstsAssumptionWitnessTransformer
-
-
- fun inlineClass(progressContext: ProgressContext, classDeclaration: ClassDeclaration): InlinedOxsts {
- return oxstsClassInliner.inline(progressContext, classDeclaration)
- }
-
- fun transformToXsts(progressContext: ProgressContext, inlinedOxsts: InlinedOxsts): XstsModel {
- return oxstsTransformer.transform(inlinedOxsts, progressContext)
- }
-
- fun runThetaTracegen(progressContext: ProgressContext, inlinedOxsts: InlinedOxsts, xstsModel: XstsModel) {
- xstsModel.property = null
- xstsModel.eResource().save(emptyMap())
-
- val path = xstsModel.eResource().uri.path().removeSuffix(".xsts")
- val workingDirectory = File(path.replaceAfterLast(File.separator, ""))
-
- val thetaExecutor = thetaXstsExecutorProvider.getExecutor()
-
- val command = listOf(
- "TRACEGEN",
- "--model", "inlined.xsts",
- "--flatten-depth", "0",
- "--stacktrace",
- "--trace-dir", "traces",
- )
-
- val logStream = workingDirectory.resolve("tracing/log.out").ensureExistsOutputStream()
- val errorStream = workingDirectory.resolve("tracing/log.err").ensureExistsOutputStream()
-
- val thetaExecutionSpecification = ThetaExecutionSpecification(
- workingDirectory,
- command,
- logStream,
- errorStream,
- 10.toDuration(DurationUnit.MINUTES),
- )
-
- val result = verificationDispatcher.runBlocking {
- thetaExecutor.execute(thetaExecutionSpecification)
- }
-
- if (result.exitCode == 0) {
- progressContext.reportProgress("Creating witnesses")
- workingDirectory.resolve("traces").walkTopDown().filter {
- it.extension == "trace"
- }.forEach {
- backannotateTrace(it, xstsModel, inlinedOxsts)
- }
- }
- }
-
- fun backannotateTrace(file: File, xstsModel: XstsModel, inlinedOxsts: InlinedOxsts) {
- val cexPath = file.toPath()
- val cexModel = cexReader.loadCexModel(cexPath)
- val cexWitness = cexAssumptionWitnessTransformer.transform(cexModel)
- val xstsWitness = xstsAssumptionWitnessTransformer.transform(xstsModel, cexWitness)
- val inlinedOxstsWitness = inlinedOxstsAssumptionWitnessTransformer.transform(inlinedOxsts, xstsWitness)
- val classWitness = oxstsClassAssumptionWitnessTransformer.transform(inlinedOxstsWitness)
- val witnessInlinedOxsts = assumptionWitnessBackAnnotator.createWitnessInlinedOxsts(classWitness)
-
- val resourceSet = inlinedOxsts.eResource().resourceSet
- val path = cexPath.pathString.replace(".trace", ".oxsts")
- val uri = URI.createURI(path)
- resourceSet.getResource(uri, false)?.delete(mutableMapOf())
- val resource = resourceSet.createResource(uri)
- resource.contents += witnessInlinedOxsts
- resource.save(emptyMap())
- }
-
- fun createSummary(progressContext: ProgressContext, classDeclaration: ClassDeclaration) {
- progressContext.reportProgress("Inlining class")
-
- val inlinedOxsts = inlineClass(progressContext, classDeclaration)
-
- progressContext.checkIsCancelled()
- progressContext.reportProgress("Transforming to Xsts")
-
- val xstsModel = transformToXsts(progressContext, inlinedOxsts)
-
- progressContext.checkIsCancelled()
- progressContext.reportProgress("Running Theta Tracegen")
-
- runThetaTracegen(progressContext, inlinedOxsts, xstsModel)
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/oxsts/InlinedOxstsAssumptionWitnessTransformer.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/oxsts/InlinedOxstsAssumptionWitnessTransformer.kt
deleted file mode 100644
index d5497ee9..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/oxsts/InlinedOxstsAssumptionWitnessTransformer.kt
+++ /dev/null
@@ -1,107 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.oxsts
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.inlinedoxsts.XstsExpressionToOxstsExpressionTransformer
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.xsts.XstsAssumptionWitness
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.xsts.XstsAssumptionWitnessState
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.xsts.XstsAssumptionWitnessStateVariableValue
-import hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts.TraceOperationTransformer
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlinedOxsts
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.InlinedOxstsAssumptionActivatedTrace
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.InlinedOxstsAssumptionWitness
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.InlinedOxstsAssumptionWitnessState
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.InlinedOxstsAssumptionWitnessStateValue
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
-import hu.bme.mit.semantifyr.xsts.lang.xsts.LiteralBoolean
-import hu.bme.mit.semantifyr.xsts.lang.xsts.TopLevelVariableDeclaration
-
-@CompilationScoped
-class InlinedOxstsAssumptionWitnessTransformer {
-
- @Inject
- private lateinit var xstsExpressionToOxstsExpressionTransformer: XstsExpressionToOxstsExpressionTransformer
-
- @Inject
- private lateinit var traceOperationTransformer: TraceOperationTransformer
-
- private inner class TransformerContext(val inlinedOxsts: InlinedOxsts) {
- val mappings = mutableMapOf()
-
- fun transform(xstsAssumptionWitnessState: XstsAssumptionWitnessState) = mappings.getOrPut(xstsAssumptionWitnessState) {
- val stateVariableValues = xstsAssumptionWitnessState.variableValues.filter {
- traceOperationTransformer.isTracerVariable(it.variableDeclaration as TopLevelVariableDeclaration) == false
- }
- val traceVariableValues = xstsAssumptionWitnessState.variableValues.filter {
- traceOperationTransformer.isTracerVariable(it.variableDeclaration as TopLevelVariableDeclaration)
- }
-
- InlinedOxstsAssumptionWitnessState(
- transformStateValues(stateVariableValues),
- transformTraceValues(traceVariableValues),
- )
- }
-
- private fun transformStateValues(stateVariableValues: List): List {
- return stateVariableValues.map {
- transform(it)
- }
- }
-
- private fun transformTraceValues(traceVariableValues: List): List {
- return traceVariableValues.filter {
- it.value is LiteralBoolean && it.value.isValue
- }.map {
- InlinedOxstsAssumptionActivatedTrace(
- traceOperationTransformer.getTraceOperation(it.variableDeclaration as TopLevelVariableDeclaration),
- )
- }
- }
-
- private fun transform(variableValue: XstsAssumptionWitnessStateVariableValue): InlinedOxstsAssumptionWitnessStateValue {
- val variable = inlinedOxsts.variables.firstOrNull {
- it.name == variableValue.variableDeclaration.name
- }
- check(variable != null) {
- "Variable with name ${variableValue.variableDeclaration.name} not found!"
- }
-
- return InlinedOxstsAssumptionWitnessStateValue(
- variable,
- xstsExpressionToOxstsExpressionTransformer.transform(variableValue.value),
- )
- }
-
- }
-
- fun transform(inlinedOxsts: InlinedOxsts, xstsAssumptionWitness: XstsAssumptionWitness): InlinedOxstsAssumptionWitness {
- val context = TransformerContext(inlinedOxsts)
-
- val initialState = context.transform(xstsAssumptionWitness.initialState)
- val initializedState = if (xstsAssumptionWitness.initializedState != null) {
- context.transform(xstsAssumptionWitness.initializedState)
- } else {
- null
- }
- val transitionStates = xstsAssumptionWitness.transitionStates.map {
- context.transform(it)
- }
- val nextStateMap = xstsAssumptionWitness.nextStateMap.map {
- context.transform(it.key) to it.value.map { context.transform(it) }
- }.toMap()
-
- return InlinedOxstsAssumptionWitness(
- initialState,
- initializedState,
- transitionStates,
- nextStateMap,
- inlinedOxsts,
- )
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/xsts/XstsAssumptionWitness.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/xsts/XstsAssumptionWitness.kt
deleted file mode 100644
index 023dee3e..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/backannotation/witness/xsts/XstsAssumptionWitness.kt
+++ /dev/null
@@ -1,95 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.xsts
-
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.cex.CexAssumptionWitness
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.cex.CexAssumptionWitnessState
-import hu.bme.mit.semantifyr.backends.theta.verification.backannotation.witness.cex.CexAssumptionWitnessStateVariableValue
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.AssumptionWitness
-import hu.bme.mit.semantifyr.semantics.transformation.backannotation.AssumptionWitnessState
-import hu.bme.mit.semantifyr.semantics.utils.SemantifyrUtils
-import hu.bme.mit.semantifyr.xsts.lang.xsts.Expression
-import hu.bme.mit.semantifyr.xsts.lang.xsts.VariableDeclaration
-import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
-
-class XstsAssumptionWitnessStateVariableValue(
- val variableDeclaration: VariableDeclaration,
- val value: Expression,
-)
-
-class XstsAssumptionWitnessState(
-// id: String,
- val variableValues: List
-) : AssumptionWitnessState()
-
-class XstsAssumptionWitness(
- override val initialState: XstsAssumptionWitnessState,
- override val initializedState: XstsAssumptionWitnessState?,
- override val transitionStates: List,
- override val nextStateMap: Map>,
- val xstsModel: XstsModel
-) : AssumptionWitness()
-
-class XstsAssumptionWitnessTransformer {
-
- private inner class TransformerContext(val xstsModel: XstsModel) {
- val cexExpressionToXstsExpressionTransformer = CexExpressionToXstsExpressionTransformer(xstsModel)
-
- val mappings = mutableMapOf()
-
- fun transform(cexAssumptionWitnessState: CexAssumptionWitnessState) = mappings.getOrPut(cexAssumptionWitnessState) {
- XstsAssumptionWitnessState(
- cexAssumptionWitnessState.variableValues.filterNot {
- SemantifyrUtils.isLocalVar(it.variableName)
- }.map {
- transform(it)
- },
- )
- }
-
- private fun transform(variableValue: CexAssumptionWitnessStateVariableValue): XstsAssumptionWitnessStateVariableValue {
- val variable = xstsModel.variableDeclarations.firstOrNull {
- it.name == variableValue.variableName
- }
- check(variable != null) {
- "Variable with name ${variableValue.variableName} not found!"
- }
-
- return XstsAssumptionWitnessStateVariableValue(
- variable,
- cexExpressionToXstsExpressionTransformer.transform(variableValue.value),
- )
- }
-
- }
-
- fun transform(xstsModel: XstsModel, cexAssumptionWitness: CexAssumptionWitness): XstsAssumptionWitness {
- val context = TransformerContext(xstsModel)
-
- val initialState = context.transform(cexAssumptionWitness.initialState)
- val initializedState = if (cexAssumptionWitness.initializedState != null) {
- context.transform(cexAssumptionWitness.initializedState)
- } else {
- null
- }
- val transitionStates = cexAssumptionWitness.transitionStates.map {
- context.transform(it)
- }
- val nextStateMap = cexAssumptionWitness.nextStateMap.map {
- context.transform(it.key) to it.value.map { context.transform(it) }
- }.toMap()
-
- return XstsAssumptionWitness(
- initialState,
- initializedState,
- transitionStates,
- nextStateMap,
- xstsModel,
- )
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/execution/ThetaPorfolioExecutor.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/execution/ThetaPorfolioExecutor.kt
deleted file mode 100644
index c1cb438d..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/execution/ThetaPorfolioExecutor.kt
+++ /dev/null
@@ -1,165 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.execution
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.ThetaArtifactManager
-import hu.bme.mit.semantifyr.backends.theta.verification.VerificationPortfolioResult
-import hu.bme.mit.semantifyr.backends.theta.verification.utils.awaitFirstSuccess
-import hu.bme.mit.semantifyr.semantics.transformation.ProgressContext
-import kotlinx.coroutines.CoroutineScope
-import kotlinx.coroutines.Deferred
-import kotlinx.coroutines.Dispatchers
-import kotlinx.coroutines.async
-import kotlinx.coroutines.cancel
-import kotlinx.coroutines.delay
-import kotlinx.coroutines.joinAll
-import kotlinx.coroutines.runBlocking
-import kotlinx.coroutines.supervisorScope
-import org.slf4j.LoggerFactory
-import java.nio.file.Path
-import kotlin.coroutines.cancellation.CancellationException
-import kotlin.io.path.absolute
-import kotlin.time.Duration
-
-class ThetaPortfolioRunner {
-
- private val logger = LoggerFactory.getLogger(ThetaPortfolioRunner::class.java)
-
- val parameters = listOf(
- "CEGAR --domain EXPL --flatten-depth 0 --refinement SEQ_ITP --maxenum 250 --initprec CTRL --stacktrace",
- "CEGAR --domain EXPL_PRED_COMBINED --flatten-depth 0 --autoexpl NEWOPERANDS --initprec CTRL --stacktrace",
- "CEGAR --domain PRED_CART --flatten-depth 0 --refinement SEQ_ITP --stacktrace",
- "BOUNDED --flatten-depth 0 --variant KINDUCTION --stacktrace",
- )
- val checkAllResults = false
-
- @Inject
- private lateinit var thetaVerificationExecutor: ThetaVerificationExecutor
-
- @Inject
- private lateinit var thetaArtifactManager: ThetaArtifactManager
-
- private suspend fun runWorkflow(
- workingDirectory: String,
- name: String,
- timeout: Duration
- ) = supervisorScope {
- logger.info("Starting verification portfolio")
-
- val jobs = parameters.indices.map { index ->
- async {
- logger.info("Starting configuration: ($index) ${parameters[index]}")
-
- try {
- val thetaVerificationSpecification = ThetaVerificationSpecification(workingDirectory, name, index, parameters[index], timeout)
- thetaVerificationExecutor.execute(thetaVerificationSpecification)
- } catch (t: CancellationException) {
- // cancellation is not logged
- throw t
- } catch (t: Throwable) {
- logger.error("Configuration failed: ($index)", t)
- throw t
- }
- }
- }
-
- // since verification is expensive, this hook ensures all verifiers are disposed of upon termination.
- // putting it here to prevent forgetting it in the specific verifier executors.
- // executors must only ensure to handle cancellation correctly.
- val shutdownThread = Thread {
- runBlocking {
- cancelAllModelCheckers(jobs)
- }
- }
-
- Runtime.getRuntime().addShutdownHook(shutdownThread)
-
- try {
- jobs.awaitFirstSuccess()
- } finally {
- logger.info("Portfolio finished, cancelling remaining jobs")
-
- if (checkAllResults) {
- checkAllModelCheckerResults(jobs)
- }
-
- cancelAllModelCheckers(jobs)
-
- Runtime.getRuntime().removeShutdownHook(shutdownThread)
- }
- }
-
- private suspend fun checkAllModelCheckerResults(jobs: List>) {
- var safe = false
- var unsafe = false
-
- jobs.forEach {
- val result = it.await()
-
- if (result is ThetaSafeVerificationResult) {
- logger.debug("Safe result for ${result.runtimeDetails.id}")
- safe = true
- } else if (result is ThetaUnsafeVerificationResult) {
- logger.debug("Unsafe result for ${result.runtimeDetails.id}")
- unsafe = true
- }
- }
-
- if (safe && unsafe) {
- logger.error("Conflicting results!")
- }
- }
-
- private suspend fun cancelAllModelCheckers(jobs: List>) {
- jobs.forEach {
- it.cancel()
- }
- jobs.joinAll()
- }
-
- private fun CoroutineScope.startCancellationChecker(progressContext: ProgressContext): Deferred {
- return async(Dispatchers.IO) {
- while (true) {
- try {
- progressContext.checkIsCancelled()
- } catch (c: CancellationException) {
- this@startCancellationChecker.coroutineContext.cancel(c)
- cancel(c)
- }
- delay(100)
- }
- }
- }
-
- fun run(
- workingDirectory: String,
- name: String,
- progressContext: ProgressContext,
- timeout: Duration
- ) = runBlocking {
- val absoluteDirectory = Path.of(workingDirectory).absolute().toString()
-
- val cancellationChecker = startCancellationChecker(progressContext)
-
- val result = runWorkflow(absoluteDirectory, name, timeout)
-
- cancellationChecker.cancel()
-
- logger.info("Winning configuration: (${result.runtimeDetails.id}) ${result.runtimeDetails.parameter}")
-
- thetaArtifactManager.serialize(
- VerificationPortfolioResult(
- result.runtimeDetails,
- parameters,
- ),
- )
-
- result
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/execution/ThetaVerificationExecutor.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/execution/ThetaVerificationExecutor.kt
deleted file mode 100644
index eb1fbd54..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/execution/ThetaVerificationExecutor.kt
+++ /dev/null
@@ -1,116 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.execution
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.utils.ensureExistsOutputStream
-import hu.bme.mit.semantifyr.backends.theta.wrapper.execution.ThetaExecutionResult
-import hu.bme.mit.semantifyr.backends.theta.wrapper.execution.ThetaExecutionSpecification
-import hu.bme.mit.semantifyr.backends.theta.wrapper.execution.ThetaXstsExecutorProvider
-import hu.bme.mit.semantifyr.semantics.verification.VerificationDispatcher
-import kotlinx.serialization.Serializable
-import java.io.File
-import kotlin.time.Duration
-
-@Serializable
-data class ThetaVerificationSpecification(
- val workingDirectory: String,
- val name: String,
- val id: Int,
- val parameter: String,
- val timeout: Duration,
-) {
- val modelFileName = "$name.xsts"
- val cexFileName = "out.cex"
- val logFileName = "theta.out"
- val errFileName = "theta.err"
-
- val modelPath = modelFileName
- val artifactsPath = "verification${File.separator}artifacts$id"
- val cexPath = "$artifactsPath${File.separator}$cexFileName"
- val logPath = "$artifactsPath${File.separator}$logFileName"
- val errPath = "$artifactsPath${File.separator}$errFileName"
-}
-
-sealed class ThetaVerificationResult(
- val runtimeDetails: ThetaVerificationSpecification
-) {
- val hasWitness = File(runtimeDetails.workingDirectory, runtimeDetails.cexPath).exists()
-}
-
-class ThetaUnknownVerificationResult(runtimeDetails: ThetaVerificationSpecification) : ThetaVerificationResult(runtimeDetails)
-class ThetaSafeVerificationResult(runtimeDetails: ThetaVerificationSpecification) : ThetaVerificationResult(runtimeDetails)
-class ThetaUnsafeVerificationResult(runtimeDetails: ThetaVerificationSpecification) : ThetaVerificationResult(runtimeDetails)
-
-fun ThetaVerificationSpecification.toVerificationResult(executionResult: ThetaExecutionResult): ThetaVerificationResult {
- if (executionResult.exitCode != 0) {
- error("Theta execution failed: $this")
- }
-
- val logFile = File(workingDirectory, logPath)
- if (logFile.exists()) {
- logFile.useLines { lines ->
- for (line in lines) {
- if (line.contains("SafetyResult Unsafe")) {
- return ThetaUnsafeVerificationResult(this)
- }
- if (line.contains("SafetyResult Safe")) {
- return ThetaSafeVerificationResult(this)
- }
- }
- }
- }
-
- return ThetaUnknownVerificationResult(this)
-}
-
-class ThetaVerificationExecutor {
-
- @Inject
- private lateinit var thetaXstsExecutorProvider: ThetaXstsExecutorProvider
-
- @Inject
- private lateinit var verificationDispatcher: VerificationDispatcher
-
- private fun ThetaVerificationSpecification.toExecutionSpecification(): ThetaExecutionSpecification {
- val workingDirectory = File(workingDirectory)
- val command = listOf(
- *parameter.split(" ").toTypedArray(),
- "--model", modelPath,
- "--cexfile", cexPath,
- )
-
- val logStream = workingDirectory.resolve(logPath).ensureExistsOutputStream()
- val errorStream = workingDirectory.resolve(errPath).ensureExistsOutputStream()
-
- return ThetaExecutionSpecification(
- workingDirectory,
- command,
- logStream,
- errorStream,
- timeout,
- )
- }
-
- suspend fun execute(thetaVerificationSpecification: ThetaVerificationSpecification): ThetaVerificationResult {
- val thetaExecutor = thetaXstsExecutorProvider.getExecutor()
- val thetaExecutionSpecification = thetaVerificationSpecification.toExecutionSpecification()
-
- val writer = thetaExecutionSpecification.logStream.bufferedWriter()
- writer.appendLine("Executing with commands:")
- writer.appendLine(thetaExecutionSpecification.command.joinToString(" "))
- writer.appendLine()
- writer.flush()
-
- val result = verificationDispatcher.execute {
- thetaExecutor.execute(thetaExecutionSpecification)
- }
-
- return thetaVerificationSpecification.toVerificationResult(result)
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsTransformer.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsTransformer.kt
deleted file mode 100644
index c88b1789..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsTransformer.kt
+++ /dev/null
@@ -1,106 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.backends.theta.verification.ThetaArtifactManager
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.EnumDeclaration
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.InlinedOxsts
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.PropertyDeclaration
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.TransitionDeclaration
-import hu.bme.mit.semantifyr.semantics.transformation.ProgressContext
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
-import hu.bme.mit.semantifyr.xsts.lang.XstsStandaloneSetup
-import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
-
-private typealias XstsTransition = hu.bme.mit.semantifyr.xsts.lang.xsts.Transition
-private typealias XstsProperty = hu.bme.mit.semantifyr.xsts.lang.xsts.Property
-private typealias XstsSequenceOperation = hu.bme.mit.semantifyr.xsts.lang.xsts.SequenceOperation
-
-@CompilationScoped
-class OxstsTransformer {
-
- @Inject
- private lateinit var oxstsOperationTransformer: OxstsOperationTransformer
-
- @Inject
- private lateinit var oxstsExpressionTransformer: OxstsExpressionTransformer
-
- @Inject
- private lateinit var oxstsDomainTransformer: OxstsDomainTransformer
-
- @Inject
- private lateinit var oxstsVariableTransformer: OxstsVariableTransformer
-
- @Inject
- private lateinit var traceOperationTransformer: TraceOperationTransformer
-
- @Inject
- private lateinit var thetaArtifactManager: ThetaArtifactManager
-
- fun transform(inlinedOxsts: InlinedOxsts, progressContext: ProgressContext): XstsModel {
- val xsts = createEmptyXsts(inlinedOxsts)
-
- progressContext.checkIsCancelled()
-
- for (variableDeclaration in inlinedOxsts.variables) {
- xsts.variableDeclarations += oxstsVariableTransformer.transformTopLevel(variableDeclaration)
- }
-
- progressContext.checkIsCancelled()
-
- xsts.env = XstsFactory.createTransition().also {
- it.branches += XstsFactory.createSequenceOperation()
- }
- xsts.tran = transform(inlinedOxsts.mainTransition)
- xsts.init = transform(inlinedOxsts.initTransition)
- xsts.property = transform(inlinedOxsts.property)
-
- progressContext.checkIsCancelled()
-
- xsts.enumDeclarations += inlinedOxsts.variables.asSequence().map {
- it.typeSpecification.domain
- }.filterIsInstance().map {
- oxstsDomainTransformer.transform(it)
- }.distinct()
-
- traceOperationTransformer.finalizeTransformedTraceOperations(xsts)
-
- progressContext.checkIsCancelled()
-
- return xsts
- }
-
- private fun createEmptyXsts(inlinedOxsts: InlinedOxsts): XstsModel {
- XstsStandaloneSetup.doSetup();
-
- val resourceSet = inlinedOxsts.eResource().resourceSet
- val uri = thetaArtifactManager.xstsUri
-
- val xstsModel = XstsFactory.createXstsModel()
-
- resourceSet.getResource(uri, false)?.delete(mutableMapOf())
- resourceSet.createResource(uri).contents += xstsModel
-
- return xstsModel
- }
-
- private fun transform(transitionDeclaration: TransitionDeclaration): XstsTransition {
- return XstsFactory.createTransition().also {
- for (branch in transitionDeclaration.branches) {
- it.branches += oxstsOperationTransformer.transform(branch) as XstsSequenceOperation
- }
- }
- }
-
- private fun transform(propertyDeclaration: PropertyDeclaration): XstsProperty {
- return XstsFactory.createProperty().also {
- it.invariant = oxstsExpressionTransformer.transform(propertyDeclaration.expression)
- }
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsTypeReferenceTransformer.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsTypeReferenceTransformer.kt
deleted file mode 100644
index dad18a34..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/OxstsTypeReferenceTransformer.kt
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
-
-import com.google.inject.Inject
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.DataTypeDeclaration
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.DomainDeclaration
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.EnumDeclaration
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.Multiplicity
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
-
-@CompilationScoped
-class OxstsTypeReferenceTransformer {
-
- @Inject
- private lateinit var oxstsDomainTransformer: OxstsDomainTransformer
-
- fun transform(domainDeclaration: DomainDeclaration): XstsType {
- return transform(domainDeclaration, null)
- }
-
- fun transform(domainDeclaration: DomainDeclaration, multplicity: Multiplicity?): XstsType {
- val xstsType = when (domainDeclaration) {
- is EnumDeclaration -> {
- XstsFactory.createEnumType().also {
- it.enumDeclaration = oxstsDomainTransformer.transform(domainDeclaration)
- }
- }
- is DataTypeDeclaration -> oxstsDomainTransformer.transform(domainDeclaration)
- else -> error("Unexpected variable type: $this")
- }
-
- if (multplicity == null) {
- return xstsType
- }
-
- return XstsFactory.createArrayType().also {
- it.indexType = XstsFactory.createIntegerType()
- it.elementType = xstsType
- }
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/TraceOperationTransformer.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/TraceOperationTransformer.kt
deleted file mode 100644
index 639e4b37..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/transformation/xsts/TraceOperationTransformer.kt
+++ /dev/null
@@ -1,73 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.transformation.xsts
-
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.TraceOperation
-import hu.bme.mit.semantifyr.semantics.transformation.injection.scope.CompilationScoped
-import hu.bme.mit.semantifyr.semantics.utils.copy
-import hu.bme.mit.semantifyr.xsts.lang.xsts.XstsModel
-
-@CompilationScoped
-class TraceOperationTransformer {
-
- private val traceOperationMap = mutableMapOf()
-
- private val tracerVariables = mutableListOf()
-
- private fun createTracerVariable(traceOperation: TraceOperation): XstsTopLevelVariableDeclaration {
- val tracerVariable = XstsFactory.createTopLevelVariableDeclaration().also {
- it.isControl = true
- it.name = traceOperation.name
- it.type = XstsFactory.createBooleanType()
- it.expression = XstsFactory.createLiteralBoolean().also {
- it.isValue = false
- }
- }
-
- traceOperationMap[tracerVariable] = traceOperation
- tracerVariables += tracerVariable
-
- return tracerVariable
- }
-
- private fun assignTracerVariable(tracerVariable: XstsTopLevelVariableDeclaration, value: Boolean): XstsOperation {
- return XstsFactory.createAssignmentOperation().also {
- it.reference = XstsFactory.createElementReferenceExpression().also {
- it.element = tracerVariable
- }
- it.expression = XstsFactory.createLiteralBoolean().also {
- it.isValue = value
- }
- }
- }
-
- fun finalizeTransformedTraceOperations(xstsModel: XstsModel) {
- for (tracerVariable in tracerVariables) {
- xstsModel.variableDeclarations += tracerVariable
-
- val resetTracerVariable = assignTracerVariable(tracerVariable, false)
- for (branch in xstsModel.tran.branches) {
- branch.steps.addFirst(resetTracerVariable.copy())
- }
- }
- }
-
- fun transformTraceOperation(traceOperation: TraceOperation): XstsOperation {
- val tracerVariable = createTracerVariable(traceOperation)
-
- return assignTracerVariable(tracerVariable, true)
- }
-
- fun isTracerVariable(variableDeclaration: XstsTopLevelVariableDeclaration): Boolean {
- return variableDeclaration in tracerVariables
- }
-
- fun getTraceOperation(tracerVariable: XstsTopLevelVariableDeclaration): TraceOperation {
- return traceOperationMap[tracerVariable] ?: error("No corresponding trace operation found!")
- }
-
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/utils/DeferredUtils.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/utils/DeferredUtils.kt
deleted file mode 100644
index a985f937..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/utils/DeferredUtils.kt
+++ /dev/null
@@ -1,35 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.utils
-
-import kotlinx.coroutines.CompletableDeferred
-import kotlinx.coroutines.Deferred
-import kotlinx.coroutines.ExperimentalCoroutinesApi
-
-@OptIn(ExperimentalCoroutinesApi::class)
-suspend fun List>.awaitFirstSuccess(): T {
- val firstSuccess = CompletableDeferred()
- var counter = 0
-
- forEach { deferred ->
- deferred.invokeOnCompletion { exception ->
- synchronized(firstSuccess) {
- val id = counter++
-
- if (!firstSuccess.isCompleted) {
- if (exception == null) {
- firstSuccess.complete(deferred.getCompleted())
- } else if (id == size - 1) {
- firstSuccess.completeExceptionally(IllegalStateException("All executed jobs failed: ", exception))
- }
- }
- }
- }
- }
-
- return firstSuccess.await()
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/utils/FileStreamUtils.kt b/subprojects/backends/theta/xsts-verifier/src/main/kotlin/utils/FileStreamUtils.kt
deleted file mode 100644
index 3d125006..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/main/kotlin/utils/FileStreamUtils.kt
+++ /dev/null
@@ -1,16 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2025 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification.utils
-
-import java.io.File
-import java.io.OutputStream
-
-fun File.ensureExistsOutputStream(): OutputStream {
- parentFile.mkdirs()
- createNewFile()
- return outputStream()
-}
diff --git a/subprojects/backends/theta/xsts-verifier/src/test/kotlin/ThetaXstsVerificationTests.kt b/subprojects/backends/theta/xsts-verifier/src/test/kotlin/ThetaXstsVerificationTests.kt
deleted file mode 100644
index 7508463c..00000000
--- a/subprojects/backends/theta/xsts-verifier/src/test/kotlin/ThetaXstsVerificationTests.kt
+++ /dev/null
@@ -1,55 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2026 The Semantifyr Authors
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-
-package hu.bme.mit.semantifyr.backends.theta.verification
-
-import com.google.inject.Inject
-import com.google.inject.Provider
-import hu.bme.mit.semantifyr.oxsts.model.oxsts.ClassDeclaration
-import hu.bme.mit.semantifyr.semantics.BaseSemantifyrVerificationTest
-import hu.bme.mit.semantifyr.semantics.InjectWithOxstsSemantics
-import hu.bme.mit.semantifyr.semantics.SemantifyrVerificationHelper
-import hu.bme.mit.semantifyr.semantics.StandaloneOxstsSemanticsRuntimeModule
-import hu.bme.mit.semantifyr.semantics.utils.loggerFactory
-import org.junit.jupiter.api.Tag
-import org.junit.jupiter.params.ParameterizedTest
-import org.junit.jupiter.params.provider.Arguments
-import org.junit.jupiter.params.provider.MethodSource
-import java.util.stream.Stream
-import kotlin.io.path.Path
-import kotlin.streams.asStream
-
-@Tag("verification")
-@InjectWithOxstsSemantics
-class ThetaXstsVerificationTests : BaseSemantifyrVerificationTest