Template Declaration PushButton

INTENTION

This class provides all definitions concerning the control of a ceiling light group using push buttons. Note that a push button is not visible for the machine and therefore this description class is not derived from the description class Actuator.

The value of the time constant T_PB has still to be provided by the domain expert.

Postreferences

:

lsref CeilingLightGroup : pb

SIGNATURE

Time Constant	T_PB

NL	:	push-to-light delay
Intention	:	This time constant represents the delay between the time point a push button is pushed and the time point a ceiling light group changes to on or off.
Scope	:	ev
Prereferences	:	akref BD_8
		akref BD_14
Postreferences	:	dkref PushButton : D_PB1
		dkref PushButton : D_PB2

Timed Predicate	light

Intention	:	This predicate represents the status of the ceiling light group existing in the real world. The predicate is true if and only if the ceiling light group is on. Note that on here means that the circuit of the ceiling light group is closed.
Scope	:	eh
Prereferences	:	akref BD_8
		akref BD_14
Postreferences	:	dkref PushButton : D_PB1
		dkref PushButton : D_PB2
		dkref CeilingLightGroup : D_CLG2

Timed Predicate	pushBut

Intention	:	This predicate represents the status of a push button existing in the real world. The predicate is true if and only if a push button is pushed.
Scope	:	eh
Prereferences	:	akref BD_8
		akref BD_14
Postreferences	:	dkref PushButton : D_PB1
		dkref PushButton : D_PB2

DOMAIN KNOWLEDGE

Property	D_PB1

Formal	:	(  light [  pushBut ]  T_PB  light )
NL	:	Whenever the ceiling light group is off and a push button is pressed, the ceiling light group changes to on within time $T\_PB$.
Prereferences	:	akref BD_8
		akref BD_14

Property	D_PB2

Formal	:	(  light [  pushBut ]  T_PB  light )
NL	:	Whenever the ceiling light group is on and a push button is pressed, the ceiling light group changes to off within time $T\_PB$.
Prereferences	:	akref BD_8
		akref BD_14