Description Class PushButton

INTENTION

This class provides all definitions concerning the control of a light using pushbuttons. The number of pushbuttons is not relevant for the behavior. Note further that the push buttons are not visible for the machine.

SIGNATURE

Time Constant	T_PB

Intention	:	This time constant represents the delay between a button push and the change of the light.
Scope	:	ev
Postreferences	:	dkref PushButton : D_PB1
		dkref PushButton : D_PB2

Timed Predicate	light

Intention	:	This predicate represents the status of the light existing in the real world. The predicate is true iff the light is on. Note that on here means that the circuit of the light is closed.
Scope	:	eh
Postreferences	:	dkref PushButton : D_PB1
		dkref PushButton : D_PB2
		dkref ControlledLight : D_CL2

Timed Predicate	pushBut

Intention	:	This predicate represents the status of the push buttons existing in the real world. The predicate is true iff one push button is pushed.
Scope	:	eh
Postreferences	:	dkref PushButton : D_PB1
		dkref PushButton : D_PB2

DOMAIN KNOWLEDGE

Property	D_PB1

Formal	:	(  light [  pushBut ]  T_PB  light )
NL	:	Whenever the light is off and any push button is pressed, the light changes to on within time $T\_PB$.

Property	D_PB2

Formal	:	(  light [  pushBut ]  T_PB  light )
NL	:	Whenever the light is on and any push button is pressed, the light changes to off within time $T\_PB$.