[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ Toolbox 1.5.5 release - warning incomplete bug fix


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.


[1] http://lamport.azurewebsites.net/tla/toolbox-1-5-5.html