.. _modelling-tips:

Alloy modelling tips
*********************

As Alloy specifications increase in size in complexity, it becomes harder to
comprehend them and interpret their instances. This chapter explores some
modelling and validation tips that can be followed to ease this task,
ranging from the usage of intelligible idioms to advanced features of the
Analyzer's instance visualizer.

.. index::
   Alloy Analyzer; visualizer

.. _aux-viz:


Improved visualisation with derived relations
==================================================

You might have realised that the instance visualizer plays an essential role
in the validation of Alloy specifications. A key feature in this process is
the ability to customise the theme so that the relevant information is
highlighted (and the irrelevant one hidden). In this section we present
another feature of the visualizer that allows further tweaking instance
visualization: the introduction of derived relations.

.. index::
   single: function, Alloy
   see: fun keyword; function, Alloy

Derived relations in Alloy are introduced through the declaration of
*functions* (much like derived formulas are introduced through the declaration
of predicates). These are declared with
the keyword :code:`fun`, followed by the function name, an optional list of
function parameters, its return type, and an expression enclosed between
braces. The return type can be any relational expression with arbitrary arity.
Once declared, these functions can be freely used in relational expressions.

Let’s get back to the file system example from chapter
:ref:`structural-design`. A function could be declared to retrieve,
for instance, all empty directories, which would be defined as follows.

.. code-block::

   fun empty_dirs : set Dir  {
     Dir - entries.Entry
   }

At first sight, if we wanted to show the set of empty directories when
visualizing an instance, we would have to declare an additional subset
signature and enforce in a fact that its value is equal to the set
:code:`empty_dirs`. However, this signature would have to be solved by the
Analyzer without actually introducing anything new in the specification.
Besides the obvious benefit of declaring re-usable expressions, Alloy
functions *without parameters* have an additional interesting feature: they
are introduced by the visualizer in the depiction of instances, and are shown
along the declared signatures and fields. Moreover, since they are introduced
by the visualizer after the solving process, they can be freely abused without
undermining the performance of the analysis. For instance, running the last
version of the :code:`example` command from chapter :ref:`structural-design`,
will now yield the depiction below.

.. image:: viz1.png
   :align: center

.. index:: themes; customisation

Notice how the empty directory at the bottom has an additional label
:code:`$empty_dirs`. All visualization elements introduced by the visualizer
are prefixed with a :code:`$`. Since :code:`empty_dirs` returns a set, it is
interpreted as a subset of :code:`Dir` which by default are shown as labels in
the theme. As expected, their depiction can be customised as any other
signature. For instance, to highlight empty directories in the depiction, open
the theme customisation menu, set :code:`$empty_dirs` to be coloured in yellow
and the displayed name to :code:`empty`. The resulting depiction is below,
where empty directories are clearly distinguished from non-empty ones. You
could also hide the label altogether and just change the colour of empty
directories by just setting to :guilabel:`Show as labels` to :guilabel:`Off`
for :code:`empty_dirs`.


.. image:: viz2.png
   :align: center

.. index::
   Skolemization
   quantifier; higher-order
   Alloy Analyzer; options

.. note:: What’s with these other :code:`$`-prefixed variables?

  You may have noticed that sometimes :code:`$`-prefixed sets (or relations)
  appear in the visualizer even without derived functions declared in the model. This is
  because some existential quantifications in :code:`run` commands (or universal ones
  in :code:`check` commands), are solved through a process known as *Skolemization*.
  This process involves creating a relation corresponding to a witness of the
  quantification to which the solver will attempt to assign a value. Besides
  improving the performance of the analysis if used sensibly (the depth level
  can be configured in :menuselection:`Options --> Skolem level`, with 2 as
  default), this actually allows the execution of commands with certain
  *higher-order quantifications*.

  Since these variables are solved by finding a value to a relation, they can
  also be depicted when visualizing the instance. This is useful since it helps us identify
  witnesses of quantifications. Their name is prefixed with :code:`$` and the
  context in which the quantification occurs. Consider, for instance, the
  following command.

  .. code-block::
  
    check no_empty_dirs { 
      all d : Dir | d in empty_dirs }

  The universal quantification on a check will be solved through
  Skolemization. This property is obviously false, and returned
  counter-examples have assigned a value to the Skolem relation of :code:`d`
  that has broken the property. Since the context of the quantification is the
  :code:`no_empty_dirs` command, the Skolem relation is named
  :code:`$no_empty_dirs_d`.

  .. image:: viz6.png
     :align: center

  Like any other subset signature, the visualization of Skolem relations can
  be configured in the theme, and they can be hidden if we feel they are
  cluttering the depiction.
  
