Template Declaration Room

INTENTION

This class provides all specifications concerning the control of ceiling light groups common to any kind of room. In more detail this means that the following cases are considered

• that safe light has to be established. This behavior is inherited from the description class Area.
• that the light is controlled manually.
• that the light is controlled using the control panel. See the intention of description class RoomCtrlPanel for a more detailed explanation of this case.

In each room there are two dimmable ceiling light groups that are controlled by the machine:

• a dimmable ceiling light group at the window and
• a dimmable ceiling light group at the wall to the hallway.

Furthermore, in each room there is a room control panel for entering values relevant for the control of the light. This is done by the user of a room. This control panel is not the same as the one the facility manager has.

Postreferences	:	lsref Office : Room
		lsref NoOffice : Room
		lsref Floor : ROOMS

FORMAL PARAMETERS

Function	numDoorHallway  NAT

Intention	:	This parameter represents the number of doors of a room to a hallway section.
Defaultvalue	:	1
Postreferences	:	lsref Room : hallwayDoor
		msref Room : M_R13
		msref Room : M_R14
		lsref Office : Room
		lsref NoOffice : Room
		lsref Floor : ROOMS

BASE CLASSES

Class	Area(numLights  = 2, numPB  = 1)

Intention

:

All definitions of description class Area are inherited. There are two ceiling light groups in a room that are controlled by the machine: light[1] represents the ceiling light group near the window and light[2] represents the ceiling light group near the wall to a hallway section.

SIGNATURE

Object	Area::light  :  DimmableCeilingLightGroup

NL	:	window light
Intention	:	The ceiling light groups in a room are dimmable ceiling light groups.
Postreferences	:	msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9
		msref Room : M_R10
		msref Room : M_R13
		msref Room : M_R14

Object	CPRoom  :  RoomCtrlPanel

NL	:	light control panel room
Intention	:	This object represents the room control panel.
Prereferences	:	pdref U5
		pdref U6
		pdref U7
		pdref U9
Postreferences	:	msref Room : M_R3
		msref Room : M_R7
		msref Room : M_R5
		msref Room : M_R2
		msref Room : M_R6
		msref Room : M_R4
		msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9
		msref Room : M_R13

Object	md  :  MotionDetector

NL	:	motion detector
Intention	:	This object represents the room motion detector.
Prereferences	:	akref BD_8
		akref BD_9
		akref BD_10
		akref BD_11
Postreferences	:	msref Room : M_R11
		msref Room : M_R12
		msref Room : M_R13
		msref Room : M_R14

Object	hallwayDoor  :  Door[ numDoorHallway]

Intention	:	Each object represents one door of a room to a hallway section.
Prereferences	:	akref BD_7
		akref BD_9
		akref BD_10
		akref BD_11
Postreferences	:	msref Room : M_R13
		msref Room : M_R14

Object	occRoom  :  Occupancy

Intention	:	This object represents the part of the light control concerning occupancy in a room as it is defined concerning the handling of light scenes. Note that in the description class Area another version of the aspect occupancy is specified representing the view of the facility manager w.r.t. the aspect occupancy.
Prereferences	:	pdref U1
		pdref U2
		pdref U3
		pdref U4
Postreferences	:	msref Room : M_R5
		msref Room : M_R6
		msref Room : M_R7
		msref Room : M_R4
		msref Room : M_R12
		msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9

Timed Function	curLightScene   LightScene

Intention	:	This function represents the current light scene that is established by the machine if light scenes are enabled.
Scope	:	mh
Prereferences	:	pdref U2
Postreferences	:	msref Room : I_M_R2
		msref Room : M_R7
		msref Room : M_R5
		msref Room : M_R6
		msref Room : M_R8
		msref Room : M_R8b

Timed Function	curDefaultLightScene   LightScene

NL	:	current standard light scene
Intention	:	This function represents the current default light scene that is established by the machine if light scenes are enabled.
Scope	:	mh
Prereferences	:	pdref U4
		pdref NF2
Postreferences	:	msref Room : I_M_R1
		msref Room : I_M_R2
		msref Floor : M_F2
		msref Room : M_R6

Timed Function	malDefaultLightScene   LightScene

NL	:	fault standard light scene
Intention	:	This function represents the light scene that is the default light scene in the case of a malfunction of the outdoor light sensors.
Scope	:	mh
Prereferences	:	pdref NF2
Postreferences	:	msref Floor : M_F2
		msref Room : M_R1

Timed Function	noMalDefaultLightScene   LightScene

NL	:	no fault standard light scene
Intention	:	This function represents the light scene that is the default light scene in the case that the outdoor light sensors have no malfunctions.
Scope	:	mh
Postreferences	:	msref Room : I_M_R1
		msref Room : M_R2

