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 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 doors to adjacent rooms. These objects are integrated in the derived description class Room.

Each room is equipped with

• one motion detector

SIGNATURE

Object	RL  :  RoomLight

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

Object	md  :  MotionDetector

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

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.

MACHINE SPECIFICATIONS

Property	M_BaR1

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.