Same question. Is stuttering now handled by the next line somehow? Spec == Init /\ [][Next]_vars Edit: Answered in the paragraph below the TLA+ code: > T

Same 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?