| plant automaton button: |
| uncontrollable u_pushed; |
| uncontrollable u_released; |
| location released: |
| initial; |
| edge u_pushed goto pushed; |
| location pushed: |
| edge u_released goto released; |
| end |
| plant automaton lamp: |
| controllable c_on; |
| controllable 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 |
| supervisor automaton timed_lamp: |
| location s0: |
| initial; |
| edge button.u_pushed goto s1; |
| edge button.u_released; |
| location s1: |
| edge lamp.c_on goto s2; |
| edge button.u_pushed, button.u_released; |
| location s2: |
| edge timer.c_start goto s3; |
| edge button.u_pushed, button.u_released; |
| location s3: |
| edge timer.u_timeout goto s4; |
| edge button.u_pushed, button.u_released; |
| location s4: |
| edge lamp.c_off goto s0; |
| edge button.u_pushed, button.u_released; |
| end |