|
Hi, the seriousness of the bug warrants a dedicated webpage [1] which describes the bug and outlines a workaround. Please note that we have also been able to reproduce the bug in the scope of the next-state relation. In other words, this bug can cause TLC to generate an incorrect set of initial states, or an incorrect set of possible next states when examining a state. Either can cause TLC to not examine all reachable states. Thanks Markus [1] http://lamport.azurewebsites.net/tla/toolbox-1-5-5.html |