R43 - modelint/types GitHub Wiki
R43 / 1:1c
Cabin is at exactly one Shaft Level
Shaft Level is location of zero or one Cabin
As a Cabin travels up and down it crosses Floor boundaries. The Transport service will update the current Floor location as the Cabin passes each Floor.
When a Cabin is between Floors moving up, the current Floor location will be the latest lower Floor boundary passed by the approximate midpoint of the Cabin. (The exact location can vary depending on where the sensors are located).
Going down, the current Floor location will be the latest upper Floor boundary passed by the approximate Cabin midpoint.
This means that the Cabin position will always be the last updated location. So a Cabin will always have a current location corresponding to a single Shaft Level.
A given Shaft Level may or may not be the current location of the Shaft’s Cabin.
Formalization
Cabin.(Shaft, Current floor) -> Shaft Level.(Shaft, Floor)