The instance evaluator¶
The Alloy instance visualizer has an evaluator that can be used to compute the value of any relational expression or formula over the instance being inspected in the visualizer. For more complex instances and counter-examples, this feature is helpful to support their interpretation.
Evaluating expressions¶
To access this evaluator just press the Evaluator button in the toolbar of the instance visualizer window. To close the evaluator and return to the normal instance visualizer just press the Close Evaluator button in the toolbar.
To illustrate this feature, we will use an instance that could have been returned as the result of the empty
run command example from Structural modeling chapter. While this is clearly
a simple instance that could perhaps be easily understood through the
visualization, as models and instances become more complex, so does the
evaluator become more relevant.
To ask for the value of an expression just type it in the evaluator and press Enter. Every relational expression denotes a relation of a certain arity. By default, the visualizer depicts the values of the signatures and fields of an instance as labelled graphs. The visualizer can also be set to depict the value of a relation (of any arity) as a table where each line is one of the tuples contained in it. The evaluator uses this latter representation to show the values of relational expressions.
A basic use of the evaluator is to just ask for the values of the signatures and
fields of the model, such as Dir or entries. However, we can
actually evaluate the value of any relational expression. For instance, we can
ask for the value of entries.objects to get the relation between
directories and the objects they contain, or
Root.^(entries.object) to get all objects indirectly contained inside
the root using the transitive closure. We can also refer any auxiliary function
defined in the model, so we can also just call function descendants to
get the descendants of the root. The result is shown below. Note that you can
navigate through the evaluator log with ↑ and ↓.
Evaluating formulas¶
The evaluator can also be used to ask for the values of arbitrary formulas,
which makes it very useful and convenient to debug constraints. For example,
when inspecting a counter-example, we can use the evaluator to find out which
sub-formulas of a constraint have been broken in that particular case. Below is
an example where we evaluate certain formulas over this instance, such as
testing whether there are any directories besides the root, or whether the root
is indirectly contained in itself. As expected, you can also call any auxiliary functions and predicates defined in the model to ease this process. So we test whether the root is in its own descendants using function descendants, or even using the reachable predicate directly.
Referring to atoms¶
Another feature of the evaluator that is sometimes helpful is that, when
inspecting an instance, unlike when writing a specification, we can refer to
concrete atoms in expressions. This is possible because the universe of atoms
for a specific instance is known during evaluation. To refer to a concrete atom
in the evaluator, you should use the label of its most specific extension signature as
the prefix and its numerical identifier as a suffix, separated by a $
mark (except for special atoms such as those from Int). Note that subset
signatures do not affect the name of an atom (since each atom may belong to
multiple subsets). Back to the example, you can for instance query the object of
entry Entry$2 with Entry$2.object, or find out all objects that
have name Name$1 with (name.Name$1).object. Or you can call descendants on Dir$0 to find out the indirect contents of that directory.
You might have noticed that in this instance, the atoms of Dir and
File do not appear numbered in the visualization. This is because, by
default, the visualizer does not number the atoms of signatures that directly contain just one atom to improve
readability (in this case signature Dir actually has 2 atoms, but one
of them is in a more specific extension, Root). To refer to those
atoms, you can use index 0, namely Dir$0 and File$0 (note that
a call to Dir refers to the signature and will actually return
Dir$0 and Root$0).
This mismatch between the names of the atoms in the evaluator, and the
pretty-printed version in the graphical visualizer can be a source of confusion.
For instance, if you try to call Entry2 you’ll get an error as that atom
does not exist (and it could actually refer to another signature since signature
names are alpha-numerical). In fact, we can even change the name of the atoms in
the graphical visualization through theme customizations, but these do not apply
to the evaluator, and the new name of atoms in the graph will not be recognized
by the evaluator. If this gets confusing, you can always temporarily tick the
option Use original atom names in the theme customizer, and all
atoms in the visualization will be shown with their original name as in the
evaluator. Below is the result after changing this option in the theme.