Derived functions without parameters are actually introduced by the visualizer
regardless of its arity, resulting in additional edges for relations of arity
higher than 1. For instance, if we wanted to depict directly the relation
between directories and their content, hiding the entry atoms in the middle,
we could define the binary relation below.

.. code-block::

  fun contents : Dir -> Object {
    entries.object
  }

Running the command again results in the depiction below, with
:code:`$contents` edges directly between directories and objects.

.. image:: viz3.png
   :align: center

Once we start introducing derived relations, it is often useful to hide others
elements in order to unclutter the visualizer. In this case, we simply set
:guilabel:`Show` to :guilabel:`Off` for the :code:`Entry` signature, resulting
in the depiction below where the content of directories is evident.

.. image:: viz4.png
   :align: center

.. index::
   relation; ternary
   relation comprehension

A consequence of short-circuiting entries in the visualizer is that we can no
longer see the name of the objects inside a directlry. Relations with arity
higher than 2 are depicted in the visualizer as edges with labels. Thus, a
ternary relation with type :code:`Dir->Name->Object` could be used to keep the
content edges between directories and objects but also show the name of the
object. Defining such relations is often not trivial, and usually requires
defining relations by comprehension. In this case this ternary relation could
be defined as follows.

.. code-block::

  fun named_contents : Dir -> Name -> Object {
    { d : Dir, n : Name, o : Object | 
      some e : Entry | e in d.entries and e.name = n and e.object = o } 
  }

Here, we are collecting all triples :code:`d->n->o` such that there is an
entry in :code:`d` that has name :code:`n` and object :code:`o`. The resulting
depiction is shown below, where the labels of relation :code:`$named_contents`
have the names of the objects appended.

.. image:: viz5.png
   :align: center

Although we focused on an example without mutable signatures or fields, this
strategy also works in that context, as we shall see in section :ref:`event-idiom`.
That's because derived relations are evaluated in the state they are called
from, and when depicting traces, the visualizer will evaluate them at each
individual state.

As a last note, recall that these derived functions (and predicates) can
always be called from the evaluator, so they may be useful for debugging
instances even if we are not interested in showing them in the visualizer.



.. _event-idiom:

An idiom to depict events
=========================

In the chapter :ref:`overview`, we remarked that the Alloy visualizer does not
show the event or events corresponding to a given transition. This is because
we modelled them as predicates and there's no way for Alloy to know that these
particular predicates should be interpreted as events. In this section,
building on the feature we presented in section :ref:`aux-viz`, we will devise
an *idiom* (a modelling pattern) that allows the depiction of events in the
visualiser. As an opportune side effect, it also facilitates the writing of
certain classes of formulas. 

To illustrate this idiom, let's consider the leader election example from
chapter :ref:`protocol-design` again. The full corresponding specification is
shown below for completeness but the idiom doesn't depend on the actual bodies
of facts and predicates. 

