Alloy traces and projection issues

Question

I find it very difficult to understand the way which traces and projections work in Alloy. I cannot get the desirable results.

In the following example I try to project over Course and see how students are enrolling, but it seems like they never have any relation.

When I use the normal view (without projection) I get multiple solutions which are fine.. but I want to know the way (step-by-step) of how they were created using traces (trace back).

open util/ordering[Course]
sig Student {}
sig Course {
    roster : set Student
}

pred Enroll (c, c' : Course, sNew : Student) {
    c'.roster = c.roster + sNew
}

pred init(c: Course) {
    no c.roster
}

fact traces {
    init[first]
    all c: Course - last | let c' = next[c] |
    some s: Student | Enroll[c, c', s]
}

pred show {}
run show for 5

Answer 1

I'm not sure of what you try to accomplish. I think the notion of Time is missing in your model. You would generally like to have a roster for a given course that is changing over this time concept.

It seems you bypassed this "good practice" by directly ordering the Course concept, so I guess you want the first Course to have no student, the second course to have a new one etc .... (which doesn't make much sense but nvm).

I guess the source of your disappointment is that when you make a projection over Course, you would expect to see the number of students in the Course roster varying when you go from Course to Course, and this is just not happening.

The reason is that when you write some s: Student | Enroll[c, c', s] you expect s to be totally new, while it only means that there's at least one. I suggest you write instead : some s: Student | s not in c.roster and Enroll[c, c', s]