Timed Function	determineLightScene  : STRING   LightScene

Intention	:	This function determines the light scene which is identified by the given name.
Scope	:	mh
Postreferences	:	msref Room : M_R7
		msref Room : M_R5

Timed Predicate	OLSMalFct

Intention	:	This predicate is true if and only if an outdoor light sensor that is used by a room has a malfunction. Which outdoor light sensors are used by a room is specified in the description class Floor.
Scope	:	mh
Prereferences	:	pdref U8
		pdref NF2
Postreferences	:	msref Floor : M_F13
		msref Floor : M_F2
		msref Floor : M_F14
		msref Floor : M_F15
		msref Floor : M_F16
		msref Floor : M_F17
		msref Floor : M_F18
		msref Floor : M_F19
		msref Floor : M_F20
		msref Floor : M_F21
		msref Floor : M_F22
		msref Floor : M_F23
		msref Floor : M_F24
		msref Floor : M_F25
		msref Floor : M_F6
		msref Floor : M_F7
		msref Floor : M_F8
		msref Floor : M_F9
		msref Floor : M_F10
		msref Floor : M_F11
		msref Floor : M_F12
		msref Room : M_R13
		msref Room : M_R14

Timed Predicate	closedDoorContactNeighborMal

Intention	:	This predicate is true if and only if a door closed contact of a door to a neighbor room has a malfunction. This predicate is refined in the description classes OfficeNoNeighbor, OfficeNeighbor, NoOfficeNoNeighbor, NoOfficeNeighbor.
Scope	:	mh
Postreferences	:	msref OfficeNeighbor : M_ON1
		msref NoOfficeNeighbor : M_NON1
		msref OfficeWithoutNeighbor : M_ONN1
		msref NoOfficeWithoutNeighbor : M_NONN1
		msref Room : M_R13
		msref Room : M_R14

Function	evalLightScene  :  LightScene,  LightScene:: CEIL_LIGHT_GROUPS,  LIGHT_VALUES  PERCENT

NL	:	the dimmer setting of 2 w.r.t. the light scene1
Intention	:	This function represents the computation of the settings for a given ceiling light group (represented by the second argument) depending on a specific light scene (represented by the first argument) and the current day light the machine assumes to be available in a room(represented by the third argument). The value of this function represents the dimmer settings and additionally the corresponding ceiling light groups has to be on if and only if the dimmer setting is greater than 0.
Scope	:	mh
Prereferences	:	pdref U2
		pdref FM1
Postreferences	:	msref Room : M_R8
		msref Room : M_R8b

MACHINE SPECIFICATIONS

Property	I_M_R1

Formal	:	curDefaultLightScene =  noMalDefaultLightScene
NL	:	Initially the current default light scene is the default light scene for the case that the outdoor light sensors have no malfunction.

Property	I_M_R2

Formal	:	curLightScene =  curDefaultLightScene
NL	:	Initially the current light scene is the current standard light scene.

Property	M_R1

Formal	:	(  malDefaultLightScene. name = ``MAL_DEFAULT''     malDefaultLightScene. ambLightLevel = 14     malDefaultLightScene. option =  LightScene:: BOTH )
NL	:	The default light scene in the case of a malfunction of the outdoor light sensors is specified as follows: the name is MAL_DEFAULT the desired ambient light level is 14 lux the option is BOTH
Prereferences	:	pdref U1

Property	M_R2

Formal	:	(  noMalDefaultLightScene =  CPRoom. defaultLightScene. checked )
NL	:	The default light scene in the case that the outdoor light sensors used by a room have no malfunction always corresponds with the default light scene determined by a user using the room control panel.
Prereferences	:	pdref U6

Property	M_R3

Formal	:	(  noSaveLight  manualControl                                     CPRoom. lightSceneSwitch. checked = 1 )
NL	:	The light intensity in a room that is occupied can be less than the light intensity needed to establish save light if and only if the light is controlled manually or light scenes are enabled or the ambient light level is enabled.
Prereferences	:	pdref U1

Property	M_R4

Formal	:	(  occRoom. noMalOcc. delay =  CPRoom. reoccDelay. checked )
NL	:	The time delay used to determine occupancy as it seen by a user corresponds always with the value entered by a user for the time within the reoccupation of a room leads to a reestablishing of the previous light scene.
Prereferences	:	pdref U7
		pdref U9

Property	M_R5

Formal	:	( ( [  occRoom. noMalOcc. areaEmpty ]  CPRoom. reoccDelay. checked  occRoom. noMalOcc. areaEmpty )      curLightScene =           determineLightScene( CPRoom. chosenLightScene. checked) )
NL	:	Whenever the room becomes non-empty now and has been non-empty sometimes within the last T_RL_2 milliseconds and the light scene l was last chosen, the light scene l is the current light scene.
Prereferences	:	pdref U3