.. code-block::

   open util/ordering[Id]

   sig Node {
     succ : one Node,
     id : one Id,
     var inbox : set Id,
     var outbox : set Id
   }

   var sig Elected in Node {}

   sig Id {}

   fact {
     // at least one node
     some Node
   }

   fact {
     // succ forms a ring
     all n : Node | Node in n.^succ
   }

   fact {
     // ids are unique
     all i : Id | lone id.i
   }

   fact {
     // initially inbox and outbox are empty
     no inbox and no outbox
     // initially there are no elected nodes
     no Elected
   }

   pred initiate[n : Node] {
     // node n initiates the protocol

     historically n.id not in n.outbox           // guard

     n.outbox' = n.outbox + n.id                 // effect on n.outbox
     all m : Node - n | m.outbox' = m.outbox     // effect on the outboxes of other nodes

     inbox'   = inbox                            // frame condition on inbox
     Elected' = Elected                          // frame condition on Elected
   }

   pred send[n : Node, i : Id] {
     // i is sent from node n to its successor

     i in n.outbox              // guard

     n.outbox' = n.outbox - i                 // effect on n.outbox
     all m : Node - n | m.outbox' = m.outbox    // effect on the outboxes of other nodes
     
     n.succ.inbox' = n.succ.inbox + i   // effect on n.succ.inbox
     all m : Node - n.succ | m.inbox' = m.inbox // effect on the inboxes of other nodes
        
     Elected' = Elected                         // frame condition on Elected
   }

   pred process[n : Node, i : Id] {
     // i is read and processed by node n

     i in n.inbox                                // guard

     n.inbox' = n.inbox - i                      // effect on n.succ.inbox
     all m : Node - n | m.inbox' = m.inbox       // effect on the inboxes of other nodes

     gt[i,n.id] implies n.outbox' = n.outbox + i // effect on n.outbox
                else    n.outbox' = n.outbox
     all m : Node - n | m.outbox' = m.outbox     // effect on the outboxes of other nodes

     i = n.id implies Elected' = Elected + n     // effect on Elected
          else Elected' = Elected 
   }

   pred stutter {
     outbox'  = outbox
     inbox'   = inbox
     Elected' = Elected
   }

   fact {
     // possible events
     always (
       stutter or 
       some n : Node | initiate[n] or
       some n : Node, i : Id | send[n,i] or
       some n : Node, i : Id | process[n,i]
     )
   }

   run example {
     eventually some Elected
   } for exactly 3 Node, exactly 3 Id

Let's consider an instance returned when executing command :code:`example`. After a short examination, and based upon our knowledge of the specification, we can determine that in this trace a :code:`stutter` event happens in state 7.

.. image:: instance1.png
   :align: center
   
However, in the general case, for more complex specifications, the fact that events aren't displayed makes their interpretation tedious and error-prone. The crux of the idiom presented here is to use *derived relations* to represent the events happening in a given state.

.. index::
   signature; enumeration signature
   see: enum keyword; enumeration signature


This may not seem immediately obvious as derived relations define relations
based on existing signatures, while we haven't got any such signature for
events, only predicates. No problem! Let's introduce a signature (more
precisely: an enumeration, since the required atoms are known and we won't need
to add fields) representing event names. Observe how we use the capitalised
names of predicates (corresponding to events) as elements of the enumeration,
in order to enhance readability. 

.. code-block::

  enum Event { Stutter, Initiate, Send, Process } // event names

.. index:: themes; customisation

Also, in the theme customisation menu, change the shape and colour of events, for instance to a red parallelogram. Then set :guilabel:`Hide unconnected nodes` to :guilabel:`On` for :code:`Event` nodes, as we don't want to see all event names at all states, but only those corresponding to events *occurring in a given state*.

.. index::
   single: function, Alloy

Now, let's introduce a first derived relation, which should be populated when the :code:`stutter` event happens. Recall that derived relations that refer to mutable elements are evaluated in the state they are being called from.

.. index::
   relation comprehension

.. code-block::

  fun stutter_happens : set Event { 
    { e: Stutter | stutter }
  }

This definition may seem strange at first but this is indeed what we want: the :code:`stutter_happens` derived relation yields, in every state, a subset of :code:`Event` that will be populated (by the name :code:`Stutter`) if the :code:`stutter` predicate is true, and empty otherwise.

Observe the effect of adding this derived relation on visualisation. First, open the theme customisation menu and set both :guilabel:`Hide unconnected nodes` and :guilabel:`Show as labels` to :guilabel:`Off` for :code:`stutter_happens`. This will override the hiding of :code:`Event` nodes that belong to :code:`stutter_happens`. Then head to the last states of the trace (where the :code:`stutter` event happens). You will now be able to observe the event happening, as shown below.

.. image:: instance2.png
   :align: center

Now, let's consider the :code:`initiate` event. This event takes a node as a parameter. In this case, the derived relation shouldn't just yield the :code:`Initiate` name as we wouldn't be able to tell for which node or nodes it is satisfied. We rather return the set of all pairs whose first coordinate is the :code:`Initiate` name and whose second coordinate is a node on which the :code:`initiate` event happens:

