Description Class 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

• three time values, $\mathit{dt}_1$, $\mathit{dt}_2$, $\mathit{dt}_3$, and
• on a predicate indicating whether a person is currently in the 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.

SIGNATURE

Timed Function	dt1  TIME

Intention	:	This function represents the current value used for the first time delay used to determine occupancy. The precise correlation between this time delay and occupancy is given in the property $P\_\mathit{NMO}_{1}$.
Scope	:	mh
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref AreaLight : M_AL3

Timed Function	dt2  TIME

Intention	:	This function represents the current value used for the second time delay used to determine occupancy. The precise correlation between this time delay and occupancy is given in property $P\_\mathit{NMO}_{1}$.
Scope	:	mh
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref AreaLight : M_AL4

Timed Function	dt3  TIME

Intention	:	This function represents the current value used for the third time delay used to determine occupancy. The precise correlation between this time delay and occupancy is given in property $P\_\mathit{NMO}_{1}$.
Scope	:	mh
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref AreaLight : M_AL5

Timed Predicate	emptyMach

Intention	:	This predicate is true iff the machine assumes that there is currently no person in the area for which occupancy is considered.
Scope	:	mh
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref HallwaySection : M_HS3
		msref BasicRoom : M_BaR1

Timed Predicate	occupied

Intention	:	This predicate is true iff the machine assumes that the area for which occupancy is considered is occupied. 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 a area or not. See timed predicate emptyMach.
Scope	:	mh
Postreferences	:	msref NoMalfunctionOccupancy : M_NMO1
		msref Occupancy : M_OCC2

MACHINE SPECIFICATIONS

Property	M_NMO1

Formal	:	(  occupied             dt1  emptyMach            *[  dt1 +  dt2  emptyMach ]  dt3  emptyMach )
NL	:	An area is defined to be occupied if and only if one of the following conditions holds: during the past $\mathit{dt}_1$ time units a person has continuously been in the area or there has already been a time span of length $\mathit{dt}_1 + \mathit{dt}_2$ such that a person has continuously been in the area, and since this has been the case for the last time, periods where the area has continuously been empty were not longer than or equal to $\mathit{dt}_3$.