R53

R53 / 1c:1c-1

Cabin is going to zero or one Accessible Shaft Level

Accessible Shaft Level is current destination of zero or one Cabin

---

At any given point in time, a Cabin may or may not have a next destination. If there are no pending floor service requests and no stop requests for a given Shaft, the associated Cabin will have no destination.

A Cabin is directed to one destination at a time, so an Accessible Shaft Level is the current destination of a Cabin only if the Cabin has been dispatched to that location.

Formalization

Transfer.Shaft -> Cabin.Shaft
Transfer.(Destination floor, Shaft) -> Accessible Shaft Level.(Floor, Shaft)

The Cabin can only be going to an Accessible Shaft Level in the same Shaft as the one the Cabin travels through, so the Shaft referential attribute is the same in both referenced classes and is consequently merged.