The assignment for this week is to take the Alloy model net2.als and add something to it.
You will define a predicate Good_header_reversible that is true of a NetworkState if whenever some header h allows some node A to send packets that are received by another node B, then a header reverse_h allows B to send packets that are received by A. The header reverse_h is derived from h by reversing the source and destination names.
Also write a predicate and a run statement that produce a small readable example of reverse reachability.
The following predicate says that the receives relation, ignoring headers, is symmetric.
pred Receives_is_symmetric [w: NetworkState] { Header.(w.receives) = ~ (Header.(w.receives)) }
In other words, if B can receive packets from A, then A can receive packets from B. Use Alloy to prove that Good_header_reversible implies Receives_is_symmetric.
Email the model, with your additions clearly marked, to pzave@cs.princeton.edu by noon on the 21st.