Property	M_R6

Formal	:	( ( [  occRoom. noMalOcc. areaEmpty ] > CPRoom. reoccDelay. checked  occRoom. noMalOcc. areaEmpty )                       curLightScene =  curDefaultLightScene )
NL	:	Whenever the room becomes non-empty now and has been continuously empty for the last T_RL_2 milliseconds then the current light scene is the current default light scene.
Prereferences	:	pdref U4

Property	M_R7

Formal	:	( l  LightScene:       ( (  occRoom. occUsed [  occRoom. occUsed ]       [  determineLightScene( CPRoom. chosenLightScene. checked)                                = l ] )                                                     curLightScene = l ) )
NL	:	Whenever the room is occupied, but has not just become occupied now, and the light scene l becomes chosen, this light scene l is the current light scene within time T_RL_1.
Prereferences	:	pdref U2
		pdref U10

Property	M_R8

Formal	:	( (  occRoom. occUsed  manualControl        CPRoom. lightSceneSwitch. checked = 1 )       ( (  light[1]. sl. usedValue = 0                 evalLightScene( curLightScene,                                        LightScene:: WINDOW,                                        dayLight) 0 )                      [  light[1]. pulse. noMalAct. adjustedEntity = 1 ] )             ( (  light[1]. sl. usedValue = 1                 evalLightScene( curLightScene,                                        LightScene:: WINDOW,                                        dayLight) = 0 )                    [  light[1]. pulse. noMalAct. adjustedEntity = 1 ] )             (  light[1]. dimmer. noMalAct. adjustedEntity =                  evalLightScene( curLightScene,                                           LightScene:: WINDOW,                                           dayLight) ) )
NL	:	Whenever the room is occupied and the light is not controlled manually and light scenes are enabled by the control panel, the window ceiling light group is dimmed and switched on or off as necessary to achieve the ambient light level of the current light scene. This means in the long form: if the window ceiling light group should be on, i.e., the computed dimmer value is not equal to 0, and the window ceiling light group is off, a pulse is given for the window ceiling light group if the window ceiling light group should be off, i.e., the computed dimmer value is equal to 0, and the window ceiling light group is on, a pulse is given for the window ceiling light group the dimmer value of the window ceiling light group is set to the computed one

Property	M_R8b

Formal	:	( (  occRoom. occUsed  manualControl        CPRoom. lightSceneSwitch. checked = 1 )       ( (  light[2]. sl. usedValue = 0                 evalLightScene( curLightScene,                                        LightScene:: WALL,                                        dayLight) 0 )                    [  light[2]. pulse. noMalAct. adjustedEntity = 1 ] )                ( (  light[2]. sl. usedValue = 1                 evalLightScene( curLightScene,                                        LightScene:: WALL,                                        dayLight) = 0 )                    [  light[2]. pulse. noMalAct. adjustedEntity = 1 ] )              (  light[2]. dimmer. noMalAct. adjustedEntity =                  evalLightScene( curLightScene,                                           LightScene:: WALL,                                           dayLight) ) )
NL	:	Whenever the room is occupied and the light is not controlled manually and light scenes are enabled by the control panel, the wall ceiling light group is dimmed and switched on or off as necessary to achieve the ambient light level of the current light scene. This means in the long form: if the wall ceiling light group should be on, i.e., the computed dimmer value is not equal to 0, and the wall ceiling light group is off, a pulse is given for the wall ceiling light group if the wall ceiling light group should be off, i.e., the computed dimmer value is equal to 0, and the wall ceiling light group is on, a pulse is given for the wall ceiling light group the dimmer value of the wall ceiling light group is set to the computed one

Property	M_R9

Formal	:	(  occRoom. occUsed  manualControl        CPRoom. lightSceneSwitch. checked = 0       (  CPRoom. winCeilLightSwitch. checked = 1       (  light[1]. dimmer. noMalAct. adjustedEntity = 100       (  light[1]. sl. usedValue = 0       [  light[1]. pulse. noMalAct. adjustedEntity = 1 ] ) ) )       (  CPRoom. winCeilLightSwitch. checked = 0       (  light[1]. dimmer. noMalAct. adjustedEntity = 0       (  light[1]. sl. usedValue = 1       [  light[1]. pulse. noMalAct. adjustedEntity = 1 ] ) ) )       (  CPRoom. wallCeilLightSwitch. checked = 1       (  light[2]. dimmer. noMalAct. adjustedEntity = 100       (  light[2]. sl. usedValue = 0       [  light[2]. pulse. noMalAct. adjustedEntity = 1 ] ) ) )       (  CPRoom. wallCeilLightSwitch. checked = 0       (  light[2]. dimmer. noMalAct. adjustedEntity = 0       (  light[2]. sl. usedValue = 1       [  light[2]. pulse. noMalAct. adjustedEntity = 1 ] ) ) ) )
NL	:	Whenever the room is occupied and the light is not manually controlled and light scenes are disabled using the the control panel, the window and wall lights are completely switched off or on as selected by a user using the control panels ceiling light switches. This means in the long form: if the window ceiling light group should be on: its dimmer is set to 100 percent if the window ceiling light group is off a pulse is given if the window ceiling light group should be off: its dimmer is set to 0 percent if the window ceiling light group is on a pulse is given if the wall ceiling light group should be on: its dimmer is set to 100 percent if the wall ceiling light group is off a pulse is given if the wall ceiling light group should be off: its dimmer is set to 0 percent if the wall ceiling light group is on a pulse is given In short: Under the mentioned conditions the light is controlled by the ceiling light switches.

