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. |
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. |
Property | I_A1 |
---|
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 |
---|
NL | : | The machine assumes a malfunction of the actuator iff one of the following conditions is fulfilled:
|