.. _signature-facts:

Signature facts
=====================

In chapter :ref:`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.

.. index::
  signature; fact
  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.

.. code-block::

  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.

.. code-block::

	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.

.. code-block::

	all this : Dir | all n : Name | lone (this.entries & name.n)

.. card-carousel:: 2

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

      :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
      ^^^
      Learn more about the logical operators provided by Alloy's relational logic.

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 :code:`@`.

To illustrate this, consider the version of fact `no_shared_entries` shown below (which was actually superseded by the stronger `one_directory_per_entry`).

.. code-block::

  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.

.. code-block::

  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.

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/signature-facts/understanding-signature-facts

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