Signature facts¶
In chapter Structural modeling we’ve seen that additional constraints can be imposed on a model through the definition of facts, which may contain arbitrary formulas. Any constraint over the model can be written in such a fact. However, often the constraints we wish to impose target a particular signature of the model, and for those cases Alloy offers an alternative syntax to encode constraints associated with a signature declaration.
Declaring signature facts¶
Signature facts are written in an optional bracket block in a signature declaration after the block of field declarations, and can be attached to top-level, extension or subset signatures. The field declaration block is not optional, so to declare a signature fact for a signature without fields you must leave an empty field block {}.
The main aspect to take into consideration when defining signature facts is that the constraints are implicitly quantified over every atom of the target signature, and that every call to a field of that signature is already projected on that quantified variable.
Consider, for instance, fact unique_names over directories, which we reproduce below.
fact unique_names {
// Different entries in the same directory must have different names
all d : Dir, n : Name | lone (d.entries & name.n)
}
Since this fact is restricting the content of directories, it would perhaps be preferable to attach it to the Dir declaration. This could be achieved as follows.
sig Dir extends Object {
entries : set Entry
} {
// Different entries in the same directory must have different names
all n : Name | lone (entries & name.n)
}
The constraint inside the signature fact is quantified for all atoms of Dir, and the occurrence of entries is actually a unary relation resulting from its application to that variable. To make its meaning more clear, that constraint is equivalent to the following.
all this : Dir | all n : Name | lone (this.entries & name.n)
Understanding signature facts¶
The variable implicitly quantified is always called this, and you can call it within signature facts if needed. In fact, this is a protected keyword in Alloy due to this. Occasionally, you may also need to refer to the non-projected version of a field to get its value for an atom other than this. The non-projected version of a field can be accessed by prefixing it with @.
To illustrate this, consider the version of fact no_shared_entries shown below (which was actually superseded by the stronger one_directory_per_entry).
fact no_shared_entries {
// Entries cannot be shared between directories
all x, y : Dir | x != y implies no (x.entries & y.entries)
}
This constraint is restricting the content of directories by quantifying over two directories. A signature fact will implicitly quantify this over one directory, but the second one must still be explicit, and to get its entries we must use the non-projected @entries. This would result in the following signature fact.
sig Dir extends Object {
entries : set Entry
} {
// Different entries in the same directory must have different names
all n : Name | lone (entries & name.n)
// Entries cannot be shared between directories
all y : Dir | this != y implies no (entries & y.@entries)
}
Although signature facts can improve a model’s readability, they are rather limited. In particular, since the signature’s fields are always projected on the left-hand side, facts such as no_shared_dirs or one_directory_per_entry can’t be elegantly encoded as signature facts.