Alloy traces visualiser and animator
1. Objective
The Alloy visualiser, available in the Alloy analyzer tool, provides support for introspection of traces. This tool, Anima improves the issues identified in the default visualiser, by employing layout and animation algorithms in order to create systematic and consistent representations.
2. Instructions
It is possible to both explore the provided examples, or upload a trace and a specification file. See instructions below.
Examples
Three examples are provided to illustrate some features of the tool. In order to explore them, select them, under "Examples".
- Farmer (Linear layouts) - Representation of the classical farmer example resorting to linear layouts.
- Line switching trains (Linear layout) - This example shows the use of linear layouts in order to represent trains switching lines, in an ERTMS inspired example.
- Chord (circular + tree layouts) - This example shows the usage of circular and tree layouts to display, while using objects of the same kind in different layout managers.
Uploading a trace and a spec
It is possible to upload a trace and a specification file to render. The trace is a XML file, which should be exported by the Alloy analyser. The specification file corresponds to a JSON file which describes how the elements should be organized. Below you can download an example of a (JSON) specification and a (XML) trace, of the Trains example.
Once downloaded, extract the file, select "Open Trace" in the anima tool, and provide the XML file. Next, select "Open Spec" to upload the JSON specification file, and the tool will process both files to create a representation.
Sample input3. Publications
Improving the Visualization of Alloy Instances - TBPImproving traces visualisation through layout managers - TBP
Contact-me at rui(dot)couto(at)di(dot)uminho(dot)pt