Skip to content

Commit

Permalink
Enable TLC's Java Assertions
Browse files Browse the repository at this point in the history 
Related to tlaplus/tlaplus#971
  • Loading branch information
@lemmy
lemmy authored Jul 16, 2024
1 parent d04f2b9 commit 590b0da
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions .github/scripts/tla_utils.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,7 @@ def check_model(
else:
tlc = subprocess.run([
'java',
'-enableassertions',
'-Dtlc2.TLC.ide=Github',
'-Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff',
'-XX:+UseParallelGC',
Expand Down

4 comments on commit 590b0da

@lemmy
Copy link
Member Author

@lemmy lemmy commented on 590b0da Jul 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems to have done nothing because aba_asyn_byz did not fail where is fails with an assertion violation (see https://github.com/tlaplus/Examples/actions/runs/9966962447/job/27539889230).

2024-07-16T22:51:03.7264870Z INFO:root:specifications\aba-asyn-byz\aba_asyn_byz.cfg
2024-07-16T22:51:08.8068184Z DEBUG:root:TLC2 Version 2.18 of Day Month 20?? (rev: fe8a2e3)
2024-07-16T22:51:08.8070296Z Running breadth-first search Model-Checking with fp 98 and seed 2926297100743383550 with 4 workers on 4 cores with 3641MB heap and 64MB offheap memory [pid: 4400] (Windows Server 2022 10.0 amd64, Eclipse Adoptium 17.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
2024-07-16T22:51:08.8071824Z Parsing file D:\a\Examples\Examples\specifications\aba-asyn-byz\aba_asyn_byz.tla
2024-07-16T22:51:08.8072641Z Parsing file D:\a\Examples\Examples\specifications\aba-asyn-byz\Naturals_UnicodeShim.tla
2024-07-16T22:51:08.8073987Z Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-2902685652457895635\_TLCTrace.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
2024-07-16T22:51:08.8075751Z Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-2902685652457895635\Naturals.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
2024-07-16T22:51:08.8077405Z Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-2902685652457895635\TLC.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
2024-07-16T22:51:08.8079181Z Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-2902685652457895635\TLCExt.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
2024-07-16T22:51:08.8081134Z Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-2902685652457895635\Sequences.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
2024-07-16T22:51:08.8082926Z Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-2902685652457895635\FiniteSets.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
2024-07-16T22:51:08.8086088Z Parsing file C:\Users\runneradmin\AppData\Local\Temp\tlc-2902685652457895635\Integers.tla (jar:file:/D:/a/Examples/Examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
2024-07-16T22:51:08.8087786Z Semantic processing of module Naturals
2024-07-16T22:51:08.8088434Z Semantic processing of module Naturals_UnicodeShim
2024-07-16T22:51:08.8089103Z Semantic processing of module Sequences
2024-07-16T22:51:08.8089697Z Semantic processing of module FiniteSets
2024-07-16T22:51:08.8090308Z Semantic processing of module TLC
2024-07-16T22:51:08.8090871Z Semantic processing of module Integers
2024-07-16T22:51:08.8091448Z Semantic processing of module TLCExt
2024-07-16T22:51:08.8092022Z Semantic processing of module _TLCTrace
2024-07-16T22:51:08.8092621Z Semantic processing of module aba_asyn_byz
2024-07-16T22:51:08.8093295Z Starting... (2024-07-16 22:51:04)
2024-07-16T22:51:08.8094054Z Implied-temporal checking--satisfiability problem has 3 branches.
2024-07-16T22:51:08.8094788Z Computing initial states...
2024-07-16T22:51:08.8095228Z Computed 2 initial states...
2024-07-16T22:51:08.8095670Z Computed 4 initial states...
2024-07-16T22:51:08.8096152Z Computed 8 initial states...
2024-07-16T22:51:08.8097133Z Finished computing initial states: 16 distinct states generated at 2024-07-16 22:51:04.
2024-07-16T22:51:08.8098524Z Progress(8) at 2024-07-16 22:51:07: 209,695 states generated (209,695 s/min), 26,407 distinct states found (26,407 ds/min), 12,434 states left on queue.
2024-07-16T22:51:08.8099636Z 
2

@ahelwer
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does this mean? You expected it to fail with an assertion but it did not?

@lemmy
Copy link
Member Author

@lemmy lemmy commented on 590b0da Jul 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, aba_asyn_byz should have encountered an assertion violation. The new manual workflow does encounter the violation:

+ echo Check specifications/aba-asyn-byz/aba_asyn_byz
+ java -ea -XX:+UseParallelGC -Dtlc2.TLC.stopAfter=180 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa[7](https://github.com/tlaplus/Examples/actions/runs/9966962447/job/27539889230#step:6:8)0d124d0c77ffff -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -tool -deadlock specifications/aba-asyn-byz/aba_asyn_byz
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.18 of Day Month 20?? (rev: fe8a2e3)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 120 and seed 69[8](https://github.com/tlaplus/Examples/actions/runs/9966962447/job/27539889230#step:6:9)7530359890376924 with 4 workers on 4 cores with 3552MB heap and 64MB offheap memory [pid: 1682] (Linux 6.5.0-1023-azure amd64, Eclipse Adoptium 11.0.23 x86_64, MSBDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/runner/work/Examples/Examples/specifications/aba-asyn-byz/aba_asyn_byz.tla
Parsing file /tmp/tlc-5700282884470[9](https://github.com/tlaplus/Examples/actions/runs/9966962447/job/27539889230#step:6:10)01973/Naturals.tla (jar:file:/home/runner/work/Examples/Examples/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module aba_asyn_byz
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2024-07-17 02:05:45)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 3 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 4 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 8 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 16 distinct states generated at 2024-07-17 02:05:46.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(8) at 2024-07-17 02:05:49: 233,228 states generated (233,228 s/min), 28,527 distinct states found (28,527 ds/min), 12,814 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(20) at 2024-07-17 02:06:49: [10](https://github.com/tlaplus/Examples/actions/runs/9966962447/job/27539889230#step:6:11),855,705 states generated (10,622,477 s/min), 946,907 distinct states found (918,380 ds/min), 206,319 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(22) at 2024-07-17 02:07:49: 21,524,282 states generated (10,668,577 s/min), 1,788,269 distinct states found (841,362 ds/min), 332,004 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(24) at 2024-07-17 02:08:45: 31,578,075 states generated (10,053,793 s/min), 2,528,385 distinct states found (740,[11](https://github.com/tlaplus/Examples/actions/runs/9966962447/job/27539889230#step:6:12)6 ds/min), 398,887 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(24) at 2024-07-17 02:08:45: 31,578,075 states generated, 2,528,385 distinct states found, 398,887 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the complete state space with 6992354 total distinct states at (2024-07-17 02:08:45)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 1000:1 @!@!@
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.AssertionError
java.lang.AssertionError
	at tlc2.tool.liveness.LiveWorker.checkSccs(LiveWorker.java:452)
	at tlc2.tool.liveness.LiveWorker.call(LiveWorker.java:1281)
	at tlc2.tool.liveness.LiveWorker.call(LiveWorker.java:42)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
	at java.base/java.lang.Thread.run(Thread.java:829)

@!@!@ENDMSG 1000 @!@!@

@ahelwer
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I see - aba-asyn-byz is marked as a large model (ten minute runtime) so is run as part of the smoke testing script; each model is only run for five seconds then terminated, so it did not reach the assertion.

Please sign in to comment.