| plant automaton button: |
| uncontrollable u_pushed, u_released; |
| |
| location released: |
| initial; |
| edge u_pushed goto pushed; |
| |
| location pushed: |
| edge u_released goto released; |
| end |
| |
| plant automaton lamp: |
| controllable c_on, c_off; |
| |
| location off: |
| initial; |
| edge c_on goto on; |
| |
| location on: |
| edge c_off goto off; |
| end |
| |
| plant automaton timer: |
| controllable c_start; |
| uncontrollable u_timeout; |
| |
| cont t der 1.0; |
| |
| location idle: |
| initial; |
| edge c_start do t := 0.0 goto running; |
| |
| location running: |
| edge u_timeout when t >= 2.0 goto idle; |
| end |