diff --git a/build.gradle.kts b/build.gradle.kts index a635a2dbb3..f09e18beac 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "1.2.1" + version = "1.3.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java index f6ae407482..4eede1fe9f 100644 --- a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java @@ -150,7 +150,14 @@ public void prune(final ArgNode node) { } node.descendants().forEach(ArgNode::unsetCoveringNode); node.descendants().forEach(ArgNode::clearCoveredNodes); + } + /** + * Prune the whole ARG, making it uninitialized. + */ + public void pruneAll() { + initNodes.clear(); + this.initialized = false; } public void minimize() { diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java index 49df31100e..139c1ef4dd 100644 --- a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java @@ -38,19 +38,22 @@ public class MultiExprTraceRefiner exprTraceChecker; private final PrecRefiner precRefiner; + private final PruneStrategy pruneStrategy; private final Logger logger; - private MultiExprTraceRefiner(final ExprTraceChecker exprTraceChecker, final PrecRefiner precRefiner, - final Logger logger) { + private MultiExprTraceRefiner(final ExprTraceChecker exprTraceChecker, + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, final Logger logger) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); + this.pruneStrategy = checkNotNull(pruneStrategy); this.logger = checkNotNull(logger); } public static MultiExprTraceRefiner create( final ExprTraceChecker exprTraceChecker, final PrecRefiner precRefiner, - final Logger logger) { - return new MultiExprTraceRefiner<>(exprTraceChecker, precRefiner, logger); + final PruneStrategy pruneStrategy, final Logger logger) { + return new MultiExprTraceRefiner<>(exprTraceChecker, precRefiner, pruneStrategy, logger); } @Override @@ -111,11 +114,21 @@ public RefinerResult refine(final ARG arg, final P prec) { refinedPrec = precRefiner.refine(refinedPrec, traces.get(i), refutations.get(i)); } } - logger.write(Level.SUBSTEP, "| | Pruning..."); - for (int i = 0; i < nodesToPrune.size(); ++i) { - if (!skip.get(i)) { - arg.prune(nodesToPrune.get(i)); - } + switch (pruneStrategy){ + case LAZY: + logger.write(Level.SUBSTEP, "| | Pruning (lazy)..."); + for (int i = 0; i < nodesToPrune.size(); ++i) { + if (!skip.get(i)) { + arg.prune(nodesToPrune.get(i)); + } + } + break; + case FULL: + logger.write(Level.SUBSTEP, "| | Pruning (full)..."); + arg.pruneAll(); + break; + default: + throw new UnsupportedOperationException("Unsupported pruning strategy"); } logger.write(Level.SUBSTEP, "done%n"); return RefinerResult.spurious(refinedPrec); diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/PruneStrategy.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/PruneStrategy.java new file mode 100644 index 0000000000..2686edede6 --- /dev/null +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/PruneStrategy.java @@ -0,0 +1,5 @@ +package hu.bme.mit.theta.analysis.expr.refinement; + +public enum PruneStrategy { + LAZY, FULL +} diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java index f8edf4dfe6..32f4118498 100644 --- a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java @@ -39,19 +39,22 @@ public final class SingleExprTraceRefiner exprTraceChecker; private final PrecRefiner precRefiner; + private final PruneStrategy pruneStrategy; private final Logger logger; private SingleExprTraceRefiner(final ExprTraceChecker exprTraceChecker, - final PrecRefiner precRefiner, final Logger logger) { + final PrecRefiner precRefiner, + final PruneStrategy pruneStrategy, final Logger logger) { this.exprTraceChecker = checkNotNull(exprTraceChecker); this.precRefiner = checkNotNull(precRefiner); + this.pruneStrategy = checkNotNull(pruneStrategy); this.logger = checkNotNull(logger); } public static SingleExprTraceRefiner create( final ExprTraceChecker exprTraceChecker, final PrecRefiner precRefiner, - final Logger logger) { - return new SingleExprTraceRefiner<>(exprTraceChecker, precRefiner, logger); + final PruneStrategy pruneStrategy, final Logger logger) { + return new SingleExprTraceRefiner<>(exprTraceChecker, precRefiner, pruneStrategy, logger); } @Override @@ -81,9 +84,19 @@ public RefinerResult refine(final ARG arg, final P prec) { assert 0 <= pruneIndex : "Pruning index must be non-negative"; assert pruneIndex <= cexToConcretize.length() : "Pruning index larger than cex length"; - logger.write(Level.SUBSTEP, "| | Pruning from index %d...", pruneIndex); - final ArgNode nodeToPrune = cexToConcretize.node(pruneIndex); - arg.prune(nodeToPrune); + switch (pruneStrategy){ + case LAZY: + logger.write(Level.SUBSTEP, "| | Pruning from index %d...", pruneIndex); + final ArgNode nodeToPrune = cexToConcretize.node(pruneIndex); + arg.prune(nodeToPrune); + break; + case FULL: + logger.write(Level.SUBSTEP, "| | Pruning whole ARG", pruneIndex); + arg.pruneAll(); + break; + default: + throw new UnsupportedOperationException("Unsupported pruning strategy"); + } logger.write(Level.SUBSTEP, "done%n"); return RefinerResult.spurious(refinedPrec); diff --git a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java index d21a32f8f0..9838cae1f5 100644 --- a/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java +++ b/subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java @@ -69,14 +69,10 @@ public enum Domain { EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT } - ; - public enum Refinement { FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE } - ; - public enum Search { BFS { @Override @@ -103,8 +99,6 @@ public ArgNodeComparator getComp(final CFA cfa) { } - ; - public enum PredSplit { WHOLE(ExprSplitters.whole()), @@ -119,8 +113,6 @@ private PredSplit(final ExprSplitter splitter) { } } - ; - public enum PrecGranularity { GLOBAL { @Override @@ -154,8 +146,6 @@ public abstract refToPrec); } - ; - public enum Encoding { SBE { @Override @@ -174,8 +164,6 @@ public CfaLts getLts() { public abstract CfaLts getLts(); } - ; - public enum InitPrec { EMPTY(new CfaEmptyInitPrec()), ALLVARS(new CfaAllVarsInitPrec()); @@ -196,6 +184,7 @@ private InitPrec(final CfaInitPrec builder) { private Encoding encoding = Encoding.LBE; private int maxEnum = 0; private InitPrec initPrec = InitPrec.EMPTY; + private PruneStrategy pruneStrategy = PruneStrategy.LAZY; public CfaConfigBuilder(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; @@ -238,6 +227,11 @@ public CfaConfigBuilder initPrec(final InitPrec initPrec) { return this; } + public CfaConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { + this.pruneStrategy = pruneStrategy; + return this; + } + public CfaConfig build(final CFA cfa) { final ItpSolver solver = solverFactory.createItpSolver(); final CfaLts lts = encoding.getLts(); @@ -258,23 +252,23 @@ public CfaConfigBuilder initPrec(final InitPrec initPrec) { switch (refinement) { case FW_BIN_ITP: refiner = SingleExprTraceRefiner.create(ExprTraceFwBinItpChecker.create(True(), True(), solver), - precGranularity.createRefiner(new ItpRefToExplPrec()), logger); + precGranularity.createRefiner(new ItpRefToExplPrec()), pruneStrategy, logger); break; case BW_BIN_ITP: refiner = SingleExprTraceRefiner.create(ExprTraceBwBinItpChecker.create(True(), True(), solver), - precGranularity.createRefiner(new ItpRefToExplPrec()), logger); + precGranularity.createRefiner(new ItpRefToExplPrec()), pruneStrategy, logger); break; case SEQ_ITP: refiner = SingleExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), solver), - precGranularity.createRefiner(new ItpRefToExplPrec()), logger); + precGranularity.createRefiner(new ItpRefToExplPrec()), pruneStrategy, logger); break; case MULTI_SEQ: refiner = MultiExprTraceRefiner.create(ExprTraceSeqItpChecker.create(True(), True(), solver), - precGranularity.createRefiner(new ItpRefToExplPrec()), logger); + precGranularity.createRefiner(new ItpRefToExplPrec()), pruneStrategy, logger); break; case UNSAT_CORE: refiner = SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(True(), True(), solver), - precGranularity.createRefiner(new VarsRefToExplPrec()), logger); + precGranularity.createRefiner(new VarsRefToExplPrec()), pruneStrategy, logger); break; default: throw new UnsupportedOperationException( @@ -335,11 +329,11 @@ public CfaConfigBuilder initPrec(final InitPrec initPrec) { Refiner, CfaAction, CfaPrec> refiner; if (refinement == Refinement.MULTI_SEQ) { - refiner = MultiExprTraceRefiner.create(exprTraceChecker, precGranularity.createRefiner(refToPrec), - logger); + refiner = MultiExprTraceRefiner.create(exprTraceChecker, + precGranularity.createRefiner(refToPrec), pruneStrategy, logger); } else { - refiner = SingleExprTraceRefiner.create(exprTraceChecker, precGranularity.createRefiner(refToPrec), - logger); + refiner = SingleExprTraceRefiner.create(exprTraceChecker, + precGranularity.createRefiner(refToPrec), pruneStrategy, logger); } final SafetyChecker, CfaAction, CfaPrec> checker = CegarChecker diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md index 68af87d76b..2dd804d433 100644 --- a/subprojects/cfa-cli/README.md +++ b/subprojects/cfa-cli/README.md @@ -64,7 +64,7 @@ If the limit is exceeded, unknown values are propagated. As a special case, `0` stands for infinite, but it should only be used if the model does not have any variable with unbounded domain. In general, values between `5` to `50` perform well (see Section 3.1.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). - `--refinement`: Refinement strategy, possible values: - - `FW_BIN_ITP`: Forward binary interpolation, only a reference implementation, does not perform well. + - `FW_BIN_ITP`: Forward binary interpolation, only performs well if `--prunestrategy` is `FULL`. - `BW_BIN_ITP`: Backward binary interpolation (see Section 3.2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information. - `SEQ_ITP`: Sequence interpolation. - `MULTI_SEQ`: Sequence interpolation with multiple counterexamples (see Section 3.2.2 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). @@ -77,6 +77,9 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J - `--precgranularity`: Granularity of the precision, possible values: - `GLOBAL`: The same precision is applied in each location of the CFA. - `LOCAL`: Each location can have a possibly different precision. +- `--prunestrategy`: Pruning strategy during refinement, possible values: + - `FULL`: The whole ARG is pruned and abstraction is completely restarted with the new precision. + - `LAZY`: The ARG is only pruned back to the first point where refinement was applied. - `--metrics`: Print metrics about the CFA without running the algorithm. - `--visualize`: Visualize the CFA without running the algorithm. If the extension of the output file is `pdf`, `png` or `svg` an automatic visualization is performed, for which [GraphViz](../../doc/Build.md) has to be available on `PATH`. diff --git a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index 1ea7653c6e..403d4fb2a9 100644 --- a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -32,6 +32,7 @@ import hu.bme.mit.theta.analysis.algorithm.SafetyResult.Unsafe; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; import hu.bme.mit.theta.analysis.expl.ExplState; +import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; import hu.bme.mit.theta.cfa.CFA; import hu.bme.mit.theta.cfa.analysis.CfaAction; import hu.bme.mit.theta.cfa.analysis.CfaState; @@ -99,6 +100,9 @@ public class CfaCli { @Parameter(names = "--initprec", description = "Initial precision of abstraction") InitPrec initPrec = InitPrec.EMPTY; + @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") + PruneStrategy pruneStrategy = PruneStrategy.LAZY; + @Parameter(names = "--loglevel", description = "Detailedness of logging") Logger.Level logLevel = Level.SUBSTEP; @@ -262,7 +266,8 @@ private CFA loadModel() throws IOException { private CfaConfig buildConfiguration(final CFA cfa) { return new CfaConfigBuilder(domain, refinement, solverFactory).precGranularity(precGranularity).search(search) - .predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec).logger(logger).build(cfa); + .predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec) + .pruneStrategy(pruneStrategy).logger(logger).build(cfa); } private void printResult(final SafetyResult status, final CFA cfa, final long totalTimeMs) { diff --git a/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfigBuilder.java b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfigBuilder.java index 7422f816a2..622f322c96 100644 --- a/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfigBuilder.java +++ b/subprojects/sts-analysis/src/main/java/hu.bme.mit.theta.sts/analysis/config/StsConfigBuilder.java @@ -71,14 +71,10 @@ public enum Domain { EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT } - ; - public enum Refinement { FW_BIN_ITP, BW_BIN_ITP, SEQ_ITP, MULTI_SEQ, UNSAT_CORE } - ; - public enum Search { BFS(ArgNodeComparators.combine(ArgNodeComparators.targetFirst(), ArgNodeComparators.bfs())), @@ -92,8 +88,6 @@ private Search(final ArgNodeComparator comparator) { } - ; - public enum PredSplit { WHOLE(ExprSplitters.whole()), @@ -108,8 +102,6 @@ private PredSplit(final ExprSplitter splitter) { } } - ; - public enum InitPrec { EMPTY(new StsEmptyInitPrec()), PROP(new StsPropInitPrec()); @@ -121,8 +113,6 @@ private InitPrec(final StsInitPrec builder) { } - ; - private Logger logger = NullLogger.getInstance(); private final SolverFactory solverFactory; private final Domain domain; @@ -130,6 +120,7 @@ private InitPrec(final StsInitPrec builder) { private Search search = Search.BFS; private PredSplit predSplit = PredSplit.WHOLE; private InitPrec initPrec = InitPrec.EMPTY; + private PruneStrategy pruneStrategy = PruneStrategy.LAZY; public StsConfigBuilder(final Domain domain, final Refinement refinement, final SolverFactory solverFactory) { this.domain = domain; @@ -157,8 +148,9 @@ public StsConfigBuilder initPrec(final InitPrec initPrec) { return this; } - public InitPrec getInitPrec() { - return initPrec; + public StsConfigBuilder pruneStrategy(final PruneStrategy pruneStrategy) { + this.pruneStrategy = pruneStrategy; + return this; } public StsConfig build(final STS sts) { @@ -183,23 +175,23 @@ public InitPrec getInitPrec() { switch (refinement) { case FW_BIN_ITP: refiner = SingleExprTraceRefiner.create(ExprTraceFwBinItpChecker.create(init, negProp, solver), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), logger); + JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); break; case BW_BIN_ITP: refiner = SingleExprTraceRefiner.create(ExprTraceBwBinItpChecker.create(init, negProp, solver), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), logger); + JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); break; case SEQ_ITP: refiner = SingleExprTraceRefiner.create(ExprTraceSeqItpChecker.create(init, negProp, solver), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), logger); + JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); break; case MULTI_SEQ: refiner = MultiExprTraceRefiner.create(ExprTraceSeqItpChecker.create(init, negProp, solver), - JoiningPrecRefiner.create(new ItpRefToExplPrec()), logger); + JoiningPrecRefiner.create(new ItpRefToExplPrec()), pruneStrategy, logger); break; case UNSAT_CORE: refiner = SingleExprTraceRefiner.create(ExprTraceUnsatCoreChecker.create(init, negProp, solver), - JoiningPrecRefiner.create(new VarsRefToExplPrec()), logger); + JoiningPrecRefiner.create(new VarsRefToExplPrec()), pruneStrategy, logger); break; default: throw new UnsupportedOperationException( @@ -258,10 +250,10 @@ public InitPrec getInitPrec() { Refiner refiner; if (refinement == Refinement.MULTI_SEQ) { refiner = MultiExprTraceRefiner.create(exprTraceChecker, - JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), logger); + JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), pruneStrategy, logger); } else { refiner = SingleExprTraceRefiner.create(exprTraceChecker, - JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), logger); + JoiningPrecRefiner.create(new ItpRefToPredPrec(predSplit.splitter)), pruneStrategy, logger); } final SafetyChecker checker = CegarChecker.create(abstractor, refiner, diff --git a/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java b/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java index 0caef9f10b..de35443f5d 100644 --- a/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java +++ b/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsExplTest.java @@ -31,6 +31,7 @@ import java.util.Collections; import java.util.function.Predicate; +import hu.bme.mit.theta.analysis.expr.refinement.*; import org.junit.Test; import hu.bme.mit.theta.analysis.Analysis; @@ -51,11 +52,6 @@ import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceChecker; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceUnsatCoreChecker; -import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.SingleExprTraceRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.VarsRefutation; import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; @@ -111,7 +107,7 @@ public void test() { Not(sts.getProp()), solver); final SingleExprTraceRefiner refiner = SingleExprTraceRefiner - .create(exprTraceChecker, JoiningPrecRefiner.create(new VarsRefToExplPrec()), logger); + .create(exprTraceChecker, JoiningPrecRefiner.create(new VarsRefToExplPrec()), PruneStrategy.LAZY, logger); final SafetyChecker checker = CegarChecker.create(abstractor, refiner, logger); diff --git a/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java b/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java index d76d0d625f..bf338f813c 100644 --- a/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java +++ b/subprojects/sts-analysis/src/test/java/hu/bme/mit/theta/sts/analysis/StsPredTest.java @@ -30,6 +30,7 @@ import java.util.function.Predicate; +import hu.bme.mit.theta.analysis.expr.refinement.*; import org.junit.Before; import org.junit.Test; @@ -46,11 +47,6 @@ import hu.bme.mit.theta.analysis.expr.ExprAction; import hu.bme.mit.theta.analysis.expr.ExprState; import hu.bme.mit.theta.analysis.expr.ExprStatePredicate; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceChecker; -import hu.bme.mit.theta.analysis.expr.refinement.ExprTraceFwBinItpChecker; -import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation; -import hu.bme.mit.theta.analysis.expr.refinement.JoiningPrecRefiner; -import hu.bme.mit.theta.analysis.expr.refinement.SingleExprTraceRefiner; import hu.bme.mit.theta.analysis.pred.ExprSplitters; import hu.bme.mit.theta.analysis.pred.ItpRefToPredPrec; import hu.bme.mit.theta.analysis.pred.PredAbstractors; @@ -109,7 +105,7 @@ public void testPredPrec() { final SingleExprTraceRefiner refiner = SingleExprTraceRefiner .create(exprTraceChecker, JoiningPrecRefiner.create(new ItpRefToPredPrec(ExprSplitters.atoms())), - logger); + PruneStrategy.LAZY, logger); final SafetyChecker checker = CegarChecker.create(abstractor, refiner, logger); diff --git a/subprojects/sts-cli/README.md b/subprojects/sts-cli/README.md index 2e93f91ef6..3780c65d8f 100644 --- a/subprojects/sts-cli/README.md +++ b/subprojects/sts-cli/README.md @@ -54,7 +54,7 @@ All arguments are optional, except `--model`. - `--search`: Search strategy in the abstract state space, possible values: - `BFS`, `DFS`: Standard breadth- and depth-first search. - `--refinement`: Refinement strategy, possible values: - - `FW_BIN_ITP`: Forward binary interpolation, only a reference implementation, does not perform well. + - `FW_BIN_ITP`: Forward binary interpolation, only performs well if `--prunestrategy` is `FULL`. - `BW_BIN_ITP`: Backward binary interpolation (see Section 3.2.1 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information. - `SEQ_ITP`: Sequence interpolation. - `MULTI_SEQ`: Sequence interpolation with multiple counterexamples (see Section 3.2.2 of [our JAR paper](https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf) for more information). @@ -64,6 +64,9 @@ All arguments are optional, except `--model`. - `WHOLE`: Keep predicates as a whole, no splitting is applied. Can perform well if the model has many Boolean variables. - `CONJUNCTS`: Split predicates into conjuncts. - `ATOMS`: Split predicates into atoms. +- `--prunestrategy`: Pruning strategy during refinement, possible values: + - `FULL`: The whole ARG is pruned and abstraction is completely restarted with the new precision. + - `LAZY`: The ARG is only pruned back to the first point where refinement was applied. ### For developer usage diff --git a/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index 9f84b83de6..0c5ba46e42 100644 --- a/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -31,6 +31,7 @@ import hu.bme.mit.theta.analysis.State; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics; +import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy; import hu.bme.mit.theta.analysis.utils.ArgVisualizer; import hu.bme.mit.theta.analysis.utils.TraceVisualizer; import hu.bme.mit.theta.common.Utils; @@ -89,6 +90,9 @@ public class StsCli { @Parameter(names = {"--initprec"}, description = "Initial precision") InitPrec initPrec = InitPrec.EMPTY; + @Parameter(names = "--prunestrategy", description = "Strategy for pruning the ARG after refinement") + PruneStrategy pruneStrategy = PruneStrategy.LAZY; + @Parameter(names = {"--loglevel"}, description = "Detailedness of logging") Logger.Level logLevel = Level.SUBSTEP; @@ -176,7 +180,7 @@ private STS loadModel() throws IOException { private StsConfig buildConfiguration(final STS sts) { return new StsConfigBuilder(domain, refinement, solverFactory).initPrec(initPrec).search(search) - .predSplit(predSplit).logger(logger).build(sts); + .predSplit(predSplit).pruneStrategy(pruneStrategy).logger(logger).build(sts); } private void printResult(final SafetyResult status, final STS sts, final long totalTimeMs) {