Description Class ControlledLight

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:

• a light sensor indicating whether the light is on or off (object ls)
• an actuator allowing the machine to switch on and off the light (object pulse)
• an actuator allowing the machine to signal that it is still active (object csa)
• a push button allowing a person to switch on and off the light (object pb)
  Note that a push of a button is not directly visible for the machine but only by the light sensor.

Furthermore, it is defined under which conditions a light is controlled manually.

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.

DOMAIN KNOWLEDGE

Property	D_CL1

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

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

NL

:

Initially the light is not controlled manually.

Property	M_CL1

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

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

NL

:

Whenever the signal control system is active is set to 1 it is set within one second to 0.

Property	M_CL4

NL

:

Whenever the signal control system is active is set to 0 it is set within 59 seconds to 1.