Concurrent Programming (19530-V)

Dr. Richard S. Hall WS 01/02

- Übung 8 -

Assigned: 19.12.2001
Due: 8.1.2002

1. Exercise

a) How do terminal state sets help us locate progress property violations?
b) What affect does changing action priorities have on an LTS graph? Why would you want to change action priorities?
c) Why did lowering the priorities of the exit actions in the SingleLangeBridge process cause a progress property violation?

2.  Exercise

On question 3 of Übung 6, we modeled a maze. In preparation for the project, create a new FSP model for that maze that allows north, south, east, and west movement actions as before, but additionally models the fact that a maze cell may be occupied and that there can only be one occupant at a time.

Hint: You will want to be able to query the state of a cell to determine if it is occupied or not. This model is actually similar to the ticket reservation system from question 3 of Übung 3; the solution for that exercise is presented below but the solution to the maze is not identical to the ticket system so do not try to copy it verbatim, just use it for ideas:

const False = 0
const True = 1
range Bool = False..True

SEAT = SEAT[False],
SEAT[reserved:Bool]
    = (reserve->SEAT[True]
      |query[reserved]->SEAT[reserved]
      |when (reserved) reserve->ERROR).

range Seats = 0..1
||SEATS = (seat[Seats]:SEAT).

LOCK=(acquire->release->LOCK).

TERMINAL = (choose[s:Seats]->acquire
    ->seat[s].query[reserved:Bool]
        ->if (!reserved) then
            (seat[s].reserve->release->TERMINAL)
          else
            (release->TERMINAL)).

||CONCERT = ({a,b}:TERMINAL || {a,b}::SEATS || {a,b}::LOCK).