will62794/tlaplus_animation

Document invariants of the examples

lemmy opened this issue · 0 comments

lemmy commented

What invariants should TLC check for LogVisibility, Raft and Elevator in order to produce an interesting animation?