diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index 976f5ebb1426d62505d74e3c4a848b0f3dfd7546..4d261526c2e31b1d5e4553e5b49b40408d3bfc59 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -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.*; @@ -254,6 +253,14 @@ public class TLC4B { System.exit(0); } } + + 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(); diff --git a/src/main/java/de/tlc4b/TLC4BCliOptions.java b/src/main/java/de/tlc4b/TLC4BCliOptions.java deleted file mode 100644 index bb86ae433d46e8d588b5874fcc9844d17c24bcf8..0000000000000000000000000000000000000000 --- a/src/main/java/de/tlc4b/TLC4BCliOptions.java +++ /dev/null @@ -1,71 +0,0 @@ -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; - } - -} diff --git a/src/main/java/de/tlc4b/TLC4BOption.java b/src/main/java/de/tlc4b/TLC4BOption.java new file mode 100644 index 0000000000000000000000000000000000000000..f88f0e70046a80f918da6f85a74465c8bdcc8e12 --- /dev/null +++ b/src/main/java/de/tlc4b/TLC4BOption.java @@ -0,0 +1,57 @@ +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; + } +} diff --git a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java index 2c0e37508b5a3db3c58d17397b95c7b809e77f6b..0749c2d1198704ef09ec8e46b6d7ac0f4c2f247d 100644 --- a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java @@ -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; diff --git a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java index 545e7f8d45042b63c500e85aaf417ef9369f74bd..502bceabf21419d8495e5401d9d81e81dbf56357 100644 --- a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java @@ -1,6 +1,6 @@ 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.*; diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java index 464541d563bd67220e1b1c996af28430f3d84df8..4b9d4d92fac48510214b64bbd98b19fb7f3e1a6d 100644 --- a/src/test/java/de/tlc4b/util/TestUtil.java +++ b/src/test/java/de/tlc4b/util/TestUtil.java @@ -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 {