Multiplicity Markings

When defining a field of a signature to be a relation, you write something like this:

  sig University {
    groupMember: Student -> Professor
  }

Here, each University knows which student is a member of which professor's research group. That is, there is a relation from Universities to Students to Professors. By writing multiplicity markings to the declaration of the relation, we can add additional constraints in a concise way. For example,

  sig University {
    groupMember: Student -> one Professor
  }

means that each student is in exactly one professor's research group. If we instead wrote this,

  sig University {
    groupMember: Student -> lone Professor
  }

Then we are saying that some students may be in no research group, but no student is in more than one. Lastly, we can write

  sig University {
    groupMember: Student -> some Professor
  }

to say that each student is in one or more research groups. When no multiplicity markings are present, there are not constraints.

You can also write multiplicity markings before the arrow. For example,

  sig University {
    groupMember: Student some -> Professor
  }

This says that every professor has at least one student in his or her research group. We can put markings on both sides of the arrow as such:

  sig University {
    groupMember: Student some -> lone Professor
  }

Here, every research group has at least one student, and each student is in up to one research group.

You can also place the lone and one multiplicity markings on signatures to control how many copies of that signature can exist (or, really, how many elements can ever be in that set defined by that signature). For example:

  one sig Root {...}
  lone sig University {...}
  some sig InitialState {...}