.. _viz-customization: .. index:: instance; visualization Visualization customization =========================== The visualizer provided by the Analyzer is one of the most popular features of Alloy, since it allows the inspection and navigation of scenarios or counter-examples. However, as models become more complex, the interpretation of instances becomes more challenging. To ease this process, the visualizer allows the graphical visualization of instances to be customized through themes. Theme customization -------------------- Let us get back to our file system example from the :ref:`structural-modeling` chapter and focus on an instance generated by command :alloy:`example`. With the default visualization of the instances, it looks as follows. .. image:: instance1.png :width: 400 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_01/filesystem.als#L66-L77 :alt: Get the code to generate this instance. .. index:: Theme button Show as attribute option Show as arcs option To customize it, we can open the theme customization menu, by pressing the button :guilabel:`Theme` in the toolbar of the instance visualizer pop-up window. The first customization we will apply is to show the names of directory entries as attributes in the respective atoms, instead of using arrows pointing to the name. This will unclutter substantially the depiction and is a very common customization for fields of multiplicity :alloy:`one`, in particular for fields that somehow act as identifiers, as is the case of :alloy:`name`. To do so, first select the field :alloy:`name`, and then tick the :guilabel:`Show as attribute` option in the top pane. This option will show the name of an entry as an attribute but still keep the respective arrows. To remove them, tick twice :guilabel:`Show as arcs` to choose the :guilabel:`Off` option. Your theme options for relation :alloy:`name` should look as follows. .. image:: theme1.png :width: 700 px :align: center .. index:: Apply button Close button By pressing :guilabel:`Apply` in the toolbar and then :guilabel:`Close` the instance will now be depicted as follows. .. image:: instance2.png :width: 450 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_02/filesystem.als#L66-L77 :alt: Get the code to generate this instance. .. index:: Show option We now have some unconnected :alloy:`Name` atoms. Since names were only used in directory entries, where they are now shown as attribute, we can remove them from the graph. To do so, select :guilabel:`Theme` again (actually when changing many options it is better to keep the theme customization menu open and just keep pressing :guilabel:`Apply` without closing it to see the effect), select the :alloy:`Name` signature, and then tick the :guilabel:`Show` option twice to choose the :guilabel:`Off` option. After pressing :guilabel:`Apply` the :alloy:`Name` atom will disappear. .. image:: theme2.png :width: 700 px :align: center .. index:: Node Color Palette option Edge Color Palette option Another common customization is to give different colors (or different shapes and borders) to atoms belonging to different signatures. First, we will select a different color palette, with more subdued colors. To do so, select the :guilabel:`general graph settings`, and then select the :guilabel:`Martha` palette both for node and edge colors. After pressing :guilabel:`Apply` we will get some nice faded colors. .. image:: theme3.png :width: 700 px :align: center Notice that since version 6.2 of Alloy, the visualizer features a colorblind-friendly palette called :guilabel:`Tol`, inspired by (but not completely equivalent to) one of Paul Tol's `color schemes `_. Since entries are auxiliary structures in defining the (supposedly) tree-like structure of the file system, we will paint them gray. To do so select signature :alloy:`Entry`, then the color :guilabel:`Gray` in the drop-down menu in the top left-hand corner, and finally :guilabel:`Apply`. .. image:: theme4.png :width: 700 px :align: center For file system objects we will choose a more eye-catching red color. We don't have to set this color separately for signatures :alloy:`Dir`, :alloy:`Root` and :alloy:`File`. By default most theme options of extension signatures are set as :guilabel:`Inherited` from their parent signature. As such, it suffices to set the color red for the :alloy:`Object` signature, and both their children will inherit this setting. You also have the option to set the color to :guilabel:`Magic`, which will assign a different color to each extension signature, instead of the default yellow. That is actually the default setting for the color of edges, as you can see by the colors of `entries` and `object`. Finally we will choose different shapes for different file system objects. Let's keep files as rectangles, but choose the shape :guilabel:`Trapezoid` for directories and a :guilabel:`House` for the root. The shape can be chosen in the drop-down menu in the top right-hand corner. The combo-box to the left of that one allows changing the style of the border. After pressing :guilabel:`Apply` we have the following visualization. .. image:: theme5.png :width: 700 px :align: center One last customization that is often useful is to change the label of an element in the graph, be it a signature, a subset or relation (for instance, to make it shorter, or to remove the namespace prepended to elements from imported modules). This can be changed in the text box in the top left-hand corner after selecting an element. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/visualization/theme-customization :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. Managing themes --------------- .. index:: Reset theme menu option Save theme menu option For the moment these are all the customizations we will use, and so we can close the theme customization menu. Notice that you can always reset your theme settings by going to the menu option :menuselection:`Theme --> Reset theme`. You can also save your theme for later use in the option :menuselection:`Theme --> Save theme`. Occasionally it is also useful to have multiple themes for the same model, highlighting different facets of the instances. .. index:: Magic Layout button Instead of customizing manually your theme, you can also try out the :guilabel:`Magic Layout` button in the toolbar of the instance visualizer. This will "magically" choose options for visualizing the different elements of your specification based on the signature and field declarations. Sometimes the results are good enough and it will save you some work. The result of magic layout for our instance is the following. .. image:: instance3.png :width: 500 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_03/filesystem.als#L66-L77 :alt: Get the code to generate this instance. .. index:: Load theme menu option More information about how the magic layout actually works can be found in [LED07]_. In this case we prefer our handmade customization and so we will load back our previously saved theme by selecting :menuselection:`Theme --> Load theme` in the menu. .. image:: instance4.png :width: 450 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_04/filesystem.als#L66-L77 :alt: Get the code to generate this instance. Improving visualizations with derived relations ----------------------------------------------- Alloy supports the definition of derived relations through the declaration of functions, whose return type can be any relational expression with arbitrary arity. *Parameterless* functions are processed by the visualizer and presented alongside the signatures and fields of the instance, even if not used in the specification at all. This section shows how to explore this feature for further tweaking instance visualization. Let's say that we want to highlight in our visualization the directories that are empty. A possibility would be to introduce a new subset signature and restrict its value to always be the set of empty directories. However, due to the nature of the Alloy analysis procedures, such a signature would have to be solved by the Analyzer, possible impacting its performance. If we introduce a function that calculates this set, the Analyzer will calculate its value after the instance is generated and present it in the visualizer. Since they are introduced by the visualizer after the solving process, they can be used without undermining the performance of the analysis. Such a function that retrieves all empty directories would be defined as follows. .. code-block:: fun empty_dirs : set Dir { Dir - entries.Entry } For instance, using the same instance as above, the visualization would now be as follows. .. image:: instance5.png :width: 450 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_05/filesystem.als#L70-L81 :alt: Get the code to generate this instance. .. index:: Show as labels option Notice how the empty directory at the bottom has an additional label :alloy:`$empty_dirs`. All visualization elements introduced in the visualizer that are not part of the model are prefixed with a :code:`$`. Since function :alloy:`empty_dirs` returns a set, it is interpreted as a subset of :alloy:`Dir` which by default are shown as labels in the theme. As expected, their depiction can be customised as any other signature. For instance, to highlight empty directories in the depiction, open the theme customisation menu, and set the border of :alloy:`$empty_dirs` subset of :alloy:`Dir` to be :guilabel:`Dotted` and the displayed name to just :alloy:`empty`. The resulting depiction is below. You could also hide the label of this subset altogether by just setting to :guilabel:`Show as labels` to :guilabel:`Off` for :alloy:`$empty_dirs`. .. image:: theme6.png :width: 700 px :align: center Parameterless derived functions are introduced in the visualization regardless of their arity, resulting in additional edges for relations of arity higher than 1. For instance, let's say we wanted to directly depict the relation between directories and their content, hiding the entry intermediary atoms. We could define the binary relation below in the specification. .. code-block:: fun contents : Dir -> Object { entries.object } Running the command again results in the depiction below, with :alloy:`$contents` edges directly between directories and objects. .. image:: instance6.png :width: 450 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_06/filesystem.als#L74-L85 :alt: Get the code to generate this instance. Once we start introducing derived relations, it is often useful to hide others elements in order to unclutter the visualizer. In this case, we simply set :guilabel:`Show` to :guilabel:`Off` for the :alloy:`Entry` signature, resulting in the compact depiction below where the content of directories is evident. .. image:: instance7.png :width: 400 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_07/filesystem.als#L74-L85 :alt: Get the code to generate this instance. .. index:: relation; ternary comprehension A consequence of short-circuiting entries in the visualizer is that we can no longer see the name of the objects inside a directory. Relations with arity higher than 2 are depicted in the visualizer as edges with labels. Thus, a ternary relation between signatures :alloy:`Dir`, :alloy:`Name` and :alloy:`Object` could be used to directly show the content of a directory but also show its name in a label. Defining such relations is often not trivial, and usually requires defining relations by comprehension. In this case this ternary relation could be defined as follows. .. code-block:: fun named_contents : Dir -> Name -> Object { { d : Dir, n : Name, o : Object | some e : Entry | e in d.entries and e.name = n and e.object = o } } Here, we are collecting all triples :alloy:`d->n->o` such that there is an entry in :alloy:`d` that has name :alloy:`n` and object :alloy:`o`. The resulting depiction is shown below, where the names of the objects inside directories can be seen as a label of the :alloy:`$named_contents` edges. .. image:: instance8.png :width: 400 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/visualization/instance_08/filesystem.als#L67-L78 :alt: Get the code to generate this instance. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/visualization/improving-visualizations-with-derived-relations :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Higher-arity relations :link-type: ref :link: nary-relations :octicon:`beaker` Further reading ^^^ The `named_contents` function returns a derived relation of arity 3. Learn more about such higher-arity relations. .. card:: Model finding :link-type: ref :link: commands :octicon:`beaker` Further reading ^^^ Sometimes we can have :code:`$` prefixed atoms in a visualization that do not correspond to a declared derived function. Learn how such Skolemized variables were introduced by the model finding analysis technique. .. index:: Viz button Txt button Table button Tree button Alternative visualizations -------------------------- As a last note, it is worth mentioning that the Analyzer also supports alternative visualizations other than the graph one we've explored in this chapter. In the visualizer toolbar, buttons :guilabel:`Viz`, :guilabel:`Txt`, :guilabel:`Table`, and :guilabel:`Tree` control the representation of the instance. Option :guilabel:`Viz` is the default graph representation, while the other 3 are textual representations of the relations in plain text, tabular format, and in hierarchical structure, respectively. For illustration purposes, below is the representation of the same instance in tabular format, where each table denotes a signature and the associated fields. Despite the usefulness of the graph visualization, when instances become too complex these simpler representations can prove helpful. .. image:: table1.png :width: 500 px :align: center .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/visualization/alternative-visualizations :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book.