Syntax for appended facts

An appended fact is written by placing constraints in curly braces immediately after a sig statement. They can make a model clearer by logically grouping related constraints together.

  sig name {
    // fields of the signature
  }{
    // appended fact constraints
  }

Any field mentioned in the appended fact has an implied "all this:name |" at its beginning, and an implied "this." in front of it. Thus:

  sig Person {
      closeFriends: set Person,
      friends: set Person
  } {
      closeFriends in friends
  }

is really saying

  sig Person {
      closeFriends: set Person,
      friends: set Person
  }

  fact {
      all x:Person | x.closeFriends in x.friends
  }

Consequently, appended fact can be more concise (and thus clearer) than the equivalent non-appended fact. However, there is also a danger in forgetting that every field mentioned in an appended fact is prepended with "this.".