group button:
  uncontrollable u_pushed, u_released;
end

group lamp:
  controllable c_on, c_off;
end

group timer:
  controllable c_start;
  uncontrollable u_timeout;
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