.. code-block::

  fun initiate_happens : Event -> Node {
    { e: Initiate, n: Node | initiate[n] }
  }

Now the first state of the trace is as follows. Since :code:`Event` nodes
related by :code:`initiate_happens` are no longer unconnected, they will show
up in the visualization without needing to change theme as was the case for
:code:`stutter_happens`.

.. image:: instance3.png
   :align: center

We can finally proceed with the last two events:

.. code-block::

  fun send_happens : Event -> Node -> Id {
    { e: Send, n: Node, i: Id | send[n, i] }
  }

  fun process_happens : Event -> Node -> Id {
    { e: Process, n: Node, i: Id | process[n, i] }
  }

As you start visualising a trace, you may realise that the depiction of events without further theme customization is deficient when an event takes two parameters or more. A possible enhancement is to show event parameters as labels rather than edges. To do so, we can introduce a further derived relation that just returns the set of names of all occurring events.

.. code-block::

  fun events : set Event { 
    stutter_happens + initiate_happens.Node + (send_happens + process_happens).Id.Node
  }

Note that, for instance, expression :code:`initiate_happens.Node` projects away any parameter of initiate events and keeps only the event name.
Then the following theme can be configured:

  - Uncheck :guilabel:`Hide unconnected nodes` for the :code:`events` set and set :guilabel:`Show as labels` to :guilabel:`Off`.
  - In the :guilabel:`relations` part, set all derived relations for events to :guilabel:`Show as attribute` and change the displayed name for the derived relations to :code:`args`.

This way, we get the following depiction. Notice how the arguments of events can be seen clearly (*e.g.* :code:`Node0` and :code:`Id2` for the event :code:`send` in state 1).

.. image:: instance4.png
   :align: center

This is it for the idiom enabling a more informative depiction of traces!

At the beginning of this section, however, we also said that the idiom is useful to specify certain classes of formulas in a nice way. Let's explore this aspect. First, the idiom allows to greatly simplify the :code:`traces` fact!

.. code-block::

  fact traces {
    // possible events
    always some events
  }

You may also check whether it is possible to witness the occurrence of two events in the same state, which happens to be the case.

.. code-block::

  check at_most_one_event {
    always lone events
  } for exactly 3 Node, exactly 3 Id

However, if, for example, we remove the guard from event :code:`initiate` this property yields the following counter-example, where an occurrence of :code:`initiate` is undistinguishable from stuttering. This was an issue already explored back in chapter :ref:`protocol-design`.

.. image:: instance6.png
   :align: center

           
More importantly, notice that predicates and functions belong to different namespaces in Alloy. Additionally, they can always be disambiguated based on the syntactic context. For this reason, it is possible to give to the functions defined above the same name as the respective predicates!

.. code::

  fun stutter : set Event { 
    { e: Stutter | stutter }
  }

  fun initiate : Event -> Node {
    { e: Initiate, n: Node | initiate[n] }
  }

  fun send : Event -> Node -> Id {
    { e: Send, n: Node, i: Id | send[n, i] }
  }

  fun process : Event -> Node -> Id {
    { e: Process, n: Node, i: Id | process[n, i] }
  }

  fun events : set Event { 
    stutter + initiate.Node + (send + process).Id.Node
  }

Now suppose you want to see the example of a trace in which two :code:`process` events happen in a row (for some arguments). Until now, you would have had to write this in a rather contrived way, for instance as follows.

.. code-block::

  run two_process_in_a_row {
    eventually (
      (some n: Node, i: Id | process[n, i]) and 
      after (some n: Node, i: Id | process[n, i])
    )
  } for exactly 3 Node, exactly 3 Id

Yet, the derived relations defined above are also useful to say that an event happens (for some parameters). Indeed, it is enough to say that the corresponding derived relation is non-empty!

.. code-block::

  run two_process_in_a_row {
    eventually (some process and after some process)
  } for exactly 3 Node, exactly 3 Id

Thus, giving the same name to a predicate (representing an event) and to the respective derived relations makes it easy to say that an event :code:`e` happens: you just have to write :code:`some e`!

