The assignment for this week is to take the Alloy model net4.als and add something to it. This model is similar to others you have seen, but many details have been changed.
The network state includes requirements for middlebox insertion. Your job is to define predicates for checking that the requirements are satisfied. Also add constraints to the model state if they are needed for the requirements to make sense.
Email the model, with your additions clearly marked, to pzave@cs.princeton.edu by class time on the 28th.