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. |
Postreferences | : | dkref ToggleActuator : D_TA1 |
dkref ToggleActuator : D_TA2 | ||
dkref Pulse : D_PUL1 | ||
dkref RangeActuator : D_RA1 | ||
dkref Dimmer : D_DIM1 | ||
dkref ControlSystemActive : D_CSA1 | ||
dkref ControlledLight : D_CL1 | ||
msref ControlledLight : M_CL1 | ||
msref ControlledLight : M_CL2 | ||
msref ControlledLight : M_CL3 | ||
msref ControlledLight : M_CL4 | ||
msref AreaLight : M_AL7 | ||
msref AreaLight : M_AL9 | ||
msref RoomLight : M_RL8 | ||
msref RoomLight : M_RL9 | ||
msref RoomLight : M_RL10 | ||
msref RoomLight : M_RL11 |
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. |
Postreferences | : | msref Actuator : M_A1 |
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. |
Postreferences | : | msref Actuator : M_A1 |
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 |
Postreferences | : | msref Actuator : I_A1 |
msref Actuator : M_A1 |
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 |
Postreferences | : | msref Actuator : M_A1 |
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:
|