How to think about an Alloy model: 3 levels

There are three basic levels of abstraction at which you can read an Alloy model.

Consider the following excerpt. A signature sig S, extending E, has a field F of type T.

  sig S extends E {
      F: one T

  fact {
      all s:S | s.F in T

The fragment can be roughly interpreted in an Object Oriented sense.

The fragment can be safely read as being about sets, elements, and relations among those sets and elements. Most users find this way of thinking intuitive after a little practice and does not lead to errors as the OO approach occasionally does.

In some sense, we are modeling a field of a class as a relation which maps instances of that class to instances of that field.

The technical meaning is in terms of atoms and relations, and is rather hairy. Most users do not need this level of understanding most of the time, but you may be curious about how things are working on the inside.