INTENTION
This class provides all definitions to describe the behavior of an actuator if it has a malfunction.
| Postreferences | : | lsref Actuator : malAct |
SIGNATURE
| Object | manualEnteredMal : EnteredValue(VALID_INPUTS = BINARY) |
|---|
| Intention | : | This object represents a value entered manually by a user
concerning a malfunction of an actuator. 1 stands for a malfunction, 0 stands for no malfunction.
Note that the value of this object is only meaningful if the timed predicate stateManualEnteredMal is true. |
| Prereferences | : | pdref FM11 |
| Postreferences | : | msref MalfunctionActuator : M_MA1 |
| Timed Predicate | malDetEnv |
|---|
| Intention | : | This predicate is true if and only if an actuator existing in the real world has a malfunction. Note that this predicate represents the value as it exists in the real world. This value is not visible for the machine. |
| Scope | : | eh |
| Prereferences | : | pdref PD_30 |
| pdref FM11 |
| Timed Predicate | malDetMach |
|---|
| Intention | : | This predicate is true if and only if the machine assumes that an actuator existing in the real world has a malfunction. Note that this predicate represents the value as it seen by the machine. |
| Scope | : | mh |
| Prereferences | : | pdref PD_30 |
| pdref FM11 | ||
| Postreferences | : | msref MalfunctionActuator : M_MA1 |
| msref HallwaySection : M_HS4 | ||
| msref Room : M_R13 | ||
| msref Room : M_R14 |
| Timed Predicate | stateManualEnteredMal |
|---|
| Intention | : | This predicate is true if and only if it has been manually
entered whether there is a malfunction of an actuator or whether there is no malfunction of it.
Note the difference between this predicate and the object manualEnteredMal. |
| Scope | : | mh |
| Prereferences | : | pdref FM11 |
| Postreferences | : | msref MalfunctionActuator : I_M_MA1 |
| msref MalfunctionActuator : M_MA1 |
| Timed Predicate | automaticDetMal |
|---|
| Intention | : | This predicate is true if and only if a malfunction of an actuator has been detected automatically, i.e. not by entering it manually. |
| Scope | : | mh |
| Prereferences | : | pdref FM11 |
| Postreferences | : | msref MalfunctionActuator : M_MA1 |
| Property | I_M_MA1 |
|---|
| Formal | : |  stateManualEnteredMal |
| NL | : | Initially it has not been entered manually whether there is a malfunction of an actuator or whether there is no malfunction of it. |
| Property | M_MA1 |
|---|
| Formal | : |  ( malDetMach 
( stateManualEnteredMal  manualEnteredMal. checked = 1 ) 
( stateManualEnteredMal automaticDetMal ) ) |
| NL | : | The machine assumes a malfunction of an actuator if and only if one of the following conditions is fulfilled:
|
| Prereferences | : | pdref FM11 |