Extract common printing

RipplB · Aug 7, 2024 · c846c51 · c846c51
1 parent ea27662
commit c846c51
Show file tree

Hide file tree

Showing 6 changed files with 33 additions and 28 deletions.
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
@@ -24,6 +24,8 @@ import com.github.ajalt.clikt.parameters.options.versionOption
 import com.github.ajalt.clikt.parameters.types.file
 import hu.bme.mit.theta.analysis.Trace
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.analysis.algorithm.arg.ARG
+import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics
 import hu.bme.mit.theta.common.logging.ConsoleLogger
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.common.logging.NullLogger
@@ -72,6 +74,15 @@ abstract class XstsCliBaseCommand(name: String? = null, help: String = "") :
         }
     }
 
+    fun printCommonResult(status: SafetyResult<*,*>, xsts: XSTS, totalTimeMs: Long) {
+        listOf(
+            status.isSafe,
+            totalTimeMs,
+            if (status.isUnsafe) "${status.asUnsafe().cex!!.length()}" else "",
+            xsts.vars.size,
+        ).forEach(writer::cell)
+    }
+
     fun registerSolverManagers() {
         SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3.Z3SolverManager.create())
         SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3legacy.Z3SolverManager.create())

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt
@@ -85,13 +85,10 @@ class XstsCliBounded : XstsCliBaseCommand(
 
     private fun printResult(status: SafetyResult<EmptyWitness, Trace<S, XstsAction>>, xsts: XSTS, totalTimeMs: Long) {
         if (!outputOptions.benchmarkMode) return
+        printCommonResult(status, xsts, totalTimeMs)
         val stats = status.stats.orElse(BoundedStatistics(0)) as BoundedStatistics
         listOf(
-            status.isSafe,
-            totalTimeMs,
             stats.iterations,
-            if (status.isUnsafe) "${status.asUnsafe().cex!!.length()}" else "",
-            xsts.vars.size,
         ).forEach(writer::cell)
         writer.newRow()
     }

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliCegar.kt
@@ -56,21 +56,18 @@ class XstsCliCegar : XstsCliBaseCommand(
     private val prunestrategy: PruneStrategy by option().enum<PruneStrategy>().default(PruneStrategy.LAZY)
     private val optimizestmts: OptimizeStmts by option().enum<OptimizeStmts>().default(OptimizeStmts.ON)
 
-    private fun printResult(status: SafetyResult<out ARG<*, *>?, out Trace<*, *>?>, sts: XSTS, totalTimeMs: Long) {
+    private fun printResult(status: SafetyResult<out ARG<*, *>?, out Trace<*, *>?>, xsts: XSTS, totalTimeMs: Long) {
         if (!outputOptions.benchmarkMode) return
+        printCommonResult(status, xsts, totalTimeMs)
         val stats = status.stats.orElse(CegarStatistics(0, 0, 0, 0)) as CegarStatistics
         listOf(
-            status.isSafe,
-            totalTimeMs,
             stats.algorithmTimeMs,
             stats.abstractorTimeMs,
             stats.refinerTimeMs,
             stats.iterations,
             status.witness!!.size(),
             status.witness!!.depth,
             status.witness!!.meanBranchingFactor,
-            if (status.isUnsafe) "${status.asUnsafe().cex!!.length()}" else "",
-            sts.vars.size,
         ).forEach(writer::cell)
         writer.newRow()
     }

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliChc.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliChc.kt
@@ -35,12 +35,7 @@ class XstsCliChc : XstsCliBaseCommand(
 
     private fun printResult(status: SafetyResult<Invariant, CexTree>, xsts: XSTS, totalTimeMs: Long) {
         if (!outputOptions.benchmarkMode) return
-        listOf(
-            status.isSafe,
-            totalTimeMs,
-            if (status.isUnsafe) "${status.asUnsafe().cex!!.length()}" else "",
-            xsts.vars.size,
-        ).forEach(writer::cell)
+        printCommonResult(status, xsts, totalTimeMs)
         writer.newRow()
     }
 

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliHeader.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliHeader.kt
@@ -19,6 +19,7 @@ package hu.bme.mit.theta.xsts.cli
 import com.github.ajalt.clikt.core.CliktCommand
 import com.github.ajalt.clikt.parameters.options.default
 import com.github.ajalt.clikt.parameters.options.option
+import com.github.ajalt.clikt.parameters.options.required
 import com.github.ajalt.clikt.parameters.types.enum
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker
 import hu.bme.mit.theta.common.table.BasicTableWriter
@@ -30,8 +31,8 @@ class XstsCliHeader : CliktCommand(name = "header") {
     enum class Algorithm { CEGAR, MDD, BOUNDED, PN_MDD, CHC }
 
     private val algorithm: Algorithm by option(
-        help = "The algorithm to prtint the header for"
-    ).enum<Algorithm>().default(Algorithm.CEGAR)
+        help = "The algorithm to print the header for"
+    ).enum<Algorithm>().required()
     private val iterationStrategy: MddChecker.IterationStrategy by option(
         help = "The state space generation algorithm for symbolic checking"
     ).enum<MddChecker.IterationStrategy>().default(MddChecker.IterationStrategy.GSAT)
@@ -46,32 +47,39 @@ class XstsCliHeader : CliktCommand(name = "header") {
         }
     }
 
+    private fun printCommonHeader() {
+        listOf(
+            "Result", "TimeMs", "CexLen", "Vars"
+        ).forEach(writer::cell)
+    }
+
     private fun printCegarHeader() {
+        printCommonHeader()
         listOf(
-            "Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations",
-            "ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen", "Vars"
+            "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations",
+            "ArgSize", "ArgDepth", "ArgMeanBranchFactor"
         ).forEach(writer::cell)
         writer.newRow()
     }
 
     private fun printBoundedHeader() {
+        printCommonHeader()
         listOf(
-            "Result", "TimeMs", "Iterations", "CexLen", "Vars"
+            "Iterations",
         ).forEach(writer::cell)
         writer.newRow()
     }
 
     private fun printMddHeader() {
+        printCommonHeader()
         listOf(
-            "Result", "TimeMs", "ViolatingSize", "StateSpaceSize", "HitCount", "QueryCount", "CacheSize", "CexLen", "Vars"
+             "ViolatingSize", "StateSpaceSize", "HitCount", "QueryCount", "CacheSize",
         ).forEach(writer::cell)
         writer.newRow()
     }
 
     private fun printChcHeader() {
-        listOf(
-            "Result", "TimeMs", "CexLen", "Vars"
-        ).forEach(writer::cell)
+        printCommonHeader()
         writer.newRow()
     }
 

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMdd.kt
@@ -55,17 +55,14 @@ class XstsCliMdd : XstsCliBaseCommand(
 
     private fun printResult(status: SafetyResult<MddWitness, MddCex>, xsts: XSTS, totalTimeMs: Long) {
         if (!outputOptions.benchmarkMode) return
+        printCommonResult(status, xsts, totalTimeMs)
         val stats = status.stats.orElse(MddAnalysisStatistics(0, 0, 0, 0, 0)) as MddAnalysisStatistics
         listOf(
-            status.isSafe,
-            totalTimeMs,
             stats.violatingSize,
             stats.stateSpaceSize,
             stats.hitCount,
             stats.queryCount,
             stats.cacheSize,
-            if (status.isUnsafe) "${status.asUnsafe().cex!!.length()}" else "",
-            xsts.vars.size,
         ).forEach(writer::cell)
         writer.newRow()
     }