As a final remark, notice that this idiom doesn't entail any performance penalty:

  - If derived relations are only used for the depiction of events, they are only computed when visualising instances.
  - If they are also used in formulas, to say for instance that an event happens, they actually use less variables than the version where a predicate is passed arguments quantified existentially.

Thus, the only price to pay is a small but systematic inflation, albeit admittedly tedious, of our models. In the future, an extension to Alloy may be proposed to automate this task.



.. index::
   Alloy Analyzer; evaluator

.. _evaluator:

Using the evaluator to debug specifications
==================================================

Chapter :ref:`structural-design` has briefly introduced the evaluator provided
by the Analyzer. The evaluator, accessible through the :guilabel:`Evaluator`
button in toolbar of the instance visualiser, allows the user to evaluate any
formula or expression over the instance currently opened in the visualizer.
For instance, let us get back to the last example instance from the previous
section. The evaluator can be used to query simple elements of the model, like
signature :code:`Dir`, field :code:`entries` or function :code:`empty_dirs`,
presenting their values for the current instance (the tuple set in tabular
style for an expression, :code:`true`/:code:`false` for a formula). But
perhaps more interesting, the evaluator is also able to interpret any valid
relational expression or formula. For instance, one may wish the content of
all directories by evaluating :code:`entries.object`, or even apply it to the
concrete signature :code:`Root`. Or one can query whether there is
:code:`some` empty directory in the instance. The result is depicted as
follows. Note that you can navigate through the evaluator log with :kbd:`↑`
and :kbd:`↓`.

.. image:: evaluator1.png
   :align: center

A feature of the evaluator that is particularly helpful when inspecting a
instance, is that unlike in the model specification, we can refer to concrete
atoms in the expressions passed to the evaluator. This is possible because
once a concrete instance is known, the universe of atoms is fixed. To refer to
a concrete atom, you should use the label of its most specific sub-signature
as the prefix and its numerical identifier as a suffix, separated by a
:code:`$` mark (except for :code:`Int` and :code:`String` atoms, which are
referred by their concrete values).. Note that subset signatures do not affect
the name of an atom (since each atom may belong to multiple subsets). Back to
the example, you can for instance query the content of directory :code:`Dir$0`
with :code:`Dir$0.entries.object` (which happens to be empty). You can also
call model functions or predicates with atoms as arguments. For instance,
consider a predicate that tests whether a given directory is empty:

.. code-block::

  pred empty_dir[d:Dir] {
    d in empty_dirs
  }

You could now simply call :code:`empty_dir[Dir$0]` in the evaluator. The
result is shown below.

.. image:: evaluator2.png
   :align: center


.. note:: Atom name mismatch.

  You may have noticed some differences between the atom names in calls to the
  evaluator and their representation in the evaluator response and in the
  visualizer, namely the absence of the :code:`$` mark. That's because the
  some pretty printing is employed to ease readability, but the evaluator must
  be able to distinguish an atom :code:`A$0` from a model signature :code:`A0`
  (recall that signature names are alpha-numerical).

  Note also that any theme customization applies only to the graph view, and
  not to the evaluator. This means that, for instance, if you change the label
  of a signature or relation in the theme, the evaluator will still only
  recognize and print the original label. If this gets confusion, you can
  always temporarily tick the option :guilabel:`Use original atom names` in
  the theme customizer.


If the instance under analysis is a trace, temporal expressions and formulas
can be freely used, and are evaluated from the currently focused state (the
one at the left-hand side of visualization). For instance, consider an
:code:`example` trace from chapter :ref:`protocol-design` where a leader is
eventually elected at the 8th state. Focusing on the 7th state, as shown
below, one can inspect how the state changed between those two states. For
instance,  calling :code:`Elected` and :code:`Elected'` will show that a node
has been elected leader. We can also evaluate temporal formulas, in this case
testing whether there had been any leader in the past, or whether there will
be some in the future (false and true, respectively, as expected). Another
interesting use of the evaluator is to understand which event has happened
between two states. As explained in :ref:`protocol-design`, since events are
just regular predicates they are not depicted in the instance, and the next
section will precisely present an idiom to visually depict the occurring
events. However, you can also just call the event predicates from the
evaluator and test their occurrence, including with concrete atom as
arguments.

