INTENTION
This class provides all specifications concerning the informing of a person if a specific condition is given.
| Postreferences | : | lsref InformUnreasonableInput : InformPerson |
| lsref InformSensActMalFct : InformPerson |
SIGNATURE
| Object | indicator : IndicatorLight |
|---|
| Intention | : | This object represents an indicator light on a control panel that is used to inform a person about a specific situation. |
| Prereferences | : | pdref U8 |
| pdref FM7 | ||
| pdref NF9 | ||
| Postreferences | : | msref InformPerson : M_IP2 |
| msref InformPerson : M_IP1 | ||
| msref InformPerson : M_IP3 | ||
| msref AreaCtrlPanelFM : I_M_ACPFM3 | ||
| msref AreaCtrlPanelFM : I_M_ACPFM4 | ||
| msref RoomCtrlPanel : I_M_RCP11 | ||
| msref RoomCtrlPanel : I_M_RCP12 | ||
| dkref InformPerson : D_IP1 | ||
| msref InformPerson : I_M_IP2 | ||
| msref Floor : M_F5 |
| Time Constant | T_MinInf |
|---|
| Intention | : | This time constant is the minimal time a person has to be informed about a specific situation. |
| Scope | : | mh |
| Prereferences | : | pdref U8 |
| pdref FM7 | ||
| pdref NF9 | ||
| Postreferences | : | msref InformPerson : M_IP2 |
| msref InformPerson : M_IP4 | ||
| msref InformUnreasonableInput : M_IUI1 | ||
| msref InformSensActMalFct : M_ISAMF1 |
| Time Constant | T_MaxInf |
|---|
| Intention | : | This time constant is the maximal time a person has to be informed about a specific situation. |
| Scope | : | mh |
| Prereferences | : | pdref U8 |
| pdref FM7 | ||
| pdref NF9 | ||
| Postreferences | : | msref InformPerson : M_IP3 |
| msref InformPerson : M_IP4 | ||
| msref InformUnreasonableInput : M_IUI2 | ||
| msref InformSensActMalFct : M_ISAMF2 |
| Time Constant | T_InfDelayNew |
|---|
| Intention | : | This time constant represents the maximal delay between the time point a specific situation about a person should be informed occurs and the time point a person is informed about this situation. |
| Scope | : | mh |
| Prereferences | : | pdref U8 |
| pdref FM7 | ||
| pdref NF9 | ||
| Postreferences | : | msref InformPerson : M_IP1 |
| msref InformUnreasonableInput : M_IUI3 | ||
| msref InformSensActMalFct : M_ISAMF3 |
| Timed Predicate | informCondEnv |
|---|
| Intention | : | This predicate is true if and only if there is a situation a person should be informed about. This predicate represent the situation as it is in the real world. |
| Scope | : | eh |
| Prereferences | : | pdref U8 |
| pdref FM7 | ||
| pdref NF9 |
| Timed Predicate | informCondMach |
|---|
| Intention | : | This predicate is true if and only if there is a situation a person should be informed about. |
| Scope | : | ev |
| Prereferences | : | pdref U8 |
| pdref FM7 | ||
| pdref NF9 | ||
| Postreferences | : | msref InformPerson : I_M_IP1 |
| msref InformPerson : M_IP1 | ||
| msref AreaCtrlPanelFM : M_ACPFM1 | ||
| msref RoomCtrlPanel : M_RCP1 | ||
| msref Floor : M_F3 | ||
| msref Floor : M_F4 | ||
| msref HallwaySection : M_HS4 | ||
| msref Room : M_R13 | ||
| msref Room : M_R14 |
| Timed Predicate | personInformed |
|---|
| Intention | : | This predicate is true if and only if a person is informed. |
| Scope | : | eh |
| Prereferences | : | pdref U8 |
| pdref FM7 | ||
| pdref NF9 | ||
| Postreferences | : | dkref InformPerson : D_IP1 |
| Property | D_IP1 |
|---|
| Formal | : |  ( indicator. noMalAct. envEntity = 1  personInformed ) |
| NL | : | Whenever the indicator light on a control panel is on then the corresponding person is informed. |
MACHINE SPECIFICATIONS
| Property | I_M_IP1 |
|---|
| Formal | : |  informCondMach |
| NL | : | Initially the situation a person has to be informed about is not given. |
| Property | I_M_IP2 |
|---|
| Formal | : | indicator. noMalAct. adjustedEntity = 0 |
| NL | : | Initially the indicator light is switched off. |
| Property | M_IP1 |
|---|
| Formal | : | ( [ informCondMach ]
  T_InfDelayNew indicator. noMalAct. adjustedEntity = 1 ) |
| NL | : | Whenever the situation a person should be informed about starts the indicator light on the control panel is on within T_InfDelayNew milliseconds. |
| Property | M_IP2 |
|---|
| Formal | : | (  T_MinInf ( indicator. noMalAct. adjustedEntity = 1 ) ) |
| NL | : | Whenever the indicator light is switched on it remains on for at least T_MinInf milliseconds. |
| Property | M_IP3 |
|---|
| Formal | : | ( [ indicator. noMalAct. adjustedEntity = 1 ]
T_MaxInf ( indicator. noMalAct. adjustedEntity = 0 ) ) |
| NL | : | Whenever the indicator light is switched on it is switched off again within the next T_MaxInf milliseconds. |
| Property | M_IP4 |
|---|
| Formal | : | ( T_MinInf < T_MaxInf ) |
| NL | : | The maximal time a person has to be informed about a specific situation is always greater than the minimal time a person has to be informed about a specific situation. |