.. _nary-relations: Higher-arity relations ====================== .. index:: relation; higher-arity relation; unary relation; binary In the main chapter we've seen how to introduce unary relations (as signatures) and binary relations (as fields), and how to compose them in relational expressions. However, Alloy actually supports relations of arity higher than 2: they are simply seen as a set of tuples of a certain arity. We call a relation with arity *n > 0* an *n-ary relation*, and it must be uniform (i.e., all tuples in it must have arity *n*). Sets and binary relations are 1-ary and 2-ary relations, respectively. Most of Alloy's relational operators actually apply to relations of arbitrary arity (except for a few that only apply to binary relations). This chapter explores relations with arity higher than 2, which we denote as *higher-arity relations* to distinguish from sets and binary relations. Declaring higher-arity fields ----------------------------- Let us get back to the file system example from the :ref:`structural-modeling` chapter, where the content of a directory is specified by a set of entries that assign a name to each of its objects. Using only binary fields, the solution we implemented used a signature :alloy:`Entry` to register exactly one name and one object; then a field :alloy:`entries` assigned a set of :alloy:`Entry` atoms to each directory. These entries are not really an essential part of the design of the file system and are not the target of any of the expected properties, but were required to group names and objects in a single entity. .. index:: field; declaration relation; ternary An alternative to this approach would be to store the objects and names contained in a directory directly, without creating the auxiliary :alloy:`Entry` signature. In practice, this entails removing the `Entry` signature and the `entries` field, and instead create a *ternary* field relating directories, names, and objects. In Alloy, such a field could be simply declared as follows: .. code:: sig Dir extends Object { contents : Name -> Object } The range type expression in the declaration of :alloy:`contents` is now the Cartesian product of `Name` and `Object`, meaning each directory is assigned a arbitrary set of pairs each with a name and object inside that directory. Field :alloy:`contents` itself is a ternary relation that is a subset of the Cartesian product :alloy:`Dir -> Name -> Object`. A ternary field is simply a set of flatted triples, and likewise binary relations can be navigated in both directions. In theory, we can declare fields of an arbitrary arity in an Alloy model. In practice, relations with a large arity become impossible to processed by the Analyzer. This limit depends on the size of the universe of discourse. For instance, a 5-ary field can only be represented in universes with less than 74 atoms. However, in our experience, relations with arity higher than 3 are very rarely useful, as manipulating them in constraints becomes very cumbersome. It should also be noted that higher-arity relations can sometimes help reduce of the size of the universe. In our example, by avoiding the creation of auxiliary signature :alloy:`Entry` we removed all those atoms from the universe. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/nary-relations/declaring-higher-arity-fields :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. Visualizing higher-arity fields ---------------------------------- .. index:: instance; visualization Let us for now ignore all additional facts that we had defined for the file system model (which we will need to adapt to the new ternary field), and just run the empty :alloy:`example` command. We need to remove any scope assigned to :alloy:`Entry` since that signature no longer exists. We will get instances such as the following. .. image:: instance1.png :width: 550 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/nary-relations/instance_01/filesystem.als#L28-L36 :alt: Get the code to generate this instance. Notice how ternary relations are still represented as edges in the Analyzer's visualizer, namely edges between the first and the last in each tuple; the middle atom is shown as a label in the edge. So, in this instance, :alloy:`Root` contains :alloy:`File0` with name :alloy:`Name0` and :alloy:`Dir` with :alloy:`Name1`. For fields of arity higher than 3, additional atoms would added to the labels of the edges separated by commas. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/nary-relations/visualizing-higher-arity-fields :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. Specifying constraints ---------------------- .. index:: operators; relational The instance above exhibits many of the issues that we addressed in the main chapter. Let us adapt the facts to the new version of the model with a ternary field. Most relational operators work for higher-arity relations as they do for binary ones. Set operators such as intersection (:alloy:`&`), union (:alloy:`+`), and difference (:alloy:`-`) can be applied between two relations of the same arbitrary arity. Composition also applies to higher arity relations. If you have a directory :alloy:`d`, :alloy:`d.contents` is a binary relation within :alloy:`Name -> Object` containing all pairs of names and objects assigned to :alloy:`d` by :alloy:`contents`. Likewise, for an object :alloy:`o`, :alloy:`contents.o` is a binary relation pairing directories with the names that object :alloy:`o` has inside them. The first fact in the model, :alloy:`unique_names`, forced different entries of a directory to have distinct names. The original version of this fact calculated all entries of each directory with a given name, and forced the resulting set to have at most one value. In the new version, we can follow a similar strategy, as follows. .. code:: fact unique_names { // Different entries in the same directory must have different names all d : Dir, n : Name | lone n.(d.contents) } If :alloy:`d.contents` is a binary relation containing alls pair of names and objects assigned to :alloy:`d`, :alloy:`n.(d.contents)` is a unary relation with the objects assigned name :alloy:`n` in directory :alloy:`d`. Since we want at most one object with each name in a directory, we restrict this set to have cardinality :alloy:`lone`. Parenthesis are needed here because composition associates to the left and :alloy:`n.d` is not a valid expression (it would have arity 0). Interestingly, once we encode the content of a directory as a ternary relation, we can actually enforce this constraint directly when declaring the field. Higher-arity fields can also be restricted by multiplicity constraints in their declaration. In this case, we want to enforce that for any directory, and for any name, there is at most one object related by :alloy:`contents`. This could be enforced as follows, as an alternative to fact :alloy:`unique_names`. .. code:: sig Dir extends Object { contents : Name -> lone Object } The second fact, :alloy:`no_shared_dirs`, forced every directory to appear at most in one entry. This one can be trivially adapted to the ternary field as follows. Relation :alloy:`contents.d` is a binary relation that pairs all directories that contain :alloy:`d` with the respective names. Since a directory can only be contained in a single directory we should restrict the cardinality of his expression with :alloy:`lone`. .. code:: fact no_shared_dirs { // A directory cannot be contained in more than one entry all d : Dir | lone contents.d } Fact :alloy:`no_dangling_objects` forced all objects, except the root, to be contained in some entry. In the previous version, expression :alloy:`Entry.object` denoted every object referred by any entry. In the ternary version, we must retrieve all objects related to any object by any name, which is represented by expression :alloy:`Name.(Object.contents)`. Given this expression, the fact could be trivially adapted as follows. .. code:: fact no_dangling_objects { // Every object except the root is contained somewhere Name.(Object.contents) = Object - Root } Fact :alloy:`one_directory_per_entry` is no longer needed in this version of the model because we no longer have entries. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/nary-relations/specifying-constraints :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: A relational logic primer :link-type: ref :link: relational-logic :octicon:`beaker` Further reading ^^^ Most relational operators of Alloy are defined for *n*-ary relations. Learn more about their semantics. Defining relations by comprehension ----------------------------------- .. index:: comprehension All the facts we have adapted thus far were as complex to specify with the ternary field as they were with the auxiliary signature :alloy:`Entry` and the binary `entries` field. Unfortunately, that is not always the case, and the last remaining fact, :alloy:`no_indirect_containment`, is a bit tricky to encode with the ternary :alloy:`contents` field. That fact, through function :alloy:`descendants`, relied on the transitive closure of the binary relation :alloy:`entries.object` to collect all objects indirectly contained in a directory. However, when two ternary relations are composed, the result is actually a quaternary relation. For instance, with the ternary :alloy:`contents`, :alloy:`contents.contents` is a quaternary relation contained in :alloy:`Dir -> Name -> Name -> Object`. So the transitive closure operations are not well-defined for non-binary relations, and are forbidden in Alloy. By inspecting function :alloy:`descendants`, it is obvious that the name of the objects inside a directory is irrelevant to calculate this relation, so what we need is to convert ternary field :alloy:`contents` in :alloy:`Dir -> Name -> Object` to a binary version in :alloy:`Dir -> Object` that relates directories with their content disregarding the name. Unfortunately, there is no straightforward way to achieve this using only relational operators, and we need to rely on defining this relation by *comprehension*. Relations can be defined by comprehension by quantifying over a sequence of variables, and keeping only the tuples that satisfy a formula defined over those variables. All relational operators (except closures) can be rewritten using a relation by comprehension. For instance, expression :alloy:`Object - Root` above could be rewritten as :alloy:`{ o : Object | o not in Root }`, and :alloy:`Dir + File` as :alloy:`{ o : Object | o in Dir or o in File }`. For our example, we want to take all directories and objects such that they are related by some name in :alloy:`contents`. This can be specified as a binary relation defined by comprehension that "selects all directories :alloy:`d` and objects :alloy:`o` such that :alloy:`d` is related to :alloy:`o` through :alloy:`some` atom". Let us define a new auxiliary function :alloy:`objects` that provides this derived relation. .. code:: fun objects : Dir -> Object { { d : Dir, o : Object | some d.contents.o } } Equipped with this relation, it is now trivial to adapt function :alloy:`descendants` (and consequently, fact :alloy:`no_indirect_containment`) to the ternary field as follows. .. code:: fun descendants [o : Object] : set Object { o.^objects } .. index:: util/ternary module Manipulating ternary relations can become cumbersome, so the Analyzer actually provides an utility module :alloy:`util/ternary` that defines functions to project and flip ternary relations. The one we just defined, that retrieves the first and last columns of a ternary relation, is provided by function `select13`. If we now run the empty :alloy:`example` command once again, we will get instances such as the following, where the issues seem to have been fixed. .. image:: instance2.png :width: 550 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/nary-relations/instance_02/filesystem.als#L46-L54 :alt: Get the code to generate this instance. You'll notice that there is now a new element in the visualization, the value of function :alloy:`objects` prefixed by a :code:`$`. Alloy introduces all functions without parameters in the visualization, and in one of the advanced topics we show how these can be used to improve the visualization of instances. For now we can just hide it as any other relation by choosing :guilabel:`Off` in the :guilabel:`Show as arcs` theme option for :alloy:`objects`. This will result in the following cleaner instance. .. image:: instance3.png :width: 550 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/nary-relations/instance_03/filesystem.als#L46-L54 :alt: Get the code to generate this instance. To finish we should of course check the :alloy:`no_partitions` assertion. Given that :alloy:`no_partitions` was defined by calling function :alloy:`descendants` (through predicate :alloy:`reachable`), nothing needs to be adapted in this assertion. After executing the command, the Analyzer will report no counter-examples, as expected. As a last note, it's not always evident when higher-arity relations should be used in a model. There is a sweet spot where employing a few higher-arity relations (almost always, ternary relations) improves the readability and maintainability of our specifications, while also improving the performance of the Analyzer by reducing the number of signatures and fields in a model (and thus the number of atoms and free relations to be solved). If too many higher arity relations are used (or relations of too high arity), models can become unmanageable and they can also have a negative impact on performance (since expressions can become considerably more complex). .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/nary-relations/defining-relations-by-comprehension :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Arrow multiplicity constraints :link-type: ref :link: bestiary :octicon:`beaker` Further reading ^^^ Alloy has a special syntax to impose multiplicity constraints that can also be applied to *n*-ary relations. .. card:: Visualization customization :link-type: ref :link: viz-customization :octicon:`beaker` Further reading ^^^ We've seen that parameterless functions are introduced in the visualization. Learn how to explore this feature.