From 54849fca3cf68bc3ee5cde1cad900390043f10b2 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sun, 18 Sep 2022 15:03:57 +0200 Subject: [PATCH 1/4] Adding stop-if-stuck flag to xsts-cli --- .../main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java | 11 +++++++++++ 1 file changed, 11 insertions(+) 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 index 9176084afd..8085ab68c4 100644 --- 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 = "--stop-if-stuck") + boolean stopIfStuck = 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 (!stopIfStuck) { + 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) From 5ae502cd60a1b2d968a6455c915a69eddd291ff6 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sun, 18 Sep 2022 23:26:47 +0200 Subject: [PATCH 2/4] Generated hash code for xsts state --- .../hu/bme/mit/theta/xsts/analysis/XstsState.java | 15 +++++++++++++++ 1 file changed, 15 insertions(+) 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 index acf2d2f52e..5f2f1536bb 100644 --- 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 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); + } } From 7227f9a1671241b8d7b5a57b49b6c4d325eb4992 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Mon, 19 Sep 2022 10:10:41 +0200 Subject: [PATCH 3/4] Negated xsts stuck flag --- .../src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 index 8085ab68c4..b6d6e720c1 100644 --- 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 @@ -103,8 +103,8 @@ public class XstsCli { @Parameter(names = {"--visualize"}, description = "Write proof or counterexample to file in dot format") String dotfile = null; - @Parameter(names = "--stop-if-stuck") - boolean stopIfStuck = false; + @Parameter(names = "--no-stuck-check") + boolean noStuckCheck = false; private Logger logger; @@ -204,7 +204,7 @@ 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 (!stopIfStuck) { + if (noStuckCheck) { ArgCexCheckHandler.instance.setArgCexCheck(false, false); } else { ArgCexCheckHandler.instance.setArgCexCheck(true, refinement.equals(Refinement.MULTI_SEQ)); From a88b8b70c4196dd4cd7b10ab35c275b255d50e2f Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Mon, 19 Sep 2022 10:12:40 +0200 Subject: [PATCH 4/4] Bump version number --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index c0406e986d..04fdbd5ca0 100644 --- 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")) }