$(3)$ Consider an elevator system that services $N>0$ floors

numbered $0$ through $N-1.$ There is an elevator door at

each floor with a call button and an indicator light that

signals whether or not the elevator has been called. In the

elevator cabin there are $N$ send buttons $($one per floor$)$ and

$N$ indicator lights that inform to which floor$($s$)$ is going to be

sent. For simplicity consider $N=4.$ Present a set of

atomic propositions try to minimize the number of

propositions that are needed to describe the following

properties of the elevator system as CTL formulae and

give the corresponding CTL formulae:

$($a$)$ The doors are safe, i$.$e$.,$ a floor door is never open if the

cabin is not present at the given floor.

$($b$)$ The indicator lights correctly reflect the current requests.

That is$,$ each time a button is pressed, there is a

corresponding request that needs to be memorized until

fulfillment $($if ever$).$

$($c$)$ The elevator only services the requested floors and does

not move when there is no request.

$($d$)$ All requests are eventually satisfied.