Arrow multiplicity constraints¶

When declaring fields in an Alloy model, one can only restrict the multiplicity of the target signature. Multiplicities on the source signature can be enforced in facts using regular relational logic, as we’ve seen in the Structural modeling chapter. However, Alloy also provides a special formula syntax to directly constrain the multiplicities of both end points of a relation.

Enforcing multiplicities with arrows¶

Consider a relation r between atoms of signature A and atoms of signature B. Let’s say we want to state that r relates every atom of source signature A to at most one atom of target signature B, and every atom of B to at least one atom of A, we could write the formula r in A some -> lone B. This kind of atomic formula can use the same multiplicities as the declaration of signatures and fields (set, some, lone, and one). Not stating a multiplicity next to an end point is the same as having multiplicity set.

Recall fact no_shared_entries from the Structural modeling chapter, repeated below.

fact no_shared_entries {
  // Entries cannot be shared between directories
  all e : Entry | lone entries.e
}

With this special syntax, we could rewrite it simply as follows.

fact no_shared_entries {
  // Entries cannot be shared between directories
  entries in Dir lone -> Entry
}

The constraint entries in Dir lone -> Entry forces relation entries to be injective, a relation where no two atoms of the source signature point to the same target atoms. This is one of the four basic properties of relations we can obtain by varying the multiplicities of the source and target signatures. If we had entries in Dir some -> Entry we would have a surjective relation, one where every atom of the target is related to some source atom. If entries in Dir -> lone Entry relation entries would be simple (or a partial-function), a relation where every source atom is related to at most one target. And if entries in Dir -> some Entry relation entries would be entire (or total), since every source atom is related to at least one target.

As another example, recall the fact one_directory_per_entry.

fact one_directory_per_entry {
  // Entries must belong to exactly one a directory
  all e : Entry | one entries.e
}

This could also be rewritten as the following fact, stating that entries is both injective and surjective (note that multiplicity one is the combination of multiplicities lone and some).

fact one_directory_per_entry {
  // Entries must belong to exactly one a directory
  entries in Dir one -> Entry
}

Alloy model

Full model for the section

Download and explore the files relevant for the model at this point of the book.

A bestiary of binary relations¶

By combining these four properties we get additional well-known kinds of relations. A relation that is both entire and simple is a function: every atom of the source is related to exactly one target. A representation is a relation that is both entire and injective, and dually, an abstraction is a relation that is both simple and surjective. An injection is a function that is also a representation, and a surjection is a function that is also an abstraction. Finally, by combining all four basic properties we get a bijection: a one-to-one mapping between the source and the target signatures. The following table summarizes these properties, and presents the full “bestiary” of binary relations that can be obtained by imposing multiplicity constraints on the source and target signatures.

injective	entire			simple		surjective
`A lone -> B`	`A -> some B`			`A -> lone B`		`A some -> B`
representation		function			abstraction
`A lone -> some B`		`A -> one B`			`A some -> lone B`
injection			surjection
`A lone -> one B`			`A some -> one B`
bijection
`A one -> one B`

Alloy model

Full model for the section

Download and explore the files relevant for the model at this point of the book.

Beyond restricting fields¶

Multiplicity arrows are more expressive than setting the multiplicity of a field between signatures, and can actually set the multiplicity of an arbitrary relation between arbitrary domains and ranges. Recall fact no_shared_dirs from the main chapter.

fact no_shared_dirs {
  // A directory cannot be contained in more than one entry
  all d : Dir | lone object.d
}

This pattern looks like the one for injectivity, but it is only restricting the portion of field object that relates to directories (object is a relation from Entry to Object). Using the Alloy range restriction operator :>, we can obtain the portion of object related to directories (object:>Dir), and then restrict it to be injective with a multiplicity arrow. This would result in following equivalent version of no_shared_dirs.

fact no_shared_dirs {
  // A directory cannot be contained in more than one entry
  object:>Dir in Entry lone -> Dir
}

For yet another example, recall fact no_dangling_objects.

fact no_dangling_objects {
  // Every object except the root is contained somewhere
  Entry.object = Object - Root
}

Expression Entry.object retrieves all objects related to an entry. By equalling it to Object - Root, we’re saying that every object, except the root, must be related to some entry by object. So we’re essentially stating that object is surjective on a restricted range. So the following is an equivalent version of no_dangling_objects using multiplicity arrows.

fact no_dangling_objects {
  // Every object except the root is contained somewhere
  object in Entry some -> (Object - Root)
}

Alloy model

Full model for the section

Download and explore the files relevant for the model at this point of the book.