TLC Liveness Checking Error-Reporting Bug
41 views
Skip to first unread message
Leslie Lamport
Apr 21, 2020, 7:10:03 PM4/21/20
to tlaplus
Because of a bug that has existed for many years, if TLC runs out of memory or
another resource while checking liveness, then it produces the correct error
message but exits normally, without producing an error code. The Toolbox
displays no error warning when this happens, and you have to look carefully
at the Model Results page to see that TLC did not complete successfully.
When run from a command line with no options that cause TLC to produce extra
output, the error message should be easy to see. A shell script that runs TLC
will probably not report the error. This bug has been fixed in the nightly
build and will be fixed in the next release.
another resource while checking liveness, then it produces the correct error
message but exits normally, without producing an error code. The Toolbox
displays no error warning when this happens, and you have to look carefully
at the Model Results page to see that TLC did not complete successfully.
When run from a command line with no options that cause TLC to produce extra
output, the error message should be easy to see. A shell script that runs TLC
will probably not report the error. This bug has been fixed in the nightly
build and will be fixed in the next release.
Reply all
Reply to author
Forward
0 new messages