[tlaplus] TLC Liveness Checking Error-Reporting Bug

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

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.  

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d04d6f4c-c19a-4d43-9741-feacd9dfa8c4%40googlegroups.com.