Assume the following properties of a protocol:
W: Getting out of (the busy wait) region w requires a reset (falsity) of (the semaphore) xProve that these assumptions imply that the system requirement S (below) is necessary and sufficient for deadlock freedom (D).
P: Once out of w, a process will also exit p
F: Processes are treated fairly in getting out of wX: Only by entering v can x be reset
V: If a process is in (release) region v, then that process will eventually exit v with x reset
S: If some process is in w (with x set), then some process will get into vExpress each formula in TL and use STeP to prove this.
D: Every process always gets out of p