Permanent link:


Final Model:

pred Inv1 {

// A phone number cannot belong to two different contacts

	all disj c1, c2: Contact | no c1.phones & c2.phones

}

pred Inv2 {

// Every called number belongs to a contact

	all c: Call | c.number in Contact.phones

}

pred Inv3 {

// Simultaneous calls cannot exist

	no disj c1, c2: Call | c1.time = c2.time

}



--------------------------------------------------------------------------

Permanent Link:


Final Model:

pred Inv1 {

// Each student must be enrolled in at least one course

	all s: Student | some c: Course | s in c.enrolled

}

pred Inv2 {

// All the members of a team are enrolled in the respective courses

	teams.members in enrolled

}

pred Inv3 {

// Only enrolled students can have a grade in a course

 grade.Grade in enrolled

}