From 56aa34038060f6e25a761a814085f0f2df906079 Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 29 Sep 2025 11:18:57 +0200 Subject: [PATCH 1/5] Implement hashCode and equals methods in IdentityNextStateDescriptor --- .../ansd/impl/IdentityNextStateDescriptor.java | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java index d617534b1c2..dcf86265f2e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java @@ -19,6 +19,7 @@ import hu.bme.mit.delta.collections.UniqueTable; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.StateSpaceInfo; +import java.util.Objects; import java.util.Optional; public final class IdentityNextStateDescriptor implements AbstractNextStateDescriptor { @@ -67,4 +68,18 @@ public Optional> split() { public boolean evaluate() { return true; } + + @Override + public int hashCode() { + return Objects.hash(getClass(), child); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) return true; + if (obj instanceof IdentityNextStateDescriptor that) { + return Objects.equals(this.child, that.child); + } + return false; + } } From b06b7258f20afaf77fffabe7e1e4173909aeeecc Mon Sep 17 00:00:00 2001 From: mondokm Date: Sat, 29 Nov 2025 16:01:34 +0100 Subject: [PATCH 2/5] Implement prototype checkin for identity descriptors --- .../analysis/algorithm/mdd/MddChecker.kt | 2 +- .../impl/IdentityNextStateDescriptor.java | 73 ++++++++++++------- 2 files changed, 49 insertions(+), 26 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt index a5d1a7a50d5..3574ea4bc92 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.kt @@ -122,7 +122,7 @@ constructor( val transNodes = mutableListOf() val descriptors = mutableListOf() - for (expr in listOf(monolithicExpr.transExpr)) { + for (expr in monolithicExpr.split) { val transExpr = And(PathUtils.unfold(expr, VarIndexingFactory.indexing(0)), And(identityExprs)) val transitionNode = diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java index dcf86265f2e..41bf5e42d8e 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/ansd/impl/IdentityNextStateDescriptor.java @@ -16,51 +16,62 @@ package hu.bme.mit.theta.analysis.algorithm.mdd.ansd.impl; import hu.bme.mit.delta.collections.IntObjMapView; -import hu.bme.mit.delta.collections.UniqueTable; +import hu.bme.mit.delta.collections.PrototypedUniqueTable; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.AbstractNextStateDescriptor; import hu.bme.mit.theta.analysis.algorithm.mdd.ansd.StateSpaceInfo; import java.util.Objects; import java.util.Optional; public final class IdentityNextStateDescriptor implements AbstractNextStateDescriptor { - private static final UniqueTable uniqueTable = - UniqueTable.newInstance(); + private final AbstractNextStateDescriptor child; + private final int cachedHash; + + private static final PrototypedUniqueTable UNIQUE_TABLE = + PrototypedUniqueTable.newInstance(); public static final AbstractNextStateDescriptor TERMINAL_IDENTITY = new IdentityNextStateDescriptor(); - public static AbstractNextStateDescriptor withChild(AbstractNextStateDescriptor child) { - return uniqueTable.checkIn(new IdentityNextStateDescriptor(child)); + public static AbstractNextStateDescriptor withChild(final AbstractNextStateDescriptor child) { + final Template proto = new Template(child); + return UNIQUE_TABLE.checkIn(proto, t -> new IdentityNextStateDescriptor(t.child)); } - private final AbstractNextStateDescriptor child; + private IdentityNextStateDescriptor() { + this.child = this; + this.cachedHash = Objects.hashCode(child); + } - private IdentityNextStateDescriptor(AbstractNextStateDescriptor child) { + private IdentityNextStateDescriptor(final AbstractNextStateDescriptor child) { this.child = child; - // TODO cache hashcode + this.cachedHash = Objects.hashCode(child); } - private IdentityNextStateDescriptor() { - this.child = this; + @Override + public boolean equals(final Object obj) { + return this == obj; + } + + @Override + public int hashCode() { + return cachedHash; } @Override - public IntObjMapView getDiagonal(StateSpaceInfo localStateSpace) { - // TODO: cache this instead of creating on demand + public IntObjMapView getDiagonal( + final StateSpaceInfo localStateSpace) { return IntObjMapView.empty(child); } @Override public IntObjMapView> getOffDiagonal( - StateSpaceInfo localStateSpace) { - // TODO: cache this instead of creating on demand + final StateSpaceInfo localStateSpace) { return IntObjMapView.empty( IntObjMapView.empty(AbstractNextStateDescriptor.terminalEmpty())); } @Override public Optional> split() { - // TODO: this might be a performance overhead return Optional.empty(); } @@ -69,17 +80,29 @@ public boolean evaluate() { return true; } - @Override - public int hashCode() { - return Objects.hash(getClass(), child); - } + private static final class Template { - @Override - public boolean equals(Object obj) { - if (this == obj) return true; - if (obj instanceof IdentityNextStateDescriptor that) { - return Objects.equals(this.child, that.child); + private final AbstractNextStateDescriptor child; + + private Template(final AbstractNextStateDescriptor child) { + this.child = child; + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) return true; + if (obj instanceof Template other) { + return Objects.equals(this.child, other.child); + } + if (obj instanceof IdentityNextStateDescriptor descriptor) { + return Objects.equals(this.child, descriptor.child); + } + return false; + } + + @Override + public int hashCode() { + return Objects.hashCode(child); } - return false; } } From c8ac33246a6cc6b5f2f40077654728a30dfca13c Mon Sep 17 00:00:00 2001 From: mondokm Date: Sat, 29 Nov 2025 16:44:27 +0100 Subject: [PATCH 3/5] Use caching for sat check in ExpressionTemplates --- .../mdd/expressionnode/MddExpressionTemplate.java | 14 ++++++++++---- .../passes/XstsStmtFlatteningTransformer.kt | 5 +++-- .../bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt | 4 ++-- .../mit/theta/xsts/cli/optiongroup/InputOptions.kt | 1 - 4 files changed, 15 insertions(+), 9 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java index d0ebf48b9f7..8f6bc4d5bcf 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java @@ -21,10 +21,7 @@ import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; import hu.bme.mit.delta.collections.RecursiveIntObjMapView; -import hu.bme.mit.delta.java.mdd.MddCanonizationStrategy; -import hu.bme.mit.delta.java.mdd.MddGraph; -import hu.bme.mit.delta.java.mdd.MddNode; -import hu.bme.mit.delta.java.mdd.MddVariable; +import hu.bme.mit.delta.java.mdd.*; import hu.bme.mit.theta.analysis.algorithm.mdd.identitynode.IdentityRepresentation; import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.IndexedConstDecl; @@ -33,8 +30,10 @@ import hu.bme.mit.theta.core.model.ExprSubstitution; import hu.bme.mit.theta.core.model.Substitution; import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.AndExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.booltype.FalseExpr; +import hu.bme.mit.theta.core.type.booltype.OrExpr; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.SolverPool; @@ -50,13 +49,20 @@ public class MddExpressionTemplate implements MddNode.Template { private static Solver lazySolver; + private static UnaryOperationCache, Boolean> satCache = new UnaryOperationCache(); + private static boolean isSat(Expr expr, SolverPool solverPool) { + Boolean cached = satCache.getOrNull(expr); + if (cached != null) { + return cached; + } if (lazySolver == null) lazySolver = solverPool.requestSolver(); boolean res; try (var wpp = new WithPushPop(lazySolver)) { lazySolver.add(expr); res = lazySolver.check().isSat(); } + satCache.addToCache(expr, res); return res; } diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt index 8c50c9bd2c8..9bf1f4ed857 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt @@ -18,6 +18,7 @@ package hu.bme.mit.theta.xsts.analysis.passes import hu.bme.mit.theta.analysis.algorithm.mdd.varordering.Event import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.stmt.* +import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not import hu.bme.mit.theta.core.utils.StmtUtils import hu.bme.mit.theta.xsts.XSTS @@ -85,8 +86,8 @@ object XstsStmtFlatteningTransformer { } is IfStmt -> { - flattenStmts(stmt.then, maxDepth, currentDepth + 1) + - flattenStmts(stmt.elze, maxDepth, currentDepth + 1) + flattenStmts(SequenceStmt.of(listOf(AssumeStmt.of(stmt.cond), stmt.then)), maxDepth, currentDepth + 1) + + flattenStmts(SequenceStmt.of(listOf(AssumeStmt.of(Not(stmt.cond)), stmt.elze)), maxDepth, currentDepth + 1) } else -> { 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 index ded6557ebf1..3d379d2dcc4 100644 --- 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 @@ -98,8 +98,8 @@ abstract class XstsCliBaseCommand(name: String? = null, help: String = "") : val concreteTrace = XstsTraceConcretizerUtil.concretize(trace, SolverManager.resolveSolverFactory(solver), xsts) val outputFile: File = outputOptions.cexfile!! - if (!outputFile.parentFile.exists()) { - outputFile.parentFile.mkdir() + outputFile.parentFile?.let { parent -> + if (!parent.exists()) parent.mkdirs() } PrintWriter(outputFile).use { printWriter -> printWriter.write(concreteTrace.toString()) } } diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt index 37add255600..899b4c30131 100644 --- a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt +++ b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/optiongroup/InputOptions.kt @@ -62,7 +62,6 @@ class InputOptions : fun isPnml() = model.path.endsWith("pnml") fun loadXsts(): XSTS { - if(flattenDepth != 0) throw UnsupportedOperationException("XSTS flattening is incorrect, don't use it for now! (--flatten-depth must be 0)") val propertyStream = if (property != null) property else From f7c2bad04863857a452f79a55635f603def4136c Mon Sep 17 00:00:00 2001 From: mondokm Date: Sat, 29 Nov 2025 17:06:43 +0100 Subject: [PATCH 4/5] Do not check satisfiability when caching models --- .../MddExpressionRepresentation.java | 2 +- .../expressionnode/MddExpressionTemplate.java | 24 ++++++++++++------- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java index 2e8f2b5f593..e2db6cce557 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionRepresentation.java @@ -596,7 +596,7 @@ private void cacheModel(Valuation valuation) { representation.mddVariable.getLower(); if (lower.isPresent()) { final MddExpressionTemplate template = - MddExpressionTemplate.of( + MddExpressionTemplate.ofKnownSat( substitutedExpr, o -> (Decl) o, representation.solverPool, diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java index 8f6bc4d5bcf..9cf7b1e9296 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java @@ -30,10 +30,8 @@ import hu.bme.mit.theta.core.model.ExprSubstitution; import hu.bme.mit.theta.core.model.Substitution; import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.AndExpr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.booltype.FalseExpr; -import hu.bme.mit.theta.core.type.booltype.OrExpr; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.solver.Solver; import hu.bme.mit.theta.solver.SolverPool; @@ -46,6 +44,7 @@ public class MddExpressionTemplate implements MddNode.Template { private final Function extractDecl; private final SolverPool solverPool; private final boolean transExpr; + private final boolean knownSat; private static Solver lazySolver; @@ -70,24 +69,31 @@ private MddExpressionTemplate( Expr expr, Function extractDecl, SolverPool solverPool, - boolean transExpr) { + boolean transExpr, + boolean knownSat) { this.expr = expr; this.extractDecl = extractDecl; this.solverPool = solverPool; this.transExpr = transExpr; + this.knownSat = knownSat; } public static MddExpressionTemplate of( Expr expr, Function extractDecl, SolverPool solverPool) { - return new MddExpressionTemplate(expr, extractDecl, solverPool, false); + return new MddExpressionTemplate(expr, extractDecl, solverPool, false, false); } public static MddExpressionTemplate of( + Expr expr, Function extractDecl, SolverPool solverPool, boolean transExpr) { + return new MddExpressionTemplate(expr, extractDecl, solverPool, transExpr, false); + } + + public static MddExpressionTemplate ofKnownSat( Expr expr, Function extractDecl, SolverPool solverPool, boolean transExpr) { - return new MddExpressionTemplate(expr, extractDecl, solverPool, transExpr); + return new MddExpressionTemplate(expr, extractDecl, solverPool, transExpr, true); } @Override @@ -110,7 +116,7 @@ public RecursiveIntObjMapView toCanonicalRepresentation( // } // Check if terminal 0 - if (canonizedExpr instanceof FalseExpr || !isSat(canonizedExpr, solverPool)) { + if (!knownSat && (canonizedExpr instanceof FalseExpr || !isSat(canonizedExpr, solverPool))) { return null; } @@ -128,7 +134,8 @@ public RecursiveIntObjMapView toCanonicalRepresentation( canonizedExpr, o -> (Decl) o, solverPool, - transExpr)); + transExpr, + knownSat)); } else { final MddGraph mddGraph = (MddGraph) mddVariable.getMddGraph(); childNode = mddGraph.getNodeFor(canonizedExpr); @@ -194,7 +201,8 @@ public RecursiveIntObjMapView toCanonicalRepresentation( overApproxExpr, extractDecl, solverPool, - transExpr)); + transExpr, + knownSat)); } else { final MddGraph mddGraph = (MddGraph) mddVariable.getMddGraph(); cont = mddGraph.getNodeFor(overApproxExpr); From 41ad045252850486f29257d3111ccd5c6886335a Mon Sep 17 00:00:00 2001 From: mondokm Date: Sat, 29 Nov 2025 17:07:58 +0100 Subject: [PATCH 5/5] Bump version, fix formatting --- build.gradle.kts | 2 +- .../mdd/expressionnode/MddExpressionTemplate.java | 11 ++++++++--- .../analysis/passes/XstsStmtFlatteningTransformer.kt | 12 ++++++++++-- .../hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt | 4 +--- 4 files changed, 20 insertions(+), 9 deletions(-) diff --git a/build.gradle.kts b/build.gradle.kts index c5ebc3f4aa9..b7080e3c4e8 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -36,7 +36,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.27.5" + version = "6.27.7" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java index 9cf7b1e9296..73ba9d9c3ed 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/MddExpressionTemplate.java @@ -48,7 +48,8 @@ public class MddExpressionTemplate implements MddNode.Template { private static Solver lazySolver; - private static UnaryOperationCache, Boolean> satCache = new UnaryOperationCache(); + private static UnaryOperationCache, Boolean> satCache = + new UnaryOperationCache(); private static boolean isSat(Expr expr, SolverPool solverPool) { Boolean cached = satCache.getOrNull(expr); @@ -84,7 +85,10 @@ public static MddExpressionTemplate of( } public static MddExpressionTemplate of( - Expr expr, Function extractDecl, SolverPool solverPool, boolean transExpr) { + Expr expr, + Function extractDecl, + SolverPool solverPool, + boolean transExpr) { return new MddExpressionTemplate(expr, extractDecl, solverPool, transExpr, false); } @@ -116,7 +120,8 @@ public RecursiveIntObjMapView toCanonicalRepresentation( // } // Check if terminal 0 - if (!knownSat && (canonizedExpr instanceof FalseExpr || !isSat(canonizedExpr, solverPool))) { + if (!knownSat + && (canonizedExpr instanceof FalseExpr || !isSat(canonizedExpr, solverPool))) { return null; } diff --git a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt index 9bf1f4ed857..894105d50f6 100644 --- a/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt +++ b/subprojects/xsts/xsts-analysis/src/main/kotlin/hu/bme/mit/theta/xsts/analysis/passes/XstsStmtFlatteningTransformer.kt @@ -86,8 +86,16 @@ object XstsStmtFlatteningTransformer { } is IfStmt -> { - flattenStmts(SequenceStmt.of(listOf(AssumeStmt.of(stmt.cond), stmt.then)), maxDepth, currentDepth + 1) + - flattenStmts(SequenceStmt.of(listOf(AssumeStmt.of(Not(stmt.cond)), stmt.elze)), maxDepth, currentDepth + 1) + flattenStmts( + SequenceStmt.of(listOf(AssumeStmt.of(stmt.cond), stmt.then)), + maxDepth, + currentDepth + 1, + ) + + flattenStmts( + SequenceStmt.of(listOf(AssumeStmt.of(Not(stmt.cond)), stmt.elze)), + maxDepth, + currentDepth + 1, + ) } else -> { 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 index 3d379d2dcc4..0fe898a3f0c 100644 --- 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 @@ -98,9 +98,7 @@ abstract class XstsCliBaseCommand(name: String? = null, help: String = "") : val concreteTrace = XstsTraceConcretizerUtil.concretize(trace, SolverManager.resolveSolverFactory(solver), xsts) val outputFile: File = outputOptions.cexfile!! - outputFile.parentFile?.let { parent -> - if (!parent.exists()) parent.mkdirs() - } + outputFile.parentFile?.let { parent -> if (!parent.exists()) parent.mkdirs() } PrintWriter(outputFile).use { printWriter -> printWriter.write(concreteTrace.toString()) } } }