refactoring tracegen options for clikt

ftsrg · Jan 23, 2025 · 8d19a23 · 8d19a23
1 parent a520e15
commit 8d19a23
Show file tree

Hide file tree

Showing 36 changed files with 69 additions and 64 deletions.
diff --git a/.idea/codeStyles/Project.xml b/.idea/codeStyles/Project.xml
diff --git a/.idea/codeStyles/codeStyleConfig.xml b/.idea/codeStyles/codeStyleConfig.xml
diff --git a/...ojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java b/...ojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgNode.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java b/...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/CegarChecker.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...s/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java b/...s/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/AdvancedArgTrace.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt b/...src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/DoubleEndNodeRemover.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt b/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/PatchArgTrace.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...c/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt b/...c/main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/TraceGenerationChecker.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/.../java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt b/.../java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/AbstractTraceSummary.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/.../main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt b/.../main/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ConcreteSummary.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt b/...hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryFwBinItpChecker.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...ain/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt b/...ain/java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/ExprSummaryStatus.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt b/...java/hu/bme/mit/theta/analysis/algorithm/tracegeneration/summary/TraceGenerationResult.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/.../analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt b/.../analysis/src/main/java/hu/bme/mit/theta/analysis/utils/AbstractTraceSummaryVisualizer.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarChangerUtils.kt b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/VarChangerUtils.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/.../xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingleExprTraceRefiner.kt b/.../xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaSingleExprTraceRefiner.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

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
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt b/...xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToTracegenChecker.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

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
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex23.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex24.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

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
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/stm.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaDslTest.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...ain/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsTraceGenerationConcretizerUtil.kt b/...ain/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsTraceGenerationConcretizerUtil.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...nalysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt b/...nalysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsTracegenPredInitPrec.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...s-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsVarListInitPrec.java b/...s-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/initprec/XstsVarListInitPrec.java
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...rc/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/TracegenerationAbstraction.kt b/...rc/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/TracegenerationAbstraction.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...lysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt b/...lysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenBuilder.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/...alysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt b/...alysis/src/main/java/hu/bme/mit/theta/xsts/analysis/tracegeneration/XstsTracegenConfig.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -98,7 +98,10 @@ abstract class XstsCliBaseCommand(name: String? = null, help: String = "") :
     val trace = status.asUnsafe().cex as Trace<XstsState<*>, XstsAction>
     val concreteTrace =
       XstsTraceConcretizerUtil.concretize(trace, SolverManager.resolveSolverFactory(solver), xsts)
-    val file: File = outputOptions.cexfile!!
-    PrintWriter(file).use { printWriter -> printWriter.write(concreteTrace.toString()) }
+    val outputFile: File = outputOptions.cexfile!!
+    if (!outputFile.parentFile.exists()) {
+      outputFile.parentFile.mkdir()
+    }
+    PrintWriter(outputFile).use { printWriter -> printWriter.write(concreteTrace.toString()) }
   }
 }
diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliTracegen.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -15,14 +15,11 @@
  */
 package hu.bme.mit.theta.xsts.cli
 
-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.types.file
 import com.google.common.base.Stopwatch
 import com.google.common.io.Files
-import com.google.common.io.MoreFiles
-import com.google.common.io.RecursiveDeleteOption
 import hu.bme.mit.theta.analysis.*
 import hu.bme.mit.theta.analysis.algorithm.tracegeneration.summary.*
 import hu.bme.mit.theta.analysis.expl.ExplState
@@ -55,11 +52,11 @@ class XstsCliTracegen :
         help =
           "Directory the traces should be written into. If not specified, output is written into model-directory/traces."
       )
-      .file(mustExist = true, canBeFile = false) // use the non-null value in traceDirPath!
-  val summary: Boolean by
+      .file(mustExist = false, canBeFile = false) // use the non-null value in traceDirPath!
+  val generateSummary: Boolean by
     option(help = "If this flag is present, a concretized summary is generated.")
       .flag(default = false)
-  val traces: Boolean by
+  val generateTraces: Boolean by
     option(help = "If this flag is present, concretized traces are generated.")
       .flag(default = false)
 
@@ -91,8 +88,6 @@ class XstsCliTracegen :
   }
 
   private fun printResult(
-    concretizationResult:
-      Map<AbstractSummaryNode<out XstsState<*>, out XstsAction>, XstsState<ExplState>>,
     abstractSummary: AbstractTraceSummary<out State, out Action>,
     totalTimeMs: Long,
     traceDirPath: File,
@@ -114,7 +109,7 @@ class XstsCliTracegen :
     logger.write(Logger.Level.SUBSTEP, "Abstract trace summary was visualized in ${visFile}\n")
 
     // trace concretization
-    if (traces) {
+    if (generateTraces) {
       var traceCount = 0
 
       val concretizationResultTuple =
@@ -151,7 +146,14 @@ class XstsCliTracegen :
     }
 
     // summary concretization
-    if (summary) {
+    if (generateSummary) {
+      val concretizationResult =
+        XstsTraceGenerationConcretizerUtil.concretizeSummary(
+          abstractSummary as AbstractTraceSummary<XstsState<*>, XstsAction>,
+          Z3LegacySolverFactory.getInstance(),
+          xsts,
+        )
+
       val concreteSummaryFile =
         traceDirPath.absolutePath + File.separator + inputOptions.model.name + ".cexs"
       val cexsString = toCexs(concretizationResult)
@@ -185,9 +187,15 @@ class XstsCliTracegen :
 
     val modelFile = inputOptions.model
     if (traceDirPath.exists()) {
-      MoreFiles.deleteRecursively(traceDirPath.toPath(), RecursiveDeleteOption.ALLOW_INSECURE)
+      val filesToDelete =
+        traceDirPath.listFiles { file ->
+          file.extension in listOf("cex", "cexs", "dot", "png") || file.name == "report.txt"
+        }
+
+      filesToDelete?.forEach { file -> file.delete() }
+    } else {
+      traceDirPath.mkdir()
     }
-    traceDirPath.mkdir()
 
     val propStream = ByteArrayInputStream(("prop {\n" + "\ttrue\n" + "}\n").toByteArray())
     val xsts =
@@ -201,20 +209,7 @@ class XstsCliTracegen :
     val result = checker.check()
     val summary = result.summary as AbstractTraceSummary<XstsState<*>, XstsAction>
 
-    val concretizationResult =
-      XstsTraceGenerationConcretizerUtil.concretizeSummary(
-        summary,
-        Z3LegacySolverFactory.getInstance(),
-        xsts,
-      )
-
     sw.stop()
-    printResult(
-      concretizationResult,
-      result.summary,
-      sw.elapsed(TimeUnit.MILLISECONDS),
-      traceDirPath,
-      xsts,
-    )
+    printResult(summary, sw.elapsed(TimeUnit.MILLISECONDS), traceDirPath, xsts)
   }
 }
diff --git a/...jects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt b/...jects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt
@@ -1,5 +1,5 @@
 /*
- *  Copyright 2024 Budapest University of Technology and Economics
+ *  Copyright 2024-2025 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.