lemmy opened this issue 7 years ago · 0 comments
What invariants should TLC check for LogVisibility, Raft and Elevator in order to produce an interesting animation?