diff --git a/build.gradle.kts b/build.gradle.kts index 992ffc29b2..83a0f58034 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "2.6.0" + version = "2.6.1" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/doc/Development.md b/doc/Development.md index 977bf65f2d..ba003ab1ff 100644 --- a/doc/Development.md +++ b/doc/Development.md @@ -20,6 +20,7 @@ We usually develop on separate branches and increment the version number just be As the main repository is read-only, we suggest you to create your own [fork](https://help.github.com/articles/fork-a-repo/). Within your fork, we also recommend to create new _branches_ for your development. This enables us later on to easily integrate your work into the main repository by using [pull requests](https://help.github.com/articles/about-pull-requests/). As the framework is under development, we suggest you to [sync your fork](https://help.github.com/articles/syncing-a-fork/) often and merge the master branch into your development branch(es). +If you are confident that only you are working on your branch, you can also [rebase instead of merge](https://www.atlassian.com/git/tutorials/merging-vs-rebasing), but be careful. ## Building diff --git a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index 3386c46d94..f79d22b568 100644 --- a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java @@ -16,10 +16,6 @@ package hu.bme.mit.theta.cfa.cli; import java.io.*; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.Queue; -import java.util.Set; import java.util.concurrent.TimeUnit; import java.util.stream.Stream; @@ -58,16 +54,6 @@ import hu.bme.mit.theta.common.table.TableWriter; import hu.bme.mit.theta.common.visualization.Graph; import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; -import hu.bme.mit.theta.core.stmt.AssignStmt; -import hu.bme.mit.theta.core.stmt.AssumeStmt; -import hu.bme.mit.theta.core.stmt.HavocStmt; -import hu.bme.mit.theta.core.type.arraytype.ArrayType; -import hu.bme.mit.theta.core.type.booltype.BoolExprs; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.bvtype.BvExprs; -import hu.bme.mit.theta.core.type.bvtype.BvType; -import hu.bme.mit.theta.core.type.inttype.IntExprs; -import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.solver.*; import hu.bme.mit.theta.solver.z3.*; @@ -76,7 +62,6 @@ */ public class CfaCli { private static final String JAR_NAME = "theta-cfa-cli.jar"; - private final SolverFactory solverFactory = Z3SolverFactory.getInstance(); private final String[] args; private final TableWriter writer; @@ -213,7 +198,8 @@ private CFA loadModel() throws Exception { private CfaConfig buildConfiguration(final CFA cfa) throws Exception { try { - return new CfaConfigBuilder(domain, refinement, solverFactory).precGranularity(precGranularity).search(search) + return new CfaConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) + .precGranularity(precGranularity).search(search) .predSplit(predSplit).encoding(encoding).maxEnum(maxEnum).initPrec(initPrec) .pruneStrategy(pruneStrategy).logger(logger).build(cfa); } catch (final Exception ex) { @@ -267,16 +253,14 @@ private void printError(final Throwable ex) { } } - private void writeCex(final Unsafe status) { + private void writeCex(final Unsafe status) throws FileNotFoundException { @SuppressWarnings("unchecked") final Trace, CfaAction> trace = (Trace, CfaAction>) status.getTrace(); - final Trace, CfaAction> concrTrace = CfaTraceConcretizer.concretize(trace, solverFactory); + final Trace, CfaAction> concrTrace = CfaTraceConcretizer.concretize(trace, Z3SolverFactory.getInstance()); final File file = new File(cexfile); PrintWriter printWriter = null; try { printWriter = new PrintWriter(file); printWriter.write(concrTrace.toString()); - } catch (final FileNotFoundException e) { - printError(e); } finally { if (printWriter != null) { printWriter.close(); diff --git a/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java index c13a75927f..dee56f1b6e 100644 --- a/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java +++ b/subprojects/sts-cli/src/main/java/hu/bme/mit/theta/sts/cli/StsCli.java @@ -65,7 +65,6 @@ */ public class StsCli { private static final String JAR_NAME = "theta-sts-cli.jar"; - private final SolverFactory solverFactory = Z3SolverFactory.getInstance(); private final String[] args; private final TableWriter writer; @@ -193,7 +192,8 @@ private STS loadModel() throws Exception { private StsConfig buildConfiguration(final STS sts) throws Exception { try { - return new StsConfigBuilder(domain, refinement, solverFactory).initPrec(initPrec).search(search) + return new StsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) + .initPrec(initPrec).search(search) .predSplit(predSplit).pruneStrategy(pruneStrategy).logger(logger).build(sts); } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); @@ -240,9 +240,9 @@ private void printError(final Throwable ex) { } } - private void writeCex(final STS sts, final SafetyResult.Unsafe status) { + private void writeCex(final STS sts, final SafetyResult.Unsafe status) throws FileNotFoundException { @SuppressWarnings("unchecked") final Trace trace = (Trace) status.getTrace(); - final Trace concrTrace = StsTraceConcretizer.concretize(sts, trace, solverFactory); + final Trace concrTrace = StsTraceConcretizer.concretize(sts, trace, Z3SolverFactory.getInstance()); final File file = new File(cexfile); PrintWriter printWriter = null; try { @@ -250,8 +250,6 @@ private void writeCex(final STS sts, final SafetyResult.Unsafe status) { for (Valuation state : concrTrace.getStates()) { printWriter.println(state.toString()); } - } catch (final FileNotFoundException e) { - printError(e); } finally { if (printWriter != null) { printWriter.close(); diff --git a/subprojects/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java index 431c60e43f..0db7a02c63 100644 --- a/subprojects/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java +++ b/subprojects/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java @@ -45,7 +45,6 @@ public class XstsCli { private static final String JAR_NAME = "theta-xsts-cli.jar"; - private final SolverFactory solverFactory = Z3SolverFactory.getInstance(); private final String[] args; private final TableWriter writer; @@ -174,8 +173,9 @@ private XSTS loadModel() throws Exception { private XstsConfig buildConfiguration(final XSTS xsts) throws Exception { try { - return new XstsConfigBuilder(domain, refinement, solverFactory).maxEnum(maxEnum).initPrec(initPrec) - .pruneStrategy(pruneStrategy).search(search).predSplit(predSplit).logger(logger).build(xsts); + return new XstsConfigBuilder(domain, refinement, Z3SolverFactory.getInstance()) + .maxEnum(maxEnum).initPrec(initPrec).pruneStrategy(pruneStrategy) + .search(search).predSplit(predSplit).logger(logger).build(xsts); } catch (final Exception ex) { throw new Exception("Could not create configuration: " + ex.getMessage(), ex); } @@ -220,18 +220,16 @@ private void printError(final Throwable ex) { } } - private void writeCex(final SafetyResult.Unsafe status, final XSTS xsts) { + private void writeCex(final SafetyResult.Unsafe status, final XSTS xsts) throws FileNotFoundException { //TODO remove temp vars, replace int values with literals @SuppressWarnings("unchecked") final Trace, XstsAction> trace = (Trace, XstsAction>) status.getTrace(); - final XstsStateSequence concrTrace = XstsTraceConcretizerUtil.concretize(trace, solverFactory, xsts); + final XstsStateSequence concrTrace = XstsTraceConcretizerUtil.concretize(trace, Z3SolverFactory.getInstance(), xsts); final File file = new File(cexfile); PrintWriter printWriter = null; try { printWriter = new PrintWriter(file); printWriter.write(concrTrace.toString()); - } catch (final FileNotFoundException e) { - printError(e); } finally { if (printWriter != null) { printWriter.close();