From ebaf60d097861297c7fd19635f30f5ae1eaf4406 Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Thu, 16 Nov 2023 14:49:16 +0000 Subject: [PATCH] Reformatted code --- .../cfa/analysis/config/CfaConfigBuilder.java | 10 +-- .../java/hu/bme/mit/theta/cfa/cli/CfaCli.java | 76 +++++++++---------- .../analysis/algorithm/imc/ImcChecker.java | 42 +++++----- .../analysis/algorithm/kind/KIndChecker.java | 47 ++++++------ .../java/hu/bme/mit/theta/sts/cli/StsCli.java | 46 +++++------ .../theta/xcfa/analysis/XcfaTransFunc.java | 53 ++++++------- .../xcfa/analysis/por/XcfaToKindImc.java | 34 ++++----- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 27 ++++--- .../analysis/XstsToMonoliticTransFunc.java | 7 +- .../analysis/config/XstsConfigBuilder.java | 14 ++-- .../hu/bme/mit/theta/xsts/cli/XstsCli.java | 2 +- 11 files changed, 182 insertions(+), 176 deletions(-) diff --git a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java index faa1d607e5..ede462bf6c 100644 --- a/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java +++ b/subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java @@ -93,12 +93,12 @@ public class CfaConfigBuilder { - public enum Algorithm { - CEGAR, - KINDUCTION, + public enum Algorithm { + CEGAR, + KINDUCTION, IMC - } - + } + public enum Domain { EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT } 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 4fe11ee2b7..a08f631078 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 @@ -80,11 +80,11 @@ public class CfaCli { private static final String JAR_NAME = "theta-cfa-cli.jar"; private final String[] args; private final TableWriter writer; - @Parameter(names = {"--algorithm"}, description = "Algorithm") - Algorithm algorithm = Algorithm.CEGAR; + @Parameter(names = {"--algorithm"}, description = "Algorithm") + Algorithm algorithm = Algorithm.CEGAR; - @Parameter(names = "--domain", description = "Abstract domain") - Domain domain = Domain.PRED_CART; + @Parameter(names = "--domain", description = "Abstract domain") + Domain domain = Domain.PRED_CART; @Parameter(names = "--refinement", description = "Refinement strategy") Refinement refinement = Refinement.SEQ_ITP; @@ -236,7 +236,7 @@ private void run() { refinementSolverFactory = SolverManager.resolveSolverFactory(solver); } - final SafetyResult status; + final SafetyResult status; if (algorithm == Algorithm.CEGAR) { final CfaConfig configuration = buildConfiguration(cfa, errLoc, abstractionSolverFactory, refinementSolverFactory); status = check(configuration); @@ -254,18 +254,18 @@ private void run() { logger.write(Logger.Level.RESULT, "%s%n", status); sw.stop(); } else { - throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); - } - - printResult(status, sw.elapsed(TimeUnit.MILLISECONDS)); - if (status.isUnsafe() && cexfile != null) { - writeCex(status.asUnsafe()); - } - } catch (final Throwable ex) { - printError(ex); - System.exit(1); - } - } + throw new UnsupportedOperationException("Algorithm " + algorithm + " not supported"); + } + + printResult(status, sw.elapsed(TimeUnit.MILLISECONDS)); + if (status.isUnsafe() && cexfile != null) { + writeCex(status.asUnsafe()); + } + } catch (final Throwable ex) { + printError(ex); + System.exit(1); + } + } private void printHeader() { Stream.of("Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations", @@ -308,27 +308,27 @@ private CFA loadModel() throws Exception { } } - private void printResult(final SafetyResult status, final long totalTimeMs) { - final CegarStatistics stats = (CegarStatistics) - status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); - if (benchmarkMode) { - writer.cell(status.isSafe()); - writer.cell(totalTimeMs); - writer.cell(stats.getAlgorithmTimeMs()); - writer.cell(stats.getAbstractorTimeMs()); - writer.cell(stats.getRefinerTimeMs()); - writer.cell(stats.getIterations()); - writer.cell(status.getArg().size()); - writer.cell(status.getArg().getDepth()); - writer.cell(status.getArg().getMeanBranchingFactor()); - if (status.isUnsafe()) { - writer.cell(status.asUnsafe().getTrace().length() + ""); - } else { - writer.cell(""); - } - writer.newRow(); - } - } + private void printResult(final SafetyResult status, final long totalTimeMs) { + final CegarStatistics stats = (CegarStatistics) + status.getStats().orElse(new CegarStatistics(0, 0, 0, 0)); + if (benchmarkMode) { + writer.cell(status.isSafe()); + writer.cell(totalTimeMs); + writer.cell(stats.getAlgorithmTimeMs()); + writer.cell(stats.getAbstractorTimeMs()); + writer.cell(stats.getRefinerTimeMs()); + writer.cell(stats.getIterations()); + writer.cell(status.getArg().size()); + writer.cell(status.getArg().getDepth()); + writer.cell(status.getArg().getMeanBranchingFactor()); + if (status.isUnsafe()) { + writer.cell(status.asUnsafe().getTrace().length() + ""); + } else { + writer.cell(""); + } + writer.newRow(); + } + } private void printError(final Throwable ex) { final String message = ex.getMessage() == null ? "" : ex.getMessage(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/imc/ImcChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/imc/ImcChecker.java index 4b12770f5d..1f1fed7ccf 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/imc/ImcChecker.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/imc/ImcChecker.java @@ -1,4 +1,5 @@ package hu.bme.mit.theta.analysis.algorithm.imc; + import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.ARG; import hu.bme.mit.theta.analysis.algorithm.MonolithicTransFunc; @@ -27,7 +28,7 @@ import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.*; -public class ImcChecker implements SafetyChecker { +public class ImcChecker implements SafetyChecker { final Expr trans; final Expr init; final Expr prop; @@ -42,7 +43,7 @@ public class ImcChecker implements S public ImcChecker(MonolithicTransFunc transFunc, int upperBound, ItpSolver solver, - Function valToState, + Function valToState, Collection> vars, boolean interpolateForward1) { this.trans = transFunc.getTransExpr(); @@ -54,63 +55,62 @@ public ImcChecker(MonolithicTransFunc transFunc, this.offset = transFunc.getOffsetIndexing(); this.valToState = valToState; this.vars = vars; - interpolateForward =interpolateForward1; + interpolateForward = interpolateForward1; } - @Override public SafetyResult check(UnitPrec prec) { - int i=0; - var exprsFromStart=new ArrayList<>(List.of(PathUtils.unfold(init,VarIndexingFactory.indexing(0)))); + int i = 0; + var exprsFromStart = new ArrayList<>(List.of(PathUtils.unfold(init, VarIndexingFactory.indexing(0)))); var listOfIndexes = new ArrayList<>(List.of(firstIndexing)); final ItpMarker a = solver.createMarker(); final ItpMarker b = solver.createMarker(); final ItpPattern pattern = solver.createBinPattern(a, b); - while(i trace = Trace.of(List.of(initial), List.of()); - return SafetyResult.unsafe(trace,ARG.create(null)); + return SafetyResult.unsafe(trace, ARG.create(null)); } // reached fixed point - while(status.isUnsat()){ + while (status.isUnsat()) { var interpolant = solver.getInterpolant(pattern); - var itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), listOfIndexes.get(1)),listOfIndexes.get(0)); + var itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), listOfIndexes.get(1)), listOfIndexes.get(0)); solver.pop(); - try (var pps = new WithPushPop(solver)){ - solver.add(a,And(itpFormula,Not(img))); - if(solver.check().isUnsat()){ + try (var pps = new WithPushPop(solver)) { + solver.add(a, And(itpFormula, Not(img))); + if (solver.check().isUnsat()) { return SafetyResult.safe(ARG.create((state1, state2) -> false)); } } - img = Or(img,itpFormula); + img = Or(img, itpFormula); solver.push(); solver.add(a, And(itpFormula, exprsFromStart.get(1))); 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 27000b5853..8852e20c19 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 @@ -44,7 +44,7 @@ import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.Not; -public class KIndChecker implements SafetyChecker { +public class KIndChecker implements SafetyChecker { final Expr trans; final Expr init; final Expr prop; @@ -61,7 +61,7 @@ public KIndChecker(MonolithicTransFunc transFunc, int upperBound, Solver solver1, Solver solver2, - Function valToState, + Function valToState, Collection> vars) { this.trans = transFunc.getTransExpr(); this.init = transFunc.getInitExpr(); @@ -76,23 +76,22 @@ public KIndChecker(MonolithicTransFunc transFunc, } - @Override public SafetyResult check(UnitPrec prec) { //var trans = action.toExpr(); //var offset = action.nextIndexing(); - int i=0; + int i = 0; var currIndex = firstIndexing; - var exprsFromStart=new ArrayList>(); - var exprsForInductivity=new ArrayList>(); + var exprsFromStart = new ArrayList>(); + var exprsForInductivity = new ArrayList>(); var listOfIndexes = new ArrayList(); solver1.add(PathUtils.unfold(init, VarIndexingFactory.indexing(0))); // VarIndexingFactory.indexing(0)? - var eqList= new ArrayList>(); - while(i>(); + while (i < upperBound) { solver1.add(PathUtils.unfold(trans, currIndex)); @@ -125,30 +124,30 @@ public SafetyResult check(UnitPrec prec) { if (solver1.check().isUnsat()) { - return SafetyResult.safe(ARG.create(null)); - } + return SafetyResult.safe(ARG.create(null)); + } solver1.pop(); // Counterexample feasibility check - // I1 and T1-2 and T2-3 and ... and Tk-1-k + // I1 and T1-2 and T2-3 and ... and Tk-1-k - // Not Pk + // Not Pk solver1.push(); solver1.add(PathUtils.unfold(Not(prop), currIndex)); if (solver1.check().isSat()) { - S initial = null; - for (int j = 0; j < listOfIndexes.size(); j++) { - var valuation = PathUtils.extractValuation(solver1.getModel(), listOfIndexes.get(j), vars); - - S st = valToState.apply(valuation); - if(initial == null) - initial = st; - } - Trace trace = Trace.of(List.of(initial), List.of()); - return SafetyResult.unsafe(trace,ARG.create(null)); + S initial = null; + for (int j = 0; j < listOfIndexes.size(); j++) { + var valuation = PathUtils.extractValuation(solver1.getModel(), listOfIndexes.get(j), vars); + + S st = valToState.apply(valuation); + if (initial == null) + initial = st; } + Trace trace = Trace.of(List.of(initial), List.of()); + return SafetyResult.unsafe(trace, ARG.create(null)); + } solver1.pop(); @@ -161,8 +160,8 @@ public SafetyResult check(UnitPrec prec) { solver2.add(PathUtils.unfold(Not(prop), currIndex.sub(firstIndexing))); if (solver2.check().isUnsat()) { - return SafetyResult.safe(ARG.create(null)); - } + return SafetyResult.safe(ARG.create(null)); + } solver2.pop(); i++; } 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 a62a617f59..545c918474 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 @@ -77,18 +77,18 @@ public class StsCli { private final TableWriter writer; enum Algorithm { - CEGAR, - KINDUCTION, + CEGAR, + KINDUCTION, IMC - } + } - @Parameter(names = {"--domain"}, description = "Abstract domain") - Domain domain = Domain.PRED_CART; + @Parameter(names = {"--domain"}, description = "Abstract domain") + Domain domain = Domain.PRED_CART; @Parameter(names = {"--algorithm"}, description = "Algorithm") - Algorithm algorithm = Algorithm.CEGAR; + Algorithm algorithm = Algorithm.CEGAR; - @Parameter(names = {"--refinement"}, description = "Refinement strategy") + @Parameter(names = {"--refinement"}, description = "Refinement strategy") Refinement refinement = Refinement.SEQ_ITP; @Parameter(names = {"--search"}, description = "Search strategy") @@ -158,14 +158,14 @@ private void run() { return; } - try { - final Stopwatch sw = Stopwatch.createStarted(); - final STS sts = loadModel(); + try { + final Stopwatch sw = Stopwatch.createStarted(); + final STS sts = loadModel(); - SafetyResult status = null; + SafetyResult status = null; if (algorithm.equals(Algorithm.CEGAR)) { - final StsConfig configuration = buildConfiguration(sts); - status = check(configuration); + final StsConfig configuration = buildConfiguration(sts); + 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()); @@ -175,16 +175,16 @@ private void run() { var checker = new ImcChecker<>(transFunc, Integer.MAX_VALUE, Z3SolverFactory.getInstance().createItpSolver(), ExplState::of, sts.getVars(), true); status = checker.check(null); } - sw.stop(); - printResult(status, sts, sw.elapsed(TimeUnit.MILLISECONDS)); - if (status.isUnsafe() && cexfile != null) { - writeCex(sts, status.asUnsafe()); - } - } catch (final Throwable ex) { - printError(ex); - System.exit(1); - } - } + sw.stop(); + printResult(status, sts, sw.elapsed(TimeUnit.MILLISECONDS)); + if (status.isUnsafe() && cexfile != null) { + writeCex(sts, status.asUnsafe()); + } + } catch (final Throwable ex) { + printError(ex); + System.exit(1); + } + } private SafetyResult check(StsConfig configuration) throws Exception { try { diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaTransFunc.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaTransFunc.java index d9d5482b84..b97c978d31 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaTransFunc.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaTransFunc.java @@ -34,32 +34,33 @@ import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; public class XcfaTransFunc extends AbstractMonolithicTransFunc { - private XcfaTransFunc(XCFA xcfa){ - Preconditions.checkArgument(xcfa.getInitProcedures().size() == 1); - var proc = xcfa.getInitProcedures().stream().findFirst().orElse(null).getFirst(); - assert proc != null; - Preconditions.checkArgument(proc.getEdges().stream().map(UtilsKt::getFlatLabels).noneMatch(it -> it.stream().anyMatch(i -> !(i instanceof StmtLabel)))); - Preconditions.checkArgument(proc.getErrorLoc().isPresent()); - int i=0; - final Map map = new HashMap<>(); - for(var x : proc.getLocs()){ - map.put(x,i++); - } - 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(), - AssignStmt.of(locVar, Int(map.get(e.getTarget()))) - ))).collect(Collectors.toList()); - final var trans = NonDetStmt.of(tranList); - var transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)); - transExpr = And(transUnfold.getExprs()); - initExpr = Eq(locVar.getRef(), Int(map.get(proc.getInitLoc()))); - firstIndex = VarIndexingFactory.indexing(0); - offsetIndex = transUnfold.getIndexing(); - propExpr = Neq(locVar.getRef(), Int(map.get(proc.getErrorLoc().get()))); + private XcfaTransFunc(XCFA xcfa) { + Preconditions.checkArgument(xcfa.getInitProcedures().size() == 1); + var proc = xcfa.getInitProcedures().stream().findFirst().orElse(null).getFirst(); + assert proc != null; + Preconditions.checkArgument(proc.getEdges().stream().map(UtilsKt::getFlatLabels).noneMatch(it -> it.stream().anyMatch(i -> !(i instanceof StmtLabel)))); + Preconditions.checkArgument(proc.getErrorLoc().isPresent()); + int i = 0; + final Map map = new HashMap<>(); + for (var x : proc.getLocs()) { + map.put(x, i++); + } + 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(), + AssignStmt.of(locVar, Int(map.get(e.getTarget()))) + ))).collect(Collectors.toList()); + final var trans = NonDetStmt.of(tranList); + var transUnfold = StmtUtils.toExpr(trans, VarIndexingFactory.indexing(0)); + transExpr = And(transUnfold.getExprs()); + initExpr = Eq(locVar.getRef(), Int(map.get(proc.getInitLoc()))); + firstIndex = VarIndexingFactory.indexing(0); + offsetIndex = transUnfold.getIndexing(); + propExpr = Neq(locVar.getRef(), Int(map.get(proc.getErrorLoc().get()))); } - public static MonolithicTransFunc create(XCFA xcfa){ - return new XcfaTransFunc(xcfa); + + public static MonolithicTransFunc create(XCFA xcfa) { + return new XcfaTransFunc(xcfa); } } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaToKindImc.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaToKindImc.java index 6524b5b2ee..902f38c115 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaToKindImc.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaToKindImc.java @@ -48,30 +48,30 @@ import static hu.bme.mit.theta.core.type.inttype.IntExprs.Neq; public class XcfaToKindImc { - Expr transExpr; - Expr initExpr; - Expr propExpr; - int upperBound; - SolverFactory solverFactory1; - Set> vars; - StmtUnfoldResult transUnfold; - - - public XcfaToKindImc(XCFA xcfa,int bound,SolverFactory solverFactory) { + Expr transExpr; + Expr initExpr; + Expr propExpr; + int upperBound; + SolverFactory solverFactory1; + Set> vars; + StmtUnfoldResult transUnfold; + + + public XcfaToKindImc(XCFA xcfa, int bound, SolverFactory solverFactory) { Preconditions.checkArgument(xcfa.getInitProcedures().size() == 1); var proc = xcfa.getInitProcedures().stream().findFirst().orElse(null).getFirst(); assert proc != null; Preconditions.checkArgument(proc.getEdges().stream().map(UtilsKt::getFlatLabels).noneMatch(it -> it.stream().anyMatch(i -> !(i instanceof StmtLabel)))); Preconditions.checkArgument(proc.getErrorLoc().isPresent()); - int i=0; - final Map map = new HashMap<>(); - for(var x : proc.getLocs()){ - map.put(x,i++); + int i = 0; + final Map map = new HashMap<>(); + for (var x : proc.getLocs()) { + map.put(x, i++); } - 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())))), + 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(), AssignStmt.of(locVar, Int(map.get(e.getTarget()))) ))).collect(Collectors.toList()); 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 575473c4e8..ceef18a03e 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 @@ -83,13 +83,16 @@ class XcfaCli(private val args: Array) { //////////// CONFIGURATION OPTIONS BEGIN //////////// //////////// input task //////////// - public enum class Algorithm{ + 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 @@ -243,7 +246,7 @@ class XcfaCli(private val args: Array) { stopwatch.reset().start() - if(algorithm == Algorithm.CEGAR) { + 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) @@ -257,13 +260,13 @@ class XcfaCli(private val args: Array) { 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) - Strategy.SERVER_DEBUG -> runServerDebug(xcfa, config, logger, parseContext) - Strategy.PORTFOLIO -> runPortfolio(xcfa, explicitProperty, logger, parseContext, debug, - argdebug) - } + when (strategy) { + Strategy.DIRECT -> runDirect(xcfa, config, logger) + Strategy.SERVER -> runServer(xcfa, config, logger, parseContext, argdebug) + Strategy.SERVER_DEBUG -> runServerDebug(xcfa, config, logger, parseContext) + Strategy.PORTFOLIO -> runPortfolio(xcfa, explicitProperty, logger, parseContext, debug, + argdebug) + } // post verification postVerificationLogging(safetyResult, parseContext) logger.write(Logger.Level.RESULT, safetyResult.toString() + "\n") @@ -276,10 +279,12 @@ class XcfaCli(private val args: Array) { 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) + ImcChecker(transFunc, Int.MAX_VALUE, + getSolver(concretizerSolver, validateConcretizerSolver).createItpSolver(), ExplState::of, + ExprUtils.getVars(transFunc.transExpr), true) } val result = checker.check(null) - logger.write(Logger.Level.RESULT,result.toString() + "\n") + logger.write(Logger.Level.RESULT, result.toString() + "\n") } } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java index 37ec83a83c..72014fbf67 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsToMonoliticTransFunc.java @@ -23,9 +23,9 @@ import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; public class XstsToMonoliticTransFunc extends AbstractMonolithicTransFunc { - private XstsToMonoliticTransFunc(XSTS xsts){ + private XstsToMonoliticTransFunc(XSTS xsts) { final StmtUnfoldResult initUnfoldResult = StmtUtils.toExpr(xsts.getInit(), VarIndexingFactory.indexing(0)); - initExpr = And(And(initUnfoldResult.getExprs()), xsts.getInitFormula()); + initExpr = And(And(initUnfoldResult.getExprs()), xsts.getInitFormula()); firstIndex = initUnfoldResult.getIndexing(); final var envTran = Stmts.SequenceStmt(List.of(xsts.getEnv(), xsts.getTran())); final StmtUnfoldResult envTranUnfoldResult = StmtUtils.toExpr(envTran, VarIndexingFactory.indexing(0)); @@ -34,7 +34,8 @@ private XstsToMonoliticTransFunc(XSTS xsts){ propExpr = xsts.getProp(); } - public static MonolithicTransFunc create(XSTS xsts){ + + public static MonolithicTransFunc create(XSTS xsts) { return new XstsToMonoliticTransFunc(xsts); } } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java index f44c398a90..f1dba9edaf 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/config/XstsConfigBuilder.java @@ -93,15 +93,15 @@ public class XstsConfigBuilder { - public enum Algorithm { - CEGAR, - KINDUCTION, + public enum Algorithm { + CEGAR, + KINDUCTION, IMC - } + } - public enum Domain { - EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT, EXPL_PRED_BOOL, EXPL_PRED_CART, EXPL_PRED_SPLIT, EXPL_PRED_COMBINED - } + public enum Domain { + EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT, EXPL_PRED_BOOL, EXPL_PRED_CART, EXPL_PRED_SPLIT, EXPL_PRED_COMBINED + } public enum Refinement { FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE 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 b218239b5b..8036298b6a 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 @@ -82,7 +82,7 @@ public class XstsCli { private final TableWriter writer; @Parameter(names = {"--algorithm"}, description = "Algorithm") - Algorithm algorithm = Algorithm.CEGAR; + Algorithm algorithm = Algorithm.CEGAR; @Parameter(names = {"--domain"}, description = "Abstract domain") Domain domain = Domain.PRED_CART;