.. image:: evaluator3.png
   :align: center

As a last note, it is worth mentioning that evaluation over a specific
instance is very efficient, so it can be used regularly.

.. _testing:

Defining test scenarios with formulas
=====================================

.. index::
   scenario

As an Alloy specification increases in size and complexity, its validation
through the exploration of arbitrary instances in the visualizer becomes less
useful, since getting varied instances is increasingly unlikely. This is even
more patent when exploring trace instances, despite the exploration operations
provided by the visualizer. At that point, one must combine this exploration
with the specification of finer :code:`run` commands. Note that often we don't want
the command completely fix the instances since we want to be able to explore
the design. Instead, we want to partially specify interesting *scenarios* that
the Analyzer will complete by solving the specification's constraints. This is
not necessarily trivial for complex specifications.

This first issue we often face is the inability to refer to concrete atoms in
Alloy specifications. Let's start with the specification of scenarios for
instances without mutable signatures and fields, on which we will later build
to specify trace scenarios. Let's consider the structural part of the leader
election example from chapter :ref:`protocol-design` and say that we want to
explore scenarios with 3 nodes with sequential identifiers.

.. index::
   command; run
   quantifier; disj
   quantifier; existential

We can achieve through an idiom based on :code:`some`/:code:`disj` patterns.
For instance, the scenario above could be defined as follows.

.. code-block::

  run scenario {
    some disj n1, n2, n3 : Node, i1, i2, i3 : Id { 
      Node = n1 + n2 + n3
      Id   = i1 + i2 + i3
      next = i1 -> i2 + i2 -> i3
      succ = n1 -> n2 + n2 -> n3 + n3 -> n1
      id   = n1 -> i1 + n2 -> i2 + n3 -> i3
    }
  } for 3

The :code:`disj` keyword is needed in order to avoid the assignment of the
same atom to different variables. For instance, without :code:`disj` here a
single node atom assigned to :code:`n1`, :code:`n2` and :code:`n3`, pointing
to itself, would be a valid instance. Moreover, the equality test with
:code:`Node` guarantees that no other atom will exist in :code:`Node` besides
the 3 quantified. The subsequent lines enforce the value of the fields to
define the desired ring topology. Always make sure that there are enough
atoms in the scope to represent the scenario, otherwise the command will
be trivially unsatisfiable. 

Due to the mechanics explained in section :ref:`aux-viz`, the quantified
variables appear identified in the visualizer, prefixed by a :code:`$` and the
name of the command, as shown below. This can be customized in the theme.

.. image:: sce1.png
   :align: center

Note that, as with anything Alloy, these specifications can be mixed with
other constraints. For instance, the same scenario, where identifiers are
sequential, could be equally specified as follows.

.. code-block::

  run scenario {
    some disj n1, n2, n3 : Node, i1, i2, i3 : Id { 
      Node = n1 + n2 + n3
      Id   = i1 + i2 + i3

      all n : Node | n.id.(next + last -> first) = n.succ.id
    }
  } for 3

As :code:`run` commands become more restricted, they become less interesting for
validation, since the room for unpredictable results is reduced. However,
these commands also serve a second purpose: they can be used as a kind of
*regression testing*, commands that we know must hold (or fail) for our
specification, and that can be re-executed whenever the specification evolves.
Alloy has an :code:`expects` keyword for commands that can help managing these
commands.

.. index::
   multiplicity constraint; one keyword

.. note:: What about multiplicity :code:`one` signatures?

  At first sight, one could declare 3 pairs of signatures with multiplicity
  :code:`one` extending :code:`Node` and :code:`Id` to specify all the atoms
  we need, and then call those signatures in :code:`run` commands. However, this
  approach has a major disadvantage: introducing such signatures in the
  specification affects all analysis commands in the specification. For
  instance, all :code:`check` commands would only consider instances
  where there were at least 3 nodes. Perhaps even worse, it would break
  the symmetry between those atoms, as they would no longer be
  uninterpreted, and isomorphic instances would be returned. Unless we are
  dealing with concepts of the domain model, we should not clutter our
  specifications with additional signatures. The :code:`some`/:code:`disj`
  pattern provides a way to specify scenarios that is local to each
  command.

