Exercises from the book chapter 7: rest of 7.3, 7.4, 7.7, 7.8.

ADDITIONAL EXERCISE (if time):

 SYMMETRIC VERSION OF THE FAIR READERS/WRITERS


1. Consider the fair Readers/Writers solution of the book
where you introduce an event requestRead and count waiting
readers (waitingR). But you do not change the conditions (yet).

2. Check that you may NOT have two write cycles after each other
even when there are waiting readers.
Hint: Use LTSA analyser and create the trace.

3. (OPTIONAL) Make a property ALTERNATE which says that two write
cycles may not follow each other if there are waiting
readers. You may modify property SAFE_RW.  Check if this is
violated by the implementation.

4. Modify the symmetric implementation above so that it satisfies
the ALTERNATE conditions --  so that you may not have several write
cycles after each other when there are waiting readers.