INTENTION
This class provides all definitions specific to any kind of room with sun blinds. In addition to the definitions of the description class Room the control of the sun blinds is considered here. Since both, light and temperature control, can influence the setting of the sun blinds there can be conflicts. The resolution of possible conflicts is represented by the function resolveBlindConflict.
FORMAL PARAMETERS
Function | numRad NAT |
---|
Intention | : | This parameter represents the number of radiators that belong to a room. |
Function | numSunBlinds NAT |
---|
Intention | : | This parameter represents the number of sun blinds that belong to a room and which can be controlled by the machine. |
Function | numDoorHallway NAT |
---|
Intention | : | This parameter represents the number of doors of a room to the hallway. |
BASE CLASSES
Class | Room(numRad = numRad, numDoorHallway = numDoorHallway) |
---|
Intention |
: | All definitions of description class Room are also provided here. |
SIGNATURE
Object | sb : SunBlind[ numSunBlinds] |
---|
Intention | : | Each object represents one sun blind of a room that can be controlled by the machine. |
Object | BasicRoom::RL : BlindedRoomLight(numSunBlinds = numSunBlinds) |
---|
Intention | : | This object represents the light control in a blinded room. |
Object | BasicRoom::RT : BlindedRoomTemperature(numSunBlinds = numSunBlinds) |
---|
Intention | : | This object represents the temperature control in a blinded room. |
Timed Function | resolveBlindConflict : NAT ( numSunBlinds ) , THREE_PT_ACT_RANGE, THREE_PT_ACT_RANGE THREE_PT_ACT_RANGE |
---|
Intention | : | This function represents the current settings of the sun blinds in a room intended by the machine. These settings are computed based on the intended settings of the temperature control (second argument) and the intended settings of the light control (third argument). |
Scope | : | mh |
Timed Predicate | manualBlind |
---|
Intention | : | This predicate is true iff the machine assumes that the sun blinds are controlled manually and not by the control system. |
Scope | : | mh |
Property | D_BR1 |
---|
Formal | : | ( numSunBlinds = numRad ) |
NL | : | The number of sun blinds in a blinded room equals the number of radiators in a blinded room. |
MACHINE SPECIFICATIONS
Property | I_BR1 |
---|
Formal | : | manualBlind |
NL | : | Initially the sun blinds are not controlled manually. |
Property | M_BR1 |
---|
Formal | : | ( manualBlind RT. modes. occ. occUsed
s NAT ( numSunBlinds ) : RL. lCPRoom. sunBlindManual[s]. checked = 1 ) |
NL | : | The machine assumes that the sun blinds are controlled manually iff a room is occupied according to the definition of this term used for temperature control and at least one sun blind is controlled manually. |
Property | M_BR2 |
---|
Formal | : | ( s NAT ( numSunBlinds ) : ( ( malTemp
RT. tempBlindSet(s) = RT. tempBlindNoMalSet(s, RT. modes. roomDesiredTemperature) ) ( malTemp RT. tempBlindSet(s) = RT. tempBlindMalSet(s, RT. modes. roomDesiredTemperature) ) ) ) |
NL | : | If the machine does not assume a serious malfunction of the sensors, used to determine the settings of the actuators controlling the temperature, the current settings of the sun blinds in a room intended by the temperature control are as determined by the function tempBlindNoMalSet.
If the machine assumes a serious malfunction of the sensors, used to determine the settings of the actuators controlling the temperature, the current settings of the sun blinds in a room intended by the temperature control are as determined by the function tempBlindMalSet. |
Property | M_BR3 |
---|
Formal | : | ( s NAT ( numSunBlinds ) :
( ( malLight RL. lightBlindSet(s) = RL. lightBlindNoMalSet(s) ) ( malLight RL. lightBlindSet(s) = RL. lightBlindMalSet(s) ) ) ) |
NL | : | If the machine does not assume a serious malfunction of the sensors, used to determine the settings of the actuators controlling the light, the current settings of the sun blinds in a room intended by the light control are as determined by the function lightBlindNoMalSet.
If the machine assumes a serious malfunction of the sensors, used to determine the settings of the actuators controlling the light, the current settings of the sun blinds in a room intended by the light control are as determined by the function lightBlindMalSet. |
Property | M_BR4 |
---|
Formal | : | ( manualBlind
s NAT ( numSunBlinds ) : sb[s]. blind. noMalAct. adjustedEntity = RL. lCPRoom. sunBlindSwitch[s]. checked ) |
NL | : | If the sun blinds are controlled manually the value adjusted by the machine for each sun blind is equal to the corresponding switch status of the control panel. |
Property | M_BR5 |
---|
Formal | : | ( manualBlind
s NAT ( numSunBlinds ) : sb[s]. blind. noMalAct. adjustedEntity = resolveBlindConflict(s, RT. tempBlindSet(s), RL. lightBlindSet(s)) ) |
NL | : | If the sun blinds are not controlled manually the value adjusted by the machine for each sun blind is equal to the value determined for the sun blinds by the function resolveBlindConflict. |