Fixed witnesses

ftsrg · Nov 15, 2024 · 45f052e · 45f052e
1 parent 7ca3c7a
commit 45f052e
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 4 deletions.
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -455,7 +455,7 @@ private fun postVerificationLogging(
         GraphmlWitnessWriter()
           .writeWitness(
             safetyResult,
-            config.inputConfig.input!!,
+            config.outputConfig.witnessConfig.inputFileForWitness ?: config.inputConfig.input!!,
             getSolver(
               config.outputConfig.witnessConfig.concretizerSolver,
               config.outputConfig.witnessConfig.validateConcretizerSolver,
@@ -467,7 +467,7 @@ private fun postVerificationLogging(
         YmlWitnessWriter()
           .writeWitness(
             safetyResult,
-            config.inputConfig.input!!,
+            config.outputConfig.witnessConfig.inputFileForWitness ?: config.inputConfig.input!!,
             config.inputConfig.property,
             (config.frontendConfig.specConfig as? CFrontendConfig)?.architecture,
             getSolver(

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -475,6 +475,7 @@ data class WitnessConfig(
       "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.",
   )
   var validateConcretizerSolver: Boolean = false,
+  @Parameter(names = ["--input-file-for-witness"]) var inputFileForWitness: File? = null,
 ) : Config
 
 data class ArgConfig(

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/bounded25.kt
@@ -80,6 +80,7 @@ fun boundedPortfolio25(
               disable = false,
               concretizerSolver = "Z3",
               validateConcretizerSolver = false,
+              inputFileForWitness = portfolioConfig.inputConfig.input,
             ),
           argConfig = ArgConfig(disable = true),
           enableOutput = portfolioConfig.outputConfig.enableOutput,

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt
@@ -117,6 +117,7 @@ fun complexPortfolio25(
               disable = false,
               concretizerSolver = "Z3",
               validateConcretizerSolver = false,
+              inputFileForWitness = portfolioConfig.inputConfig.input,
             ),
           argConfig = ArgConfig(disable = true),
           enableOutput = portfolioConfig.outputConfig.enableOutput,

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/horn25.kt
@@ -71,6 +71,7 @@ fun hornPortfolio25(
               disable = false,
               concretizerSolver = "Z3",
               validateConcretizerSolver = false,
+              inputFileForWitness = portfolioConfig.inputConfig.input,
             ),
           argConfig = ArgConfig(disable = true),
           enableOutput = portfolioConfig.outputConfig.enableOutput,

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/YmlWitnessWriter.kt
@@ -36,6 +36,7 @@ import hu.bme.mit.theta.xcfa.model.MetaData
 import hu.bme.mit.theta.xcfa.toC
 import java.io.File
 import java.util.*
+import kotlinx.serialization.encodeToString
 
 class YmlWitnessWriter {
 
@@ -97,7 +98,7 @@ class YmlWitnessWriter {
             },
         )
 
-      witnessfile.writeText(WitnessYamlConfig.encodeToString(YamlWitness.serializer(), witness))
+      witnessfile.writeText(WitnessYamlConfig.encodeToString(listOf(witness)))
     } else if (safetyResult.isSafe) {
 
       val witness =
@@ -107,7 +108,7 @@ class YmlWitnessWriter {
           content = safetyResult.asSafe().proof.toContent(inputFile, parseContext),
         )
 
-      witnessfile.writeText(WitnessYamlConfig.encodeToString(YamlWitness.serializer(), witness))
+      witnessfile.writeText(WitnessYamlConfig.encodeToString(listOf(witness)))
     }
   }
 }