Merge pull request #112 from ftsrg/xsts-loops

Loops, stmt optimization, unified PROD domain

build.gradle.kts

@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.12.1"
+    version = "2.13.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

doc/CEGAR-algorithms.md

@@ -36,8 +36,7 @@ The domain controls the abstract information that is being tracked about the sys
 * `PRED_BOOL`: [Boolean predicate abstraction](https://link.springer.com/article/10.1007/s10009-002-0095-0) keeps track of arbitrary Boolean combination of predicates.
 * `PRED_SPLIT`: Boolean predicate abstraction, but states are [split]((https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf)) into sub-states along disjunctions.
 * `EXPL`: [Explicit-value abstraction]((https://link.springer.com/chapter/10.1007/978-3-642-37057-1_11)) keeps track of concrete values, but only for a (continuously expanded) set of variables.
-* `PROD`: Product abstraction, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly while others are tracked by predicates.
-* `PROD_AUTO`: Automatic product abstraction, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly. Other variables are also tracked explicitly if they appear in a given number of predicates (defined with the `--maxpredcount` option).
+* `EXPL_PRED_CARD`, `EXPL_PRED_SPLIT` and `EXPL_PRED_BOOL`: Product abstraction domains, available for XSTS models. The set of control variables (marked with `ctrl`) are tracked explicitly while others are tracked by predicates (using the corresponding predicate domain). Other variables are also tracked explicitly if they appear in a given number of predicates (defined with the `--maxpredcount` option).
 
 Predicate abstraction (`PRED_*`) tracks logical formulas instead of concrete values of variables, which can be efficient for variables with large (or infinite) domain.
 Explicit-values (`EXPL`) keep track of a subset of system variables, which can be efficient if variables are mostly deterministic or have a small domain.
@@ -58,7 +57,7 @@ Controls the initial precision of the abstraction (e.g., what predicates or vari
 * `ALLVARS`: Tracks all variables from the beginning. Available for CFA and XSTS if `--domain` is `EXPL`.
 * `ALLASSUMES`: Track all assumptions by default (e.g., branch/loop conditions). Only applicable for CFA and if `--domain` is `PRED_*`.
 * `PROP`: Available for XSTS. Tracks variables from the property if `--domain` is `EXPL` and predicates from the property if `--domain` is `PRED_*`.
-* `CTRL`: Available for XSTS if `--domain` is `PROD` or `EXPL`. Tracks all control variables.
+* `CTRL`: Available for XSTS if `--domain` is `EXPL` or `EXPL_PRED_*`. Tracks all control variables.
 
 We observed that usually the `EMPTY` initial precision yields good performance: the algorithm can automatically determine the precision.
 However, if the system is mostly deterministic, it might be suitable to track all variables from the beginning.
@@ -93,7 +92,7 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J
 ### `--maxpredcount`
 
 Available for XSTS.
-The number of predicates a variable has to appear in before it is tracked explicitly when the `PRED_AUTO` domain is used.
+The number of predicates a variable has to appear in before it is tracked explicitly when `--domain` is `EXPL_PRED_*`. Default is `0` (unlimited).
 
 ### `--refinement`
 

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaInitPrecs.java

@@ -10,8 +10,8 @@
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.utils.ExprUtils;
 
-import java.util.HashMap;
-import java.util.HashSet;
+import hu.bme.mit.theta.common.container.Containers;
+
 import java.util.Map;
 import java.util.Set;
 
@@ -20,9 +20,9 @@ public final class CfaInitPrecs {
     private CfaInitPrecs() {}
 
     public static LocalCfaPrec<PredPrec> collectAssumesLocal(CFA cfa) {
-        Map<CFA.Loc, PredPrec> precs = new HashMap<>();
+        Map<CFA.Loc, PredPrec> precs = Containers.createMap();
         for (CFA.Loc l : cfa.getLocs()) {
-            Set<Expr<BoolType>> exprs = new HashSet<>();
+            Set<Expr<BoolType>> exprs = Containers.createSet();
             for (CFA.Edge e : l.getInEdges()) {
                 CFA.Edge running = e;
                 while (running != null) {
@@ -42,7 +42,7 @@ public static LocalCfaPrec<PredPrec> collectAssumesLocal(CFA cfa) {
     }
 
     public static GlobalCfaPrec<PredPrec> collectAssumesGlobal(CFA cfa) {
-        Set<Expr<BoolType>> assumes = new HashSet<>();
+        Set<Expr<BoolType>> assumes = Containers.createSet();
         for (CFA.Edge e : cfa.getEdges()) {
             if (e.getStmt() instanceof AssumeStmt) {
                 AssumeStmt assumeStmt = (AssumeStmt)e.getStmt();

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/DistToErrComparator.java

@@ -17,7 +17,7 @@
 
 import static com.google.common.base.Preconditions.checkArgument;
 
-import java.util.HashMap;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
@@ -83,7 +83,7 @@ private int getDistanceToError(final Loc loc) {
 
 	static Map<Loc, Integer> calculateDistancesToError(final CFA cfa, final Loc errLoc) {
 		List<Loc> queue = new LinkedList<>();
-		final Map<Loc, Integer> distancesToError = new HashMap<>();
+		final Map<Loc, Integer> distancesToError = Containers.createMap();
 		queue.add(errLoc);
 		distancesToError.put(errLoc, 0);
 		int distance = 1;

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/impact/ImpactReachedSet.java

@@ -20,7 +20,7 @@
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
-import java.util.HashMap;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.List;
 import java.util.Map;
 import java.util.function.Function;
@@ -38,7 +38,7 @@ public final class ImpactReachedSet<S extends State, A extends Action, K> implem
 
 	private ImpactReachedSet(final Function<? super S, ? extends K> partitioning) {
 		this.partitioning = checkNotNull(partitioning);
-		partitions = new HashMap<>();
+		partitions = Containers.createMap();
 	}
 
 	public static <S extends State, A extends Action, K> ImpactReachedSet<S, A, K> create(

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/lts/CfaCachedLts.java

@@ -1,7 +1,7 @@
 package hu.bme.mit.theta.cfa.analysis.lts;
 
 import java.util.Collection;
-import java.util.HashMap;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.Map;
 
 import hu.bme.mit.theta.cfa.CFA.Loc;
@@ -19,7 +19,7 @@ public final class CfaCachedLts implements CfaLts {
 
 	public CfaCachedLts(final CfaLts lts) {
 		this.lts = lts;
-		this.actionCache = new HashMap<>();
+		this.actionCache = Containers.createMap();
 	}
 
 	@Override

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrec.java

@@ -18,7 +18,7 @@
 import static com.google.common.base.Preconditions.checkNotNull;
 
 import java.util.Collections;
-import java.util.HashMap;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.Map;
 import java.util.Map.Entry;
 import java.util.NoSuchElementException;
@@ -80,7 +80,7 @@ public P getPrec(final Loc loc) {
 	public LocalCfaPrec<P> refine(final Map<Loc, P> refinedPrecs) {
 		checkNotNull(refinedPrecs);
 
-		final Map<Loc, P> refinedMapping = new HashMap<>(this.mapping);
+		final Map<Loc, P> refinedMapping = Containers.createMap(this.mapping);
 
 		for (final Entry<Loc, P> entry : refinedPrecs.entrySet()) {
 			final Loc loc = entry.getKey();

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/prec/LocalCfaPrecRefiner.java

@@ -18,7 +18,7 @@
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 
-import java.util.HashMap;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.Map;
 
 import hu.bme.mit.theta.analysis.Action;
@@ -59,7 +59,7 @@ public CfaPrec<P> refine(final CfaPrec<P> prec, final Trace<CfaState<S>, A> trac
 		// joining them to the old precision of the location
 
 		final LocalCfaPrec<P> genPrec = (LocalCfaPrec<P>) prec;
-		final Map<Loc, P> runningPrecs = new HashMap<>();
+		final Map<Loc, P> runningPrecs = Containers.createMap();
 		for (final CfaState<S> state : trace.getStates()) {
 			runningPrecs.put(state.getLoc(), genPrec.getPrec(state.getLoc()));
 		}

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/utils/CfaVisualizer.java

@@ -16,7 +16,7 @@
 package hu.bme.mit.theta.cfa.analysis.utils;
 
 import java.awt.Color;
-import java.util.HashMap;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.LinkedHashSet;
 import java.util.Map;
 import java.util.Optional;
@@ -56,7 +56,7 @@ private CfaVisualizer() {
 
 	public static Graph visualize(final CFA cfa) {
 		final Graph graph = new Graph(CFA_ID, CFA_LABEL);
-		final Map<Loc, String> ids = new HashMap<>();
+		final Map<Loc, String> ids = Containers.createMap();
 		addVars(graph, cfa);
 		for (final Loc loc : cfa.getLocs()) {
 			addLocation(graph, cfa, loc, ids);

subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/EncodingTest.java

@@ -15,7 +15,7 @@
 
 import java.io.FileInputStream;
 import java.io.IOException;
-import java.util.HashSet;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.Set;
 
 public class EncodingTest {
@@ -30,7 +30,7 @@ private CFA.Loc getLocByName(String name) {
 	}
 
 	private Set<String> getNextLocs(CfaLts lts, String loc) {
-		Set<String> locs = new HashSet<>();
+		Set<String> locs = Containers.createSet();
 		SS ss = new SS();
 		for (var act : lts.getEnabledActionsFor(CfaState.of(getLocByName(loc), ss))) {
 			locs.add(act.getTarget().getName());

subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaMetrics.java

@@ -25,7 +25,7 @@
 import hu.bme.mit.theta.core.type.bvtype.BvType;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 
-import java.util.HashSet;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.LinkedList;
 import java.util.Queue;
 import java.util.Set;
@@ -48,7 +48,7 @@ public static void printMetrics(Logger logger, CFA cfa){
 	}
 
 	public static int getCfaComponents(final CFA cfa) {
-		final Set<CFA.Loc> visited = new HashSet<>();
+		final Set<CFA.Loc> visited = Containers.createSet();
 		int components = 0;
 
 		for (final CFA.Loc loc : cfa.getLocs()) {

subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/CFA.java

@@ -27,6 +27,7 @@
 import com.google.common.collect.ImmutableSet;
 
 import hu.bme.mit.theta.common.Utils;
+import hu.bme.mit.theta.common.container.Containers;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.stmt.Stmt;
 import hu.bme.mit.theta.core.utils.StmtUtils;
@@ -176,7 +177,7 @@ public static final class Builder {
 		private boolean built;
 
 		private Builder() {
-			locs = new HashSet<>();
+			locs = Containers.createSet();
 			edges = new LinkedList<>();
 			built = false;
 		}

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

@@ -21,7 +21,7 @@
 import static java.util.stream.Collectors.toList;
 
 import java.util.Collection;
-import java.util.HashSet;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.Optional;
 import java.util.OptionalInt;
 import java.util.stream.Stream;
@@ -42,7 +42,7 @@ public final class ARG<S extends State, A extends Action> {
 	final PartialOrd<S> partialOrd;
 
 	private ARG(final PartialOrd<S> partialOrd) {
-		initNodes = new HashSet<>();
+		initNodes = Containers.createSet();
 		this.partialOrd = partialOrd;
 		this.initialized = false;
 	}

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

@@ -20,7 +20,7 @@
 
 import java.util.ArrayList;
 import java.util.Collection;
-import java.util.HashSet;
+import hu.bme.mit.theta.common.container.Containers;
 import java.util.Optional;
 import java.util.stream.Stream;
 
@@ -58,7 +58,7 @@ public final class ArgNode<S extends State, A extends Action> {
 		inEdge = Optional.empty();
 		outEdges = new ArrayList<>();
 		coveringNode = Optional.empty();
-		coveredNodes = new HashSet<>();
+		coveredNodes = Containers.createSet();
 		expanded = false;
 	}
 

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/ExplStmtOptimizer.java

@@ -0,0 +1,23 @@
+package hu.bme.mit.theta.analysis.expl;
+
+import hu.bme.mit.theta.analysis.stmtoptimizer.StmtOptimizer;
+import hu.bme.mit.theta.analysis.stmtoptimizer.StmtSimplifier;
+import hu.bme.mit.theta.core.stmt.Stmt;
+
+public class ExplStmtOptimizer implements StmtOptimizer<ExplState> {
+
+    private ExplStmtOptimizer(){}
+
+    private static class LazyHolder {
+        static final ExplStmtOptimizer INSTANCE = new ExplStmtOptimizer();
+    }
+
+    public static ExplStmtOptimizer getInstance() {
+        return LazyHolder.INSTANCE;
+    }
+
+    @Override
+    public Stmt optimizeStmt(final ExplState state, final Stmt stmt) {
+        return StmtSimplifier.simplifyStmt(state,stmt);
+    }
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/expl/StmtApplier.java

@@ -32,7 +32,7 @@
 import java.util.ArrayList;
 import java.util.List;
 
-final class StmtApplier {
+public final class StmtApplier {
 
 	public enum ApplyResult {
 		FAILURE, SUCCESS, BOTTOM
@@ -62,6 +62,9 @@ public static ApplyResult apply(final Stmt stmt, final MutableValuation val, fin
 		} else if (stmt instanceof OrtStmt) {
 			final OrtStmt ortStmt = (OrtStmt) stmt;
 			return applyOrt(ortStmt, val, approximate);
+		} else if (stmt instanceof LoopStmt) {
+			final LoopStmt loopStmt = (LoopStmt) stmt;
+			return applyLoop(loopStmt, val, approximate);
 		} else {
 			throw new UnsupportedOperationException("Unhandled statement: " + stmt);
 		}
@@ -170,6 +173,11 @@ private static ApplyResult applySequence(final SequenceStmt stmt, final MutableV
 		return ApplyResult.SUCCESS;
 	}
 
+	private static ApplyResult applyLoop(final LoopStmt stmt, final MutableValuation val,
+											 final boolean approximate) {
+		throw new UnsupportedOperationException(String.format("Loop statement %s was not unrolled",stmt));
+	}
+
 	private static ApplyResult applyNonDet(final NonDetStmt stmt, final MutableValuation val,
 										   final boolean approximate) {
 		List<MutableValuation> valuations = new ArrayList<MutableValuation>();