Q$9.$ Suppose we have two users $U1$ and $U2,$ and a single printer. Both users print their

results on this printer. Since there is only a single printer, only one user can print a job at

a time. Suppose we have the following atomic propositions for U $1$ and U $2$ :

$"$U$1.$req" $("$U$2.$req"$)$: Indicates that U$1($U$2)$ requests usage of the printer.

$"$U$1.$use" $("$U$2.$use"$)$: Indicates that U$1($U$2)$ uses the printer.

$"$U$1.$release" $("$U$2.$release"$)$: Indicates that U$1($U$2)$ releases the printer.

Use PLTL to specify the following properties:

a$.$ Mutual exclusion: only one user at a time can use the printer. $(4$P$)$

b$.$ Finite time of usage: a user can print only for a finite amount of time. $(4$P$)$

c$.$ Absence of starvation: if a user wants to print something, he$/$she eventually is able to

do so$.(4$P$)$

d$.$ Alternating access: users must strictly alternate in printing. $(6$P$)$