Alloy4Fun Courses is Exercise 1.e in Structural design with Alloy in the book Formal Software Design with Alloy 6. I am working through it and have been quite confused by its predicate inv13, and now that I have figured it out, I think it is wrong, as in I think it is not specified as intended.
The description of pred inv13 reads:
A student with the highest mark in a course must have worked on a project on that course
I understand it as that for any given course c, among all students enrolled in c, given the student s who has got the highest grade, s must have worked on a project mandated by c.
Therefore I set out to specify it as Listing 1:
// Listing 1
all s : Student, c : Course | grades[c][s] = grades[c][Student].max
implies some s.projects & c.projects
Alloy then gave me an instance with a course having no grades, for which this would reject, because for that c there are no s and thus no s.projects. (I love Alloy for this.) So I put in or no c.grades to handle this case (Listing 2):
// Listing 2
all s : Student, c : Course | grades[c][s] = grades[c][Student].max
implies some s.projects & c.projects or no c.grades
Alloy then presented Figure 1:
Figure 1 image not embedded due to forum limit
I was greatly confused by this instance. Person0 is the only Student, so Person0 has the highest Grade in every Course, including Course0. By the description, Person0 “must have worked on a project on” Course0. Yet “ThisShouldBeAccepted”?
Remembering the shock from Alloy4Fun Photo Sharing Social Network, I went into detective mode. Maybe I should accept that some courses have no projects? I appended or no c.projects (Listing 3):
// Listing 3
all s : Student, c : Course | grades[c][s] = grades[c][Student].max
implies some s.projects & c.projects or no c.grades or no c.projects
Alloy replied with Figure 2:
Figure 2 image not embedded due to forum limit
I have manually adjusted the positions of the nodes to show the similarities and differences of this instance with the previous one. By my understanding, this instance is in principle the same as the previous one. Person0 is the only Student, who has the highest Grade in both Course0 and Course1, but Person0 has not worked on a project on Course0. Yet “ThisShouldBeRejected”?
After going back and forth on or no c.projects for an hour or so, I got hit by a thought: what if “the highest mark” is specified differently? Instead of the highest within each course, what if it is the highest among all courses? After some more trial and error, I arrived at Listing 4 which has prompted Alloy to give me the final revealing instance (Figure 3):
// Listing 4
all s : Student, c : Course | grades[c][s] = grades[Course][Student].max
implies some s.projects & c.projects or no c.grades
Figure 3
Figure 3 was what hinted to me that what matters is Grade2, that is, Grade.max. Sure enough, changing that gets me the “No counter-example found” (Listing 5):
// Listing 5
all s : Student, c : Course | grades[c][s] = Grade.max
implies some s.projects & c.projects or no c.grades
To review the description of predicate inv13:
A student with the highest mark in a course must have worked on a project on that course
I do not think Grade.max is a plausible stretch to make from “the highest mark in a course”.
More importantly, I think in this model Listing 5 is far less meaningful a predicate than inv13 as described.
P.S.: I later found out that I can also get Figure 3 by pressing “Next instance” more times on Listing 2.