Alternatives for "one" and appended facts

Alternatives to "one" and appended facts

In File System Lesson 1, we wrote

  // There exists a root
  one sig Root extends Dir { } { no parent }

Equivalently, we could have accomplished the same effect by writing two additional facts:

  sig Root extends Dir { }
  fact { one Root }
  fact { no Root.parent }

We could also combine those two fact statements into one. Notice that when more than one constraint appears in a fact, they are automatically conjoined together as if you used the && operator.

  sig Root extends Dir { }
  fact {
    one Root
    no Root.parent
  }

We could also reword the second constraint in the fact (although there is no particular reason to do so) as follows:

  sig Root extends Dir { }
  fact {
    one Root
    all r:Root | no r.parent
  }

this rewriting works because "." gets mapped onto the elements of a set it is applies to.

Both of these syntatic shorthands can make a model more concise and clearer, but are not always appropriate. When and how you use them is a matter of style.