Advanced Programming: Concurrency, Lab 8

  1. Alter the code for the DiningPhilosophers so that forks may be picked up in any order. Is the system deadlock free? (Try to answer this before you do the test with LTSA)

  2. Are the following equivalent? Investigate the LTS graphs:

  3. Investigate the examples in Chapter 7:

  4. Look at the SingleLaneBridge.lts specification. First clean up the definition so that no warnings are given during LTSA compilation. Confirm that without the BRIDGE constraints you get property violations for ONEWAY.

  5. Look at the CongestedSingleLaneBridge.lts specification. Make sure you understand why you get BLUECROSS and REDCROSS progress violations even for 2 red and 2 blue cars.