One final comment: I'd be wary of the number of strongly fair labels you've placed in your spec. My understanding is that strong fairness is rarely used, as it's difficult to implement actual systems that satisfy it. It definitely has its place, but it's not common. Placing it on every process and label in your spec is most likely not the correct course of action.
I understand doing it given your initial assumption that "looping forever was prohibited by these strong fairness clauses", but as we've shown, your assumption was incorrect.
I just don't want you or your students to think that the right way to approach these specs is by marking everything as strongly fair.