3 ms·
@hwayne, thanks for the explanation. Can you explain how a time-step without a transaction is handled by the final TLA+ code? My confusion stems from: Next
by djoldman 2y ago
@hwayne, thanks for the explanation.
Can you explain how a time-step without a transaction is handled by the final TLA+ code?
My confusion stems from:
Next ==
AliceToBob
\/ BobToAlice
...so does it matter which "pathway is taken"? This reminds me of context free grammars / PEG grammars.
- sriram_malhar 2y agoNo, it doesn’t matter. All paths are explored
- itishappy 2y agoSame question. Is stuttering now handled by the next line somehow? Spec == Init /\ [][Next]_vars Edit: Answered in the paragraph below the TLA+ code: > The only thing that's "unusual" (besides == for definition) is the [][Next]_vars bit. That's TLA+ notation for [](Next || Stutter): Next or Stutter always happens. I guess the `_vars` notation is shorthand for stutter. Anyone know where I can learn more?
- Tomte 2y agoThe TLA+ book, freely available online: https://lamport.azurewebsites.net/tla/book.html https://lamport.azurewebsites.net/tla/book.html
- deleted 2y ago[deleted]