Assignment for 21 February 2017

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.