INTENTION
This class provides all definitions to describe the behavior common to any kind of room. This includes the definitions of the light and temperature control in a room as well as the aggregation of the objects that are installed in each room. In this class we do not consider such objects for which the number of installed instances can vary from room to room, e.g. the number of installed radiators. These objects are integrated in the derived description class Room.
Each room is equipped with
SIGNATURE
Object | RL : RoomLight |
---|
Intention | : | This object represents the part that describes the behavior of a room concerning the light control. |
Object | RT : RoomTemperature |
---|
Intention | : | This object represents the part that describes the behavior of a room concerning the temperature control. |
Object | md : MotionDetector |
---|
Intention | : | This object represents the room motion detector. |
Object | rt : RoomTempSensor[3] |
---|
Intention | : | Each object represents one of the three air temperature sensors in a room. |
Timed Function | valueEstimation : RoomTempSensor:: ROOM_TEMP, RoomTempSensor:: ROOM_TEMP RoomTempSensor:: ROOM_TEMP |
---|
Intention | : | This function represents the value determined for a room temperature sensor depending on the values of the other two room temperature sensors.
This function is used in the case of a malfunction of a room temperature sensor. |
Scope | : | mh |
Timed Predicate | malfunctionAllTempSens |
---|
Intention | : | This predicate is true iff all temperature sensors of a room have a malfunction. |
Scope | : | mh |
Timed Predicate | malLight |
---|
Intention | : | This predicate is true iff the machine assumes that the sensors, used to determine the settings of the actuators controlling the light, have such a serious malfunction that the settings of the actuators have to be determined using makeshift operations. |
Scope | : | mh |
Property | M_BaR1 |
---|
Formal | : | ( rt[1]. malSens. automaticDetermValue =
valueEstimation( rt[2]. noMalSens. convertedEntity, rt[3]. noMalSens. convertedEntity) ) |
NL | : | If the first room temperature sensor has a malfunction its value is estimated using the other two room temperature sensors. |
Property | M_BaR2 |
---|
Formal | : | ( rt[2]. malSens. automaticDetermValue =
valueEstimation( rt[1]. noMalSens. convertedEntity, rt[3]. noMalSens. convertedEntity) ) |
NL | : | If the second room temperature sensor has a malfunction its value is estimated using the other two room temperature sensors. |
Property | M_BaR3 |
---|
Formal | : | ( rt[3]. malSens. automaticDetermValue =
valueEstimation( rt[1]. noMalSens. convertedEntity, rt[2]. noMalSens. convertedEntity) ) |
NL | : | If the third room temperature sensor has a malfunction its value is estimated using the other two room temperature sensors. |
Property | M_BaR4 |
---|
Formal | : | ( malfunctionAllTempSens rt[1]. malSens. malDetMach
rt[2]. malSens. malDetMach rt[3]. malSens. malDetMach ) |
NL | : | All room temperature sensors have a malfunction iff the machine assumes for each room temperature sensor a malfunction. |
Property | M_BaR5 |
---|
Formal | : | ( RL. occ. noMalOcc. emptyMach md. usedValue = 0 ) |
NL | : | Concerning the light control the machine always assumes that there is currently no person in a room iff the value of the motion detector is 0. |
Property | M_BaR6 |
---|
Formal | : | ( RT. modes. occ. noMalOcc. emptyMach md. usedValue = 0 ) |
NL | : | Concerning the temperature control the machine always assumes that there is currently no person in a room iff the value of the motion detector is 0. |