hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
185 stars 39 forks source link

Clarify model for the threads example #30

Closed ramz-san closed 1 year ago

ramz-san commented 2 years ago

For the threads example in the concurrency section there is no indication on how assign the constant NULL when running the model after adding the lock. I think it might be a good idea to explicitly state how to run the model.

If I understand correctly both assigning a model variable or an ordinary assignment of, say, -1 would work equally well in this case, but the model variable would be preferable. If that's the case it might also be a good idea to explain the difference between both possibilities.

hwayne commented 1 year ago

I'll make some updates!