INTENTION
This class provides all definitions to describe the general aspects of lights in an area. An area is here the generalization of rooms and hallways. In more detail this class provides:
FORMAL PARAMETERS
Function | numLights NAT |
---|
Intention | : | This parameter represents the number of lights in an area that are controlled by the machine. |
SIGNATURE
Object | occ : Occupancy |
---|
Intention | : | This object represents the part of the definition of area light defining whether a room is occupied or not. |
Postreferences | : | msref AreaLight : M_AL3 |
msref AreaLight : M_AL4 | ||
msref AreaLight : M_AL5 | ||
msref AreaLight : M_AL6 | ||
msref AreaLight : M_AL7 | ||
msref AreaLight : M_AL8 | ||
msref HallwaySection : M_HS3 | ||
msref RoomLight : M_RL5 | ||
msref RoomLight : M_RL6 | ||
msref RoomLight : M_RL7 | ||
msref RoomLight : M_RL8 | ||
msref RoomLight : M_RL9 | ||
msref RoomLight : M_RL10 | ||
msref RoomLight : M_RL12 | ||
msref RoomLight : M_RL13 | ||
msref RoomLight : M_RL14 | ||
rsref AreaLight : R_AL1 | ||
rsref AreaLight : R_AL2 | ||
rsref Floor : R_F1 | ||
msref BasicRoom : M_BaR1 | ||
rsref AreaLight : R_AL3 |
Object | light : ControlledLight[ numLights] |
---|
Intention | : | These objects represent the lights in area that are controlled by the machine. |
Prereferences | : | akref BD_26 |
akref BD_28 | ||
akref BD_32 | ||
akref BD_31 | ||
Postreferences | : | dkref AreaLight : D_AL2 |
lsref RoomLight : light | ||
msref AreaLight : M_AL7 | ||
msref AreaLight : M_AL8 | ||
msref AreaLight : M_AL9 | ||
rsref AreaLight : R_AL1 | ||
rsref AreaLight : R_AL2 | ||
rsref HallwaySection : R_HS1 | ||
rsref HallwaySection : R_HS2 | ||
rsref Floor : R_F1 |
Object | lCPFM : AreaLightCtrlPanelFM |
---|
Intention | : | This object represents the light control panel containing the entities for which the facility manager can enter a value. |
Postreferences | : | lsref RoomLight : lCPFM |
msref AreaLight : M_AL5 | ||
rsref AreaLight : R_AL1 |
Time Constant | T_AL1 |
---|
Intention | : | This time constant represents the maximal time delay for the following two situations:
|
Scope | : | ev |
Prereferences | : | pdref U1 |
Postreferences | : | dkref AreaLight : D_AL1 |
msref AreaLight : M_AL1 | ||
rsref AreaLight : R_AL1 | ||
rsref AreaLight : R_AL2 | ||
rsref AreaLight : R_AL3 |
Time Constant | T_AL2 |
---|
Intention | : | This time constant represents the maximal delay between the time point the machine assumes an occupation of an area and the time point the machine has set the corresponding actuators to establish safe light. |
Scope | : | ev |
Prereferences | : | pdref U1 |
Postreferences | : | dkref AreaLight : D_AL1 |
msref AreaLight : M_AL2 | ||
msref AreaLight : M_AL7 |
Timed Predicate | lightFMControlled |
---|
Intention | : | This predicate is true iff the light is controlled by the facility manager using the control panel. |
Scope | : | eh |
Prereferences | : | pdref FM6 |
Postreferences | : | msref AreaLight : I_AL2 |
rsref AreaLight : R_AL1 | ||
rsref AreaLight : R_AL2 |
Timed Predicate | allLightsOff |
---|
Intention | : | This predicate is true iff all lights in an area that are controlled by the machine are off. |
Scope | : | eh |
Prereferences | : | pdref FM2 |
pdref FM3 | ||
Postreferences | : | dkref AreaLight : D_AL2 |
Timed Predicate | safeLight |
---|
Intention | : | This predicate is true, iff there is sufficient light to move safely. |
Scope | : | eh |
Prereferences | : | pdref U1 |
pdref U17 | ||
Postreferences | : | rsref AreaLight : R_AL3 |
Timed Predicate | noSaveLight |
---|
Intention | : | This predicate is true iff the light intensity in an area that is occupied can be less than the light intensity needed to establish safe light. This is for example the case if the light is controlled manually. |
Scope | : | mh |
Prereferences | : | pdref U1 |
Postreferences | : | msref AreaLight : I_AL1 |
msref AreaLight : M_AL7 | ||
msref HallwaySection : M_HS2 | ||
msref RoomLight : M_RL4 | ||
rsref AreaLight : R_AL3 |
Timed Predicate | manualControl |
---|
Intention | : | This predicate is true iff the machine assumes that the light in this area is controlled manually. |
Scope | : | mh |
Postreferences | : | msref AreaLight : M_AL8 |
msref AreaLight : M_AL9 | ||
msref HallwaySection : M_HS2 | ||
msref RoomLight : M_RL4 | ||
msref RoomLight : M_RL8 | ||
msref RoomLight : M_RL9 | ||
msref RoomLight : M_RL10 | ||
msref RoomLight : M_RL11 |
Function | evalSaveLight : NAT ( numLights ) BINARY |
---|
Intention | : | This function represents the computation that results in the decision which light has to be on in order to achieve safe light in an area. evalSaveLight[i]=i means that the i-th light has to be on. |
Scope | : | mh |
Prereferences | : | pdref U12 |
Postreferences | : | msref AreaLight : M_AL7 |
Property | D_AL1 |
---|
Formal | : | ( T_AL2 < T_AL1 ) |
NL | : | The time constant is allways smaller than the time constant . |
Property | D_AL2 |
---|
Formal | : | ( allLightsOff n NAT ( numLights ) :
light[n]. ls. noMalSens. envEntity = 0 ) |
NL | : | The predicate allLightsOff is true iff all lights that are controlled by the machine are off. |
REQUIREMENT SPECIFICATIONS
Property | R_AL1 |
---|
Formal | : | ( lightFMControlled occ. occUsed T_AL1
n NAT ( numLights ) : ( light[n]. ls. noMalSens. envEntity = lCPFM. lightOn. checked ) ) |
NL | : | Whenever the light is controlled by the facility manager using the control panel and the area is unoccupied for at least milliseconds, the status of the machine controlled lights equals within this time the status as it is determined by the facility manager. |
Prereferences | : | pdref FM6 |
Property | R_AL2 |
---|
Formal | : | ( lightFMControlled occ. occUsed T_AL1
n NAT ( numLights ) : ( light[n]. ls. noMalSens. envEntity = 0 ) ) |
NL | : | Whenever the light is not controlled by the facility manager using the control panel and the area is unoccupied for at least milliseconds, all machine controlled lights are off within this time and remains off at least as long as the precondition is true. |
Prereferences | : | pdref FM2 |
pdref FM3 |
Property | R_AL3 |
---|
Formal | : | ( noSaveLight occ. occUsed T_AL1 safeLight ) |
NL | : | Whenever safe light has to be established and the area is occupied for at least milliseconds, the light is sufficient to move safely within this time span and remains sufficient to move safely at least as long as the precondition is true. |
Prereferences | : | pdref U1 |
pdref U17 |
MACHINE SPECIFICATIONS
Property | I_AL1 |
---|
Formal | : | noSaveLight |
NL | : | Initially safe light has to be established if an area is occupied. |
Property | I_AL2 |
---|
Formal | : | lightFMControlled |
NL | : | Initially the light is not controlled by the facility manager using his control panel. |
Property | M_AL1 |
---|
Formal | : | ( T_AL1 = 50 ) |
NL | : | The value of is always 50 miliiseconds. |
Property | M_AL2 |
---|
Formal | : | ( T_AL2 = 30 ) |
NL | : | The value of is always 30 miliiseconds. |
Property | M_AL3 |
---|
Formal | : | ( occ. noMalOcc. dt1 = 1000 ) |
NL | : | The first time delay used to determine occupancy concerning the light control is always 1 second. |
Property | M_AL4 |
---|
Formal | : | ( occ. noMalOcc. dt2 = 0 ) |
NL | : | The second time delay used to determine occupancy concerning the light control is always 0 second. |
Property | M_AL5 |
---|
Formal | : | ( occ. noMalOcc. dt3 = lCPFM. unoccDelay. checked ) |
NL | : | The third time delay used to determine occupancy concerning the light control corresponds always with the value entered by the facility manager for the time a certain area has to be unoccupied continuously before the lights are switched off. |
Property | M_AL6 |
---|
Formal | : | ( occ. malOcc. automaticDetermValue ) |
NL | : | The value determined automatically by the machine for occupancy concerning the light control in the case of a malfunction of some sensors used to determine occupancy concerning the light control is occupancy. |
Prereferences | : | pdref NF4 |
Property | M_AL7 |
---|
Formal | : | ( noSaveLight occ. occUsed n NAT ( numLights ) :
( evalSaveLight(n) = 1 light[n]. ls. usedValue = 0 T_AL2 light[n]. pulse. noMalAct. adjustedEntity = 1 ) ) |
NL | : | Whenever safe light has to be established and the area is occupied the necessary actuators, i.e. pulse lines, are set within milliseconds to establish safe light. |
Prereferences | : | pdref U1 |
pdref U17 |
Property | M_AL8 |
---|
Formal | : | ( manualControl
n NAT ( numLights ) : ( light[n]. manualControl ) occ. occUsed ) |
NL | : | The machine assumes that the light is controlled manually in an area iff at least one light in this area is controlled manually and the area is occupied. |
Property | M_AL9 |
---|
Formal | : | ( manualControl
n NAT ( numLights ) : ( [ light[n]. pulse. noMalAct. adjustedEntity = 1 ] ) ) |
NL | : | If the light in an area is controlled manually, the settings of all lights remain unchanged. |