$(20$ points$)$ Consider there are two users, Sam and Angela, and a single autonomous system, a

Drone. Both users develop different programs to run on the Drone, and every now and then

they want to remotely execute their programs on the Drone. Since, there is only one Drone, only

one user can test the programs at a time. Consider the following atomic propositions for Sam

$($similar atomic propositions exists for Angela$)$:

Sam.request ::$=$ indicates that Sam requests usage of the Drone;

Sam.use ::$=$ indicates that Sam uses the Drone;

Sam.release ::$=$ indicates that Sam releases the Drone.

For Angela, similar predicates are defined. Specify the following properties using Uppaal's notation

TCTL $($AP$,$ A$[]$P$,$ EP$,$ E$[]$p$,$ p $->$ q and A$[]$ not deadlock$)$ and identify if any further variables are

needed to specify the properties. If so declare them and include them in the formal properties.

$($a$)$ Mutual exclusion, i$.$e$.,$ only one user at a time can use the Drone.

$($b$)$ Finite time of usage, i$.$e$.,$ a user can use the Drone for a finite amount of time.

$($c$)$ Absence of individual starvation, i$.$e$.,$ if a user wants to test the Drone, he$/$she eventually is

able to do so$.$

$($d$)$ Absence of blocking, i$.$e$.,$ a user can always request to use the Drone

$($e$)$ Alternating access, i$.$e$.,$ users must strictly alternate in using the Done.