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

Open lemmy opened this issue 5 years ago • 1 comments

https://github.com/tlaplus/tlaplus/issues/485

Peek 2020-07-09 17-55

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, Firefox/Chrome becomes the bottleneck. TLC simulator takes ~1 minute.

Jul 10 '20 00:07 lemmy

Another variant that renders the animation with ffmpeg instead of a browser: https://github.com/lemmy/tlaplus_specs/blob/908abbb9c3e61ba504643a4a51717cc2f854ee74/AsyncGameOfLifeAnimGlider.tla#L25-L41

Jul 15 '20 15:07 lemmy