TLCExtTest.java fails when running on Java 1.8

[pfeodrippe]

When running ant test (with showoutput="yes") on Java 1.8 (assuming that https://github.com/tlaplus/CommunityModules/issues/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 sec

We 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?

[pfeodrippe]

When running on Java 9, it shows success (and you can see the loading of the overriding modules).

    [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 [pid: 20010] (Linux 4.15.0-128-generic amd64, Ubuntu 11.0.9.1 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:09:21)
    [junit] Loading TLCExt!Trace operator override from jar:file:/home/rafael/dev/CommunityModules/dist/CommunityModules-20210172309.jar!/tlc2/overrides/TLCExt.class with signature: <Java Method: public static synchronized tlc2.value.impl.Value tlc2.overrides.TLCExt.getTrace(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel) throws java.io.IOException>.
    [junit] Loading TLCExt!AssertError operator override from jar:file:/home/rafael/dev/CommunityModules/dist/CommunityModules-20210172309.jar!/tlc2/overrides/TLCExt.class with signature: <Java Method: public static synchronized tlc2.value.impl.Value tlc2.overrides.TLCExt.assertError(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel)>.
    [junit] Loading TLCExt!PickSuccessor operator override from jar:file:/home/rafael/dev/CommunityModules/dist/CommunityModules-20210172309.jar!/tlc2/overrides/TLCExt.class with signature: <Java Method: public static synchronized tlc2.value.impl.Value tlc2.overrides.TLCExt.pickSuccessor(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel)>.
    [junit] Loading TLCExt!TraceFrom operator override from jar:file:/home/rafael/dev/CommunityModules/dist/CommunityModules-20210172309.jar!/tlc2/overrides/TLCExt.class with signature: <Java Method: public static synchronized tlc2.value.impl.Value tlc2.overrides.TLCExt.getTraceFrom(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel) throws java.io.IOException>.
    [junit] Loading TLCExt!TLCDefer operator override from jar:file:/home/rafael/dev/CommunityModules/dist/CommunityModules-20210172309.jar!/tlc2/overrides/TLCExt.class with signature: <Java Method: public static tlc2.value.impl.Value tlc2.overrides.TLCExt.tlcDefer(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel)>.
    [junit] Computing initial states...
    [junit] Error: Attempted to apply the operator overridden by the Java method
    [junit] public static synchronized tlc2.value.impl.Value tlc2.overrides.TLCExt.getTrace(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel) throws java.io.IOException,
    [junit] but it produced the following error:
    [junit] In evaluating TLCExt!Trace, the state is not completely specified yet (variables v, w undefined).
    [junit] Error: The error occurred when TLC was evaluating the nested
    [junit] expressions at the following positions:
    [junit] 0. Line 8, column 3 to line 11, column 13 in IncompleteStates
    [junit] 1. Line 8, column 6 to line 8, column 11 in IncompleteStates
    [junit] 2. Line 9, column 6 to line 9, column 10 in IncompleteStates
    [junit] 
    [junit] 
    [junit] The coverage statistics at 2021-01-07 23:09:21
    [junit] <Init line 7, col 1 to line 7, col 4 of module IncompleteStates>: 0:0
    [junit] <Next line 13, col 1 to line 13, col 4 of module IncompleteStates>: 0:0
    [junit]   line 14, col 6 to line 14, col 19 of module IncompleteStates: 0
    [junit] End of statistics.
    [junit] 0 states generated, 0 distinct states found, 0 states left on queue.
    [junit] The depth of the complete state graph search is 1.
    [junit] Finished in 00s at (2021-01-07 23:09:21)
    [junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0,776 sec

[lemmy]

Yikes, class file format incompatibilities: java.lang.ClassCastException: tlc2.overrides.TLCOverrides cannot be cast to tlc2.overrides.ITLCOverrides in TLC's tlc2.tool.impl.SpecProcessor.processSpec(Mode) when loading the CommunityModules TLCOverrides class file.

The fix is likely to make the builds of the CommunityModules and TLC compatible such that they produce matching class files. Looking at the stats, this has very low priority.

[pfeodrippe]

Yikes, class file format incompatibilities: java.lang.ClassCastException: tlc2.overrides.TLCOverrides cannot be cast to tlc2.overrides.ITLCOverrides in TLC's tlc2.tool.impl.SpecProcessor.processSpec(Mode) when loading the CommunityModules TLCOverrides class file.

Hunn, which steps did you took to find this message? Added -debug to the tlc CLI execution?

The fix is likely to make the builds of the CommunityModules and TLC compatible such that they produce matching class files. Looking at the stats, this has very low priority.

Oh, are these statistics directly from the users who use the toolbox/VSCode? So can we deprioritize the 1.8 issues found?

[lemmy]

I debugged TLC in Eclipse. The stats are reported by TLC if a user has opted into execution statistics. Fixing compatibility with 1.8 has low priority because of the stats, but let's make sure we don't add additional incompatibilities.

[lemmy]

Outdated