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 |
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 |
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 |
Property | D_PB1 |
---|
NL | : | Whenever the light is off and any push button is pressed, the light changes to on within time . |
Property | D_PB2 |
---|
NL | : | Whenever the light is on and any push button is pressed, the light changes to off within time . |