Description Class HallwaySection

INTENTION

This class provides all definitions to describe the hallway specific light requirements. Each hallway section is equipped with

• one group of not dimmable ceiling lights that are considered here as one ceiling light,
• three motion detectors: one at each end of a hallway section and one in the middle of a hallway section.

Note that there are no requirements concerning the temperature in a hallway.

REQUIREMENT SPECIFICATIONS

Property	R_HS1

NL

:

Whenever a person is continuously in the near of a hallway door of the hallway section for at least T_HS1 time units indicating that he wants to enter the hallway section, then the light in the hallway section will be on within this time span, and remains on at least as long as the person is near the hallway section.

Property	R_HS2

NL

:

Whenever the lights are neither controllable automatically nor manually for at least T_HS2 time units, then eventually within this time span, the light in the hallway section is on and remains so at least as long as the lights are neither controllable automatically nor manually.

MACHINE SPECIFICATIONS

Property	M_HS1

NL

:

The value of $T\_ \mathit{HS}_1$ is always 50 milliseconds.

Property	M_HS2

NL

:

Whenever the light is not controlled manually the light intensity in a hallway section that is occupied has to be greater than or equal to the light intensity needed to establish save light.

Property	M_HS3

NL

:

The machine always assumes that there is currently no person in a hallway section iff the values of all three motion detectors are 0.