From 54849fca3cf68bc3ee5cde1cad900390043f10b2 Mon Sep 17 00:00:00 2001 From: AdamZsofi Date: Sun, 18 Sep 2022 15:03:57 +0200 Subject: [PATCH] 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)