====== Generating Animations of State Changes ======

Writing animation specifications is straightforward. There is a module that provides TLA+ definitions of SVG primitives. Below are a few examples. The first three are for TLC, and the other ones are for Will Schultz’s TLA-web. Despite being for different systems, the definitions are quite similar.

  * https:%%//%%github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998_anim.tla
  * https:%%//%%github.com/tlaplus/Examples/blob/master/specifications/ewd687a/EWD687a_anim.tla
  * https:%%//%%github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840_anim.tla
  * https:%%//%%github.com/will62794/tla-web/blob/master/specs/EWD998.tla#L123-L201
  * https:%%//%%github.com/will62794/tla-web/blob/master/specs/AbstractRaft_anim.tla#L210-L280

The animations can be created in the Toolbox with:

  - Check model BlockingQueue.cfg
  - Set ''%%Animation%%'' as the trace expression in the Error-Trace console
  - Hit Explore and export/copy the resulting trace to clipboard
  - Paste into http:%%//%%localhost:10996/files/animator.html

Without the Toolbox, something similar to this:

  - Check model BlockingQueue.cfg with ''%%java -jar tla2tools.jar -deadlock -generateSpecTE BlockingQueue%%'' (‘-generateSpecTE’ causes TLC to generate SpecTE.tla/.cfg)
  - State trace expression ''%%Animation%%'' (BlockingQueueAnim.tla)in SpecTE.tla
  - Download https:%%//%%github.com/tlaplus/CommunityModules/releases/download/20200107.1/CommunityModules-202001070430.jar
  - Check SpecTE with ''%%java -jar tla2tools.jar:CommunityModules-202001070430.jar tlc2.TLC SpecTE%%''
  - Copy trace into http:%%//%%localhost:10996/files/animator.html (minor format changes needed)