Template Declaration Occupancy

INTENTION

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

• occupancy is specified under the condition that all sensors used to determine occupancy have no malfunction
• occupancy is specified under the condition that some sensors used to determine occupancy 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.

Postreferences	:	lsref Area : occFM
		lsref Room : occRoom

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_O1
		msref HallwaySection : M_HS3
		msref Room : M_R11
		msref Room : M_R5
		msref Room : M_R4
		msref Room : M_R6
		msref Room : M_R12
		msref Area : M_A3

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_O1
		msref Area : M_A4

Timed Predicate	occUsed

Intention	:	This predicate is true if and only if the machine assumes occupancy independent whether a sensor used to determine occupancy has a malfunction or not (compare timed predicate occupied in description class NoMalfunctionOccupancy).
Scope	:	mh
Prereferences	:	pdref PD_30
Postreferences	:	msref Occupancy : M_O1
		msref Room : M_R7
		rsref Area : R_A3
		rsref Floor : R_F1
		rsref Area : R_A1
		msref Area : M_A5
		msref Area : M_A6
		msref Area : M_A7
		msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9

Timed Predicate	occEnv

Intention	:	This predicate is true if and only if an area is occupied. Note that this predicate represents the phenomenon as it exists in the environment.
Scope	:	eh
Postreferences	:	dkref HallwaySection : D_HS1
		rsref Area : R_A2

MACHINE SPECIFICATIONS

Property	M_O1

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.
Prereferences	:	pdref PD_30
Propreferences	:	rsref Area : R_A2