INTENTION
This description class provides all definitions of sensors and actuators relevant for the control of a light that is not dimmable. This installation includes:
SIGNATURE
Object | ls : LightSensor |
---|
Intention | : | This object represents the light sensor indicating whether the light is on or off. |
Object | pulse : Pulse |
---|
Intention | : | This object represents the actuator the machine uses to switch the light on or off. |
Object | csa : ControlSystemActive |
---|
Intention | : | This object represents the actuator the machine uses to signal that it is still active. |
Object | pb : PushButton |
---|
Intention | : | This object represents the actuatori.e. the push button, a person can use to switch the light on or off. Note that a push of a button is not directly visible for the machine. |
Timed Predicate | manualControl |
---|
Intention | : | This predicate is true iff the machine assumes that the light is controlled manually. |
Scope | : | mh |
Property | D_CL1 |
---|
Formal | : | ( ls. noMalSens. envEntity = pulse. noMalAct. envEntity ) |
NL | : | The phenomenon in the real world which is measured by the light sensor is identical with the phenomenon adjusted by the pulse actuator. |
Property | D_CL2 |
---|
Formal | : | ( ( ls. noMalSens. envEntity = 1 ) pb. light ) |
NL | : | The phenomenon in the real world which is measured by the light sensor is identical with the phenomenon adjusted by the push buttons. |
MACHINE SPECIFICATIONS
Property | I_CL1 |
---|
Formal | : | manualControl |
NL | : | Initially the light is not controlled manually. |
Property | M_CL1 |
---|
Formal | : | ( ( pulse. noMalAct. reactionTime [ pulse. noMalAct. adjustedEntity = 1 ]
( [ ls. noMalSens. convertedEntity = 1 ] [ ls. noMalSens. convertedEntity = 0 ] ) ) manualControl ) |
NL | : | If no pulse has been sent by the machine for the last
pulse.noMalAct.reactionTime milliseconds and the measured value of the light sensor changes the light is controlled manually. |
Property | M_CL2 |
---|
Formal | : | ( pulse. noMalAct. reactionTime [ pulse. noMalAct. adjustedEntity = 1 ]
manualControl ) |
NL | : | If a pulse has been sent by the machine within the last
pulse.noMalAct.reactionTime milliseconds the light is not controlled manually. |
Property | M_CL3 |
---|
Formal | : | ( [ csa. noMalAct. adjustedEntity = 1 ] 1000
[ csa. noMalAct. adjustedEntity = 0 ] ) |
NL | : | Whenever the signal control system is active is set to 1 it is set within one second to 0. |
Property | M_CL4 |
---|
Formal | : | ( [ csa. noMalAct. adjustedEntity = 0 ] 59000
[ csa. noMalAct. adjustedEntity = 1 ] ) |
NL | : | Whenever the signal control system is active is set to 0 it is set within 59 seconds to 1. |