Handling recursion¶
The transitive closure operator supported by the Alloy language allows the
specification of many reachability constraints that otherwise would have to be specified
through recursive definitions. Let us get back to the file system model defined
in the Structural modeling chapter. Assertion no_partitions
required computing all objects indirectly contained in the root,
traversing the complete file hierarchy. In a concrete implementation, this would
probably be computed with a recursive procedure. In Alloy, we easily collected
all objects using the transitive closure on entries.object. While
extremely useful, transitive closure cannot be used to specify all constraints that can be specified with recursion.
For instance, let us try to compute the (maximum) depth of a file in the file
system. We could use the transitive closure of entries.object to
retrieve all ancestors of a certain file. However, files can be shared among
directories, and the result of the transitive closure would be a flat set of
objects without information about their provenance within the file system. Thus,
it cannot be used to calculate file depth.
The predefined natural module¶
To calculate the maximum depth of a file, we will need to calculate the depth of
its ancestors, select the maximum depth among them, and increment by 1. Since
the depth of the file system is always a positive integer number, we can encode
it as a natural number. Alloy provides a predefined library
util/natural that provides a codification of natural numbers in plain
Alloy, and allows us to refrain from using the built-in type Int. To
use this library, we need only to import it at the beginning of the Alloy model,
as follows.
open util/natural
This module introduces a signature Natural with two distinguished singleton signatures, Zero and One. You can inspect all functions and predicates provided for Natural by opening util/natural in the menu . These include functions inc[n : Natural] and dec[n : Natural] to increment and decrement a natural by 1, respectively, and arithmetic operations such as add[n1, n2 : Natural] and sub[n1, n2 : Natural], for addition and subtraction, respectively. A total order is also imposed over Natural using the predefined Alloy module ordering, which introduces function such as max[ns : set Natural] and min[ns : set Natural], and predicates such as gt[n1, n2 : Natural] and lt[n1, n2 : Natural].
Note that by encoding naturals as a signature, they are bounded by the scope
specified for signature Natural. For instance, if you increment a
natural beyond those allowed by the scope, it will just yield an empty set
(without any kind of error or warning). Luckily, in this example it is easy to
identify the maximum natural number needed, since we cannot have a file depth
larger than maximum number of Object atoms specified in the scope.
Recursive Alloy functions¶
Let us try to calculate the depth of the file system with the most obvious strategy: a recursive Alloy function. Although not a particularly simple function, it is possible to define it in Alloy. One possibility is to define it as follows.
fun depth [o : Object] : Natural {
o in Root implies Zero
else inc[max[{n : Natural | some x : entries.object.o | n = depth[x]}]
}
Given an object, if it is the root then return 0; else, calculate all naturals that correspond to the depth of the directories that contain that object, select the maximum and increment it by 1. The tricky part here is calculating the set of depths of all the ancestors of an object. We’ve defined it by comprehension by collecting all naturals for which there is a parent directory directory with that depth.
We can now use this function to define a run command that generates a
file system with a file at a certain depth. For instance, for depth 2, we could
execute the following command.
run depth2 {
some f : File | depth[f] = inc[One]
} for 5 but 3 Name
The scope of 5 applies to both Object and Natural, so the
bound on naturals is enough to encode all possible file depths. However, you’ll
actually get the following error from the Analyzer: fun this/depth cannot call
itself recursively! The fact is, the Analyzer’s procedures, based on SAT
solving, cannot handle recursive definitions. Any recursive call to a function
would have to be explicitly unrolled, but it is not possible to know how many
unrolls would be needed in each case. Nonetheless, Alloy does support recursive
function definitions, but in a very restrictive manner since we have to impose a
bound on the number of function unrolls. This feature is disabled by default,
and must be turned on the options, and is limited to a maximum of 3 unrolls due
to performance issues. So, if we follow the menu option and set it to rather than
, and then run the command again, we will finally
obtain the following instance.
Now, let us try instead to find a file system with depth 3 with the following command.
run depth3 {
some f : File | depth[f] = inc[inc[One]]
} for 5 but 3 Name
Perhaps unsurprisingly, there is no such instance. That is because with a
recursion depth of 2, it is not possible for depth to ever calculate
value 3 (it actually just returns none in those cases). If we set menu
option to 3, we will now get the
following instance.
It’s evident that this approach can easily lead to unpredictable results. The
outcome of a command is dependent on an Analyzer option, which in general is a
bad practice in Alloy where models are expected to be self-contained. When the
maximum recursion depth allowed is exceeded, it just “fails silently” by
returning an empty relation. Moreover, the maximum recursion depth allowed by
the Analyzer is just 3, so we will never be able to calculate a file
depth of 4 with this approach. Luckily, we can use a specification
pattern that allows us to circumvent these issues altogether. It is very rare
that recursive functions are useful in Alloy, so let’s just keep
as .
Recursion through memoization¶
The alternative approach follows a strategy that resembles memoization: we introduce a new field in the signature that is to be recursively traversed, and store in this field the local result of the recursive call. Then, we declaratively specify the value of this field for all atoms using only the the value for its ancestors. There is, of course, a trade-off: now the recursive result will be computed for all atoms of the signature, and not only for a specific atom when called in a function.
In our example, we start by introducing a field to represent the depth of each object, as follows.
abstract sig Object {
depth : one Natural
}
Next, we have to restrict the value of this field to the correct depth. This can be done declaratively through the following fact.
fact calculate_depth {
all o : Object |
o in Root implies o.depth = Zero
else o.depth = inc[max[(entries.object.o).depth]]]
}
This fact defines the depth of each object o as follows: if o is
the root, it has depth 0; else it collects all the depths of the ancestors of
o, selects the maximum, and increments it by 1. Notice that we no longer
need a relation by comprehension to collect the depths of the contents, since
they are already stored in a field.
The run commands above could be executed exactly as they are due to the
dual syntax of dot join and box join. However, let us define them using dot join
to make it clear that depth is now a field.
run depth2 {
some f : File | f.depth = inc[One]
} for 5 but 3 Name
After a few theme customizations (showing depth as an attribute rather
than an edge, hiding Natural atoms, and removing the namespace from
their labels), we obtain instances such as the following.
We can now ask for file systems with a depth as big as that supported by the scope on naturals. For instance, the following command still generates instances, namely the example shown below.
run depth4 {
some f : File | f.depth = inc[inc[inc[One]]]
} for 5 but 3 Name
Beyond depth 4, with the current scope it is not possible to generate instances,
since there are obviously not enough objects. But even if we increase the scope
on objects and entries, it will not be possible to generate instances since the
natural 5 requires a scope of 6 on Natural (natural 0 is also an atom).
So be careful to always update the scope of Natural as needed.