Enumeration signatures¶
Models often require enumerated types that are expected to contain certain specific elements. For example, let’s build on the file system example from the Structural modeling chapter, and extend it with Unix-like file permissions, where the file’s owner, file’s group and every other user are assigned either read, write or execute permission.
Declaring enumeration signatures¶
In Alloy it is very common to use extension signatures of multiplicity
one to specialize signatures that are supposed to represent enumerated data
types. The following specification declares a Permission signature that
contains exactly three permissions: Read, Write, and
Execute.
abstract sig Permission {}
one sig Read, Write, Execute extends Permission {}
Here we see another feature of the Alloy language: if two or more signatures share the same features (multiplicity, parent signature, fields, etc.) they can all be defined together in the same declaration with names separated by commas. This also applies to fields and variable declarations.
This pattern for declaring signatures that represent
enumerated data types is so common that Alloy has a keyword
enum for that purpose. Using this keyword, the
Permission signature could be declared as follows.
enum Permission { Read, Write, Execute }
Using enumeration signatures¶
Enumeration signatures can be used as any other regular signature. In our example, we want each object in the file system to have a permission assigned to each group, so signature Object could be extended as follows.
abstract sig Object {
user_permission : set Permission,
group_permission : set Permission,
others_permission : set Permission
}
Here, each of the 3 fields determines the permissions assigned to a scope. Running an empty example command yields instances such as the following, after some theme customization (including hiding the enumeration and setting the permission fields to be shown as attributes).
An alternative encoding¶
While this models the desirable information, it is perhaps not the easiest encoding to maintain. An alternative is to also encode the different classes as an enumeration signature, and then create a new signature that acts as a “record” that combines classes and permissions. This could be encoded as follows.
enum Class { User, Group, Other }
sig PermissionAssignment {
permission : set Permission,
class : one Class
}
abstract sig Object {
mode : set PermissionAssignment
}
However, this no longer guarantees that for each object, there is exactly one permission assigned to each group. This requires the following additional fact.
fact all_classes_assigned {
// There is one permission assigned to each group
all o : Object, c : Class | one o.mode & class.c
}
Unfortunately, this encoding also has a limitation: the number of distinct assignments of permissions to classes is determined by the scope on signature PermissionAssignment. Since there are 3 different classes, this already uses up the complete default scope for PermissionAssignment, and commands like the following yield no instance.
run distinct_permissions {
some disj o1, o2 : Object | o1.mode != o2.mode
}
If we increase, for instance, the overall scope to 4, the command will be able generate instances such as the following (again, after some similar theme customizations).
Yet another alternative encoding that would address both the maintainability and scope issues could be to define the permissions using a ternary relation. The declaration and use of such higher arity relations are addressed in another advanced topic.
There is just a subtle difference between declaring enumeration signatures with
keyword enum and declaring them with singleton extensions as we did initially: the former additionally imposes a total order between the
respective atoms, corresponding to the order in which they are declared inside
the braces. Total orders in Alloy are also explored in a separate advanced topic.