Syntax for writing sig statements

  sig name { }

Following each signature declaration, we find a signature body whose within a pair of braces. In the signature body, we can define a series of relations for which the set defined by the signature is the domain. For instance, in the FSObject signature body, we define a relation called "parent" which relates FSObjects to Dirs.

A sig may also have fields, which look like this (brackets indicate optional text):

  sig name {
    //most fields look like this:
    field-name-1: field-type-1,
    //A signature may refer to signatures not
    // defined until later in the model.

    //multiple fields with the same type look like this:
    field-name-2a, field-name-2b: field-type-2
  }

A signature extending another signature is a partition of that other signature:

  sig A extends C {
    //fields
  }

  sig B extends C {
    //fields
  }

means that A and B are disjoint subsets of C. If A and B have identical bodies, then we can get the same effect by writing

  sig A, B extends C {
    //fields
  }

We can use in instead of extends to get a slightly different effect -- in declares that one sig is a subsets of another, but does not enforce that it is disjoint from other sigs with the same parent. That is,

  sig A in C {
    //fields
  }

  sig B in C {
    //fields
  }

means that A and B are both subsets of C, but they are not necessarily disjoint. Once again, if A and B have identical bodies, we can use the shorthand

  sig A, B in C {
    //fields
  }

In general, two (or more) sigs which have the same definition may be declared together, like this:

  sig name1, name2 {
    //fields
  }

the abstract keyword is analogous to the abstract keyword of OO languages like Java, although it is not a perfect analogy. Consider some signature defined as follows:

  abstract sig Foo {
    //fields
  }

  sig Bar extends Foo {
    //fields
  }

  sig Cuz extends Foo {
    //fields
  }

By using the abstract keyword, we make guarantee that there will be no Foo that is not also either a Bar or a Cuz. However, had there been no signatures declared as subsets of Foo or extending it, then this restriction is relaxed; if a signature has no subsets then writing abstract has no effect.

You can force there to always be exactly one instance of (element in) a signature by using the one keyword. This also makes sure that every reference to this signature refers to the same atom.

  one sig name {
      // fields
  }

Examples:

  sig FSObject { }

  sig Dir {
      contents: set FSObject
  }

  sig FileSystem {
      root: one Dir,
      objects: set FSObject,
      contents: Dir lone->set FSObject,
      parent: FSObject set->lone Dir
  }