This page gives a quick introduction to Sterling’s features. As it is under active development, expect this page to change as new features are added and existing ones are tweaked.

This tour is for version 0.3.0.

Alloy

Sterling is built on top of Alloy 5.0.0.1, making only a few minor changes to the Alloy interface to support a connection to the browser. Aside from these changes, the Alloy side of Sterling is identical to Alloy itself. Additionally, users of Sterling are not required to visualize instances using the Sterling visualizer, as the default Alloy visualizer is still included.

Note the message Visualization server running: http://localhost:45441. You can click this link to open the Sterling visualizer in the browser, or you can wait to open it from the built-in Alloy visualizer. Also note that the port is chosen automatically and changes each time Sterling is opened.

Upon generating an instance and opening the Alloy visualizer (as seen above), the user may open the Sterling visualizer by clicking the Web button located in the toolbar to the left of the Theme button.

Sterling Visualizer

The Sterling visualizer provides a user interface that is similar to the built-in Alloy visualizer. There are four tabs:

  • Graph: A snapshot view of the instance
  • Table: A set of tables showing all relations in the instance
  • Tree: A tree showing the hierarchical structure of the instance
  • Source: All source code files used to generate the instance

Additionally, there is a Next button that allows the user to step through solutions directly from the browser. When the visualizer is opened without Alloy having generated an instance, each tab will be empty, as seen in the image above.

Each time a new instance is generated by Alloy, the data in the visualizer will update to show the new instance in all four tabs.

Graph View

The graph view is similar to the existing Alloy visualizer Viz tab, with two major exceptions: (1) the view is a “snapshot” as defined in Daniel Jackson’s Software Abstractions rather than just a directed graph, and as a result, (2) the layout algorithm is different.

This means that while sometimes at first glance it may seem as though the visualizations are the same, it is likely that they aren’t.

Currently, interactivity with the Graph view is limited to zooming and panning using the mouse. While edge labels will likely be cluttered, they will be highlighted in the same that they are in the Alloy visualizer when hovered over.

Projections are also supported by Sterling. By clicking the + button and selecting a signature, a new projection is added to the toolbar. Choose the atom to project over by either clicking the current atom to show a dropdown menu or by clicking the left or right arrows to step through.

Table View

The table view simply displays all of the atoms and relations in an instance as a set of tables.

There are currently three options for customizing the display of the tables.

  • Compact View/Normal View: Update the cell spacing to show more or less compact tables
  • Show/Hide Built-in Signatures: Display built-in signatures such as Int
  • Show/Hide Empty Tables: Display tables that have no rows

Tree View

The tree view displays the instance as a hierarchical tree, the nodes of which can be expanded and collapsed by clicking. Panning and zooming are also supported.

Source View

The source view simply provides the user with all of the Alloy source files used to generate the instance. These files are not editable, and only serve as a convenient way to refer back to the models.