Template Declaration CeilingLightGroup

INTENTION

This description class provides all definitions of sensors and actuators relevant for the control of a ceiling light group that is not dimmable. This installation includes:

• a status line indicating whether the ceiling light group is on or off represented by the object ls
• an actuator allowing the machine to switch on and off the ceiling light group, represented by the object pulse
• an actuator allowing the machine to signal that it is still active, represented by the object csa
• numPB many push buttons allowing a person to switch on and off the ceiling light group, represented by the object-array pb.
  Note that a push of a push button is not directly visible for the machine but only through the status line.

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

Postreferences	:	lsref DimmableCeilingLightGroup : CeilingLightGroup
		lsref Area : light

FORMAL PARAMETERS

Function	numPB  NAT

Intention	:	This parameter represents the number of push buttons with direct control of the ceiling light group (bypassing the machine). The default number is 1, i.e., if nothing else is specified there is one such push button.
Defaultvalue	:	1
Postreferences	:	lsref CeilingLightGroup : pb
		dkref CeilingLightGroup : D_CLG2
		lsref Area : light

SIGNATURE

Object	sl  :  StatusLine

Intention	:	This object represents the status line indicating whether a ceiling light group is on or off.
Prereferences	:	akref BD_8
		akref BD_14
		akref Table1
		akref BD_19
		akref Figure3
Postreferences	:	dkref CeilingLightGroup : D_CLG1
		dkref CeilingLightGroup : D_CLG2
		dkref CeilingLightGroup : D_CLG3
		msref CeilingLightGroup : M_CLG1
		rsref Floor : R_F1
		rsref Area : R_A1
		rsref Area : R_A2
		msref Area : M_A5
		msref Area : M_A6
		rsref HallwaySection : R_HS1
		rsref HallwaySection : R_HS2
		msref HallwaySection : M_HS4
		msref Room : M_R13
		msref Room : M_R14
		msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9

Object	pulse  :  Pulse

Intention	:	This object represents the actuator of a ceiling light group the machine uses to switch the ceiling light group on or off.
Prereferences	:	akref Table1
		akref BD_19
		akref Figure3
Postreferences	:	dkref CeilingLightGroup : D_CLG1
		msref CeilingLightGroup : M_CLG1
		msref CeilingLightGroup : M_CLG2
		msref Area : M_A5
		msref Area : M_A6
		msref Area : M_A8
		msref HallwaySection : M_HS4
		msref HallwaySection : M_HS5
		msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9
		msref Room : M_R10
		msref Room : M_R13
		msref Room : M_R14

Object	csa  :  ControlSystemActive

Intention	:	This object represents the actuator of a ceiling light group the machine uses to signal that it is still active.
Prereferences	:	akref Table2
		akref BD_19
		akref Figure3
Postreferences	:	dkref CeilingLightGroup : D_CLG3
		msref CeilingLightGroup : M_CLG3
		msref CeilingLightGroup : M_CLG4
		dkref DimmableCeilingLightGroup : D_DCLG1
		msref HallwaySection : M_HS4
		msref Room : M_R13
		msref Room : M_R14

Object	pb  :  PushButton[ numPB]

Intention	:	These objects represent the push buttons of a ceiling light group a person can use to switch the light on or off. Note that a push of a button is not directly visible to the machine.
Prereferences	:	akref BD_8
		akref BD_14
		akref BD_19
		akref Figure3
Postreferences	:	dkref CeilingLightGroup : D_CLG2

Timed Predicate	manualControl

Intention	:	This predicate is true if and only if the machine assumes that the ceiling light group is controlled manually.
Scope	:	mh
Prereferences	:	pdref PD_30
Postreferences	:	msref CeilingLightGroup : I_CLG1
		msref CeilingLightGroup : M_CLG1
		msref CeilingLightGroup : M_CLG2
		msref Area : M_A7

DOMAIN KNOWLEDGE

Property	D_CLG1

Formal	:	(  sl. noMalSens. envEntity =  pulse. noMalAct. envEntity )
NL	:	The phenomenon in the real world which is measured by the status line is identical with the phenomenon adjusted by the pulse actuator.
Propreferences	:	rsref Area : R_A2

Property	D_CLG2

Formal	:	( i NAT (  numPB ) :                      ( (  sl. noMalSens. envEntity = 1 )  pb[i]. light ) )
NL	:	The phenomenon in the real world which is measured by the status line is identical with the phenomenon adjusted by the push buttons.

Property	D_CLG3

Formal	:	( 60000  csa. noMalAct. envEntity 1                                                     sl. noMalSens. envEntity = 1 )
NL	:	If the signal control system active is not sent for at least 60 seconds, a ceiling light group is on.

MACHINE SPECIFICATIONS

Property	I_CLG1

Formal	:	manualControl
NL	:	Initially the light is not controlled manually.

Property	M_CLG1

Formal	:	( (  pulse. noMalAct. reactionTime [  pulse. noMalAct. adjustedEntity = 1 ]            ( [  sl. noMalSens. convertedEntity = 1 ]              [  sl. 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 status line changes the ceiling light group is controlled manually.

Property	M_CLG2

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 a ceiling light group is not controlled manually.

Property	M_CLG3

Formal	:	( [  csa. noMalAct. adjustedEntity = 1 ] 1000                                          [  csa. noMalAct. adjustedEntity = 0 ] )
NL	:	Whenever the signal control system active is set to 1 it is set within one second to 0.

Property	M_CLG4

Formal	:	( [  csa. noMalAct. adjustedEntity = 0 ] 59000                                          [  csa. noMalAct. adjustedEntity = 1 ] )
NL	:	Whenever the signal control system active is set to 0 it is set within 59 seconds to 1.