search

tlaplus / Examples

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

Minor correction of a comment #13

Closed sayyadabdi closed 4 years ago

sayyadabdi commented 4 years ago

Hi, I believe the comment in the spec Bakery.tla that says "MutualExclusion asserts that two distinct processes are in their critical sections." is problematic, because no two distinct processes are allowed to be in the critical sections at the same time.

muenchnerkindl commented 4 years ago

Thanks for spotting this – I fixed the typo.