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
}