tlaplus_animation

tlaplus_animation copied to clipboard

One-liner to quickly generate long animations with new `Alias` feature

1

https://github.com/tlaplus/tlaplus/issues/485  `java -cp /opt/toolbox/tla2tools.jar:CommunityModules.jar tlc2.TLC -simulate num=1 -depth 32001 -config AsyncGameOfLife.cfg AsyncGameOfLifeAnim.tla | grep anim | sed 's;anim = ;anim |-> ;g' | xclip` With 32.000 states/frames,...

lemmy

FWIW: Traces with ~2000 states become very sluggish in Chrome. Use Firefox instead!

lemmy

FYI: With TLC nightly, a ```CommunityModules.jar``` will automatically be loaded if it is located in the same folder as ```tla2tools.jar```. This removes the need to reference a specific version of...

lemmy

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

lemmy