property PS = (a -> (b -> PS | a -> PS) | b -> a -> PS).
CARPARKCONTROL(N=4) = SPACES[N],
SPACES[i:0..N] = ( when(i>0) arrive -> SPACES[i-1]
| when(i<N) depart -> SPACES[i+1]
).
ARRIVALS = (arrive -> ARRIVALS).
DEPARTURES = (depart -> DEPARTURES).
||CARPARK = (ARRIVALS || CARPARKCONTROL(4) || DEPARTURES).
Specify a safety property that asserts that the car park does not
overflow. Specify a progress property which asserts that cars
eventually enter the park. If car departure has lower priority than
car arrival, does starvation occur? Specify an FSP composition with
action priority that you could use to check this (via LTSA's Check
Safety facility).
t0.noncrit.enter -> t0.noncrit.exit -> t0.inCS0.write[1] -> t0.turn.write[1] -> t0.inCS1.read[0] -> t0.turn.read[0] -> t0.crit.enter -> t0.crit.exit -> t0.inCS0.write[0]and similarly for Thread 1.
Show your solution to your tutor when done. COMP2310 students are expected to complete the first 3 parts, COMP6310 students all 4. Worth 1 Prac Point.
RW_LOCK = RW[0][False][0][0][False],
RW[readers:0..Nread][writing:Bool]
[waitingW:0..Nwrite][waitingR:0..Nread][readersturn:Bool] =
( when (!writing && (waitingW==0||readersturn))
acquireRead -> RW[readers+1][writing][waitingW][waitingR-1][readersturn]
| releaseRead -> RW[readers-1][writing][waitingW][waitingR][False]
| requestRead -> RW[readers][writing][waitingW][waitingR+1][False]
| when (readers==0 && !writing && (waitingR==0||!readersturn))
acquireWrite -> RW[readers][True][waitingW-1][waitingR][readersturn]
| releaseWrite -> RW[readers][False][waitingW][waitingR][True]
| requestWrite -> RW[readers][writing][waitingW+1][waitingR][readersturn]
).
Show your solution to your tutor when done. Worth
1 Prac Point.