diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index ed6d4f79766d717a0398f0f8109307b71ea16fd6..c00d21c0c4c83fd82c817716f76c191009bc3a4f 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -277,7 +277,16 @@ public class TLC4B { } int maxint = Integer.parseInt(args[index]); TLC4BGlobals.setMAX_INT(maxint); - } else if (args[index].toLowerCase().equals("-minint")) { + } else if (args[index].toLowerCase().equals("-default_setsize")) { + index = index + 1; + if (index == args.length) { + throw new TLC4BIOException( + "Error: Number requiered after option '-default_setsize'."); + } + int deferredSetSize = Integer.parseInt(args[index]); + TLC4BGlobals.setDEFERRED_SET_SIZE(deferredSetSize); + } + else if (args[index].toLowerCase().equals("-minint")) { index = index + 1; if (index == args.length) { throw new TLC4BIOException(