TLCExtTest.java fails when running on Java 1.8 #34
Description
When running ant test (with showoutput="yes") on Java 1.8 (assuming that #31 is fixed), TLCExtTest.java fails
[junit] Running tlc2.overrides.TLCExtTest
[junit] TLC2 Version 2.15 of Day Month 20?? (rev: 674ca73)
[junit] Running breadth-first search Model-Checking with fp 0 and seed 1 with 1 worker on 4 cores with 3516MB heap and 0MB offheap memory (Linux 4.15.0-128-generic amd64, Private Build 1.8.0_275 x86_64, OffHeapDiskFPSet, DiskStateQueue).
[junit] Parsing file /home/rafael/dev/CommunityModules/tests/IncompleteStates.tla
[junit] Parsing file /tmp/TLCExt.tla
[junit] Parsing file /tmp/TLC.tla
[junit] Parsing file /tmp/Naturals.tla
[junit] Parsing file /tmp/Sequences.tla
[junit] Parsing file /tmp/FiniteSets.tla
[junit] Semantic processing of module Naturals
[junit] Semantic processing of module Sequences
[junit] Semantic processing of module FiniteSets
[junit] Semantic processing of module TLC
[junit] Semantic processing of module TLCExt
[junit] Semantic processing of module IncompleteStates
[junit] Starting... (2021-01-07 23:32:24)
[junit] Computing initial states...
[junit] Finished computing initial states: 1 distinct state generated at 2021-01-07 23:32:24.
[junit] Model checking completed. No error has been found.
[junit] Estimates of the probability that TLC did not check all reachable states
[junit] because two distinct states had the same fingerprint:
[junit] calculated (optimistic): val = 5.4E-20
[junit] The coverage statistics at 2021-01-07 23:32:24
[junit] <Init line 7, col 1 to line 7, col 4 of module IncompleteStates>: 1:1
[junit] line 8, col 3 to line 11, col 13 of module IncompleteStates: 1
[junit] <Next line 13, col 1 to line 13, col 4 of module IncompleteStates>: 0:1
[junit] line 14, col 6 to line 14, col 19 of module IncompleteStates: 1
[junit] End of statistics.
[junit] 2 states generated, 1 distinct states found, 0 states left on queue.
[junit] The depth of the complete state graph search is 1.
[junit] The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
[junit] Finished in 00s at (2021-01-07 23:32:24)
[junit] Tests run: 1, Failures: 2, Errors: 0, Skipped: 0, Time elapsed: 0,539 secWe can see that there is no overriding of the TLCExt by its java counterpart, so I assume that there is some difference at the loading of overriding modules between different JVMs, is this intentional?