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.

BASE CLASSES

Class	AreaLight(numLights  = 1)

Intention

:

All definitions of description class AreaLight are also provided here. There is one light in a hallway section that is controlled by the machine.

SIGNATURE

Object	eastMd  :  MotionDetector

Intention	:	This object represents the motion detector in a hallway which is installed at the more eastern door of the hallway.
Postreferences	:	msref HallwaySection : M_HS3

Object	westMd  :  MotionDetector

Intention	:	This object represents the motion detector in a hallway which is installed at the more western door of the hallway.
Postreferences	:	msref HallwaySection : M_HS3

Object	middleMd  :  MotionDetector

Intention	:	This object represents the motion detector in a hallway which is installed in the middle of the hallway.
Postreferences	:	msref HallwaySection : M_HS3

Object	eastDoor  :  Door

Intention	:	This object represents the door at the eastern end of the hallway.
Postreferences	:	dkref Floor : D_F7
		dkref Floor : D_F8

Object	westDoor  :  Door

Intention	:	This object represents the door at the western end of the hallway.
Postreferences	:	dkref Floor : D_F7
		dkref Floor : D_F8

Time Constant	T_HS1

Intention	:	This constant represents the time delay between a time point a person is near a hallway door indicating that he wants to enter this hallway section and switching on the lights.
Scope	:	ev
Postreferences	:	msref HallwaySection : M_HS1
		rsref HallwaySection : R_HS1

Time Constant	T_HS2

Intention	:	This constant represents the time delay between the loss of light control in this hallway section and switching on the lights.
Scope	:	ev
Postreferences	:	rsref HallwaySection : R_HS2

Timed Predicate	nearHallwayDoor

Intention	:	This predicate is true iff a person is near a hallway door to this hallway section indicating that he wants to enter the hallway section.
Scope	:	eh
Postreferences	:	rsref HallwaySection : R_HS1

Timed Predicate	hwLightUncontroll

Intention	:	This predicate is true iff the light is neither automatically nor manually controllable.
Scope	:	eh
Postreferences	:	rsref HallwaySection : R_HS2

REQUIREMENT SPECIFICATIONS

Property	R_HS1

Formal	:	(  nearHallwayDoor  T_HS1  light[1]. ls. noMalSens. envEntity = 1 )
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

Formal	:	(  hwLightUncontroll  T_HS2  light[1]. ls. noMalSens. envEntity = 1 )
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

Formal	:	(  T_HS1 = 50 )
NL	:	The value of $T\_ \mathit{HS}_1$ is always 50 milliseconds.

Property	M_HS2

Formal	:	(  manualControl  noSaveLight )
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

Formal	:	(  occ. noMalOcc. emptyMach                      ( (  eastMd. usedValue = 0 )                        (  westMd. usedValue = 0 )                        (  middleMd. usedValue = 0 ) ) )
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.