Set of examples

Our first exploration

sig Person { }
sig Course {
  teacher  : Person,
  students : set Person
}

Everything is a set

sig Person { }
sig Course {
  teacher  : Person,
  students : some Person
} {
  no teacher & students
}

Counter-examples

assert NoTeacherIsStudent {
  all c1 : Course | no c2 : Course | c1.teacher in c2.students
}

check NoTeacherIsStudent for 3

Referees and players

abstract sig Person { }  // no elements
sig Referee extends Person { }
sig Player  extends Person { }

Matches for a given week

// a week is tied to a match
sig Week  { }
sig Match { week : Week }

fact EachWeekHasOneMatch {
  all w : Week | some week.w  // post-join
}

Cart model - describing a snapshot

open util/integer

one sig Product {
  available: Int
}

enum Status { Open, CheckedOut }

sig Cart {
  status: Status,
  amount: Int
}

There’s more!

Relations

sig Person { }

abstract sig Grade { }
one sig Fail extends Grade { }
sig Pass extends Grade { }

sig Course { 
  grades : Person -> one Grade
}

Dependent fields

sig Person { }
sig Team {
  players : set Person,
  captain : one players
}