Skip to content

Commit

Permalink
Add version info option to CLI tools
Browse files Browse the repository at this point in the history
  • Loading branch information
hajduakos committed Sep 22, 2020
1 parent 2d39677 commit 2254f57
Show file tree
Hide file tree
Showing 9 changed files with 53 additions and 1 deletion.
2 changes: 1 addition & 1 deletion build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ buildscript {

allprojects {
group = "hu.bme.mit.inf.theta"
version = "2.4.2"
version = "2.5.0"

apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
}
Expand Down
1 change: 1 addition & 0 deletions subprojects/cfa-cli/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ If the extension of the output file is `pdf`, `png` or `svg` an automatic visual
Otherwise, the output is simply in `dot` format.

The arguments related to the algorithm are described in more detail (along with best practices) in [CEGAR-algorithms.md](../../doc/CEGAR-algorithms.md).
* `--version`: Print version info (in this case `--model` is of course not required).

### For developer usage

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@
import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Search;
import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer;
import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
import hu.bme.mit.theta.common.CliUtils;
import hu.bme.mit.theta.common.logging.ConsoleLogger;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.Logger.Level;
Expand Down Expand Up @@ -130,6 +131,9 @@ public class CfaCli {
@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
boolean stacktrace = false;

@Parameter(names = "--version", description = "Display version", help = true)
boolean versionInfo = false;

private Logger logger;

public CfaCli(final String[] args) {
Expand Down Expand Up @@ -158,6 +162,11 @@ private void run() {
return;
}

if (versionInfo) {
CliUtils.printVersion(System.out);
return;
}

try {
final Stopwatch sw = Stopwatch.createStarted();
final CFA cfa = loadModel();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
package hu.bme.mit.theta.common;

import java.io.PrintStream;

public class CliUtils {
private CliUtils() { }

public static void printVersion(PrintStream ps) {
String ver = new CliUtils().getClass().getPackage().getImplementationVersion();
if (ver == null) ver = "Unknown version. Are you running from JAR file?";
ps.println(ver);
}
}
1 change: 1 addition & 0 deletions subprojects/sts-cli/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ All arguments are optional, except `--model`.
* `--cex`: Output file where the counterexample is written (if the result is unsafe). If the argument is not given (default) the counterexample is not printed. Use `CON` (Windows) or `/dev/stdout` (Linux) as argument to print to the standard output.
* `--loglevel`: Detailedness of logging.
* Possible values (from the least to the most detailed): `RESULT`, `MAINSTEP`, `SUBSTEP` (default), `INFO`, `DETAIL`, `VERBOSE`
* `--version`: Print version info (in this case `--model` is of course not required).

The arguments related to the algorithm are described in more detail (along with best practices) in [CEGAR-algorithms.md](../../doc/CEGAR-algorithms.md).

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@
import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics;
import hu.bme.mit.theta.analysis.expr.ExprState;
import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy;
import hu.bme.mit.theta.common.CliUtils;
import hu.bme.mit.theta.common.Utils;
import hu.bme.mit.theta.common.logging.ConsoleLogger;
import hu.bme.mit.theta.common.logging.Logger;
Expand Down Expand Up @@ -104,6 +105,9 @@ public class StsCli {
@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
boolean stacktrace = false;

@Parameter(names = "--version", description = "Display version", help = true)
boolean versionInfo = false;

private Logger logger;

public StsCli(final String[] args) {
Expand Down Expand Up @@ -132,6 +136,11 @@ private void run() {
return;
}

if (versionInfo) {
CliUtils.printVersion(System.out);
return;
}

try {
final Stopwatch sw = Stopwatch.createStarted();
final STS sts = loadModel();
Expand Down
1 change: 1 addition & 0 deletions subprojects/xsts-cli/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ All arguments are optional, except `--model` and `--property`.
* `--cex`: Output file where the counterexample is written (if the result is unsafe). If the argument is not given (default) the counterexample is not printed. Use `CON` (Windows) or `/dev/stdout` (Linux) as argument to print to the standard output.
* `--loglevel`: Detailedness of logging.
* Possible values (from the least to the most detailed): `RESULT`, `MAINSTEP`, `SUBSTEP` (default), `INFO`, `DETAIL`, `VERBOSE`.
* `--version`: Print version info (in this case `--model` and `--property` is of course not required).

The arguments related to the algorithm are described in more detail (along with best practices) in [CEGAR-algorithms.md](../../doc/CEGAR-algorithms.md).

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
import hu.bme.mit.theta.analysis.algorithm.*;
import hu.bme.mit.theta.analysis.algorithm.cegar.*;
import hu.bme.mit.theta.analysis.expr.refinement.PruneStrategy;
import hu.bme.mit.theta.common.CliUtils;
import hu.bme.mit.theta.common.logging.ConsoleLogger;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.NullLogger;
Expand Down Expand Up @@ -90,6 +91,9 @@ public class XstsCli {
@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
boolean stacktrace = false;

@Parameter(names = "--version", description = "Display version", help = true)
boolean versionInfo = false;

private Logger logger;

public XstsCli(final String[] args) {
Expand Down Expand Up @@ -118,6 +122,11 @@ private void run() {
return;
}

if (versionInfo) {
CliUtils.printVersion(System.out);
return;
}

try {
final Stopwatch sw = Stopwatch.createStarted();
final XSTS xsts = loadModel();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
import hu.bme.mit.theta.analysis.unit.UnitPrec;
import hu.bme.mit.theta.analysis.utils.ArgVisualizer;
import hu.bme.mit.theta.analysis.utils.TraceVisualizer;
import hu.bme.mit.theta.common.CliUtils;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.table.BasicTableWriter;
import hu.bme.mit.theta.common.table.TableWriter;
Expand Down Expand Up @@ -68,6 +69,9 @@ public final class XtaCli {
@Parameter(names = "--stacktrace", description = "Print full stack trace in case of exception")
boolean stacktrace = false;

@Parameter(names = "--version", description = "Display version", help = true)
boolean versionInfo = false;

public XtaCli(final String[] args) {
this.args = args;
this.writer = new BasicTableWriter(System.out, ",", "\"", "\"");
Expand All @@ -93,6 +97,11 @@ private void run() {
return;
}

if (versionInfo) {
CliUtils.printVersion(System.out);
return;
}

try {
final XtaSystem system = loadModel();
final SafetyChecker<?, ?, UnitPrec> checker = LazyXtaCheckerFactory.create(system, dataStrategy,
Expand Down

0 comments on commit 2254f57

Please sign in to comment.