Tuesday, 29 September 2009

Roller-coaster

A roller-coaster control system only permits its car to depart when it is full. Passengers arriving at the departure platform are registered with the roller-coaster controller by a turnstile. The controller signals the car to depart when there are enough passengers on the platform to fill the car to its maximum capacity of M passengers. The car goes around the roller-coaster track and then waits for another M passengers. A maximum of M passengers may occupy the platform. Ignore the synchronization detail of passengers embarking from the platform and car departure. The roller coaster consists of three processes: TURNSTILE, CONTROL and CAR. TURNSTILE and CONTROL interact by the shared action passenger indicating an arrival and CONTROL and CAR interact by the shared action depart signaling car departure. Draw the structure diagram for the system and provide FSP descriptions for each process and the overall composition.
const M = 3
TURNSTILE = (passenger -> TURNSTILE).
CONTROL = CONTROL[0],
CONTROL[i:0..M] = (when (i CONTROL[i+1]
|when (i==M) depart -> CONTROL[0]).
CAR = (depart -> CAR).
||ROLLERCOASTER = (TURNSTILE || CONTROL || CAR).

Museum

A museum allows visitors to enter through the east entrance and leave through its west exit. Arrivals and departures are signaled to the museum controller by the turnstiles at the entrance and exit. At opening time, the museum director signals the controller that the museum is open and then the controller permits both arrivals and departures. At closing time, the director signals that the museum is closed, at which point only departures are permitted by the controller. Give that it consists of the four processes EAST, WEST, CONTROL and DIRECTOR, draw the structure diagram for the museum and decide which should be threads and which should be monitor(s).

Represent the above case using FSP and justify your selection of monitor(s).

const N = 4

EAST = (arrive -> EAST).

WEST = (leave -> WEST).

DIRECTOR = (open -> DIRECTOR | close -> DIRECTOR).

CONTROL = CLOSED[0],

CLOSED[i:0..N] = (when (i==0) open -> OPENED[0]

|when (i>0) leave -> CLOSED[i-1]),

OPENED[i:0..N] = (close -> CLOSED[i] | when (i OPENED[i+1] | when (i>0) leave -> OPENED[i-1]).

||MUSEUM = (EAST || CONTROL || WEST).