using:generating_animation

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:

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

Without the Toolbox, something similar to this:

  1. Check model BlockingQueue.cfg with java -jar tla2tools.jar -deadlock -generateSpecTE BlockingQueue (‘-generateSpecTE’ causes TLC to generate SpecTE.tla/.cfg)
  2. State trace expression Animation (BlockingQueueAnim.tla)in SpecTE.tla
  3. Download https://github.com/tlaplus/CommunityModules/releases/download/20200107.1/CommunityModules-202001070430.jar
  4. Check SpecTE with java -jar tla2tools.jar:CommunityModules-202001070430.jar tlc2.TLC SpecTE
  5. Copy trace into http://localhost:10996/files/animator.html (minor format changes needed)
  • using/generating_animation.txt
  • Last modified: 2024/09/28 15:58
  • by 127.0.0.1