-
Notifications
You must be signed in to change notification settings - Fork 37
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
TLCExtTest.java fails when running on Java 1.8 #34
Comments
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 |
Hunn, which steps did you took to find this message? Added
Oh, are these statistics directly from the users who use the toolbox/VSCode? So can we deprioritize the 1.8 issues found? |
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. |
Outdated |
When running
ant test
(withshowoutput="yes"
) on Java 1.8 (assuming that #31 is fixed),TLCExtTest.java
failsWe 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?The text was updated successfully, but these errors were encountered: