Defining Animations for a Spec

Spectacle currently provides support for creating animations of specifications in a relatively simple and ergonomic manner. If you want to create an animation for a specification Spec.tla, the recommended way is to create a separate file Spec_anim.tla that extends Spec and contains the animation definition. This convention allows visualizations to be defined separately from a main spec, avoiding pollution of standard specifications with visualization specific details. If such an adjacent animation spec file exists, the tool will attempt to automatically load it and use it as the animation for your spec.

An animation can then be defined by creating an AnimView definition in your Spec_anim.tla file that is an expression producing an SVG element as a function of your spec's state variables. You can see a simple example of in the lockserver.tla and lockserver_anim.tla specs. Note that you can also define an AnimView animation definition inline, right in your existing spec if you desire. This will also be automatically detected and loaded as a visualization in the trace explorer. If such an inline animation exists, this will take precedence over any external animations defined in an accompanying Spec_anim.tla file.

SVG Description Language

For defining SVG elements as part of your animation view expression (AnimView), you can currently use the existing definitions in the SVG module, which can be automatically extended to include the definitions contained there. There are also some experimental additions to these raw SVG elements that allow for higher level visualization constructs like directed graphs (see example), some of which may be modified or extended in the future.