INTENTION
This class provides all definitions to describe the hallway specific light requirements. Each hallway section is equipped with
BASE CLASSES
Class | AreaLight(numLights = 1) |
---|
Intention |
: | All definitions of description class AreaLight are also provided here. There is one light in a hallway section that is controlled by the machine. |
SIGNATURE
Object | eastMd : MotionDetector |
---|
Intention | : | This object represents the motion detector in a hallway which is installed at the more eastern door of the hallway. |
Object | westMd : MotionDetector |
---|
Intention | : | This object represents the motion detector in a hallway which is installed at the more western door of the hallway. |
Object | middleMd : MotionDetector |
---|
Intention | : | This object represents the motion detector in a hallway which is installed in the middle of the hallway. |
Time Constant | T_HS1 |
---|
Intention | : | This constant represents the time delay between a time point a person is near a hallway door indicating that he wants to enter this hallway section and switching on the lights. |
Scope | : | ev |
Time Constant | T_HS2 |
---|
Intention | : | This constant represents the time delay between the loss of light control in this hallway section and switching on the lights. |
Scope | : | ev |
Timed Predicate | nearHallwayDoor |
---|
Intention | : | This predicate is true iff a person is near a hallway door to this hallway section indicating that he wants to enter the hallway section. |
Scope | : | eh |
Timed Predicate | hwLightUncontroll |
---|
Intention | : | This predicate is true iff the light is neither automatically nor manually controllable. |
Scope | : | eh |
Property | R_HS1 |
---|
Formal | : | ( nearHallwayDoor T_HS1 light[1]. ls. noMalSens. envEntity = 1 ) |
NL | : | Whenever a person is continuously in the near of a hallway door of the hallway section for at least T_HS1 time units indicating that he wants to enter the hallway section, then the light in the hallway section will be on within this time span, and remains on at least as long as the person is near the hallway section. |
Property | R_HS2 |
---|
Formal | : | ( hwLightUncontroll T_HS2 light[1]. ls. noMalSens. envEntity = 1 ) |
NL | : | Whenever the lights are neither controllable automatically nor manually for at least T_HS2 time units, then eventually within this time span, the light in the hallway section is on and remains so at least as long as the lights are neither controllable automatically nor manually. |
MACHINE SPECIFICATIONS
Property | M_HS1 |
---|
Formal | : | ( T_HS1 = 50 ) |
NL | : | The value of is always 50 milliseconds. |
Property | M_HS2 |
---|
Formal | : | ( manualControl noSaveLight ) |
NL | : | Whenever the light is not controlled manually the light intensity in a hallway section that is occupied has to be greater than or equal to the light intensity needed to establish save light. |
Property | M_HS3 |
---|
Formal | : | ( occ. noMalOcc. emptyMach
( ( eastMd. usedValue = 0 ) ( westMd. usedValue = 0 ) ( middleMd. usedValue = 0 ) ) ) |
NL | : | The machine always assumes that there is currently no person in a hallway section iff the values of all three motion detectors are 0. |