Added ARG and precision check against getting stuck in the analysis

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

@@ -67,6 +67,11 @@ public boolean isBottom() {
 		return state.isBottom();
 	}
 
+	@Override
+	public boolean isTop() {
+		return state.isTop();
+	}
+
 	@Override
 	public Expr<BoolType> toExpr() {
 		// TODO Should be loc = l and toExpr(state)

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

@@ -27,4 +27,6 @@ public interface State {
 	 */
 	boolean isBottom();
 
+	default boolean isTop() { return false; }
+
 }

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

@@ -22,6 +22,8 @@
 
 import java.util.Collection;
 import hu.bme.mit.theta.common.container.Containers;
+
+import java.util.Objects;
 import java.util.Optional;
 import java.util.OptionalInt;
 import java.util.stream.Stream;
@@ -41,6 +43,19 @@ public final class ARG<S extends State, A extends Action> {
 	private int nextId = 0;
 	final PartialOrd<S> partialOrd;
 
+	@Override
+	public boolean equals(Object o) {
+		if (this == o) return true;
+		if (o == null || getClass() != o.getClass()) return false;
+		ARG<?, ?> arg = (ARG<?, ?>) o;
+		return initialized == arg.initialized && nextId == arg.nextId && initNodes.equals(arg.initNodes) && partialOrd.equals(arg.partialOrd);
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(initNodes.stream().map(ArgNode::getState), initialized, nextId, partialOrd);
+	}
+
 	private ARG(final PartialOrd<S> partialOrd) {
 		initNodes = Containers.createSet();
 		this.partialOrd = partialOrd;

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

@@ -17,14 +17,21 @@
 
 import static com.google.common.base.Preconditions.checkNotNull;
 
+import java.util.Collection;
+import java.util.LinkedHashSet;
+import java.util.Objects;
+import java.util.Set;
 import java.util.concurrent.TimeUnit;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 import com.google.common.base.Stopwatch;
 
 import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.algorithm.ARG;
+import hu.bme.mit.theta.analysis.algorithm.ArgNode;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.common.Utils;
@@ -44,6 +51,10 @@ public final class CegarChecker<S extends State, A extends Action, P extends Pre
 	private final Refiner<S, A, P> refiner;
 	private final Logger logger;
 
+	// controlled restart
+	private Set<AbstractArg> args = new LinkedHashSet<>();
+	private P lastPrecision = null;
+
 	private CegarChecker(final Abstractor<S, A, P> abstractor, final Refiner<S, A, P> refiner, final Logger logger) {
 		this.abstractor = checkNotNull(abstractor);
 		this.refiner = checkNotNull(refiner);
@@ -60,6 +71,28 @@ public static <S extends State, A extends Action, P extends Prec> CegarChecker<S
 		return new CegarChecker<>(abstractor, refiner, logger);
 	}
 
+	private class AbstractArg {
+		private final Collection<State> states;
+
+
+		private AbstractArg(final Stream<ArgNode<S, A>> nodes){
+			states = nodes.map(ArgNode::getState).collect(Collectors.toSet());
+		}
+
+		@Override
+		public boolean equals(Object o) {
+			if (this == o) return true;
+			if (o == null || getClass() != o.getClass()) return false;
+			AbstractArg that = (AbstractArg) o;
+			return states.equals(that.states);
+		}
+
+		@Override
+		public int hashCode() {
+			return Objects.hash(states);
+		}
+	}
+
 	@Override
 	public SafetyResult<S, A> check(final P initPrec) {
 		logger.write(Level.INFO, "Configuration: %s%n", this);
@@ -81,6 +114,29 @@ public SafetyResult<S, A> check(final P initPrec) {
 			abstractorTime += stopwatch.elapsed(TimeUnit.MILLISECONDS) - abstractorStartTime;
 			logger.write(Level.MAINSTEP, "| Checking abstraction done, result: %s%n", abstractorResult);
 
+			AbstractArg abstractArg = new AbstractArg(arg.getNodes());
+			if(args.contains(abstractArg) && lastPrecision != null && lastPrecision.equals(prec)) {
+				System.err.println("Not solvable!");
+				throw new RuntimeException("Not solvable!");
+			}
+			args.add(abstractArg);
+			lastPrecision = prec;
+
+			/*Stream<ArgNode<S, A>> argNodeStream = arg.getNodes().filter(saArgNode -> !saArgNode.getState().isTop() && saArgNode.isSafe());
+			List<ArgNode<S, A>> collect = arg.getNodes().filter(saArgNode -> !saArgNode.getState().isTop() && saArgNode.isSafe()).collect(Collectors.toList());
+
+			if(argNodeStream.count() == 0) {
+				System.err.println("True arg");
+				if(lastArgTrue && lastPrecision != null && lastPrecision.equals(prec)) {
+					System.err.println("Not solvable!");
+					throw new RuntimeException("Not solvable!");
+				}
+				lastArgTrue = true;
+			} else {
+				lastArgTrue = false;
+			}
+			lastPrecision = prec;*/
+
 			if (abstractorResult.isUnsafe()) {
 				logger.write(Level.MAINSTEP, "| Refining abstraction...%n");
 				final long refinerStartTime = stopwatch.elapsed(TimeUnit.MILLISECONDS);

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

@@ -124,6 +124,11 @@ public boolean isBottom() {
 			return false;
 		}
 
+		@Override
+		public boolean isTop() {
+			return val.getDecls().isEmpty();
+		}
+
 		@Override
 		public String toString() {
 			return Utils.lispStringBuilder(ExplState.class.getSimpleName()).aligned()
@@ -183,4 +188,5 @@ private static class BottomLazyHolder {
 	private static class TopLazyHolder {
 		static final ExplState INSTANCE = new NonBottom(ImmutableValuation.empty());
 	}
+
 }