Merge branch 'nolazy'

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"))
 }

subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java

@@ -150,7 +150,14 @@ public void prune(final ArgNode<S, A> 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() {

subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/MultiExprTraceRefiner.java

@@ -38,19 +38,22 @@ public class MultiExprTraceRefiner<S extends ExprState, A extends ExprAction, P
 
 	private final ExprTraceChecker<R> exprTraceChecker;
 	private final PrecRefiner<S, A, P, R> precRefiner;
+	private final PruneStrategy pruneStrategy;
 	private final Logger logger;
 
-	private MultiExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker, final PrecRefiner<S, A, P, R> precRefiner,
-								  final Logger logger) {
+	private MultiExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
+								  final PrecRefiner<S, A, P, R> 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 <S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation> MultiExprTraceRefiner<S, A, P, R> create(
 			final ExprTraceChecker<R> exprTraceChecker, final PrecRefiner<S, A, P, R> 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<S, A, P> refine(final ARG<S, A> 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);

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
+}

subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/expr/refinement/SingleExprTraceRefiner.java

@@ -39,19 +39,22 @@ public final class SingleExprTraceRefiner<S extends ExprState, A extends ExprAct
 
 	private final ExprTraceChecker<R> exprTraceChecker;
 	private final PrecRefiner<S, A, P, R> precRefiner;
+	private final PruneStrategy pruneStrategy;
 	private final Logger logger;
 
 	private SingleExprTraceRefiner(final ExprTraceChecker<R> exprTraceChecker,
-								   final PrecRefiner<S, A, P, R> precRefiner, final Logger logger) {
+								   final PrecRefiner<S, A, P, R> 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 <S extends ExprState, A extends ExprAction, P extends Prec, R extends Refutation> SingleExprTraceRefiner<S, A, P, R> create(
 			final ExprTraceChecker<R> exprTraceChecker, final PrecRefiner<S, A, P, R> 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<S, A, P> refine(final ARG<S, A> 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<S, A> nodeToPrune = cexToConcretize.node(pruneIndex);
-			arg.prune(nodeToPrune);
+			switch (pruneStrategy){
+				case LAZY:
+					logger.write(Level.SUBSTEP, "|  |  Pruning from index %d...", pruneIndex);
+					final ArgNode<S, A> 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);

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 <S extends ExprState, A extends Action, P extends Prec, R extend
 				RefutationToPrec<P, R> 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<? extends State, ? extends Action, ? extends Prec> 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<CfaState<PredState>, CfaAction, CfaPrec<PredPrec>> 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<CfaState<PredState>, CfaAction, CfaPrec<PredPrec>> checker = CegarChecker

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`.

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) {

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,15 +113,14 @@ private InitPrec(final StsInitPrec builder) {
 
 	}
 
-	;
-
 	private Logger logger = NullLogger.getInstance();
 	private final SolverFactory solverFactory;
 	private final Domain domain;
 	private final Refinement refinement;
 	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<? extends State, ? extends Action, ? extends Prec> 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<PredState, StsAction, PredPrec> 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<PredState, StsAction, PredPrec> checker = CegarChecker.create(abstractor, refiner,