Next: Template Declaration Room Up: No Title Previous: Template Declaration Area

Template Declaration HallwaySection

INTENTION

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

one ceiling light group
three motion detectors: one at each end of a hallway section and one in the middle of a hallway section.

Postreferences : lsref Floor : h1

lsref Floor : h2

lsref Floor : h3

lsref Floor : HALLWAYS

FORMAL PARAMETERS

Function numPB NAT

Intention : This parameter represents the number of push buttons that can be used by a person to control the ceiling light group in a hallway section by bypassing the machine.

Postreferences : lsref HallwaySection : Area

Function	numPB NAT

BASE CLASSES

Class Area(numLights = 1, numPB = numPB)

Intention
: All definitions of description class Area are inherited. There is one ceiling light group in a hallway section that is controlled by the machine and there are numPB many push buttons for controlling this ceiling light group.

Class	Area(numLights = 1, numPB = numPB)

SIGNATURE

Object eastMd : MotionDetector

NL : motion detector

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

Prereferences : akref BD_14

Postreferences : msref HallwaySection : M_HS3

dkref HallwaySection : D_HS1

msref HallwaySection : M_HS4

Object	eastMd : MotionDetector

Object westMd : MotionDetector

NL : motion detectors

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

Prereferences : akref BD_14

Postreferences : msref HallwaySection : M_HS3

dkref HallwaySection : D_HS1

msref HallwaySection : M_HS4

Object	westMd : MotionDetector

Object middleMd : MotionDetector

NL : motion detectors

Intention : This object represents the motion detector in a hallway section which is installed in the middle of the hallway.

Prereferences : akref BD_14

Postreferences : msref HallwaySection : M_HS3

dkref HallwaySection : D_HS1

msref HallwaySection : M_HS4

Object	middleMd : MotionDetector

Object eastDoor : Door

Intention : This object represents the door at the eastern end of a hallway section.

Prereferences : akref BD_13

Postreferences : dkref Floor : D_F7

dkref Floor : D_F8

msref HallwaySection : M_HS4

Object	eastDoor : Door

Object westDoor : Door

Intention : This object represents the door at the western end of a hallway section.

Prereferences : akref BD_13

Postreferences : dkref Floor : D_F7

dkref Floor : D_F8

msref HallwaySection : M_HS4

Object	westDoor : Door

Time Constant T_HS1

NL : near-to-light delay

Intention : This constant represents the maximal delay between a time point a person is near a hallway door indicating that he wants to enter a hallway section and the time point the ceiling light group of this hallway section is on.

Scope : ev

Prereferences : pdref U14

Postreferences : msref HallwaySection : M_HS1

rsref HallwaySection : R_HS1

Time Constant	T_HS1

Time Constant T_HS2

NL : nocontrol-to-light delay

Intention : This constant represents the maximal delay between a time point the ceiling light group of a hallway section is neither automatically nor manually controllable and the time point the ceiling light group in this hallway section is on.

Scope : ev

Prereferences : pdref NF5

Postreferences : rsref HallwaySection : R_HS2

Time Constant	T_HS2

Time Constant T_OccReact

Intention : This time constant represents the maximal time delay between the time point a hallway section becomes occupied and the time point one of the three motion detectors installed in a hallway section delivers a 1.

Scope : ev

Postreferences : dkref HallwaySection : D_HS1

msref HallwaySection : M_HS5

Time Constant	T_OccReact

Timed Predicate nearHallwayDoor

NL : near a hallway door

Intention : This predicate is true if and only if a person is near a hallway door to a hallway section indicating that he wants to enter this hallway section.

Scope : eh

Prereferences : pdref U14

Postreferences : rsref HallwaySection : R_HS1

Timed Predicate	nearHallwayDoor

Timed Predicate hwLightUncontroll

NL : hallway light uncontrollable

Intention : This predicate is true if and only if the ceiling light group in a hallway section is neither automatically nor manually controllable.

Scope : eh

Prereferences : pdref NF5

Postreferences : rsref HallwaySection : R_HS2

DOMAIN KNOWLEDGE

Timed Predicate	hwLightUncontroll

Property D_HS1

Formal : ( occFM. occEnv _{T_OccReact} ( eastMd. usedValue = 1
westMd. usedValue = 1
middleMd. usedValue = 1 ) )

NL : Whenever a hallway section is occupied then within T_OccReact milliseconds the motion detector installed at the more eastern door or the motion detector installed at the more western door or the motion detector installed in the middle of the hallway delivers a 1 and one of these motion detectors delivers a 1 at least as long as the hallway section is occupied.
And whenever a hallway section is not occupied then within T_OccReact milliseconds all three motion detectors installed in a hallway section delivers a 0 and remain delivering a 0 at least as long as the hallway section is not occupied.

