INTENTION
This class provides all definitions to describe an actuator. It is composed of the behavior of an actuator if there is no malfunction and the case that there is a malfunction.
FORMAL PARAMETERS
| Sort | ENV_DOMAIN |
|---|
| Intention | : | This domain contains the possible values of the phenomenon existing in the real world in the case that a sensor has no malfunction. |
| Sort | ADJUSTED_DOMAIN |
|---|
| Intention | : | This domain contains the possible values that can be adjusted by the machine in the case that a sensor has no malfunction. |
SIGNATURE
| Object | noMalAct : NoMalfunctionActuator(ENV_DOMAIN = ENV_DOMAIN, ADJUSTED_DOMAIN = ADJUSTED_DOMAIN) |
|---|
| Intention | : | This object represents the part of the actuator describing the behavior of the actuator if it has no malfunction, i.e. if the machine assumes that it has no malfunction. |
| Object | malAct : MalfunctionActuator |
|---|
| Intention | : | This object represents the part of the actuator describing the behavior of the actuator if it has a malfunction, i.e. if the machine assumes that it has a malfunction. |
| Object | manualEnteredMal : EnteredValue(CHECKED_DOM = BINARY) |
|---|
| Intention | : | This object represents a value entered manually by a user concerning a malfunction of the 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. |
| Timed Predicate | stateManualEnteredMal |
|---|
| Intention | : | This predicate is true iff it has been manually entered whether there is a malfunction of the actuator or whether there is no malfunction of it.
Note the difference between this predicate and the object manualEnteredMal. |
| Scope | : | mh |
| Timed Predicate | automaticDetMal |
|---|
| Intention | : | This predicate is true iff a malfunction of the actuator has been detected automatically, i.e. not by entering it manually. |
| Scope | : | mh |
| Property | I_A1 |
|---|
| Formal | : |  stateManualEnteredMal |
| NL | : | Initially it has not been entered manually whether there is a malfunction of the actuator or whether there is no malfunction of it. |
| Property | M_A1 |
|---|
| Formal | : |  ( malAct. malDetMach 
( stateManualEnteredMal  manualEnteredMal. checked = 1 ) 
( stateManualEnteredMal automaticDetMal ) ) |
| NL | : | The machine assumes a malfunction of the actuator iff one of the following conditions is fulfilled:
|