Skip to content

Commit

Permalink
fixed --traces and --summary in xsts cli
Browse files Browse the repository at this point in the history
  • Loading branch information
AdamZsofi committed Nov 25, 2024
1 parent 000ebfb commit ec1a632
Showing 1 changed file with 6 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@
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.boolean
import com.github.ajalt.clikt.parameters.types.file
import com.google.common.base.Stopwatch
import com.google.common.io.Files
Expand Down Expand Up @@ -58,12 +58,10 @@ class XstsCliTracegen :
.file(mustExist = true, canBeFile = false) // use the non-null value in traceDirPath!
val summary: Boolean by
option(help = "If this flag is present, a concretized summary is generated.")
.boolean()
.default(false)
.flag(default = false)
val traces: Boolean by
option(help = "If this flag is present, concretized traces are generated.")
.boolean()
.default(false)
.flag(default = false)

private fun toCexs(
summaryStateMap:
Expand Down Expand Up @@ -121,7 +119,9 @@ class XstsCliTracegen :

val concretizationResultTuple =
XstsTraceGenerationConcretizerUtil.concretizeTraceList(
traces as List<Trace<XstsState<ExplState>, XstsAction>>,
abstractSummary.sourceTraces.map {
it.toTrace() as Trace<XstsState<ExplState>, XstsAction>
},
Z3LegacySolverFactory.getInstance(),
xsts,
)
Expand Down

0 comments on commit ec1a632

Please sign in to comment.