Propreferences : rsref Area : R_A2

Property	D_HS1

REQUIREMENT SPECIFICATIONS

Property R_HS1

Formal : ( nearHallwayDoor _{T_HS1} light[1]. sl. noMalSens. envEntity = 1 )

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

Property	R_HS1

Property R_HS2

Formal : ( hwLightUncontroll _{T_HS2} light[1]. sl. noMalSens. envEntity = 1 )

NL : Whenever the ceiling light group in a hallway section is controllable neither automatically nor manually for at least T_HS_2 time units, then eventually within this time span, the ceiling light group in this hallway section is on and remains so at least as long as the ceiling light group is controllable neither automatically nor manually.

Property	R_HS2

MACHINE SPECIFICATIONS

Property M_HS1

Formal : ( T_HS1 = 50 )

NL : The value of T_ HS_1 is always 50 milliseconds.

Property	M_HS1

Property M_HS2

Formal : ( manualControl noSaveLight )

NL : Whenever the ceiling ight group in a hallway section 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_HS2

Property M_HS3

Formal : ( occFM. noMalOcc. areaEmpty
                     ( ( eastMd. usedValue = 0 )
                       ( westMd. usedValue = 0 )
                       ( middleMd. usedValue = 0 ) ) )

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

Propreferences : rsref Area : R_A2

Property	M_HS3

Property M_HS4

Formal : ( CPFM. indicatorMalFct. informCondMach
                     eastMd. malSens. malDetMach
                     westMd. malSens. malDetMach
                     middleMd. malSens. malDetMach
                     eastDoor. doorClosedContact. malSens. malDetMach
                     westDoor. doorClosedContact. malSens. malDetMach
                     light[1]. sl. malSens. malDetMach
                     light[1]. pulse. malAct. malDetMach
                     light[1]. csa. malAct. malDetMach )

NL : The facility manager should be informed about a malfunction if one of the following sensors or actuators has a malfunction:

the motion detector installed at the more eastern door of a hallway section
the motion detector installed at the more western door of a hallway section
the motion detector installed in the middle of a hallway section
the door closed contact of the door at the eastern end of a hallway section
the door closed contact of the door at the western end of a hallway section
the status line of the ceiling light group
the pulse of the ceiling light group
the control system active of the ceiling light group

Property	M_HS4

Property M_HS5

Formal : ( T_A1
T_OccReact + T_A2 + light[1]. pulse. noMalAct. reactionTime )

NL : The time constant T_A1 is always greater than the sum of the time constants T_A2, T_OccReact, and the reaction time of the pulse of a ceiling light group.

Propreferences : rsref Area : R_A2

Property	M_HS5

Next: Template Declaration Room Up: No Title Previous: Template Declaration Area

Forest-System
2000-09-06

Postreferences	:	lsref Floor : h1
		lsref Floor : h2
		lsref Floor : h3
		lsref Floor : HALLWAYS

Intention	:	This parameter represents the number of push buttons that can be used by a person to control the ceiling light group in a hallway section by bypassing the machine.
Postreferences	:	lsref HallwaySection : Area

NL	:	motion detector
Intention	:	This object represents the motion detector in a hallway section which is installed at the more eastern door of the hallway.
Prereferences	:	akref BD_14
Postreferences	:	msref HallwaySection : M_HS3
		dkref HallwaySection : D_HS1
		msref HallwaySection : M_HS4

NL	:	motion detectors
Intention	:	This object represents the motion detector in a hallway section which is installed at the more western door of the hallway.
Prereferences	:	akref BD_14
Postreferences	:	msref HallwaySection : M_HS3
		dkref HallwaySection : D_HS1
		msref HallwaySection : M_HS4

Intention	:	This object represents the door at the eastern end of a hallway section.
Prereferences	:	akref BD_13
Postreferences	:	dkref Floor : D_F7
		dkref Floor : D_F8
		msref HallwaySection : M_HS4

Intention	:	This object represents the door at the western end of a hallway section.
Prereferences	:	akref BD_13
Postreferences	:	dkref Floor : D_F7
		dkref Floor : D_F8
		msref HallwaySection : M_HS4

NL	:	near-to-light delay
Intention	:	This constant represents the maximal delay between a time point a person is near a hallway door indicating that he wants to enter a hallway section and the time point the ceiling light group of this hallway section is on.
Scope	:	ev
Prereferences	:	pdref U14
Postreferences	:	msref HallwaySection : M_HS1
		rsref HallwaySection : R_HS1

