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.
Postreferences	:	dkref ControlledLight : D_CL1
		dkref ControlledLight : D_CL2
		dkref AreaLight : D_AL2
		msref ControlledLight : M_CL1
		msref AreaLight : M_AL7
		rsref AreaLight : R_AL1
		rsref AreaLight : R_AL2
		rsref HallwaySection : R_HS1
		rsref HallwaySection : R_HS2
		rsref Floor : R_F1

Object	pulse  :  Pulse

Intention	:	This object represents the actuator the machine uses to switch the light on or off.
Postreferences	:	dkref ControlledLight : D_CL1
		msref ControlledLight : M_CL1
		msref ControlledLight : M_CL2
		msref AreaLight : M_AL7
		msref AreaLight : M_AL9
		msref RoomLight : M_RL8
		msref RoomLight : M_RL9
		msref RoomLight : M_RL10

Object	csa  :  ControlSystemActive

Intention	:	This object represents the actuator the machine uses to signal that it is still active.
Postreferences	:	msref ControlledLight : M_CL3
		msref ControlledLight : M_CL4

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.
Postreferences	:	dkref ControlledLight : D_CL2

Timed Predicate	manualControl

Intention	:	This predicate is true iff the machine assumes that the light is controlled manually.
Scope	:	mh
Postreferences	:	msref ControlledLight : I_CL1
		msref ControlledLight : M_CL1
		msref ControlledLight : M_CL2
		msref AreaLight : M_AL8

DOMAIN KNOWLEDGE

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.