Encoding test instances¶
As models evolve, we should always check whether
instances that were expected to hold are still valid. Using the enumeration
operation New provided by the Analyzer is not feasible for this kind
of regression tests that should be executed automatically every time the model
changes. This chapter explores how we can write run commands
that search for specific instances and that can thus act as unit tests for our models.
Regression tests for models¶
We’ve already seen that run commands are very useful to encode and
explore interesting classes of instances. During validation we often want these
commands to be loosely defined in order to allow for unexpected instances that
may exhibit issues of the model. However, we can also write commands that are
very restrictive and generate a specific instance. These are not as relevant for
validation, but allow the encoding of a kind of unit tests, which we call a
test instance. When the model suffers any change, we can just hit menu option
and see if expected test instances are
still valid.
Alloy does not have any particular support to specify concrete instances, so they have to be defined using regular relational logic formulas. If we follow a well-defined idiom, test instances can be easily encoded as formulas. Let’s get back to the file system example from chapter Structural modeling, and try to encode a very simple test instance where the root contains one directory and one file, and the directory another file, all with different names. This should obviously be a valid instance in our model.
The first issue we face when encoding an instance is the inability to refer to
concrete atoms in Alloy specifications. At first sight, we could feel tempted
to declare several multiplicity one signatures to denote distinguished
atoms in the instance being encoded. However, this approach has a major
disadvantage: such signatures will now exist in all instances of the model,
regardless of the executed command. For instance, if we defined a singleton
files F1 and F2 for this test instance, then the model will no
longer have instances without any file. Moreover, it would break the symmetry
between F1, F2 and the other File atoms, as the former
would now belong to a distinct signature, so isomorphic instances would be
returned. Unless we are dealing with concepts that exist in the domain model
(such as the Root), we should not clutter our specifications with
additional singleton signatures.
The some/disj pattern¶
The alternative is to use an idiom based on some/disj patterns,
which will allow instances to be encoded as a formula that is local to each
command. This pattern works as follows:
create an existential disjoint quantification for the expected atoms for each signature;
restrict the value of all signatures to the union of the respective quantified variables;
restrict the value of all fields to the union of tuples created from the quantified variables;
define a scope that is sufficient to represent the instance.
For the test instance described above, this would amount to the following command.
run test_root_file_dir {
some disj d0, d1 : Dir, disj f0, f1 : File, disj e0, e1, e2 : Entry, disj n0, n1, n2 : Name {
Root = d0
Dir = d0 + d1
File = f0 + f1
Entry = e0 + e1 + e2
Name = n0 + n1 + n2
entries = d0 -> e0 + d0 -> e1 + d1 -> e2
name = e0 -> n0 + e1 -> n1 + e2 -> n2
object = e0 -> d1 + e1 -> f0 + e2 -> f1
}
} for 4 Object, 3 Entry, 3 Name
If we now execute this command, we get the instance below. The command fully
specifies this instance: if you ask for a different instance with
New, you’ll get a message saying there are no more satisfying
instances. We could perhaps imagine other instances that encode the same
instance by just permuting the atoms, for instance assigning Name1 to
File0 and Name0 to File1. However, as we’ve seen, atoms
are uninterpreted and the Analyzer’s symmetry breaking algorithm considers this
instance to be isomorphic to the one above.
Forcing the signatures to be exactly the union of the quantified variables
guarantees that there are no other atoms in the universe besides the ones
quantified. Scope 4 on Object is needed to encode all needed objects
(recall the default overall scope is 3). The disj keyword is needed in
order to avoid the assignment of the same atom to different variables. For
instance, without disj the same file atom could be assigned to variables
f0 and f1 or the same entry atom to e0 and e1.
For instance, the instance below would also be generated, which although valid
in our file system model, is not the test instance we were trying to encode.
Note that a disj keyword must be applied to each group of quantified variables, and not just at the beginning of the quantification. Always make sure that there are enough atoms in the scope to represent the instance, otherwise the command will be trivially inconsistent.
This idiom is the one used throughout the book to encode the presented example instances.
Skolemization and visualization¶
When an Alloy run command has outermost existential quantifications, the
Analyzer performs a process called Skolemization that solves those variables
by creating additional free relations that must also be solved. This improves
the efficiency of the analysis procedures, and as a side-effect such relations
are now also part of the instance as singleton sets, and appear in the
visualization. Such Skolemized variables appear prefixed by a $ and the
name of the command, as could be seen in the instances above. Such relations can
be treated as any other element of the instance, including being called in the
evaluator, or have their visualization customized in the theme. In particular,
we can just hide this label by unchecking Show as labels for those
subsets. Alternatively, you can check the option Hide skolem sigs/relations within general graph settings, which will hide all such atoms. Note however that this will also hide derived functions from the visualization, which are treated as Skolemized variables. The result is the
the following, cleaner visualization. Note that you cannot simply uncheck
Show for those subsets: that would actually remove the atoms in the
subset from the subset, not only hide the label. If you find it important to know which
atom corresponds to each variable, you can still show a shorter and more readable
label by changing the label of those sets in the theme.
Negative test instances¶
Besides encoding tests that are expected to be instances of our model, we should also make sure that invalid instances are in fact not allowed by our model. In Alloy, these will take the shape of run commands that are not satisfiable, that are not able to generate an instance. We can use exactly the same strategy as above, but imposing instead invalid constraints.
Let us try to generate an instance similar to the previous one, but where the
same name is assigned to the file and the directory contained in the root. The
following is similar to the command test_root_file_dir_same_name but
without name n2.
run test_root_file_dir_bad_name {
some disj d1, d2 : Dir, disj f1, f2 : File, disj e1, e2, e3 : Entry, disj n1, n3 : Name {
Root = d1
Dir = d1 + d2
File = f1 + f2
Entry = e1 + e2 + e3
Name = n1 + n3
entries = d1 -> e1 + d1 -> e2 + d2 -> e3
name = e1 -> n1 + e2 -> n1 + e3 -> n3
object = e1 -> d2 + e2 -> f1 + e3 -> f2
}
} for 4 Object, 3 Entry, 2 Name
When running this command, the Analyzer will now report that there is no satisfying instance, which is the expected.
If you have many positive and negative test instances, and rely on
, it may become difficult to detect whether each
command is supposed to be valid or not. To help manage this, we can annotate the
commands the expected outcome, namely stating after the scope definition
expect 1 for positive test instances and expect 0 for negative
test cases. After running (assuming that there are
no other commands in the model), we would get the following feedback from the
Analyzer.
Note only that once you state expect 1, symmetry breaking is turned off
for that command, so the argument above that there is a single acceptable instance
no longer holds (isomorphic instances will be returned).
Extracting instances from the visualizer¶
As you might have noticed, writing the constraints that encode a scenario can become quite cumbersome. Luckily, the Analyzer provides a feature that can ease this process. When navigating instances in the visualizer, you can export them to another format through menu option . Options include exporting to a file representing the graph view, or to an file. But what’s more interesting to the context of this chapter is that they can also be exported as a (also available through shortcut cmd-p). This will provide the user a formula that exactly encodes the instance being visualized. The formula follows precisely the some/disj pattern defined above, although it will be a bit more cluttered since it will also define the values of some built-in signatures even if they are not relevant for the current model.
So let’s say that when verifying your model a check command, a
counter-example was found that was not expected to be an acceptable instance of
the model. You’ll fix the model, and then expect that counter-example to no
longer be a valid instance. So you can extract the predicate that represents
that counter-example and define a negative test command in the Alloy model with
it, which will act as a regression test once the model is fixed.