module Speed =

type Speed_code_msg = enum (CarStarter, updateSpeed, giveSpeed);

type Speed_message = struct (Speed_code_msg id; code_sender sender; integer deadline;);

%constant Speed_message default_Speed_message = (#CarStarter, #dummy, 0);% 

process exec_Speed_chart =
   { integer Regulator_fifo_size; }
   ( ? event upsample_clk;
       integer upsample_counter;
       event ms;
       event CarStarter;
       event trigger_giveSpeed;
       code_sender received_giveSpeed_caller;
     ! event speedTooLow;
       integer speed; code_sender sent_giveSpeed_caller;
   )
   (| (shifted_CarStarter, shifted_trigger_updateSpeed, shifted_trigger_giveSpeed, shifted_received_giveSpeed_caller) := unfold(upsample_clk, upsample_counter, CarStarter, trigger_updateSpeed, trigger_giveSpeed, received_giveSpeed_caller)
    | msg_in := putMsg(shifted_CarStarter, shifted_trigger_updateSpeed, shifted_trigger_giveSpeed, shifted_received_giveSpeed_caller)
    | (msg_out, alarm_empty, alarm_full, OK_put, OK_get) := FIFO{Speed_message, Speed_fifo_size%, default_Speed_message%} (upsample_clk, msg_in, clk_getMsg)
    | first_msg := (not (^first_msg)) $ init true
    | first_msg ^= when OK_put
    | (provided_CarStarter, provided_call_updateSpeed, provided_call_giveSpeed, provided_giveSpeed_caller) := getMsg(msg_out, OK_get)
    | no_input_event := when (not OK_get)
    | (end_step, trigger_updateSpeed, speedTooLow, speed, sent_giveSpeed_caller) := Speed_chart(upsample_clk, ms, provided_CarStarter, provided_call_updateSpeed, provided_call_giveSpeed, provided_giveSpeed_caller)
    | ReadyToExecute := (when first_msg) ^+ end_step ^+ no_input_event
    | clk_getMsg := shift_event(ReadyToExecute, upsample_clk)
    |)
   where
     boolean OK_put, OK_get, first_msg;
     event alarm_empty, alarm_full;
     Speed_message msg_in, msg_out;
     event no_input_event, end_step, ReadyToExecute, clk_getMsg;
     event shifted_CarStarter, shifted_trigger_updateSpeed, shifted_trigger_giveSpeed;
     code_sender shifted_received_giveSpeed_caller;
     event provided_CarStarter, provided_call_updateSpeed, provided_call_giveSpeed;
     code_sender provided_giveSpeed_caller;
     event trigger_updateSpeed;

     process unfold =
        ( ? event upsample_clk;
            integer upsample_counter;
            event CarStarter, trigger_updateSpeed, trigger_giveSpeed;
            code_sender received_giveSpeed_caller;
          ! event shifted_CarStarter, shifted_trigger_updateSpeed, shifted_trigger_giveSpeed;
            code_sender shifted_received_giveSpeed_caller;
        )
        (| shifted_CarStarter := CarStarter
         | shifted_trigger_updateSpeed := shift_event(trigger_updateSpeed, when (upsample_counter = nb_inserted))
         | shifted_trigger_giveSpeed := shift_event(trigger_giveSpeed, when (upsample_counter = (nb_inserted - 1)))
         | shifted_received_giveSpeed_caller := (received_giveSpeed_caller cell shifted_trigger_giveSpeed) when shifted_trigger_giveSpeed
         |)
     ;

     process putMsg =
        ( ? event CarStarter, trigger_updateSpeed, trigger_giveSpeed;
            code_sender received_giveSpeed_caller;
          ! Speed_message msg;
        )
        (| msg.id := (#CarStarter when CarStarter)
                     default (#updateSpeed when trigger_updateSpeed)
                     default (#giveSpeed when trigger_giveSpeed)
         | msg.sender := (received_giveSpeed_caller when trigger_giveSpeed) default #dummy
         | msg.deadline := 0
         |)
     ;

     process getMsg =
        ( ? Speed_message msg;
            boolean OK_get;
          ! event provided_CarStarter, provided_call_updateSpeed, provided_call_giveSpeed;
            code_sender provided_giveSpeed_caller;
        )
        (| provided_CarStarter := when (msg.id = #CarStarter) when OK_get
         | provided_call_updateSpeed := when (msg.id = #updateSpeed) when OK_get
         | provided_call_giveSpeed := when (msg.id = #giveSpeed) when OK_get
         | provided_giveSpeed_caller := msg.sender when provided_call_giveSpeed
         |)
     ;

   end;

process Speed_chart =
   ( ? event Tick;
       event ms;
       event CarStarter, call_updateSpeed, call_giveSpeed;
       code_sender received_giveSpeed_caller;
     ! event end_step;
       event trigger_updateSpeed;
       event speedTooLow;
       integer speed; code_sender sent_giveSpeed_caller;
   )
   (| (| case Speed_State in
           {#notReady}:
              (| Speed_futureState ::= #Ready when CarStarter
               | notReady_ignored_events := call_updateSpeed ^+ call_giveSpeed
               | end_transition_from_notReady := CarStarter ^+ notReady_ignored_events
               |)
           {#Ready}:
              (| Speed_futureState ::= (#notReady when CarStarter)
                                    default (#Ready when (call_updateSpeed ^+ call_giveSpeed))
               | (Ready_end_updateSpeed, speedTooLow) := updateSpeed(call_updateSpeed)
               | (Ready_end_giveSpeed, speed, sent_giveSpeed_caller) := giveSpeed(call_giveSpeed, received_giveSpeed_caller)
               | end_transition_from_Ready := CarStarter ^+ Ready_end_updateSpeed ^+ Ready_end_giveSpeed
               |)
         end
       | Speed_futureState ::= defaultvalue Speed_futureState $
       | Speed_futureState ^= Speed_newState ^= Speed_State
       | Speed_end_transition := end_transition_from_notReady ^+ end_transition_from_Ready
       | Speed_newState := (Speed_futureState when Speed_end_transition) cell ^Speed_State
       | Speed_nextState := Speed_newState
       | Speed_State := Speed_nextState $ init #notReady
       | Speed_currentState := Speed_State
       | Speed_currentState ^= Tick
       |)
    | (| start_Ready_state := when (Speed_nextState = #Ready) when (Speed_currentState /= #Ready)
       | stop_Ready_state := when (Speed_nextState /= #Ready) when (Speed_currentState = #Ready)
       | will_exit_Ready_state := stop_Ready_state
       | updateSpeed_interval := DEF_INTERVAL{false}(Ready_end_updateSpeed, will_exit_Ready_state)
       | updateSpeed_interval ^= Speed_State
       | trigger_updateSpeed := start_Ready_state ^+ (when ((ms after Ready_end_updateSpeed) = 500) when updateSpeed_interval)
       |)
    | end_step := Speed_end_transition
    |)
   where
     type Speed_states = enum (notReady, Ready);

     Speed_states Speed_State, Speed_futureState, Speed_newState, Speed_nextState, Speed_currentState;

     event notReady_ignored_events, end_transition_from_notReady;
     event Ready_end_updateSpeed, Ready_end_giveSpeed, end_transition_from_Ready;
     event Speed_end_transition;

     event clk_Ready_state, start_Ready_state, stop_Ready_state, will_exit_Ready_state;
     boolean updateSpeed_interval;

   end;


process giveSpeed =
   ( ? event start_giveSpeed;
       code_sender received_giveSpeed_caller;
     ! event end_giveSpeed;
       integer speed;
       code_sender sent_giveSpeed_caller;
   )
   (| speed := Speed_value ? when start_giveSpeed
    | sent_giveSpeed_caller := received_giveSpeed_caller when start_giveSpeed
    | end_giveSpeed := start_giveSpeed
    |);


process updateSpeed =
   ( ? event start_updateSpeed;
     ! event end_updateSpeed;
       event speedTooLow;
   )
   (| newSpeed := getSpeed(start_updateSpeed)
    | speedTooLow := when (newSpeed < 50)
    | Speed_value ::= newSpeed
    | end_updateSpeed := start_updateSpeed
    |)
   where
     integer newSpeed;
   end;

use General;
use A_fifo;

end;