search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

Add CRDT-Bug and asyncio-lock examples #38

Closed Alexander-N closed 3 years ago

Alexander-N commented 3 years ago

https://github.com/Alexander-N/tla-specs/issues/1

muenchnerkindl commented 3 years ago

Thank you for your nice contributions! I am happy to merge your PR, but I'd suggest that you add a few comments to the specs illustrating the CRDT bug, for your own benefit and that of others.

Alexander-N commented 3 years ago

Thanks for the feedback. Don't you feel that this would simply duplicate information from the readme? Since these are direct translations of the pseudocode all context is contained in the twitter thread. Maybe I can add some comments to make the mapping to the pseudocode more explicit?

muenchnerkindl commented 3 years ago

Of course this was just a suggestion, and it is entirely up to you. I was mainly thinking of explaining the relationship between the pseudocode and the TLA spec, as well as highlighting the changes in the fixed version. In my experience, one entirely forgets about the details of the spec after a few months.