Description Class Occupancy

INTENTION

This class provides all definitions to describe the occupancy in a specific area. It is a composition of the following two cases:

• occupancy is computed under the condition that all sensors used to determine occupance have no malfunction
• occupancy is computed under the condition that some sensors used to determine occupance have a malfunction

To compose these two cases some entities are introduced that allow to determine whether some sensors used to determine occupancy have a malfunction.

SIGNATURE

Object	noMalOcc  :  NoMalfunctionOccupancy

Intention	:	This object represents the part of the occupancy determination describing the behavior if the sensors used to determine occupancy have no malfunction, i.e. if the machine assumes that they have no malfunction.
Postreferences	:	msref Occupancy : M_OCC2
		msref AreaLight : M_AL3
		msref AreaLight : M_AL4
		msref AreaLight : M_AL5
		msref HallwaySection : M_HS3
		msref BasicRoom : M_BaR1

Object	malOcc  :  MalfunctionOccupancy

Intention	:	This object represents the part of the occupancy determination describing the behavior if the sensors used to determine occupancy have a malfunction, i.e. if the machine assumes that they have a malfunction.
Postreferences	:	msref Occupancy : M_OCC1
		msref Occupancy : M_OCC2
		msref AreaLight : M_AL6

Object	manualEnteredMal  :  EnteredValue(CHECKED_DOM  =  BINARY)

Intention	:	Manually entered value concerning a malfunction of the sensors determining occupancy entered by a user. 1 stands for a malfunction, 0 stands for no malfunction. Note that the value of this object is only meaningful if the timed predicate stateManualEnteredMal is true.
Postreferences	:	msref Occupancy : M_OCC1

Timed Predicate	stateManualEnteredMal

Intention	:	This predicate is true iff it has been manually entered whether there is a malfunction of the sensors determining occupancy or whether there is no malfunction of them.
Scope	:	mh
Postreferences	:	msref Occupancy : I_OCC1
		msref Occupancy : M_OCC1

Timed Predicate	automaticDetMal

Intention	:	This predicate is true iff a malfunction of the sensors used to determine occupancy has been detected automatically, i.e. not by entering it manually.
Scope	:	mh
Postreferences	:	msref Occupancy : M_OCC1

Timed Predicate	occUsed

Intention	:	This predicate is true iff the machine assumes occupancy.
Scope	:	mh
Postreferences	:	msref Occupancy : M_OCC2
		msref AreaLight : M_AL7
		msref AreaLight : M_AL8
		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
		rsref AreaLight : R_AL3

MACHINE SPECIFICATIONS

Property	I_OCC1

Formal	:	stateManualEnteredMal
NL	:	Initially it has not been entered manually whether there is a malfunction of the sensors determining occupancy or whether there is no malfunction of them.

Property	M_OCC1

Formal	:	(  malOcc. malOccDetMach            ( (  stateManualEnteredMal                manualEnteredMal. checked = 1 )              (  stateManualEnteredMal  automaticDetMal ) ) )
NL	:	The machine assumes a malfunction of some sensors used to determine occupancy iff one of the following conditions is fulfilled: a malfunction has been entered manually or it has not been entered manually that there is no malfunction and a malfunction has been detected automatically.

Property	M_OCC2

Formal	:	(  occUsed            ( (  malOcc. malOccDetMach  malOcc. occMal )              (  malOcc. malOccDetMach  noMalOcc. occupied ) ) )
NL	:	The machine assumes occupancy if and only if one of the following condition is fulfilled: the machine assumes a malfunction of some sensors used to detect occupancy and the predicate representing the value concerning occupancy assumed in this case is true, the machine assumes no malfunction and the predicate representing the value concerning occupancy assumed in this case is true.