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.

MACHINE SPECIFICATIONS

Property	M_NMO1

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$.