module Speed =

type Speed_states = enum (notReady, Ready);

process Speed_chart =
   ( ? event Tick;
       event ms;
       event CarStarter;
     ! Speed_states Speed_currentState;
       event speedTooLow;
   )
   (| (| case Speed_currentState in
           {#notReady}:
              (| Speed_nextState ::= #Ready when CarStarter
               |)
           {#Ready}:
              (| Speed_nextState ::= #notReady when CarStarter
               |)
           else
              (| Speed_nextState ::= Speed_currentState
               |)
         end
       | Speed_currentState := Speed_nextState $ init #notReady
       | Speed_currentState ^= Tick
       |)
    | clk_Ready_state := when (Speed_currentState = #Ready)
    | start_Ready_state := when (Speed_nextState = #Ready) when (Speed_currentState /= #Ready)
    | enter_Ready_state := shift_event(start_Ready_state, Tick)
    | (counter, call_getSpeed) := topmod{500}(enter_Ready_state)
    | counter ^= (enter_Ready_state ^+ ms) ^* (enter_Ready_state ^+ clk_Ready_state)
    | SpeedValue := getSpeed(call_getSpeed)
    | speedTooLow := updateSpeed(^SpeedValue,SpeedValue)
    |)
   where
     Speed_states Speed_nextState;
     event clk_Ready_state, start_Ready_state, enter_Ready_state;
     event call_getSpeed;
     integer counter;
     integer SpeedValue;
   end;


process giveSpeed =
   ( ? event clk_giveSpeed;
     ! integer speed;
   )
   spec (| clk_giveSpeed ^= speed |)
   (| speed := Speed_value ?
    |);


process updateSpeed =
   ( ? event clk_updateSpeed;
       integer newSpeed;
     ! event speedTooLow;
   )
   spec (| clk_updateSpeed ^= newSpeed |)
   (| speedTooLow := when (newSpeed < 50)
    | Speed_value ::= newSpeed
    |);

use General;

end;