.. index::
   temporal operator; sequence

Moving to the mutable context, we must now extend such formulas to restrict
multiple states. The main issue here is that with the temporal operators we
have seen so far, this would result in either nested :code:`and`/:code:`after`
formulas, or expressions with several appended primes :code:`'`, neither being
a scalable approach. Luckily, Alloy has a sequential temporal operator
:code:`;` that greatly eases specifying such formulas. For instance, the code
below restricts the value of inboxes and outboxes in the first 3 states.

.. code-block::

  run scenario {
    some disj n1, n2, n3 : Node, i1, i2, i3 : Id { 
      Node = n1 + n2 + n3
      Id   = i1 + i2 + i3
      next = i1 -> i2 + i2 -> i3
      succ = n1 -> n2 + n2 -> n3 + n3 -> n1
      id   = n1 -> i1 + n2 -> i2 + n3 -> i3

      no outbox; outbox = n1 -> i1; outbox = n1 -> i1 + n2 -> i2
      no inbox;  no inbox;          no inbox
    }
  } for 3 but 10 steps

Again, we can leave these formulas as underspecified as we wish. For instance,
we are not restricting the value of :code:`Elected`, which will be solved
during analysis. Moreover, by restricting only 3 states, the succeeding ones
will be freely solved by the Analyzer. Again, make sure that there are steps
in the scope to represent the scenario. Alternatively, one could enforce a
final state forbidding any further changes with a temporal :code:`always` as
follows.

.. code-block::

  run scenario {
    some disj n1, n2, n3 : Node, i1, i2, i3 : Id { 
      Node = n1 + n2 + n3
      Id   = i1 + i2 + i3
      next = i1 -> i2 + i2 -> i3
      succ = n1 -> n2 + n2 -> n3 + n3 -> n1
      id   = n1 -> i1 + n2 -> i2 + n3 -> i3

      no outbox; outbox = n1 -> i1; always outbox = n1 -> i1 + n2 -> i2
      no inbox;  no inbox;          always no inbox
    }
  } for 3 but 10 steps

.. image:: sce2.png
   :align: center

In fact, all formulas inside the sequence can also be temporal, but they
become difficult to manage outside this pattern.

The example above followed a relation-wise definition of the trace. Sometimes,
however, it's easier to think about scenarios state-wise, particularly for
relations closely related. Following this idiom, this could also be achieved
as follows.

.. code-block::

  run scenario {
    some disj n1, n2, n3 : Node, i1, i2, i3 : Id { 
      Node = n1 + n2 + n3
      Id   = i1 + i2 + i3
      next = i1 -> i2 + i2 -> i3
      succ = n1 -> n2 + n2 -> n3 + n3 -> n1
      id   = n1 -> i1 + n2 -> i2 + n3 -> i3

      no outbox + inbox; 
      outbox = n1 -> i1 and no inbox; 
      always (outbox = n1 -> i1 + n2 -> i2 and no inbox)
    }
  } for 3 but 10 steps


As a last tip, sometimes we end up defining multiple scenario commands that
share a certain part of the specification. At this point it is often useful to
refactor-out parts of the specification into derived predicates. For
instance, if we wanted to define multiple scenarios for the same ring
topology:

.. index::
  predicate, Alloy

.. code-block::

  pred seq_ring [n1, n2, n3 : Node, i1, i2, i3 : Id] {
    Node = n1 + n2 + n3
    Id   = i1 + i2 + i3
    next = i1 -> i2 + i2 -> i3
    succ = n1 -> n2 + n2 -> n3 + n3 -> n1
    id   = n1 -> i1 + n2 -> i2 + n3 -> i3
  }

  run scenario {
    some disj n1, n2, n3 : Node, i1, i2, i3 : Id { 
      seq_ring[n1,n2,n3,i1,i2,i3]

      no outbox + inbox; 
      outbox = n1 -> i1 and inbox = n1 -> i1; 
      always (outbox = n1 -> i1 + n2 -> i2 and inbox = n1 -> i1 + n2 -> i2)
    }
  } for 3 but 10 steps