Template Declaration NoMalfunctionOccupancy

INTENTION

This class provides all definitions to describe the term occupancy for an area in the case that there is no malfunction of the sensors used to determine occupancy in this area.

Whether the machine assumes occupancy in an area or not depends on

• a time value delay and
• on a predicate indicating whether a person is currently in an area or not.

Note that the status of occupancy in general does not correspond with the fact whether there is a person in an area or not. Occupancy is a derived term depending on this fact.

Postreferences

:

lsref Occupancy : noMalOcc

SIGNATURE

Timed Function	delay  TIME

Intention	:	This function represents the maximal time an area can be empty - after it has been not empty - but still being defined to be occupied.
Scope	:	mh
Prereferences	:	pdref U3
		pdref U4
		pdref U7
		pdref U9
		pdref FM2
		pdref FM3
		pdref FM4
		pdref FM5
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref Room : M_R4
		msref Area : M_A3

Timed Predicate	areaEmpty

NL	:	=1 : the machine supposes an empty area. =0 : the machine supposes a non-empty area
Intention	:	This predicate is true if and only if the machine assumes that there is currently no person in the area for which occupancy is considered.
Scope	:	mh
Prereferences	:	pdref U3
		pdref U4
		pdref U7
		pdref U9
		pdref FM2
		pdref FM3
		pdref FM4
		pdref FM5
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref HallwaySection : M_HS3
		msref Room : M_R11
		msref Room : M_R5
		msref Room : M_R6
		msref Room : M_R12

Timed Predicate	occupied

NL	:	=1 : the machine supposes an occupied area =0 : the machine supposes an unoccupied area
Intention	:	This predicate is true if and only if the machine assumes that the area for which occupancy is considered is occupied under the precondition that there is no malfunction of the sensors used to determine occupancy (compare timed predicate occUsed in description class Occupancy). This predicate represents the situation as it is seen by the machine and not how it is in the real world. Note that this predicate does not describe whether a person is in an area or not. See timed predicate areaEmpty.
Scope	:	mh
Prereferences	:	pdref U3
		pdref U4
		pdref U7
		pdref U9
		pdref FM2
		pdref FM3
		pdref FM4
		pdref FM5
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref Occupancy : M_O1

MACHINE SPECIFICATIONS

Property	M_NMO1

Formal	:	(  occupied  delay  areaEmpty )
NL	:	An area is defined to be occupied if and only if during the past delay milliseconds the area has been not empty continuously, i.e., during this time a person has been in the area.
Prereferences	:	pdref U3
		pdref U4
		pdref FM2
		pdref FM3
Propreferences	:	rsref Area : R_A2