using:experimental

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision		 Previous revision
using:experimental [2024/11/14 10:37] – created fponziusing:experimental [2024/11/17 13:00] (current) – fponzi
Line 1: Line 1:
 ====== Experimental Features ====== ====== Experimental Features ======
-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 +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. 
 + 
 +===== How they work ===== 
 +These features are behind feature flags. The feature flags take the form of: 
 +<code> 
 +private boolean halt = !Boolean.getBoolean(TLC.class.getName() + ".nohalt"); 
 +</code> 
 + 
 +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. 
 + 
 +====== Unsorted List of Features ====== 
 + 
 +Grep on the codebase for Boolean.getBoolean: 
 +<code> 
 +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"); 
 +</code> 
 +Grep on the codebase for Integer.getInteger: 
 +<code> 
 +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); 
 +</code> 
 + 
  • using/experimental.1731580672.txt.gz
  • Last modified: 2024/11/14 10:37
  • by fponzi