.. _ordering: The predefined :alloy:`ordering` module ========================================= .. index:: util/ordering module Alloy has some predefined modules in a special :alloy:`util` namespace. One of them is :alloy:`util/ordering`, a parametrized module that can be used to impose a total order in a signature. In particular, this module defines a :alloy:`next` relation that given an atom returns the next atom in the total order, and two derived singleton signatures :alloy:`first` and :alloy:`last` with the first and last atoms of the order, respectively. Note that :alloy:`last` is the only atom without a :alloy:`next` atom in the order. Module :alloy:`util/ordering` also defines several derived predicates and functions to compare and compute the maximum or minimum of sets of elements (for example, :alloy:`gt` is a predicate that can be used to compare if one atom is greater than another, and :alloy:`max` is a function that computes the maximum of a given set of atoms). Declaring totally ordered signatures ------------------------------------ For example, let's suppose we wanted to enrich our file system model with the creation timestamp of each entry. Since we will want to compare timestamps, we could first declare a totally ordered signature :alloy:`Time` as follows. .. code-block:: open util/ordering[Time] sig Time {} The definition of signature :alloy:`Entry` could now be changed to include the creation timestamp attribute. .. code-block:: sig Entry { object : one Object, name : one Name, time : one Time } Of course, we should impose a new constraint stating that the creation timestamp of an entry should precede that of its children. .. code-block:: fact children_timestamp { // The timestamp of an entry precedes that of its children all e : Entry, t : e.object.entries.time | lt[e.time, t] } Note the use of a chain of compositions to get all timestamps of all entries contained in the object of an entry. If the object is a file this set will be obviously empty and the constraint holds trivially. If it is a directory, then the timestamp of the respective entry must be less than those of all its children. If we run the :alloy:`example` command with a scope of 3, and customize the theme to show timestamps as attributes, we could get the following example filesystem. .. image:: instance1.png :width: 400 :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/ordering/instance_01/filesystem.als#L85-L96 :alt: Get the code to generate this instance. You can see in the visualization relations :alloy:`first`, :alloy:`last`, and :alloy:`next` introduced by module :alloy:`util/ordering`. If we are not interested in seeing these relations in the visualization, we can omit them. In principle, this would make it very difficult to understand how the timestamps are ordered, and check if instances are valid. However, the module :alloy:`util/ordering` is handled in special way be the Alloy Analyzer, which will attempt to name the inhabitants of the ordered signature sequentially according to the order defined by :alloy:`next`. So you can see in our instance that :alloy:`Time0` is the :alloy:`first`, which is followed by :alloy:`Time1`, and then by :alloy:`Time3`, which is the :alloy:`last`. If we really want to confirm the value of the :alloy:`next` relation we could go to the evaluator and ask for its value. However, we will get an ambiguity error since :alloy:`next` is also defined in the :alloy:`util/integer` module that is imported by default. To disambiguate we could type the qualified name :alloy:`ordering/next` instead. .. image:: evaluator1.png :width: 550 :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/ordering/instance_02/filesystem.als#L85-L96 :alt: Get the code to generate this instance. To see what other functions and derived relations are declared in :alloy:`util/ordering` you can open it in the menu :menuselection:`File --> Open Sample Models...`. The above fact, imposing that the creation timestamp of an entry should precede that of its children, actually makes fact :alloy:`no_indirect_containment` redundant, since it is no longer possible for directories to contain themselves directly or indirectly. We can confirm this by changing that fact to an assertion and using the Analyzer to verify it. .. code-block:: assert no_indirect_containment { // Directories cannot contain themselves directly or indirectly all d : Dir | d not in descendants[d] } check no_indirect_containment for 6 .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/ordering/declaring-totally-ordered-signatures :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Module system :link-type: ref :link: modules :octicon:`beaker` Further reading ^^^ Learn how to define your own modules in Alloy, and the strategy used in :alloy:`ordering`. .. card:: The instance evaluator :link-type: ref :link: evaluator_instance :octicon:`beaker` Further reading ^^^ Learn how to use the evaluator, so that you can check the value of the `next` relation. Analysis scopes --------------------------------- Besides naming the atoms according to the total order, module :alloy:`util/ordering` has another peculiarity concerning the analysis. The scope of the signature that is passed as parameter to :alloy:`util/ordering` is always exact even if not declared with :alloy:`exactly`. The reason for this is to make analysis faster, but one should always be aware of this detail when running commands, as it can sometimes introduce inconsistencies, making :alloy:`run` commands trivially unsatisfiable or :alloy:`check` commands trivially valid. As an example, consider the following (rather arbitrary) model of a finite sequence of natural numbers, distinguishing between even and odd numbers, and requiring the first in the sequence to be even and the last to be odd. .. code-block:: open util/ordering[Nat] abstract sig Nat {} sig Even, Odd extends Nat {} fact { all n : Even | n.next in Odd all n : Odd | n.next in Even first in Even last in Odd } run example {} If we execute the command :alloy:`example` we get no instance! This is due to the fact that the default scope for :alloy:`Nat` is 3, and since this signature is being totally ordered with :alloy:`util/ordering` this scope is required to be exact. Unfortunately, with exactly 3 atoms in :alloy:`Nat` it is impossible to satisfy the given constraints. If we change the scope of :alloy:`example` to 4 then we will obtain one instance. .. image:: instance2.png :width: 400 :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/ordering/instance_03/nat_ordering.als#L21 :alt: Get the code to generate this instance. This is also an example where the naming of the atoms does not help in understanding what is the total order, since the ordered signature :alloy:`Nat` is abstract and extended by :alloy:`Even` and :alloy:`Odd`. If you omit the `util/ordering` relations from the visualization, you can always use the evaluator to consult the atom order. .. image:: evaluator2.png :width: 550 :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/ordering/instance_04/nat_ordering.als#L21 :alt: Get the code to generate this instance. As a last note on scopes, for efficiency reasons the :alloy:`util/ordering` module also requires the parameter signature to be non-empty (it forces :alloy:`first` and :alloy:`last` to always contain exactly one atom), meaning that setting its scope to 0 will also result in an inconsistent specification. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/ordering/analysis-scopes :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Full models for this topic :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/ordering :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Commands in detail :link-type: ref :link: commands :octicon:`beaker` Further reading ^^^ Learn the full details about analysis commands and their scopes.