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
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 . |
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 . |
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 . |
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. |
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. |
Property | M_NMO1 |
---|
NL | : | An area is defined to be occupied if and only if one of the following conditions holds:
|