These features are experimental. They are expected to work correctly but are not officially supported. If you are want, you can test them out and report your feedback on Github.

Also, other than experimental features, it's possible to tweak some of the default values using system properties.

These features are behind feature flags. The feature flags take the form of:

private boolean halt = !Boolean.getBoolean(TLC.class.getName() + ".nohalt");

They are stored in the program's properties and referenced with Boolean.getBoolean using the classname + a flag name.

To set a feature flag, using the -DParameter=value argument on java's cli.

Grep on the codebase for Boolean.getBoolean:

src/tlc2/output/MP.java:225:	private static final boolean DO_DEBUG = Boolean.getBoolean(MP.class.getName() + ".noDebug");
src/tlc2/output/MP.java:1699:    	if (Boolean.getBoolean(MP.class.getName() + ".warning2error")) {
src/tlc2/output/MP.java:1728:    	if (Boolean.getBoolean(MP.class.getName() + ".warning2error")) {
src/tlc2/output/MP.java:1814:    	if (Boolean.getBoolean(MP.class.getName() + ".noTimestamps")) {
src/tlc2/value/impl/LazyValue.java:82:	public static final boolean LAZYEVAL_OFF = Boolean.getBoolean(tlc2.value.impl.LazyValue.class.getName() + ".off");
src/tlc2/tool/impl/Tool.java:158:  private static final boolean PROBABILISTIC = Boolean.getBoolean(PROBABILISTIC_KEY);
src/tlc2/tool/impl/Tool.java:215:		if (mode == Mode.Simulation || mode == Mode.Executor || mode == Mode.MC_DEBUG || Boolean.getBoolean(TLCSTATEMUTEXT_KEY)) {
src/tlc2/tool/impl/Tool.java:1410:			if (Boolean.getBoolean(CDOT_KEY)) {
src/tlc2/tool/impl/Tool.java:2695:				if (Boolean.getBoolean(CDOT_KEY)) {
src/tlc2/tool/impl/Tool.java:3294:				if (Boolean.getBoolean(CDOT_KEY)) {
src/tlc2/tool/impl/SpecProcessor.java:796:		if (mode == Mode.Simulation || mode == Mode.MC_DEBUG || Boolean.getBoolean(Tool.TLCSTATEMUTEXT_KEY)) {
src/tlc2/tool/coverage/CostModelCreator.java:416:        if (Boolean.getBoolean(CostModelCreator.class.getName() + ".implied")) {
src/tlc2/tool/coverage/CostModelCreator.java:490:        if (Boolean.getBoolean(CostModelCreator.class.getName() + ".implied")) {
src/tlc2/tool/AbstractChecker.java:56:	public static boolean LIVENESS_TESTING_IMPLEMENTATION = Boolean.getBoolean(ILiveCheck.class.getName() + ".testing");
src/tlc2/tool/AbstractChecker.java:58:	protected static final boolean LIVENESS_STATS = Boolean.getBoolean(Liveness.class.getPackage().getName() + ".statistics");
src/tlc2/tool/distributed/TLCWorker.java:48:	private static final boolean unsorted = Boolean.getBoolean(TLCWorker.class.getName() + ".unsorted");
src/tlc2/tool/distributed/TLCServer.java:99:	private static final boolean VETO_CLEANUP = Boolean.getBoolean(TLCServer.class.getName() + ".vetoCleanup");
src/tlc2/tool/Simulator.java:129:			if (Boolean.getBoolean(Simulator.class.getName() + ".rl")) {
src/tlc2/tool/Simulator.java:133:			} else if (Boolean.getBoolean(Simulator.class.getName() + ".rlaction")) {
src/tlc2/tool/Simulator.java:948:		if (Boolean.getBoolean(Simulator.class.getName() + ".rl")) {
src/tlc2/tool/Simulator.java:950:		} else if (Boolean.getBoolean(Simulator.class.getName() + ".rlaction")) {
src/tlc2/tool/liveness/LiveCheck.java:594:			if (Boolean.getBoolean(LiveCheck.class.getName() + ".debug")) {
src/tlc2/tool/ModelChecker.java:55:	public static final boolean VETO_CLEANUP = Boolean.getBoolean(ModelChecker.class.getName() + ".vetoCleanup");
src/tlc2/tool/RLSimulationWorker.java:50:	protected static final boolean ENABLED_ONLY = Boolean.getBoolean(Simulator.class.getName() + ".rl.enabledOnly");
src/tlc2/tool/queue/IStateQueue.java:26:		if (Boolean.getBoolean(ModelChecker.class.getName() + ".BAQueue")) {
src/tlc2/TLC.java:186:    private boolean suspend = !Boolean.getBoolean(TLC.class.getName() + ".nosuspend");
src/tlc2/TLC.java:187:    private boolean halt = !Boolean.getBoolean(TLC.class.getName() + ".nohalt");
src/tlc2/TLC.java:1293:					TLCGlobals.tool || Boolean.getBoolean(TLC.class.getName() + ".asMilliSeconds")
src/tlc2/TLC.java:1333:		result.put("sched", Boolean.getBoolean(Simulator.class.getName() + ".rl") ? "RL" : "Random");
src/tla2sany/explorer/DotExplorerVisitor.java:62:	private final boolean includeLineNumbers = Boolean.getBoolean(DotExplorerVisitor.class.getName() + ".includeLineNumbers");

Grep on the codebase for Integer.getInteger:

src/tlc2/output/StatePrinter.java:15:	private static final int STATE_OVERWRITE_INTERVAL = Integer.getInteger(StatePrinter.class.getName() + ".overwrite", -1);
src/tlc2/value/impl/FcnRcdValue.java:35:	private static final int LINEAR_SEARCH_THRESHOLD = Integer.getInteger(FcnRcdValue.class.getName() + ".threshold", 32);
src/tlc2/value/Values.java:32:	private static int WIDTH = Integer.getInteger(Values.class.getName() + ".width", 80);
src/tlc2/tool/fp/OffHeapDiskFPSet.java:114:	private static final int PROBE_LIMIT = Integer.getInteger(OffHeapDiskFPSet.class.getName() + ".probeLimit", 1024);
src/tlc2/tool/fp/HeapBasedDiskFPSet.java:25:	protected static final int LogLockCnt = Integer.getInteger(DiskFPSet.class.getName() + ".logLockCnt", (31 - Integer.numberOfLeadingZeros(TLCGlobals.getNumWorkers()) + 8));
src/tlc2/tool/distributed/TLCTimerTask.java:26:	private static final int TIMEOUT = Integer.getInteger(TLCTimerTask.class.getName() + ".timeout", 60) * 1000;
src/tlc2/tool/distributed/TLCWorker.java:302:		final int numCores = Integer.getInteger(TLCWorker.class.getName()
src/tlc2/tool/distributed/TLCServer.java:89:	public static int Port = Integer.getInteger(TLCServer.class.getName() + ".port", 10997);
src/tlc2/tool/distributed/TLCServer.java:94:	private static final int REPORT_INTERVAL = Integer.getInteger(TLCServer.class.getName() + ".report", 1 * 60 * 1000);
src/tlc2/tool/distributed/TLCServer.java:105:	private static final int expectedFPSetCount = Integer.getInteger(TLCServer.class.getName() + ".expectedFPSetCount", 0);
src/tlc2/tool/distributed/selector/StaticBlockSelector.java:16:	private final static int BlockSize = Integer.getInteger(BLOCK_SIZE, 1024);
src/tlc2/tool/queue/DiskStateQueue.java:28:	private final static int BufSize = Integer.getInteger(DiskStateQueue.class.getName() + ".BufSize", 8192);
src/tlc2/tool/queue/DiskByteArrayQueue.java:46:	private final static int BufSize = Integer.getInteger(DiskStateQueue.class.getName() + ".BufSize", 8192);
src/tlc2/TLCGlobals.java:129:			.max(Math.abs(Integer.getInteger(TLC.class.getName() + ".progressInterval", 60)), 1) * 1000;
src/tlc2/TLCGlobals.java:132:	public static long chkptDuration = Integer.getInteger(
src/tlc2/TLCGlobals.java:268:		private static final int coverage = Integer.getInteger(TLCGlobals.class.getName() + ".coverage", 0);