Enhance debugging options and Linux compatibility

.gitignore

@@ -6,3 +6,7 @@
 .idea/
 .gradle/
 /**/build/
+
+*.err
+*.out
+*.cex

.run/Compile SimpleMission LeaderOperational_Unsafe.run.xml

@@ -6,7 +6,7 @@
     <shortenClasspath name="NONE" />
     <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/subprojects/semantifyr" />
     <method v="2">
-      <option name="Make" enabled="true" />
+      <option name="Gradle.BeforeRunTask" enabled="true" tasks="assemble" externalProjectPath="$PROJECT_DIR$" vmOptions="" scriptParameters="" />
     </method>
   </configuration>
 </component>

.run/Verify SimpleMission LeaderOperational_Unsafe.run.xml

@@ -6,7 +6,7 @@
     <shortenClasspath name="NONE" />
     <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/subprojects/semantifyr" />
     <method v="2">
-      <option name="Make" enabled="true" />
+      <option name="Gradle.BeforeRunTask" enabled="true" tasks="assemble" externalProjectPath="$PROJECT_DIR$" vmOptions="" scriptParameters="" />
     </method>
   </configuration>
 </component>

.run/Verify XSTS SimpleMission LeaderOperational_Unsafe.run.xml

@@ -6,7 +6,7 @@
     <shortenClasspath name="NONE" />
     <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/subprojects/semantifyr" />
     <method v="2">
-      <option name="Make" enabled="true" />
+      <option name="Gradle.BeforeRunTask" enabled="true" tasks="assemble" externalProjectPath="$PROJECT_DIR$" vmOptions="" scriptParameters="" />
     </method>
   </configuration>
 </component>

doc/development.md

@@ -0,0 +1,15 @@
+<!--
+  SPDX-FileCopyrightText: 2023-2024 The Semantifyr Authors
+
+  SPDX-License-Identifier: EPL-2.0
+-->
+
+## 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`

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

@@ -33,6 +33,7 @@ State:
 ;
 
 ExplState:
+    {ExplState}
     "(" "ExplState"
         (variableStates += ExplVariableState)*
     ")"

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 {}
 

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<void>((resolve, reject) => {                    
-                    const process = childProcess.spawn(runner, [commandArg, compilerExecutable, 'compile', documentPath, workspaceFolder, targetName, '-o', outputFile]);
+                return new Promise<void>((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<void>((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<void>((resolve, reject) => {
-                    const process = childProcess.spawn(runner, [commandArg, compilerExecutable, 'verify-xsts', documentPath]);
+                    const process = spawnProcess(compilerExecutable, 'verify-xsts', [documentPath]);
 
                     outputChannel.clear();
 

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

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")
+    }
 }