I like this method of explanation; I think it helps with getting an intuition for how time is implicit in TLA+. Quantifying over t: Time seems like it makes sense once you've introduced quantifiers, and then you can motivate priming as a straightforward followup from that.
Possible typo in the code block after introducing priming; right now it says
Transfer =
some value in 1..=alice:
1. alice' = alice
2. bob' = bob
Should that be
1. alice' = alice + value
2. bob' = bob - value
?
I like this method of explanation; I think it helps with getting an intuition for how time is implicit in TLA+. Quantifying over
t: Timeseems like it makes sense once you've introduced quantifiers, and then you can motivate priming as a straightforward followup from that.Possible typo in the code block after introducing priming; right now it says
Transfer = some value in 1..=alice: 1. alice' = alice 2. bob' = bobShould that be1. alice' = alice + value 2. bob' = bob - value?