Everything is a Relation (or an Atom) in Alloy

The Alloy universe consists of atoms and relations, although everything that you can get your hands on and describe in the language is a relation. Atoms only exist behind the scenes.

An atom is a primary entity which is

A relation is a structure which relates atoms. Each relation is a set of ordered tuples (vectors of atoms). Each tuple indicates that those atoms are related in a certain way (as dictated by the relation itself). The "arity" of the relation is the number of atoms in each tuple.

For instance, one might have an arity-2 relation called "works-in" which relates engineers with their cubicles. Each tuple indicates an engineer (an atom) and the cubicle he works in (another atom). If several engineers share the same cubicle C, then there will be more than one tuple in the "works-in" relation with C in the second slot. If an engineer D works in more than one cubicle, then there will be more than once tuple in the "works in" relation with D in the first slot.

In the real world, essentially nothing is atomic, but that won't stop us from modelling them as such. In fact, our modeling approach has no built-in notion of composits at all; to model some X consisting of parts A and B, we would make X, A, and B all atomic. To represent the fact that X is related to A and B in a special way, we would adjust the contains relation to map X to both A and B. Containment is just one example of a structural relationship, and there is little reason to single it out for special treatment.

Alloy does not contain explicit notions of sets and scalars, but they are easy to simulate. A set is simply an atom which the containment relation map to the contents of that set. When you declare a signature (using the sig construct ), you are defining both an atom which will behave as a set (and the body of the signature defines relations from that atom to other signatures.

Alloy does not distinguish between an atom and the set containing just that atom. Another concequence is that set membership and subset are the same thing; both are denoted in. Otherwise, Alloy set operations behave as you would expect. Alloy syntax does not permit you to directly refer to atoms. If you wish to constraint a particular atom, you can do what amounts to writing the equivalent constraint for the singleton set containing that atom and no other atoms. That is what we are doign when we write constraints about the Root directory, in Chapter 1.