CSE 128 Spring 2004

Problem 2.3: For the first part of the question, remember that "leads to" is typed as "~>". For the book, the macro package changes the tilda to a space.

To solve the second part of this question, you need to define two properties: one for the conjunction of two weak fairness properties and one for weak fairness on the disjunction of the two actions. Call these two properties F1 and F2. You will show that AltSpec => (F1 => F2) /\ (F2 => F1). That is, you show that of all the behaviors of AltSpec (which includes no fairness), those that satisfy F1 also satisfy F2 and vice versa.

Problem 2.8:  For RelayRing, use Call as the external action, and have the parameter be a pair <i, v> where i is the  process and v
is a value from Input. For example, if Input is {0, 1} and N = 3, then a behavior might be:

arg: <0, 0> -> arg: <1, 1> -> arg: <2, 1>; arg: <0, 1> -> ...

TokenPass will generate the same external actions.