Property	M_R10

Formal	:	(  manualControl       ( ( [  light[1]. pulse. noMalAct. adjustedEntity = 1 ]            p  PERCENT:             (  light[1]. dimmer. noMalAct. adjustedEntity = p               (  light[1]. dimmer. noMalAct. adjustedEntity = p                                                                         manualControl ) ) )            ( [  light[2]. pulse. noMalAct. adjustedEntity = 1 ]            p  PERCENT:             (  light[2]. dimmer. noMalAct. adjustedEntity = p               (  light[2]. dimmer. noMalAct. adjustedEntity = p                                                                         manualControl ) ) ) ) )
NL	:	As long as the light is controlled manually, all settings of the window and wall ceiling light group remain unchanged. This means: no pulse is given for the window ceiling light group to switch it on or off the dimmer setting of the window ceiling light group is not changed no pulse is given for the wall ceiling light group to switch it on or off the dimmer setting of the wall ceiling light group is not changed

Property	M_R11

Formal	:	(  occFM. noMalOcc. areaEmpty  md. usedValue = 0 )
NL	:	The machine always assumes that there is currently no person in a room concerning the specification of occupancy as it is seen by the facility manager if and only if the value of the motion detector is 0.

Property	M_R12

Formal	:	(  occRoom. noMalOcc. areaEmpty  md. usedValue = 0 )
NL	:	The machine always assumes that there is currently no person in a room concerning the specification of occupancy as it is seen by the user if and only if the value of the motion detector is 0.

Property	M_R13

Formal	:	(  CPRoom. indicatorMalFct. informCondMach             md. malSens. malDetMach             light[1]. sl. malSens. malDetMach             light[1]. pulse. malAct. malDetMach             light[1]. csa. malAct. malDetMach             light[1]. dimmer. malAct. malDetMach             light[2]. sl. malSens. malDetMach             light[2]. pulse. malAct. malDetMach             light[2]. csa. malAct. malDetMach             light[2]. dimmer. malAct. malDetMach             md. malSens. malDetMach            n NAT (  numDoorHallway ) :                  hallwayDoor[n]. doorClosedContact. malSens. malDetMach             closedDoorContactNeighborMal             OLSMalFct )
NL	:	A user should be informed about a malfunction if one of the following sensors or actuators has a malfunction: the status line of the window ceiling light group the pulse of the window ceiling light group the control system active of the window ceiling light group the dimmer of the window ceiling light group the status line of the wall ceiling light group the pulse of the wall ceiling light group the control system active of the wall ceiling light group the dimmer of the wall ceiling light group the motion detector the door closed contact of a door to a hallway section the door closed contact of a door to a neighbor room the outdoor light sensors used by a room

Property	M_R14

Formal	:	(  CPFM. indicatorMalFct. informCondMach             md. malSens. malDetMach             light[1]. sl. malSens. malDetMach             light[1]. pulse. malAct. malDetMach             light[1]. csa. malAct. malDetMach             light[1]. dimmer. malAct. malDetMach             light[2]. sl. malSens. malDetMach             light[2]. pulse. malAct. malDetMach             light[2]. csa. malAct. malDetMach             light[2]. dimmer. malAct. malDetMach             md. malSens. malDetMach            n NAT (  numDoorHallway ) :                  hallwayDoor[n]. doorClosedContact. malSens. malDetMach             closedDoorContactNeighborMal             OLSMalFct )
NL	:	The facility manager should be informed about a malfunction if one of the following sensors or actuators has a malfunction: the status line of the window ceiling light group the pulse of the window ceiling light group the control system active of the window ceiling light group the dimmer of the window ceiling light group the status line of the wall ceiling light group the pulse of the wall ceiling light group the control system active of the wall ceiling light group the dimmer of the wall ceiling light group the motion detector the door closed contact of a door to a hallway section the door closed contact of a door to a neighbor room the outdoor light sensors used by a room