Skip to content
Snippets Groups Projects
Commit bb96aaf0 authored by dgelessus's avatar dgelessus
Browse files

Move CLI options enum to top level

This will break the ProB Java API and ProB 2 UI for a short moment.
Please bear with me. :)
parent 5e1e8684
No related branches found
No related tags found
No related merge requests found
Pipeline #140130 passed
......@@ -33,8 +33,7 @@ import org.apache.commons.cli.HelpFormatter;
import org.apache.commons.cli.Options;
import org.apache.commons.cli.ParseException;
import static de.tlc4b.TLC4BCliOptions.*;
import static de.tlc4b.TLC4BCliOptions.TLCOption.*;
import static de.tlc4b.TLC4BOption.*;
import static de.tlc4b.util.StopWatch.Watches.*;
import static de.tlc4b.MP.*;
......@@ -255,6 +254,14 @@ public class TLC4B {
}
}
private static Options getCommandlineOptions() {
Options options = new Options();
for (TLC4BOption option : TLC4BOption.values()) {
options.addOption(option.arg(), option.expectsArg() != null, option.desc());
}
return options;
}
private void handleParameter(String[] args) {
DefaultParser parser = new DefaultParser();
Options options = getCommandlineOptions();
......
package de.tlc4b;
import org.apache.commons.cli.Options;
public class TLC4BCliOptions {
public enum TLCOption {
NODEAD("nodead", "do not look for deadlocks", null),
NOTLC("notlc", "do not run TLC", null),
NOTRANSLATION("notranslation", "proceed without machine translation", null),
NOGOAL("nogoal", "do not look for GOAL predicate", null),
NOINV("noinv", "do not look for invariant violations", null),
NOASS("noass", "do not look for ASSERTION violations", null),
WDCHECK("wdcheck", "", null),
SYMMETRY("symmetry", "", null),
TOOL("tool", "", null),
TMP("tmp", "", null),
NOLTL("noltl", "no checking of LTL assertions", null),
LAZYCONSTANTS("lazyconstants", "", null),
TESTSCRIPT("testscript", "", null),
NOTRACE("notrace", "do not generate counter example trace", null),
DEL("del", "", null),
PARINVEVAL("parinveval", "", null),
LOG("log", "write statistics to CSV file", String.class),
MAXINT("maxint", "set value of MAXINT", Integer.class),
DEFAULT_SETSIZE("default_setsize", "", Integer.class),
MININT("minint", "set value of MININT", Integer.class),
WORKERS("workers", "specify number of workers", Integer.class),
DFID("dfid", "depth-first model checking with iterative deepening, specify initial depth", Integer.class),
CONSTANTSSETUP("constantssetup", "use constants found by ProB for TLC model checking", String.class),
LTLFORMULA("ltlformula", "provide an additional LTL formula", String.class),
VERBOSE("verbose", "put TLC4B in verbose mode", null),
SILENT("silent", "put TLC4B in silent mode", null),
OUTPUT("output", "provide path for output directory", String.class),
COVERAGE("coverage", "print operation coverage", null);
private final String arg, desc;
private final Class<?> expectsArg;
TLCOption(String arg, String desc, Class<?> expectsArg) {
this.arg = arg;
this.desc = desc;
this.expectsArg = expectsArg;
}
public String arg() {
return arg;
}
public String cliArg() {
return "-" + arg;
}
public String desc() {
return desc;
}
public Class<?> expectsArg() {
return expectsArg;
}
}
static Options getCommandlineOptions() {
Options options = new Options();
for (TLCOption option : TLCOption.values()) {
options.addOption(option.arg(), option.expectsArg() != null, option.desc());
}
return options;
}
}
package de.tlc4b;
public enum TLC4BOption {
NODEAD("nodead", "do not look for deadlocks", null),
NOTLC("notlc", "do not run TLC", null),
NOTRANSLATION("notranslation", "proceed without machine translation", null),
NOGOAL("nogoal", "do not look for GOAL predicate", null),
NOINV("noinv", "do not look for invariant violations", null),
NOASS("noass", "do not look for ASSERTION violations", null),
WDCHECK("wdcheck", "", null),
SYMMETRY("symmetry", "", null),
TOOL("tool", "", null),
TMP("tmp", "", null),
NOLTL("noltl", "no checking of LTL assertions", null),
LAZYCONSTANTS("lazyconstants", "", null),
TESTSCRIPT("testscript", "", null),
NOTRACE("notrace", "do not generate counter example trace", null),
DEL("del", "", null),
PARINVEVAL("parinveval", "", null),
LOG("log", "write statistics to CSV file", String.class),
MAXINT("maxint", "set value of MAXINT", Integer.class),
DEFAULT_SETSIZE("default_setsize", "", Integer.class),
MININT("minint", "set value of MININT", Integer.class),
WORKERS("workers", "specify number of workers", Integer.class),
DFID("dfid", "depth-first model checking with iterative deepening, specify initial depth", Integer.class),
CONSTANTSSETUP("constantssetup", "use constants found by ProB for TLC model checking", String.class),
LTLFORMULA("ltlformula", "provide an additional LTL formula", String.class),
VERBOSE("verbose", "put TLC4B in verbose mode", null),
SILENT("silent", "put TLC4B in silent mode", null),
OUTPUT("output", "provide path for output directory", String.class),
COVERAGE("coverage", "print operation coverage", null);
private final String arg, desc;
private final Class<?> expectsArg;
TLC4BOption(String arg, String desc, Class<?> expectsArg) {
this.arg = arg;
this.desc = desc;
this.expectsArg = expectsArg;
}
public String arg() {
return arg;
}
public String cliArg() {
return "-" + arg;
}
public String desc() {
return desc;
}
public Class<?> expectsArg() {
return expectsArg;
}
}
......@@ -12,7 +12,7 @@ import org.junit.runner.RunWith;
import java.io.File;
import java.util.ArrayList;
import static de.tlc4b.TLC4BCliOptions.TLCOption.DFID;
import static de.tlc4b.TLC4BOption.DFID;
import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
......
package de.tlc4b.tlc.integration;
import static de.tlc4b.TLC4BCliOptions.TLCOption.*;
import static de.tlc4b.TLC4BOption.*;
import static de.tlc4b.tlc.TLCResults.TLCResult.*;
import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.*;
......
......@@ -19,7 +19,7 @@ import de.tlc4b.tlc.TLCResults.TLCResult;
import util.ToolIO;
import static de.tlc4b.TLC4BCliOptions.TLCOption.NOTRACE;
import static de.tlc4b.TLC4BOption.NOTRACE;
import static org.junit.Assert.assertEquals;
public class TestUtil {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment