diff --git a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index a08f631078..96cf1df146 100644 --- a/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -243,7 +243,7 @@ private void run() { sw.stop(); } else if (algorithm == Algorithm.KINDUCTION) { var transFunc = CfaToMonoliticTransFunc.create(cfa); - var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, cfa.getVars()); + var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, cfa.getVars()); status = checker.check(null); logger.write(Logger.Level.RESULT, "%s%n", status); sw.stop(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java index 8852e20c19..f0153c5adc 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/kind/KIndChecker.java @@ -45,20 +45,24 @@ public class KIndChecker implements SafetyChecker { - final Expr trans; - final Expr init; - final Expr prop; - final int upperBound; - Solver solver1; - Solver solver2; - final VarIndexing firstIndexing; - final VarIndexing offset; - final Function valToState; - final Collection> vars; + private final Expr trans; + private final Expr init; + private final Expr prop; + private final int upperBound; + private final int inductionStartBound; + private final int inductionFrequency; + private Solver solver1; + private Solver solver2; + private final VarIndexing firstIndexing; + private final VarIndexing offset; + private final Function valToState; + private final Collection> vars; public KIndChecker(MonolithicTransFunc transFunc, int upperBound, + int inductionStartBound, + int inductionFrequency, Solver solver1, Solver solver2, Function valToState, @@ -67,6 +71,8 @@ public KIndChecker(MonolithicTransFunc transFunc, this.init = transFunc.getInitExpr(); this.prop = transFunc.getPropExpr(); this.upperBound = upperBound; + this.inductionStartBound = inductionStartBound; + this.inductionFrequency = inductionFrequency; this.solver1 = solver1; this.solver2 = solver2; this.firstIndexing = transFunc.getInitIndexing(); @@ -78,32 +84,24 @@ public KIndChecker(MonolithicTransFunc transFunc, @Override public SafetyResult check(UnitPrec prec) { - //var trans = action.toExpr(); - //var offset = action.nextIndexing(); - int i = 0; var currIndex = firstIndexing; - var exprsFromStart = new ArrayList>(); - var exprsForInductivity = new ArrayList>(); var listOfIndexes = new ArrayList(); - solver1.add(PathUtils.unfold(init, VarIndexingFactory.indexing(0))); // VarIndexingFactory.indexing(0)? + solver1.add(PathUtils.unfold(init, VarIndexingFactory.indexing(0))); var eqList = new ArrayList>(); while (i < upperBound) { solver1.add(PathUtils.unfold(trans, currIndex)); - // külső lista üres var finalList = new ArrayList>(); for (int j = 0; j < listOfIndexes.size(); j++) { - // új belső lista az adott indexű állapothoz var tempList = new ArrayList>(); for (var v : vars) { - // a mostani listához adom az Eq-et tempList.add(Eq(PathUtils.unfold(v.getRef(), currIndex), PathUtils.unfold(v.getRef(), listOfIndexes.get(j)))); } finalList.add(Not(And(tempList))); diff --git a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index 545c918474..c7c403c630 100644 --- a/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -168,7 +168,7 @@ private void run() { status = check(configuration); } else if (algorithm.equals(Algorithm.KINDUCTION)) { var transFunc = StsToMonoliticTransFunc.create(sts); - var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, sts.getVars()); + var checker = new KIndChecker<>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), ExplState::of, sts.getVars()); status = checker.check(null); } else if (algorithm.equals(Algorithm.IMC)) { var transFunc = StsToMonoliticTransFunc.create(sts); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java index d835166696..ea58eaf1c2 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaMonolithicTransFunc.java @@ -53,7 +53,7 @@ private XcfaMonolithicTransFunc(XCFA xcfa) { for (var x : proc.getLocs()) { map.put(x, i++); } - var locVar = Decls.Var("loc", Int()); + var locVar = Decls.Var("__loc_", Int()); List tranList = proc.getEdges().stream().map(e -> SequenceStmt.of(List.of( AssumeStmt.of(Eq(locVar.getRef(), Int(map.get(e.getSource())))), e.getLabel().toStmt(), diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt index e015dca75e..2d97ffed40 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt @@ -59,7 +59,8 @@ enum class InputType { enum class Backend { CEGAR, - BMC, + KIND, + IMC, LAZY } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index c15d022c54..b07acb428b 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -25,10 +25,7 @@ import com.google.gson.JsonParser import hu.bme.mit.theta.analysis.Trace import hu.bme.mit.theta.analysis.algorithm.SafetyResult import hu.bme.mit.theta.analysis.algorithm.debug.ARGWebDebugger -import hu.bme.mit.theta.analysis.algorithm.imc.ImcChecker -import hu.bme.mit.theta.analysis.algorithm.kind.KIndChecker import hu.bme.mit.theta.analysis.expl.ExplState -import hu.bme.mit.theta.analysis.expr.StmtAction import hu.bme.mit.theta.analysis.utils.ArgVisualizer import hu.bme.mit.theta.analysis.utils.TraceVisualizer import hu.bme.mit.theta.c2xcfa.getXcfaFromC @@ -39,7 +36,6 @@ import hu.bme.mit.theta.common.logging.UniqueWarningLogger import hu.bme.mit.theta.common.visualization.Graph import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter import hu.bme.mit.theta.common.visualization.writer.WebDebuggerLogger -import hu.bme.mit.theta.core.utils.ExprUtils import hu.bme.mit.theta.frontend.ParseContext import hu.bme.mit.theta.frontend.chc.ChcFrontend import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig @@ -48,7 +44,6 @@ import hu.bme.mit.theta.llvm2xcfa.XcfaUtils.fromFile import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager import hu.bme.mit.theta.xcfa.analysis.ErrorDetection import hu.bme.mit.theta.xcfa.analysis.XcfaAction -import hu.bme.mit.theta.xcfa.analysis.XcfaMonolithicTransFunc import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread @@ -83,16 +78,6 @@ class XcfaCli(private val args: Array) { //////////// CONFIGURATION OPTIONS BEGIN //////////// //////////// input task //////////// - public enum class Algorithm { - - CEGAR, - KINDUCTION, - IMC - } - - @Parameter(names = ["--algorithm"], description = "Algorithm") - var algorithm: Algorithm = Algorithm.CEGAR - @Parameter(names = ["--input"], description = "Path of the input C program", required = true) var input: File? = null @@ -168,6 +153,10 @@ class XcfaCli(private val args: Array) { @Parameter(names = ["--cex-solver"], description = "Concretizer solver name") var concretizerSolver: String = "Z3" + @Parameter(names = ["--validate-cex-solver"], + description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.") + var validateConcretizerSolver: Boolean = false + @Parameter(names = ["--to-c-use-arrays"]) var useArr: Boolean = false @@ -177,10 +166,6 @@ class XcfaCli(private val args: Array) { @Parameter(names = ["--to-c-use-ranges"]) var useRange: Boolean = false - @Parameter(names = ["--validate-cex-solver"], - description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.") - var validateConcretizerSolver: Boolean = false - @Parameter(names = ["--seed"], description = "Random seed used for DPOR") var randomSeed: Int = -1 @@ -245,21 +230,21 @@ class XcfaCli(private val args: Array) { // verification stopwatch.reset().start() + val safetyResult: SafetyResult<*, *> = + if (backend == Backend.CEGAR) { + logger.write(Logger.Level.INFO, + "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using $backend\n") + registerAllSolverManagers(solverHome, logger) + logger.write(Logger.Level.INFO, + "Registered solver managers successfully (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") + stopwatch.reset().start() + val config = parseCEGARConfigFromCli(parseContext) + if (strategy != Strategy.PORTFOLIO && printConfigFile != null) { + printConfigFile!!.writeText(gsonForOutput.toJson(config)) + } + logger.write(Logger.Level.INFO, "Parsed config (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") + stopwatch.reset().start() - if (algorithm == Algorithm.CEGAR) { - logger.write(Logger.Level.INFO, - "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using $backend\n") - registerAllSolverManagers(solverHome, logger) - logger.write(Logger.Level.INFO, - "Registered solver managers successfully (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") - stopwatch.reset().start() - val config = parseConfigFromCli(parseContext) - if (strategy != Strategy.PORTFOLIO && printConfigFile != null) { - printConfigFile!!.writeText(gsonForOutput.toJson(config)) - } - logger.write(Logger.Level.INFO, "Parsed config (in ${stopwatch.elapsed(TimeUnit.MILLISECONDS)} ms)\n") - stopwatch.reset().start() - val safetyResult: SafetyResult<*, *> = when (strategy) { Strategy.DIRECT -> runDirect(xcfa, config, logger) Strategy.SERVER -> runServer(xcfa, config, logger, parseContext, argdebug) @@ -267,25 +252,22 @@ class XcfaCli(private val args: Array) { Strategy.PORTFOLIO -> runPortfolio(xcfa, explicitProperty, logger, parseContext, debug, argdebug) } - // post verification - postVerificationLogging(safetyResult, parseContext) - logger.write(Logger.Level.RESULT, safetyResult.toString() + "\n") - } else { - val transFunc = XcfaMonolithicTransFunc.create(xcfa) - registerAllSolverManagers(solverHome, logger) - val checker = if (algorithm == Algorithm.KINDUCTION) { - KIndChecker(transFunc, Int.MAX_VALUE, - getSolver(concretizerSolver, validateConcretizerSolver).createSolver(), - getSolver(concretizerSolver, validateConcretizerSolver).createSolver(), ExplState::of, - ExprUtils.getVars(transFunc.transExpr)) } else { - ImcChecker(transFunc, Int.MAX_VALUE, - getSolver(concretizerSolver, validateConcretizerSolver).createItpSolver(), ExplState::of, - ExprUtils.getVars(transFunc.transExpr), true) + registerAllSolverManagers(solverHome, logger) + val checker = if (backend == Backend.KIND) { + val kindConfig = parseKindConfigFromCli() + kindConfig.getKindChecker(xcfa) + } else if (backend == Backend.IMC) { + val kindConfig = parseIMCConfigFromCli() + kindConfig.getIMCChecker(xcfa) + } else { + error("Backend $backend not supported") + } + checker.check(null) } - val result = checker.check(null) - logger.write(Logger.Level.RESULT, result.toString() + "\n") - } + // post verification + postVerificationLogging(safetyResult, parseContext) + logger.write(Logger.Level.RESULT, safetyResult.toString() + "\n") } private fun runDirect(xcfa: XCFA, config: XcfaCegarConfig, logger: ConsoleLogger) = @@ -534,7 +516,35 @@ class XcfaCli(private val args: Array) { } } else ErrorDetection.ERROR_LOCATION - private fun parseConfigFromCli(parseContext: ParseContext): XcfaCegarConfig { + private fun parseIMCConfigFromCli(): XcfaImcConfig { + val imcConfig = XcfaImcConfig() + try { + JCommander.newBuilder().addObject(imcConfig).programName(JAR_NAME).build() + .parse(*remainingFlags.toTypedArray()) + } catch (ex: ParameterException) { + println("Invalid parameters, details:") + ex.printStackTrace() + ex.usage() + exitProcess(ExitCodes.INVALID_PARAM.code) + } + return imcConfig + } + + private fun parseKindConfigFromCli(): XcfaKindConfig { + val kindConfig = XcfaKindConfig() + try { + JCommander.newBuilder().addObject(kindConfig).programName(JAR_NAME).build() + .parse(*remainingFlags.toTypedArray()) + } catch (ex: ParameterException) { + println("Invalid parameters, details:") + ex.printStackTrace() + ex.usage() + exitProcess(ExitCodes.INVALID_PARAM.code) + } + return kindConfig + } + + private fun parseCEGARConfigFromCli(parseContext: ParseContext): XcfaCegarConfig { val cegarConfig = XcfaCegarConfig() try { JCommander.newBuilder().addObject(cegarConfig).programName(JAR_NAME).build() diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaImcConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaImcConfig.kt new file mode 100644 index 0000000000..c286cf6b15 --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaImcConfig.kt @@ -0,0 +1,50 @@ +/* + * Copyright 2023 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.xcfa.cli + +import com.beust.jcommander.Parameter +import hu.bme.mit.theta.analysis.algorithm.imc.ImcChecker +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.analysis.expr.StmtAction +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.xcfa.analysis.XcfaMonolithicTransFunc +import hu.bme.mit.theta.xcfa.model.XCFA + +data class XcfaImcConfig( + @Parameter(names = ["--imc-solver"], description = "BMC solver name") + var imcSolver: String = "Z3", + @Parameter(names = ["--validate-imc-solver"], + description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.") + var validateIMCSolver: Boolean = false, + @Parameter(names = ["--max-bound"], + description = "How many successors to enumerate in a transition. Only relevant to the explicit domain. Use 0 for no limit.") + var maxBound: Int = Int.MAX_VALUE, +) { + + fun getIMCChecker(xcfa: XCFA): ImcChecker { + val transFunc = XcfaMonolithicTransFunc.create(xcfa) + return ImcChecker( + transFunc, + maxBound, + getSolver(imcSolver, validateIMCSolver).createItpSolver(), + ExplState::of, + ExprUtils.getVars(transFunc.transExpr), + true) + } + +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaKindConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaKindConfig.kt new file mode 100644 index 0000000000..2882b05281 --- /dev/null +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaKindConfig.kt @@ -0,0 +1,63 @@ +/* + * Copyright 2023 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. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.xcfa.cli + +import com.beust.jcommander.Parameter +import hu.bme.mit.theta.analysis.algorithm.kind.KIndChecker +import hu.bme.mit.theta.analysis.expl.ExplState +import hu.bme.mit.theta.analysis.expr.ExprAction +import hu.bme.mit.theta.analysis.expr.ExprState +import hu.bme.mit.theta.core.utils.ExprUtils +import hu.bme.mit.theta.xcfa.analysis.XcfaMonolithicTransFunc +import hu.bme.mit.theta.xcfa.model.XCFA + +data class XcfaKindConfig( + @Parameter(names = ["--bmc-solver"], description = "BMC solver name") + var bmcSolver: String = "Z3", + @Parameter(names = ["--validate-bmc-solver"], + description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.") + var validateBMCSolver: Boolean = false, + @Parameter(names = ["--induction-solver"], description = "Induction solver name") + var indSolver: String = "Z3", + @Parameter(names = ["--validate-induction-solver"], + description = "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.") + var validateIndSolver: Boolean = false, + @Parameter(names = ["--max-bound"], + description = "How many successors to enumerate in a transition. Only relevant to the explicit domain. Use 0 for no limit.") + var maxBound: Int = Int.MAX_VALUE, + @Parameter(names = ["--ind-min-bound"], + description = "Start induction after reaching this bound") + var indMinBound: Int = 0, + @Parameter(names = ["--ind-frequency"], + description = "Frequency of induction check") + var indFreq: Int = 1, +) { + + fun getKindChecker(xcfa: XCFA): KIndChecker { + val transFunc = XcfaMonolithicTransFunc.create(xcfa) + return KIndChecker( + transFunc, + maxBound, + indMinBound, + indFreq, + getSolver(bmcSolver, validateBMCSolver).createSolver(), + getSolver(indSolver, validateIndSolver).createSolver(), + ExplState::of, + ExprUtils.getVars(transFunc.transExpr)) + } + +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt index 9c462bfb24..0de0b7ba98 100644 --- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt +++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt @@ -163,4 +163,18 @@ class XcfaCliVerifyTest { )) } + @ParameterizedTest + @MethodSource("cFiles") + fun testCVerifyKind(filePath: String, extraArgs: String?) { + val params = arrayOf( + "--algorithm", "KINDUCTION", + "--input-type", "C", + "--input", javaClass.getResource(filePath)!!.path, + "--stacktrace", + *(extraArgs?.split(" ")?.toTypedArray() ?: emptyArray()), + "--debug" + ) + main(params) + } + } diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java index 8036298b6a..d9703729b9 100644 --- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java +++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java @@ -205,7 +205,7 @@ private void run() { sw.stop(); } else if (algorithm.equals(Algorithm.KINDUCTION)) { var transFunc = XstsToMonoliticTransFunc.create(xsts); - var checker = new KIndChecker, XstsAction>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), (x) -> XstsState.of(ExplState.of(x), false, true), xsts.getVars()); + var checker = new KIndChecker, XstsAction>(transFunc, Integer.MAX_VALUE, inductionStartBound, inductionFrequency, Z3SolverFactory.getInstance().createSolver(), Z3SolverFactory.getInstance().createSolver(), (x) -> XstsState.of(ExplState.of(x), false, true), xsts.getVars()); status = checker.check(null); logger.write(Logger.Level.RESULT, "%s%n", status); sw.stop();