NL	:	nocontrol-to-light delay
Intention	:	This constant represents the maximal delay between a time point the ceiling light group of a hallway section is neither automatically nor manually controllable and the time point the ceiling light group in this hallway section is on.
Scope	:	ev
Prereferences	:	pdref NF5
Postreferences	:	rsref HallwaySection : R_HS2

Intention	:	This time constant represents the maximal time delay between the time point a hallway section becomes occupied and the time point one of the three motion detectors installed in a hallway section delivers a 1.
Scope	:	ev
Postreferences	:	dkref HallwaySection : D_HS1
		msref HallwaySection : M_HS5

NL	:	near a hallway door
Intention	:	This predicate is true if and only if a person is near a hallway door to a hallway section indicating that he wants to enter this hallway section.
Scope	:	eh
Prereferences	:	pdref U14
Postreferences	:	rsref HallwaySection : R_HS1

NL	:	hallway light uncontrollable
Intention	:	This predicate is true if and only if the ceiling light group in a hallway section is neither automatically nor manually controllable.
Scope	:	eh
Prereferences	:	pdref NF5
Postreferences	:	rsref HallwaySection : R_HS2

Formal	:	( occFM. occEnv _{T_OccReact} ( eastMd. usedValue = 1 westMd. usedValue = 1 middleMd. usedValue = 1 ) )
NL	:	Whenever a hallway section is occupied then within T_OccReact milliseconds the motion detector installed at the more eastern door or the motion detector installed at the more western door or the motion detector installed in the middle of the hallway delivers a 1 and one of these motion detectors delivers a 1 at least as long as the hallway section is occupied. And whenever a hallway section is not occupied then within T_OccReact milliseconds all three motion detectors installed in a hallway section delivers a 0 and remain delivering a 0 at least as long as the hallway section is not occupied.
Propreferences	:	rsref Area : R_A2

Formal	:	( nearHallwayDoor _{T_HS1} light[1]. sl. noMalSens. envEntity = 1 )
NL	:	Whenever a person is continuously near to a hallway door of a hallway section for at least T_HS_1 time units indicating that he wants to enter the hallway section, then the ceiling light group in this hallway section will be on within this time span, and remains on at least as long as the preconditions are fulfilled.

Formal	:	( hwLightUncontroll _{T_HS2} light[1]. sl. noMalSens. envEntity = 1 )
NL	:	Whenever the ceiling light group in a hallway section is controllable neither automatically nor manually for at least T_HS_2 time units, then eventually within this time span, the ceiling light group in this hallway section is on and remains so at least as long as the ceiling light group is controllable neither automatically nor manually.

Formal	:	( T_HS1 = 50 )
NL	:	The value of T_ HS_1 is always 50 milliseconds.

Formal	:	( manualControl noSaveLight )
NL	:	Whenever the ceiling ight group in a hallway section 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.

Formal	:	( occFM. noMalOcc. areaEmpty ( ( eastMd. usedValue = 0 ) ( westMd. usedValue = 0 ) ( middleMd. usedValue = 0 ) ) )
NL	:	The machine always assumes that there is currently no person in a hallway section if and only if the values of all three motion detectors are 0.
Propreferences	:	rsref Area : R_A2

Formal	:	( CPFM. indicatorMalFct. informCondMach eastMd. malSens. malDetMach westMd. malSens. malDetMach middleMd. malSens. malDetMach eastDoor. doorClosedContact. malSens. malDetMach westDoor. doorClosedContact. malSens. malDetMach light[1]. sl. malSens. malDetMach light[1]. pulse. malAct. malDetMach light[1]. csa. malAct. malDetMach )
NL	:	The facility manager should be informed about a malfunction if one of the following sensors or actuators has a malfunction: the motion detector installed at the more eastern door of a hallway section the motion detector installed at the more western door of a hallway section the motion detector installed in the middle of a hallway section the door closed contact of the door at the eastern end of a hallway section the door closed contact of the door at the western end of a hallway section the status line of the ceiling light group the pulse of the ceiling light group the control system active of the ceiling light group

Formal	:	( T_A1 T_OccReact + T_A2 + light[1]. pulse. noMalAct. reactionTime )
NL	:	The time constant T_A1 is always greater than the sum of the time constants T_A2, T_OccReact, and the reaction time of the pulse of a ceiling light group.
Propreferences	:	rsref Area : R_A2