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.

DOMAIN KNOWLEDGE

Property	D_PB1

NL

:

Whenever the light is off and any push button is pressed, the light changes to on within time $T\_PB$.

Property	D_PB2

NL

:

Whenever the light is on and any push button is pressed, the light changes to off within time $T\_PB$.