Description Class BasicRoom

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

• one motion detector
• three temperature sensors

SIGNATURE

Object	RL  :  RoomLight

Intention	:	This object represents the part that describes the behavior of a room concerning the light control.
Postreferences	:	lsref BlindedRoom : RL
		msref BasicRoom : M_BaR5
		msref Floor : M_F2

Object	RT  :  RoomTemperature

Intention	:	This object represents the part that describes the behavior of a room concerning the temperature control.
Postreferences	:	lsref BlindedRoom : RT
		msref BasicRoom : M_BaR6
		msref Room : M_R2
		msref Floor : M_F3
		msref Floor : M_F4
		msref Floor : M_F5
		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

Object	md  :  MotionDetector

Intention	:	This object represents the room motion detector.
Postreferences	:	msref BasicRoom : M_BaR5
		msref BasicRoom : M_BaR6

Object	rt  :  RoomTempSensor[3]

Intention	:	Each object represents one of the three air temperature sensors in a room.
Postreferences	:	msref BasicRoom : M_BaR1
		msref BasicRoom : M_BaR2
		msref BasicRoom : M_BaR3
		msref BasicRoom : M_BaR4

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
Postreferences	:	msref BasicRoom : M_BaR1
		msref BasicRoom : M_BaR2
		msref BasicRoom : M_BaR3

Timed Predicate	malfunctionAllTempSens

Intention	:	This predicate is true iff all temperature sensors of a room have a malfunction.
Scope	:	mh
Postreferences	:	msref BasicRoom : M_BaR4
		msref Room : M_R1

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
Postreferences	:	msref BlindedRoom : M_BR3

MACHINE SPECIFICATIONS

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.