draw of my situation
In the link above, we can see the class Student and Class. I want to make an invariant constraint to make sure a Student can't register for more than 5 classes each sessionYear.
With this constraint, I can determine if Student as more than 5 classes
context Student
inv maxClassStudent: classTaken->collect(sessionYear)->size() < 6
But, what I want is to find the size for a collection formed only with the same sessionYear. In other words, I wish to make a collection for every different sessionYear to verify if, for that year, the Student had less than 6 classes.
I thought that I could maybe make use of forAll(c1,c2|c1<>c2 implies c1.sessionYear <> c2.sessionYear) or something similar to difference Class based on its sessionYear, but I can't seem to figure it out.
Hard problems are often soluble by breaking them into smaller pieces...
let sessionYears = classTaken->collect(sessionYear)->asSet() in sessionYears->forAll(sy | classTaken->select(sessionYear = sy)->size() < 6)