diff --git a/.gitignore b/.gitignore
index e2d695a9..a84e2e06 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,7 @@
.idea/
.gradle/
/**/build/
+
+*.err
+*.out
+*.cex
diff --git a/.run/Compile SimpleMission LeaderOperational_Unsafe.run.xml b/.run/Compile SimpleMission LeaderOperational_Unsafe.run.xml
index d7f18d35..4943bbdd 100644
--- a/.run/Compile SimpleMission LeaderOperational_Unsafe.run.xml
+++ b/.run/Compile SimpleMission LeaderOperational_Unsafe.run.xml
@@ -6,7 +6,7 @@
-
+
\ No newline at end of file
diff --git a/.run/Verify SimpleMission LeaderOperational_Unsafe.run.xml b/.run/Verify SimpleMission LeaderOperational_Unsafe.run.xml
index 191bbf23..703713a9 100644
--- a/.run/Verify SimpleMission LeaderOperational_Unsafe.run.xml
+++ b/.run/Verify SimpleMission LeaderOperational_Unsafe.run.xml
@@ -6,7 +6,7 @@
-
+
\ No newline at end of file
diff --git a/.run/Verify XSTS SimpleMission LeaderOperational_Unsafe.run.xml b/.run/Verify XSTS SimpleMission LeaderOperational_Unsafe.run.xml
index 625443c3..24686a4c 100644
--- a/.run/Verify XSTS SimpleMission LeaderOperational_Unsafe.run.xml
+++ b/.run/Verify XSTS SimpleMission LeaderOperational_Unsafe.run.xml
@@ -6,7 +6,7 @@
-
+
\ No newline at end of file
diff --git a/doc/development.md b/doc/development.md
new file mode 100644
index 00000000..2312d688
--- /dev/null
+++ b/doc/development.md
@@ -0,0 +1,15 @@
+
+
+## General Workflow
+
+You have the following options on how to use and/or debug Semantifyr:
+- open the project in Intellij IDE and use the existing Kotlin configurations/make your own
+- open the `semantifyr-vscode` subproject in VS Code and press *F5* to
+ - _make sure that the `Gradle for Java` and other Java extensions are disabled/set up to not auto-build, so that VS Code will not try to rebuild the project and that the recommended extensions (`.vscode/extensions.json`) are installed_
+- install semantifyr as a VS code extension, for example: `code --install-extension ./subprojects/semantifyr-vscode/build/vscode/semantifyr-0.0.1.vsix`
+ - make sure to `gradle build` or `gradle assemble` beforehand and restart VS code after
+ - if the extension is installed successfully, just open VS code, open `subprojects/semantifyr/TestModels` or your own models and use the commands popping up over the `Target`
diff --git a/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext b/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext
index 46ab45bf..84c0cee3 100644
--- a/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext
+++ b/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/Cex.xtext
@@ -33,6 +33,7 @@ State:
;
ExplState:
+ {ExplState}
"(" "ExplState"
(variableStates += ExplVariableState)*
")"
diff --git a/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2 b/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2
index 65facd13..6358d0c9 100644
--- a/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2
+++ b/subprojects/cex.lang/src/main/java/hu/bme/mit/semantifyr/cex/lang/GenerateCex.mwe2
@@ -42,7 +42,7 @@ Workflow {
}
language = StandardLanguage {
name = "hu.bme.mit.semantifyr.cex.lang.Cex"
- fileExtensions = "cex"
+ fileExtensions = "cex, cexs"
fragment = ecore2xtext.Ecore2XtextValueConverterServiceFragment2 auto-inject {}
diff --git a/subprojects/semantifyr-vscode/src/extension.ts b/subprojects/semantifyr-vscode/src/extension.ts
index ea1c8259..26e7af22 100644
--- a/subprojects/semantifyr-vscode/src/extension.ts
+++ b/subprojects/semantifyr-vscode/src/extension.ts
@@ -62,13 +62,25 @@ class OxstsCodeLensProvider implements vscode.CodeLensProvider {
export function activate(context: ExtensionContext) {
const runner = os.type() === 'Windows_NT' ? 'cmd' : 'sh';
- const commandArg = os.type() === 'Windows_NT' ? '/c' : '-c';
+ const commandArg = os.type() === 'Windows_NT' ? '/c' : '';
const executablePostfix = os.type() === 'Windows_NT' ? '.bat' : '';
const oxstsIdeExecutable = path.join(context.extensionPath, 'bin', 'oxsts.lang.ide', 'bin', `oxsts.lang.ide${executablePostfix}`);
const xstsIdeExecutable = path.join(context.extensionPath, 'bin', 'xsts.lang.ide', 'bin', `xsts.lang.ide${executablePostfix}`);
const compilerExecutable = path.join(context.extensionPath, 'bin', 'semantifyr', 'bin', `semantifyr${executablePostfix}`);
+ // TODO: needs testing on Windows
+ function spawnProcess(compilerExecutable: string, semantifyrCommand: string, remainingArgs: string[]) {
+ if (os.type() === 'Windows_NT') {
+ const args = [commandArg, compilerExecutable, semantifyrCommand].concat(remainingArgs)
+ return childProcess.spawn(runner, args);
+ } else { // assume linux
+ // -c does not work (would probably work if args would be concatenated to a string), but also not necessary
+ const args = [compilerExecutable, semantifyrCommand].concat(remainingArgs)
+ return childProcess.spawn(runner, args);
+ }
+ }
+
outputChannel = vscode.window.createOutputChannel("Semantifyr");
context.subscriptions.push(outputChannel);
@@ -91,8 +103,8 @@ export function activate(context: ExtensionContext) {
title: `Compiling target: ${targetName}`,
cancellable: false
}, () => {
- return new Promise((resolve, reject) => {
- const process = childProcess.spawn(runner, [commandArg, compilerExecutable, 'compile', documentPath, workspaceFolder, targetName, '-o', outputFile]);
+ return new Promise((resolve, reject) => {
+ const process = spawnProcess(compilerExecutable, 'compile', [documentPath, workspaceFolder, targetName, "-o", outputFile]);
outputChannel.clear();
@@ -141,12 +153,13 @@ export function activate(context: ExtensionContext) {
cancellable: false
}, () => {
return new Promise((resolve, reject) => {
- const args = [commandArg, compilerExecutable, 'verify', documentPath, workspaceFolder, targetName]
+ const args = [documentPath, workspaceFolder, targetName]
+
if (generateWitness) {
args.push("--witness")
}
- const process = childProcess.spawn(runner, args);
+ const process = spawnProcess(compilerExecutable, 'verify', args);
outputChannel.clear();
@@ -192,7 +205,7 @@ export function activate(context: ExtensionContext) {
cancellable: false
}, () => {
return new Promise((resolve, reject) => {
- const process = childProcess.spawn(runner, [commandArg, compilerExecutable, 'verify-xsts', documentPath]);
+ const process = spawnProcess(compilerExecutable, 'verify-xsts', [documentPath]);
outputChannel.clear();
diff --git a/subprojects/semantifyr/src/main/kotlin/commands/BaseVerifyCommand.kt b/subprojects/semantifyr/src/main/kotlin/commands/BaseVerifyCommand.kt
index 985acb22..16c66ca1 100644
--- a/subprojects/semantifyr/src/main/kotlin/commands/BaseVerifyCommand.kt
+++ b/subprojects/semantifyr/src/main/kotlin/commands/BaseVerifyCommand.kt
@@ -8,8 +8,10 @@ import com.github.ajalt.clikt.parameters.options.multiple
import com.github.ajalt.clikt.parameters.options.option
import com.github.ajalt.clikt.parameters.types.file
import com.github.ajalt.clikt.parameters.types.long
+import hu.bme.mit.semantifyr.oxsts.semantifyr.theta.ThetaDockerExecutor
import hu.bme.mit.semantifyr.oxsts.semantifyr.theta.ThetaExecutor
import hu.bme.mit.semantifyr.oxsts.semantifyr.theta.ThetaRuntimeDetails
+import hu.bme.mit.semantifyr.oxsts.semantifyr.theta.ThetaShellExecutor
import org.slf4j.Logger
import java.io.File
import java.util.concurrent.TimeUnit
@@ -23,30 +25,39 @@ abstract class BaseVerifyCommand(name: String) : CliktCommand(name) {
val thetaVersion by option().default("6.5.2")
val thetaConfiguration by option().multiple(
default = listOf(
- "--domain EXPL --refinement SEQ_ITP --maxenum 250 --initprec CTRL --stacktrace",
- "--domain EXPL_PRED_COMBINED --autoexpl NEWOPERANDS --initprec CTRL --stacktrace",
- "--domain PRED_CART --refinement SEQ_ITP --stacktrace",
- "--stacktrace",
+ "CEGAR --domain EXPL --refinement SEQ_ITP --maxenum 250 --initprec CTRL --stacktrace",
+ "CEGAR --domain EXPL_PRED_COMBINED --autoexpl NEWOPERANDS --initprec CTRL --stacktrace",
+ "CEGAR --domain PRED_CART --refinement SEQ_ITP --stacktrace",
+ "CEGAR --stacktrace",
),
)
- fun runVerification(xstsPath: String): ThetaRuntimeDetails {
+ fun runVerification(xstsPath: String, thetaStartPath: String = ""): ThetaRuntimeDetails {
val xstsFile = File(xstsPath)
- logger.info("Executing Theta (v$thetaVersion) on $xstsPath")
-
- val thetaExecutor = ThetaExecutor(
- thetaVersion,
- thetaConfiguration,
- timeout,
- TimeUnit.MINUTES
- )
-
val workingDirectory = xstsFile.parentFile.absolutePath
val fileName = xstsFile.nameWithoutExtension
+ val thetaExecutor : ThetaExecutor = if(thetaStartPath!="") {
+ // using a local release (Theta-xsts.zip)
+ logger.info("Executing local Theta from JAR ($thetaStartPath) on $xstsPath")
+ ThetaShellExecutor(
+ thetaStartPath,
+ thetaConfiguration,
+ timeout,
+ TimeUnit.MINUTES
+ )
+ } else {
+ // using docker
+ logger.info("Executing Theta (v$thetaVersion) on $xstsPath")
+ ThetaDockerExecutor(
+ thetaVersion,
+ thetaConfiguration,
+ timeout,
+ TimeUnit.MINUTES
+ )
+ }
val runtimeDetails = thetaExecutor.run(workingDirectory, fileName)
-
logger.info("Verification result: isUnsafe = ${runtimeDetails.isUnsafe}")
return runtimeDetails
diff --git a/subprojects/semantifyr/src/main/kotlin/commands/VerifyCommand.kt b/subprojects/semantifyr/src/main/kotlin/commands/VerifyCommand.kt
index 6c6bf5b9..b5453443 100644
--- a/subprojects/semantifyr/src/main/kotlin/commands/VerifyCommand.kt
+++ b/subprojects/semantifyr/src/main/kotlin/commands/VerifyCommand.kt
@@ -1,8 +1,11 @@
package hu.bme.mit.semantifyr.oxsts.semantifyr.commands
import com.github.ajalt.clikt.parameters.arguments.argument
+import com.github.ajalt.clikt.parameters.options.default
import com.github.ajalt.clikt.parameters.options.flag
import com.github.ajalt.clikt.parameters.options.option
+import com.github.ajalt.clikt.parameters.options.optionalValue
+import com.github.ajalt.clikt.parameters.options.optionalValueLazy
import com.github.ajalt.clikt.parameters.types.file
import hu.bme.mit.semantifyr.oxsts.semantifyr.reader.OxstsReader
import hu.bme.mit.semantifyr.oxsts.semantifyr.reader.prepareOxsts
@@ -20,6 +23,7 @@ class VerifyCommand : BaseVerifyCommand("verify") {
override val logger by loggerFactory()
+ val thetaStartScript by option("--theta-start-sh").default("")
val libraryDirectory by argument().file(mustExist = true, canBeDir = true)
val targetName by argument()
val generateWitness by option("-w", "--witness").flag()
@@ -47,11 +51,16 @@ class VerifyCommand : BaseVerifyCommand("verify") {
logger.info("Producing xsts file to $output")
- val result = runVerification(output)
+ val result = runVerification(output, thetaStartScript)
- if (generateWitness && result.isUnsafe) {
+ if (generateWitness && result.isUnsafe && File(result.cexPath).exists()) {
generateWitness(result, reader)
}
+
+ // in case of tracegen generating .cexs, safety of result does not matter
+ if (generateWitness && File(result.cexsPath).exists()) {
+ generateSummaryWitness(result, reader)
+ }
}
private fun generateWitness(
@@ -76,4 +85,25 @@ class VerifyCommand : BaseVerifyCommand("verify") {
logger.info("Saved witness to $witnessPath")
}
+ private fun generateSummaryWitness(
+ result: ThetaRuntimeDetails,
+ reader: OxstsReader
+ ) {
+ logger.info("Generating witness from ${result.cexsPath}")
+
+ prepareCex()
+
+ val cexReader = CexReader()
+ val cex = cexReader.readCexFile(File(result.cexsPath))
+
+ val witnessCreator = WitnessCreator(reader)
+
+ val witnessPath = model.path.replace(".oxsts", ".cexs.oxsts")
+ val resource = reader.resourceSet.createResource(URI.createFileURI(witnessPath))
+ resource.contents += witnessCreator.createWitness(targetName, cex)
+
+ resource.save(null)
+
+ logger.info("Saved witness to $witnessPath")
+ }
}
diff --git a/subprojects/semantifyr/src/main/kotlin/theta/ThetaExecutor.kt b/subprojects/semantifyr/src/main/kotlin/theta/ThetaExecutor.kt
index c0ffe1b3..901e0d37 100644
--- a/subprojects/semantifyr/src/main/kotlin/theta/ThetaExecutor.kt
+++ b/subprojects/semantifyr/src/main/kotlin/theta/ThetaExecutor.kt
@@ -36,6 +36,8 @@ import java.util.concurrent.TimeUnit
import kotlin.io.path.absolute
import kotlin.time.toDuration
import kotlin.time.toDurationUnit
+import kotlinx.coroutines.sync.Mutex
+import kotlinx.coroutines.sync.withLock
class ThetaRuntimeDetails(
val id: Int,
@@ -44,25 +46,70 @@ class ThetaRuntimeDetails(
) {
val modelFile = "$name.xsts"
val cexFile = "$name$id.cex"
+ val cexsFile = "$name.cexs"
val logFile = "theta$id.out"
val errFile = "theta$id.err"
val modelPath = "$workingDirectory${File.separator}$modelFile"
- val cexPath = "$workingDirectory${File.separator}$cexFile"
+ // Theta can produce several kinds of output files, even images
+ // it's probably a good idea to group all of those under here
+ val outputPath = "$workingDirectory${File.separator}theta-traces"
+
+ val cexPath = "$outputPath${File.separator}$cexFile"
+ val cexsPath = "$outputPath${File.separator}$cexsFile"
val logPath = "$workingDirectory${File.separator}$logFile"
val errPath = "$workingDirectory${File.separator}$errFile"
val isUnsafe: Boolean by lazy {
- Files.exists(Paths.get(cexPath))
+ val filePath = Paths.get(logPath)
+ if (Files.exists(filePath)) {
+ Files.lines(filePath).use { lines ->
+ lines.anyMatch { it.contains("SafetyResult Unsafe") }
+ }
+ } else {
+ false
+ }
+ }
+}
+
+abstract class ThetaExecutor {
+ abstract fun run(workingDirectory: String, name: String) : ThetaRuntimeDetails
+
+ // Some Theta parameters are only important to Theta (e.g., what abstraction to use),
+ // but some are important here as well, such as if the output is a single or several .cex files, or .cexs files, etc. (see TRACEGEN).
+ // To keep the different executors uniform, they should use this helper function to get their Theta parameters.
+ fun getParameters(parameter: String, thetaRuntimeDetails: ThetaRuntimeDetails, docker: Boolean = false): Array {
+ val params = parameter.split(" ").toTypedArray()
+ val outputFlag = if(parameter.contains("TRACEGEN")) {
+ if(docker) {
+ "--trace-dir " + "/host/${File(thetaRuntimeDetails.cexsPath).parent}"
+ } else {
+ "--trace-dir " + File(thetaRuntimeDetails.cexsPath).parent
+ }
+ } else {
+ if(docker) {
+ // Mainline Theta will not create the folder and will concatenate absolute paths incorrectly here
+ // TODO will add fix in PR later to properly support output directories and absolute paths
+ "--cexfile " + "/host/${File(thetaRuntimeDetails.outputPath).name}${File.separator}${thetaRuntimeDetails.cexFile}"
+ } else {
+ "--cexfile " + "${File(thetaRuntimeDetails.outputPath).name}${File.separator}${thetaRuntimeDetails.cexFile}"
+ }
+ }
+ val modelFlag = if(docker) {
+ "--model " + "/host/${thetaRuntimeDetails.modelFile}"
+ } else {
+ "--model " + thetaRuntimeDetails.modelFile
+ }
+ return (params + outputFlag + modelFlag).joinToString(" ").split(" ").toTypedArray()
}
}
-class ThetaExecutor(
+class ThetaDockerExecutor(
private val version: String,
private val parameters: List,
private val timeout: Long = 3,
private val timeUnit: TimeUnit = TimeUnit.MINUTES
-) {
+) : ThetaExecutor() {
private val logger by loggerFactory()
@@ -116,7 +163,7 @@ class ThetaExecutor(
logger.info("Theta finished ($id)")
} else {
logger.error("Theta failed ($id)")
- throw IllegalStateException("Theta execution failed with code ${result.statusCode}. See $thetaRuntimeDetails")
+ throw IllegalStateException("Theta execution failed with code ${result.statusCode}. See ${thetaRuntimeDetails.errPath} (and .out) files")
}
return thetaRuntimeDetails
@@ -148,12 +195,11 @@ class ThetaExecutor(
val hostConfig = HostConfig.newHostConfig()
.withBinds(Bind(thetaRuntimeDetails.workingDirectory, Volume("/host")))
+ val param = super.getParameters(parameter, thetaRuntimeDetails, true)
+
val container = dockerClient.createContainerCmd("ftsrg/theta-xsts-cli:$version")
.withCmd(
- "CEGAR",
- "--model", "/host/${thetaRuntimeDetails.modelFile}",
- "--cexfile", "/host/${thetaRuntimeDetails.cexFile}",
- *parameter.split(" ").toTypedArray(),
+ *param
)
.withHostConfig(hostConfig)
.exec()
@@ -179,6 +225,7 @@ class ThetaExecutor(
}
}
+ override
fun run(workingDirectory: String, name: String) = runBlocking {
val absoluteDirectory = Path.of(workingDirectory).absolute().toString()
@@ -186,3 +233,111 @@ class ThetaExecutor(
}
}
+
+class ThetaShellExecutor(
+ private val shPath: String,
+ private val parameters: List,
+ private val timeout: Long = 3,
+ private val timeUnit: TimeUnit = TimeUnit.MINUTES
+) : ThetaExecutor() {
+
+ private val logger by loggerFactory()
+ private val mutex = Mutex()
+
+ init {
+ if (System.getProperty("os.name").contains("Windows", ignoreCase = true)) {
+ throw UnsupportedOperationException("ThetaShellExecutor does not support Windows for now")
+ }
+ }
+
+ private suspend fun runTheta(
+ workingDirectory: String,
+ name: String,
+ parameter: String,
+ id: Int
+ ): ThetaRuntimeDetails {
+ logger.info("Starting theta ($id)")
+
+ val thetaRuntimeDetails = ThetaRuntimeDetails(id, workingDirectory, name)
+
+ val param = super.getParameters(parameter, thetaRuntimeDetails, false)
+
+ val processBuilder = ProcessBuilder(
+ shPath,
+ *param
+ )
+ processBuilder.directory(File(workingDirectory))
+
+ val process = try {
+ withTimeout(timeout.toDuration(timeUnit.toDurationUnit())) {
+ mutex.withLock {
+ processBuilder.start()
+ }
+ }
+ } catch (e: TimeoutCancellationException) {
+ logger.info("Theta timed out ($id)")
+ throw e
+ } catch (e: Exception) {
+ logger.error("Theta execution failed ($id)", e)
+ throw e
+ }
+
+ val exitCode = try {
+ withTimeout(timeout.toDuration(timeUnit.toDurationUnit())) {
+ process.waitFor()
+ }
+ } catch (e: TimeoutCancellationException) {
+ logger.info("Theta timed out ($id)")
+ process.destroy()
+ throw e
+ } finally {
+ saveProcessLogs(thetaRuntimeDetails, process)
+ }
+
+ if (exitCode == 0) {
+ logger.info("Theta finished ($id)")
+ } else {
+ logger.error("Theta failed ($id) with code $exitCode")
+ throw IllegalStateException("Theta execution failed with code $exitCode. See ${thetaRuntimeDetails.errPath} (and .out) files")
+ }
+
+ return thetaRuntimeDetails
+ }
+
+ private fun saveProcessLogs(thetaRuntimeDetails: ThetaRuntimeDetails, process: Process) {
+ try {
+ val logFile = File(thetaRuntimeDetails.logPath)
+ val errFile = File(thetaRuntimeDetails.errPath)
+
+ process.inputStream.bufferedReader().use { logFile.writeText(it.readText()) }
+ process.errorStream.bufferedReader().use { errFile.writeText(it.readText()) }
+ } catch (e: Exception) {
+ logger.error("Exception during saving logging details (${thetaRuntimeDetails.id})", e)
+ }
+ }
+
+ private suspend fun runWorkflow(workingDirectory: String, name: String) = supervisorScope {
+ val jobs = parameters.indices.map { index ->
+ async(Dispatchers.IO) {
+ runTheta(workingDirectory, name, parameters[index], index)
+ }
+ }
+
+ try {
+ logger.debug("Awaiting jobs")
+ jobs.awaitAny()
+ } finally {
+ logger.debug("Canceling jobs")
+ jobs.forEach {
+ it.cancelAndJoin()
+ }
+ }
+ }
+
+ override
+ fun run(workingDirectory: String, name: String) = runBlocking {
+ val absoluteDirectory = Path.of(workingDirectory).absolute().toString()
+
+ runWorkflow(absoluteDirectory, name)
+ }
+}
diff --git a/subprojects/semantifyr/src/test/kotlin/GammaVerificationTests.kt b/subprojects/semantifyr/src/test/kotlin/GammaVerificationTests.kt
index e111db34..063b9373 100644
--- a/subprojects/semantifyr/src/test/kotlin/GammaVerificationTests.kt
+++ b/subprojects/semantifyr/src/test/kotlin/GammaVerificationTests.kt
@@ -44,7 +44,7 @@ class GammaVerificationTests : VerificationTest() {
@JvmStatic
fun prepare() {
prepareOxsts()
- thetaExecutor.initTheta()
+ thetaDockerExecutor.initTheta()
}
}
diff --git a/subprojects/semantifyr/src/testFixtures/kotlin/VerificationTest.kt b/subprojects/semantifyr/src/testFixtures/kotlin/VerificationTest.kt
index 49d9598a..91358609 100644
--- a/subprojects/semantifyr/src/testFixtures/kotlin/VerificationTest.kt
+++ b/subprojects/semantifyr/src/testFixtures/kotlin/VerificationTest.kt
@@ -9,7 +9,7 @@ package hu.bme.mit.semantifyr.oxsts.semantifyr
import hu.bme.mit.semantifyr.oxsts.model.oxsts.Target
import hu.bme.mit.semantifyr.oxsts.semantifyr.reader.OxstsReader
import hu.bme.mit.semantifyr.oxsts.semantifyr.serialization.XstsSerializer
-import hu.bme.mit.semantifyr.oxsts.semantifyr.theta.ThetaExecutor
+import hu.bme.mit.semantifyr.oxsts.semantifyr.theta.ThetaDockerExecutor
import hu.bme.mit.semantifyr.oxsts.semantifyr.transformation.XstsTransformer
import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.EnvVar
import hu.bme.mit.semantifyr.oxsts.semantifyr.utils.loggerFactory
@@ -35,13 +35,13 @@ open class VerificationTest {
companion object {
val thetaVersion by EnvVar()
- val thetaExecutor = ThetaExecutor(
+ val thetaDockerExecutor = ThetaDockerExecutor(
thetaVersion,
listOf(
- "--domain EXPL --refinement SEQ_ITP --maxenum 250 --initprec CTRL --stacktrace",
- "--domain EXPL_PRED_COMBINED --autoexpl NEWOPERANDS --initprec CTRL --stacktrace",
- "--domain PRED_CART --refinement SEQ_ITP --stacktrace",
- "--stacktrace",
+ "CEGAR --domain EXPL --refinement SEQ_ITP --maxenum 250 --initprec CTRL --stacktrace",
+ "CEGAR --domain EXPL_PRED_COMBINED --autoexpl NEWOPERANDS --initprec CTRL --stacktrace",
+ "CEGAR --domain PRED_CART --refinement SEQ_ITP --stacktrace",
+ "CEGAR --stacktrace",
),
)
@@ -87,7 +87,7 @@ open class VerificationTest {
logger.info("Executing theta on $modelPath")
- val result = thetaExecutor.run(targetDirectory, targetName)
+ val result = thetaDockerExecutor.run(targetDirectory, targetName)
logger.info("Checking results of Theta")