Skip to content

Commit

Permalink
Adding stop-if-stuck flag to xsts-cli
Browse files Browse the repository at this point in the history
  • Loading branch information
AdamZsofi committed Sep 18, 2022
1 parent 4cbef24 commit 54849fc
Showing 1 changed file with 11 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 54849fc

Please sign in to comment.