.. _subset-signatures:

Subset signatures
=====================

.. index::
   signature; subset
   signature; extension
   in keyword; in signature declaration

Sets (unary relations) can be introduced in a model through subset signatures.
As we've already seen, unlike sub-signatures defined by extension, these are not
guaranteed to be disjoint among themselves. In chapter
:ref:`structural-modeling` we've seen the basic use of subset signatures, but
since we actually expected those subset signatures to be disjoint, they were
better modelled as extension signatures. That is not always the case, and in fact
subset signatures can be used to encode powerful patterns, including something
that resembles multiple inheritance.

Mixing subset and extension signatures
--------------------------------------

Suppose we wanted to add the ability to tag objects in a file system, for example as supported by operating systems like
macOS. The concept of tagged object is transversal to the signature
:alloy:`Object`, since both regular files and directories can be tagged. On the
other hand, not all objects are necessarily tagged. So this feature is best
encoded as a subset signature as follows.

.. code-block::

    sig Tagged in Object {}

If we now ask the Analyzer for instances of this model there may exist objects
that are both in :alloy:`File` and :alloy:`Tagged` and :alloy:`Dir` and
:alloy:`Tagged`. The following is one such possible instance for the empty
command :alloy:`example`. The fact
that an atom belongs to the :alloy:`Tagged` subset signature is depicted with an attribute label below its name
(the name of the atom itself is based on the most specific extension signature to which it belongs).

.. image:: instance1.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/subset-signatures/instance_01/filesystem.als#L78-L90
   :alt: Get the code to generate this instance.
   
Even more interesting, subset signatures can have their own fields declared
within. For instance, let's introduce a signature :alloy:`Tag` to represent
abstract tags, and then extend signature :alloy:`Tagged` to also register the
non-empty set of tags assigned to each object, as follows.

.. code-block::

    sig Tag {}

    sig Tagged in Object {
      tags : some Tag
    }

Now, for instance, any tagged directory will both be related through relations
:alloy:`entries` (inherited from :alloy:`Dir`) and :alloy:`tags` (inherited from
:alloy:`Tagged`). Below is one such example for the same command, where the root
has both entries and tags (in the theme, we've hidden :alloy:`Tag` atoms, and set
field :alloy:`tags` to be shown as an attribute).

.. image:: instance2.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/subset-signatures/instance_02/filesystem.als#L82-L97
   :alt: Get the code to generate this instance.

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/subset-signatures/mixing-subset-and-extension-signatures

      :octicon:`file-badge` Alloy model 
      ^^^
      Download and explore the files relevant for the model at this point of the book.

Simulating multiple inheritance
-------------------------------

.. index::
   multiple inheritance

Suppose now we wanted to discriminate different kinds of tags, so that these can  either be shapes (with a color) or labels (with a text message). This tag hierarchy could be declared as follows.

.. code-block::

    sig Color, Text {}

    abstract sig Tag {}

    sig Shape extends Tag {
      color : one Color
    }

    sig Label extends Tag {
      text : one Text
    }

Suppose now we also wanted to add alerts that are tags that are both shapes and labels. In Alloy we don't have multiple inheritance, so we cannot declare a signature `Alert` that both extends `Shape` and `Label`. Using subset signatures we could simulate multiple inheritance. The key idea would be to declare all three signatures as subsets of the `Tag` signature, and then use a fact to encode the type hierarchy constraints, namely the fact that `Tag` is abstract and that `Alert` is the set of tags that are both shapes and labels. We could do so as follows. Note that alerts would inherit both the `color` and `text` fields.

.. code-block::

  sig Tag {}

  sig Color, Text {}

  sig Shape in Tag {
    color : one Color
  }

  sig Label in Tag {
    text : one Text
  }

  sig Alert in Tag {}

One of the problems of this approach is that since the different kinds of tags are not proper extensions, their atom names will all begin with `Tag`, so to distinguish the different kinds of tags we would need to use the subset signature labels. Of course, we could also customize the theme to help us distinguish which tags fall in each category. In the following instance, we've
set the abstract top-level `Tag` signature to be white and have the default rectangle shape. Then, shapes are instead colored yellow, while labels are shaped as ellipses. As a consequence, alerts are yellow colored ellipses.

.. image:: instance3.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/subset-signatures/instance_03/filesystem.als#L100-L118
   :alt: Get the code to generate this instance.

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/subset-signatures/simulating-multiple-inheritance

      :octicon:`file-badge` Alloy model 
      ^^^
      Download and explore the files relevant for the model at this point of the book.

   .. card:: Visualization customization
      :link-type: ref
      :link: viz-customization

      :octicon:`beaker` Further reading
      ^^^
      In this topic we've have used advanced theme customizations to ease the visualization of instances. Learn more about the Alloy Analyzer's theme customization feature. 

Cross-signature subsets
-----------------------

Another interesting feature of subset signatures is that they can be defined to
be a subset of a union of multiple signatures using the :alloy:`+` operator,
rather than just one as we've seen thus far. Let us extend our example again,
and consider that our file system also supports symbolic links as a distinct
type of object.

.. code-block::

  sig Symlink extends Object {}

If we do not want symbolic links to be tagged, we could enforce this through an additional fact that
restricted the value of :alloy:`Tagged`, but this can be directly achieved at the
signature level by adapting its declaration as follows.

.. code-block::

  sig Tagged in Dir + File {
    tags : some Tag
  }

Now subset signature :alloy:`Tagged` is restricted to only :alloy:`Dir` and :alloy:`File`
atoms, excluding other kinds of objects. In this example :alloy:`Dir` and
:alloy:`File` share the same top-level signature :alloy:`Object`, but signatures can
be defined as the subset of the union of completely unrelated signatures. To properly visualize instances, you will have to customize the theme again at this
point. This is because in the previous version, subset signature :alloy:`Tagged` and field
:alloy:`tags` were defined for the full signature :alloy:`Object` in the theme; now, they are no longer defined for all objects, but only for signatures
:alloy:`File` and :alloy:`Dir`. At the theme customization pane, this will originate two duplicates of :alloy:`Tagged` and :alloy:`tags`, one for each of these two signatures, which
both have to be customized again.

.. index::
   equality operator; in signature declaration

One last, and less common, way to define subset signatures is through equality
rather than inclusion using the operator :alloy:`=`. For instance, let's say that
we wish to assign user permissions to all directories and files, but not to symbolic links. This could be done as follows.

.. code-block::

  sig Permission {}

  sig NonSymlink = Dir + File {
    permission : one Permission
  }

An instance for the empty command for this version of the model is the following.

.. image:: instance4.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/subset-signatures/instance_04/filesystem.als#L107-L129
   :alt: Get the code to generate this instance.

Obviously, this example is a bit contrived since a simpler solution would be to
extend :alloy:`Object` with an abstract signature `NonSymlink` and then
have :alloy:`Dir` and :alloy:`File` extend that signature. However, we could also declare a subset that is equal to the union
of unrelated signatures, and that could not be declared in such a manner.

On a last note, due to all the flexibility of subset signatures, particularly the fact that they may contain atoms from unrelated signatures, they cannot be extended, only contain other subset signatures.

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/subset-signatures/cross-signature-subsets

      :octicon:`file-badge` Alloy model 
      ^^^
      Download and explore the files relevant for the model at this point of the book.