.. _bestiary: Arrow multiplicity constraints ============================== When declaring fields in an Alloy model, one can only restrict the multiplicity of the target signature. Multiplicities on the source signature can be enforced in facts using regular relational logic, as we've seen in the :ref:`structural-modeling` chapter. However, Alloy also provides a special formula syntax to directly constrain the multiplicities of both end points of a relation. .. index:: multiplicity arrow operator Enforcing multiplicities with arrows ------------------------------------ Consider a relation :alloy:`r` between atoms of signature :alloy:`A` and atoms of signature :alloy:`B`. Let's say we want to state that :alloy:`r` relates every atom of source signature :alloy:`A` to at most one atom of target signature :alloy:`B`, and every atom of :alloy:`B` to at least one atom of :alloy:`A`, we could write the formula :alloy:`r in A some -> lone B`. This kind of atomic formula can use the same multiplicities as the declaration of signatures and fields (:alloy:`set`, :alloy:`some`, :alloy:`lone`, and :alloy:`one`). Not stating a multiplicity next to an end point is the same as having multiplicity :alloy:`set`. Recall fact :alloy:`no_shared_entries` from the :ref:`structural-modeling` chapter, repeated below. .. code-block:: fact no_shared_entries { // Entries cannot be shared between directories all e : Entry | lone entries.e } With this special syntax, we could rewrite it simply as follows. .. code-block:: fact no_shared_entries { // Entries cannot be shared between directories entries in Dir lone -> Entry } .. index:: relation; injective relation; surjective relation; simple relation; entire relation; function relation; representation relation; abstraction relation; bijection The constraint :alloy:`entries in Dir lone -> Entry` forces relation :alloy:`entries` to be *injective*, a relation where no two atoms of the source signature point to the same target atoms. This is one of the four basic properties of relations we can obtain by varying the multiplicities of the source and target signatures. If we had :alloy:`entries in Dir some -> Entry` we would have a *surjective* relation, one where every atom of the target is related to some source atom. If :alloy:`entries in Dir -> lone Entry` relation :alloy:`entries` would be *simple* (or a *partial-function*), a relation where every source atom is related to at most one target. And if :alloy:`entries in Dir -> some Entry` relation :alloy:`entries` would be *entire* (or *total*), since every source atom is related to at least one target. As another example, recall the fact :alloy:`one_directory_per_entry`. .. code-block:: fact one_directory_per_entry { // Entries must belong to exactly one a directory all e : Entry | one entries.e } This could also be rewritten as the following fact, stating that :alloy:`entries` is both injective and surjective (note that multiplicity :alloy:`one` is the combination of multiplicities :alloy:`lone` and :alloy:`some`). .. code-block:: fact one_directory_per_entry { // Entries must belong to exactly one a directory entries in Dir one -> Entry } .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/bestiary/enforcing-multiplicities-with-arrows :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. A bestiary of binary relations ------------------------------ By combining these four properties we get additional well-known kinds of relations. A relation that is both entire and simple is a *function*: every atom of the source is related to exactly one target. A *representation* is a relation that is both entire and injective, and dually, an *abstraction* is a relation that is both simple and surjective. An *injection* is a function that is also a representation, and a *surjection* is a function that is also an abstraction. Finally, by combining all four basic properties we get a *bijection*: a one-to-one mapping between the source and the target signatures. The following table summarizes these properties, and presents the full "bestiary" of binary relations that can be obtained by imposing multiplicity constraints on the source and target signatures. .. table:: :align: center +----------------------+----------------------+----------------------+----------------------+ | injective | entire | simple | surjective | +----------------------+----------------------+----------------------+----------------------+ | :alloy:`A lone -> B` | :alloy:`A -> some B` | :alloy:`A -> lone B` | :alloy:`A some -> B` | +----------------------+-------+--------------+-------------+--------+----------------------+ | representation | function | abstraction | +------------------------------+----------------------------+-------------------------------+ | :alloy:`A lone -> some B` | :alloy:`A -> one B` | :alloy:`A some -> lone B` | +------------------------------+-------------+--------------+-------------------------------+ | injection | surjection | +--------------------------------------------+----------------------------------------------+ | :alloy:`A lone -> one B` | :alloy:`A some -> one B` | +--------------------------------------------+----------------------------------------------+ | bijection | +-------------------------------------------------------------------------------------------+ | :alloy:`A one -> one B` | +-------------------------------------------------------------------------------------------+ .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/bestiary/a-bestiary-of-binary-relations :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. Beyond restricting fields ------------------------- Multiplicity arrows are more expressive than setting the multiplicity of a field between signatures, and can actually set the multiplicity of an arbitrary relation between arbitrary domains and ranges. Recall fact :alloy:`no_shared_dirs` from the main chapter. .. code-block:: fact no_shared_dirs { // A directory cannot be contained in more than one entry all d : Dir | lone object.d } This pattern looks like the one for injectivity, but it is only restricting the portion of field :alloy:`object` that relates to directories (:alloy:`object` is a relation from :alloy:`Entry` to :alloy:`Object`). Using the Alloy range restriction operator :alloy:`:>`, we can obtain the portion of :alloy:`object` related to directories (:alloy:`object:>Dir`), and then restrict it to be injective with a multiplicity arrow. This would result in following equivalent version of :alloy:`no_shared_dirs`. .. code-block:: fact no_shared_dirs { // A directory cannot be contained in more than one entry object:>Dir in Entry lone -> Dir } For yet another example, recall fact :alloy:`no_dangling_objects`. .. code-block:: fact no_dangling_objects { // Every object except the root is contained somewhere Entry.object = Object - Root } Expression :alloy:`Entry.object` retrieves all objects related to an entry. By equalling it to :alloy:`Object - Root`, we're saying that every object, except the root, must be related to some entry by :alloy:`object`. So we're essentially stating that :alloy:`object` is surjective on a restricted range. So the following is an equivalent version of :alloy:`no_dangling_objects` using multiplicity arrows. .. code-block:: fact no_dangling_objects { // Every object except the root is contained somewhere object in Entry some -> (Object - Root) } .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/bestiary/beyond-restricting-fields :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Higher-arity relations :link-type: ref :link: nary-relations :octicon:`beaker` Further reading ^^^ These multiplicity arrows can also be applied to higher-arity fields. Learn how to use higher-arity relations. .. card:: A relational logic primer :link-type: ref :link: relational-logic :octicon:`beaker` Further reading ^^^ If you're not familiar with operators like :alloy:`:>`, you can learn about the full syntax and semantics of Alloy's relational logic.