.. _enumerations:

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 
:ref:`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
--------------------------------

.. index::
   signature; enumeration
   signature; singleton
   signature; declaration
   one keyword; as multiplicity

In Alloy it is very common to use extension signatures of multiplicity
:alloy:`one` to specialize signatures that are supposed to represent enumerated data
types.  The following specification declares a :alloy:`Permission` signature that
contains exactly three permissions: :alloy:`Read`, :alloy:`Write`, and
:alloy:`Execute`.

.. code-block::

    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.

.. index::
   enum keyword

This pattern for declaring signatures that represent
enumerated data types is so common that Alloy has a keyword
:alloy:`enum` for that purpose. Using this keyword, the
:alloy:`Permission` signature could be declared as follows.

.. code-block::

    enum Permission { Read, Write, Execute }

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/enumerations/declaring-enumeration-signatures

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

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 :alloy:`Object` could be extended as follows.

.. code-block::

    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 :alloy:`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).

.. image:: instance1.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/enumerations/instance_01/filesystem.als#L81-L95
   :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/enumerations/using-enumeration-signatures

      :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 some theme customizations to simplify the depiction of instances. Learn more about the Alloy Analyzer's theme customization feature. 

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.

.. code-block::

    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.

.. code-block::

    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 :alloy:`PermissionAssignment`. Since there are 3 different classes, this already uses up the complete default scope for :alloy:`PermissionAssignment`, and commands like the following yield no instance.

.. code-block::

   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).

.. image:: instance2.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/enumerations/instance_02/filesystem.als#L96-L113
   :alt: Get the code to generate this instance.
   
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 :alloy:`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.

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/enumerations/an-alternative-encoding

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

   .. card:: The predefined :alloy:`ordering` module
      :link-type: ref
      :link: ordering

      :octicon:`beaker` Further reading
      ^^^
      Learn what are the consequences of having a total order imposed on enumeration signatures.  

   .. card:: Higher-arity relations
      :link-type: ref
      :link: nary-relations

      :octicon:`beaker` Further reading
      ^^^
      Learn about fields of higher arity, which could be used to simplify the representation of the permissions.