[tlaplus] Important TLC Bugfix: Upgrade Recommended

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

A rare yet severe bug in TLC has been identified and resolved. This bug was present in the initial implementation of TLC. It could have caused TLC to generate an incorrect set of initial states, or an incorrect set of possible next states when examining a state. Either issue might have resulted in TLC not examining all reachable states. Technical details can be found at issue #798 [1].

Users can verify if they have been affected by the bug by running TLC with the Java system property `-Dtlc2.value.impl.LazyValue.off=true` and observing whether the number of initial and distinct states changes. However, please note that disabling LazyValue may lead to significant performance degradation.

We strongly recommend that all users upgrade to the 1.7.3 maintenance release [2]. Regrettably, we are unable to provide Toolbox maintenance releases. Instead, we advise users to switch to the latest 1.8.0 build [3]. In addition, the most recent TLA+ VSCode nightly build [4] also includes the bugfix.

Markus

[1] https://github.com/tlaplus/tlaplus/issues/798
[2] https://github.com/tlaplus/tlaplus/releases/tag/v1.7.3
[3] https://github.com/tlaplus/tlaplus/releases/tag/v1.8.0
[4] https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus-nightly

-- 
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/1BC48D98-0F6C-4922-87CE-738F966ACEF5%40lemmster.de.