Merge pull request #175 from ftsrg/xsts-stuck-flag

Adding no refinement progress detection to XSTS cli
ftsrg · Sep 20, 2022 · 431773b · 431773b
2 parents 4cbef24 + a88b8b7
commit 431773b
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 1 deletion.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -11,7 +11,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "4.2.1"
+    version = "4.2.2"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsState.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/XstsState.java
@@ -5,6 +5,8 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 
+import java.util.Objects;
+
 public final class XstsState<S extends ExprState> implements ExprState {
 
 	private final S state;
@@ -47,4 +49,17 @@ public boolean isBottom() {
 	public String toString() {
 		return Utils.lispStringBuilder(getClass().getSimpleName()).aligned().add(initialized ? "post_init" : "pre_init").add(lastActionWasEnv ? "last_env" : "last_internal").body().add(state).toString();
 	}
+
+	@Override
+	public boolean equals(Object o) {
+		if (this == o) return true;
+		if (o == null || getClass() != o.getClass()) return false;
+		XstsState<?> xstsState = (XstsState<?>) o;
+		return lastActionWasEnv == xstsState.lastActionWasEnv && initialized == xstsState.initialized && state.equals(xstsState.state);
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(state, lastActionWasEnv, initialized);
+	}
 }
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
@@ -7,6 +7,7 @@
 import hu.bme.mit.theta.analysis.Trace;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics;
+import hu.bme.mit.theta.analysis.algorithm.runtimecheck.ArgCexCheckHandler;
 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;
@@ -102,6 +103,9 @@ public class XstsCli {
 	@Parameter(names = {"--visualize"}, description = "Write proof or counterexample to file in dot format")
 	String dotfile = null;
 
+	@Parameter(names = "--no-stuck-check")
+	boolean noStuckCheck = false;
+
 	private Logger logger;
 
 	public XstsCli(final String[] args) {
@@ -199,6 +203,13 @@ private XSTS loadModel() throws Exception {
 	}
 
 	private XstsConfig<?, ?, ?> buildConfiguration(final XSTS xsts) throws Exception {
+		// set up stopping analysis if it is stuck on same ARGs and precisions
+		if (noStuckCheck) {
+			ArgCexCheckHandler.instance.setArgCexCheck(false, false);
+		} else {
+			ArgCexCheckHandler.instance.setArgCexCheck(true, refinement.equals(Refinement.MULTI_SEQ));
+		}
+
 		try {
 			return new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance())
 					.maxEnum(maxEnum).autoExpl(autoExpl).initPrec(initPrec).pruneStrategy(pruneStrategy)