module Regulator =

type Regulator_code_msg = enum (CarStarter, OnOffReg, speedTooLow, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal, maintainSpeed, stopRegulating);

type Regulator_message = struct (Regulator_code_msg id; code_sender sender; integer deadline;);

%constant Regulator_message default_Regulator_message = (#CarStarter, #dummy, 0);% 

process exec_Regulator_chart =
   { integer Regulator_fifo_size; }
   ( ? event upsample_clk;
       integer upsample_counter;
       event ms;
       event CarStarter, OnOffReg, speedTooLow, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal;
       integer speed; code_sender received_giveSpeed_caller;
     ! event trigger_giveSpeed;
       code_sender sent_giveSpeed_caller;
   )
   (| (shifted_CarStarter, shifted_OnOffReg, shifted_speedTooLow, shifted_pressBrakePedal, shifted_pressAcceleratorPedal, shifted_releaseAcceleratorPedal, shifted_trigger_maintainSpeed, shifted_trigger_stopRegulating) := unfold(upsample_clk, upsample_counter, CarStarter, OnOffReg, speedTooLow, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal, trigger_maintainSpeed, trigger_stopRegulating)
    | msg_in := putMsg(shifted_CarStarter, shifted_OnOffReg, shifted_speedTooLow, shifted_pressBrakePedal, shifted_pressAcceleratorPedal, shifted_releaseAcceleratorPedal, shifted_trigger_maintainSpeed, shifted_trigger_stopRegulating)
    | (msg_out, alarm_empty, alarm_full, OK_put, OK_get) := FIFO{Regulator_message, Regulator_fifo_size%, default_Regulator_message%} (upsample_clk, msg_in, clk_getMsg)
    | first_msg := (not (^first_msg)) $ init true
    | first_msg ^= when OK_put
    | (provided_CarStarter, provided_OnOffReg, provided_speedTooLow, provided_pressBrakePedal, provided_pressAcceleratorPedal, provided_releaseAcceleratorPedal, provided_call_maintainSpeed, provided_call_stopRegulating) := getMsg(msg_out, OK_get)
    | no_input_event := when (not OK_get)
    | (end_step, trigger_maintainSpeed, trigger_stopRegulating, trigger_giveSpeed, sent_giveSpeed_caller) := Regulator_chart(upsample_clk, ms, provided_CarStarter, provided_OnOffReg, provided_speedTooLow, provided_pressBrakePedal, provided_pressAcceleratorPedal, provided_releaseAcceleratorPedal, provided_call_maintainSpeed, provided_call_stopRegulating, speed, received_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;
     Regulator_message msg_in, msg_out;
     event no_input_event, end_step, ReadyToExecute, clk_getMsg;
     event shifted_CarStarter, shifted_OnOffReg, shifted_speedTooLow, shifted_pressBrakePedal, shifted_pressAcceleratorPedal, shifted_releaseAcceleratorPedal, shifted_trigger_maintainSpeed, shifted_trigger_stopRegulating;
     event provided_CarStarter, provided_OnOffReg, provided_speedTooLow, provided_pressBrakePedal, provided_pressAcceleratorPedal, provided_releaseAcceleratorPedal, provided_call_maintainSpeed, provided_call_stopRegulating;
     event trigger_maintainSpeed, trigger_stopRegulating;

     process unfold =
        ( ? event upsample_clk;
            integer upsample_counter;
            event CarStarter, OnOffReg, speedTooLow, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal, trigger_maintainSpeed, trigger_stopRegulating;
          ! event shifted_CarStarter, shifted_OnOffReg, shifted_speedTooLow, shifted_pressBrakePedal, shifted_pressAcceleratorPedal, shifted_releaseAcceleratorPedal, shifted_trigger_maintainSpeed, shifted_trigger_stopRegulating;
        )
        (| shifted_CarStarter := CarStarter
         | shifted_OnOffReg := shift_event(OnOffReg, when (upsample_counter = nb_inserted))
         | shifted_speedTooLow := shift_event(speedTooLow, when (upsample_counter = (nb_inserted - 1)))
         | shifted_pressBrakePedal := shift_event(pressBrakePedal, when (upsample_counter = (nb_inserted - 2)))
         | shifted_pressAcceleratorPedal := shift_event(pressAcceleratorPedal, when (upsample_counter = (nb_inserted - 3)))
         | shifted_releaseAcceleratorPedal := shift_event(releaseAcceleratorPedal, when (upsample_counter = (nb_inserted - 4)))
         | shifted_trigger_maintainSpeed := shift_event(trigger_maintainSpeed, when (upsample_counter = (nb_inserted - 5)))
         | shifted_trigger_stopRegulating := shift_event(trigger_stopRegulating, when (upsample_counter = (nb_inserted - 6)))
         |)
     ;

     process putMsg =
        ( ? event CarStarter, OnOffReg, speedTooLow, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal, trigger_maintainSpeed, trigger_stopRegulating;
          ! Regulator_message msg;
        )
        (| msg.id := (#CarStarter when CarStarter)
                     default (#OnOffReg when OnOffReg)
                     default (#speedTooLow when speedTooLow)
                     default (#pressBrakePedal when pressBrakePedal)
                     default (#pressAcceleratorPedal when pressAcceleratorPedal)
                     default (#releaseAcceleratorPedal when releaseAcceleratorPedal)
                     default (#maintainSpeed when trigger_maintainSpeed)
                     default (#stopRegulating when trigger_stopRegulating)
         | msg.sender := #dummy
         | msg.deadline := 0
         |)
     ;

     process getMsg =
        ( ? Regulator_message msg;
            boolean OK_get;
          ! event provided_CarStarter, provided_OnOffReg, provided_speedTooLow, provided_pressBrakePedal, provided_pressAcceleratorPedal, provided_releaseAcceleratorPedal, provided_call_maintainSpeed, provided_call_stopRegulating;
        )
        (| provided_CarStarter := when (msg.id = #CarStarter) when OK_get
         | provided_OnOffReg := when (msg.id = #OnOffReg) when OK_get
         | provided_speedTooLow := when (msg.id = #speedTooLow) when OK_get
         | provided_pressBrakePedal := when (msg.id = #pressBrakePedal) when OK_get
         | provided_pressAcceleratorPedal := when (msg.id = #pressAcceleratorPedal) when OK_get
         | provided_releaseAcceleratorPedal := when (msg.id = #releaseAcceleratorPedal) when OK_get
         | provided_call_maintainSpeed := when (msg.id = #maintainSpeed) when OK_get
         | provided_call_stopRegulating := when (msg.id = #stopRegulating) when OK_get
         |)
     ;

   end;

process Regulator_chart =
   ( ? event Tick;
       event ms;
       event CarStarter, OnOffReg, speedTooLow, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal, call_maintainSpeed, call_stopRegulating;
       integer speed; code_sender received_giveSpeed_caller;
     ! event end_step;
       event trigger_maintainSpeed, trigger_stopRegulating, trigger_giveSpeed;
       code_sender sent_giveSpeed_caller;
   )
   (| (| case Regulator_State in
           {#notReady}:
              (| Regulator_futureState ::= #Ready when CarStarter
               | notReady_end_initRegulating := initRegulating(CarStarter)
               | notReady_ignored_events := OnOffReg ^+ speedTooLow ^+ pressBrakePedal ^+ pressAcceleratorPedal ^+ releaseAcceleratorPedal ^+ call_stopRegulating ^+ call_maintainSpeed
               | end_transition_from_notReady := notReady_end_initRegulating ^+ notReady_ignored_events
               |)
           {#Ready}:
              (| Regulator_futureState ::= #notReady when CarStarter
               | Ready_end_disableRegulating := disableRegulating(CarStarter)
               | Ready_ignored_events := OnOffReg ^+ speedTooLow ^+ pressBrakePedal ^+ pressAcceleratorPedal ^+ releaseAcceleratorPedal ^+ call_stopRegulating ^+ call_maintainSpeed
               | end_transition_from_Ready := Ready_end_disableRegulating ^+ Ready_ignored_events
               |)
         end
       | Regulator_futureState ::= defaultvalue Regulator_futureState $
       | Regulator_futureState ^= Regulator_newState ^= Regulator_State
       | Regulator_end_transition := end_transition_from_notReady ^+ end_transition_from_Ready
       | Regulator_newState := (Regulator_futureState when Regulator_end_transition) cell ^Regulator_State
       | Regulator_nextState := Regulator_newState
       | Regulator_State := Regulator_nextState $ init #notReady
       | Regulator_currentState := Regulator_State
       | Regulator_currentState ^= Tick
       |)
    | clk_Ready_chart := when (Regulator_currentState = #Ready)
    | start_Ready_chart := when (Regulator_nextState = #Ready) when (Regulator_currentState /= #Ready)
    | stop_Ready_chart := when (Regulator_nextState /= #Ready) when (Regulator_currentState = #Ready)
    | Ready_State ^= clk_Ready_chart ^+ start_Ready_chart
    | (| case Ready_State in
           {#Stopped}:
              (| Ready_futureState ::= #Regulating when OnOffReg
               | (Stopped_end_startRegulating, trigger_maintainSpeed1, trigger_stopRegulating1, trigger_giveSpeed1, sent_giveSpeed_caller1) := startRegulating(OnOffReg, speed, received_giveSpeed_caller)
               | Stopped_ignored_events := CarStarter ^+ speedTooLow ^+ pressBrakePedal ^+ pressAcceleratorPedal ^+ releaseAcceleratorPedal ^+ call_stopRegulating ^+ call_maintainSpeed
               | end_transition_from_Stopped := Stopped_end_startRegulating ^+ Stopped_ignored_events
               |)
           {#Regulating}:
              (| Ready_futureState ::= (#Stopped when (OnOffReg ^+ speedTooLow ^+ pressBrakePedal ^+ call_stopRegulating))
                                    default (#Suspended when pressAcceleratorPedal)
                                    default (#Regulating when call_maintainSpeed)
               | Regulating_end_stopRegulating := stopRegulating(OnOffReg ^+ speedTooLow ^+ pressBrakePedal ^+ call_stopRegulating)
               | Regulating_end_suspendRegulating := suspendRegulating(pressAcceleratorPedal)
               | (Regulating_end_maintainSpeed, trigger_giveSpeed2, sent_giveSpeed_caller2) := maintainSpeed(call_maintainSpeed, speed, received_giveSpeed_caller)
               | Regulating_ignored_events := CarStarter ^+ releaseAcceleratorPedal
               | end_transition_from_Regulating := Regulating_end_stopRegulating ^+ Regulating_end_suspendRegulating ^+ Regulating_end_maintainSpeed ^+ Regulating_ignored_events
               |)
           {#Suspended}:
              (| Ready_futureState ::= (#Stopped when (OnOffReg ^+ speedTooLow))
                                    default (#Regulating when releaseAcceleratorPedal)
               | Suspended_end_stopRegulating := stopRegulating(OnOffReg ^+ speedTooLow)
               | (Suspended_end_reinstateRegulating, trigger_maintainSpeed2) := reinstateRegulating(releaseAcceleratorPedal)
               | Suspended_ignored_events := CarStarter ^+ pressAcceleratorPedal ^+ pressBrakePedal ^+ call_stopRegulating ^+ call_maintainSpeed
               | end_transition_from_Suspended := Suspended_end_stopRegulating ^+ Suspended_end_reinstateRegulating ^+ Suspended_ignored_events
               |)
         end
       | Ready_futureState ::= defaultvalue Ready_futureState $
       | Ready_futureState ^= Ready_newState ^= Ready_State
       | Ready_end_transition := end_transition_from_Stopped ^+ end_transition_from_Regulating ^+ end_transition_from_Suspended
       | Ready_newState := (Ready_futureState when Ready_end_transition) cell ^Ready_State
       | Ready_nextState := (#Stopped when start_Ready_chart) default Ready_newState
       | Ready_State := Ready_nextState $ init #Stopped
       | Ready_currentState := Ready_State when clk_Ready_chart
       | (| (| stop_Regulating_state := when (Ready_nextState /= #Regulating) when (Ready_currentState = #Regulating)
             | will_exit_Regulating_state := stop_Regulating_state ^+ stop_Ready_chart
             | maintainSpeed_interval := DEF_INTERVAL{false}(Regulating_end_maintainSpeed, will_exit_Regulating_state)
             | maintainSpeed_interval ^= Ready_State
             | trigger_maintainSpeed3 := when ((ms after Regulating_end_maintainSpeed) = 500) when maintainSpeed_interval
             |)
          | trigger_maintainSpeed := trigger_maintainSpeed1 ^+ trigger_maintainSpeed2 ^+ trigger_maintainSpeed3
          | trigger_stopRegulating := trigger_stopRegulating1
          | trigger_giveSpeed := trigger_giveSpeed1 ^+ trigger_giveSpeed2
          | sent_giveSpeed_caller := sent_giveSpeed_caller1 default sent_giveSpeed_caller2
          | end_step := Regulator_end_transition ^+ Ready_end_transition
          |)
       |)
    |)
   where
     type Regulator_states = enum (notReady, Ready);
     type Regulator_Ready_states = enum (Stopped, Regulating, Suspended);

     Regulator_states Regulator_State, Regulator_futureState, Regulator_newState, Regulator_nextState, Regulator_currentState;
     Regulator_Ready_states Ready_State, Ready_futureState, Ready_newState, Ready_nextState, Ready_currentState;

     event notReady_end_initRegulating, notReady_ignored_events, end_transition_from_notReady;
     event Ready_end_disableRegulating, Ready_ignored_events, end_transition_from_Ready;
     event Regulator_end_transition;

     event Stopped_end_startRegulating, Stopped_ignored_events, end_transition_from_Stopped;
     event Regulating_end_stopRegulating, Regulating_end_suspendRegulating, Regulating_end_maintainSpeed, Regulating_ignored_events, end_transition_from_Regulating;
     event Suspended_end_stopRegulating, Suspended_end_reinstateRegulating, Suspended_ignored_events, end_transition_from_Suspended;
     event Ready_end_transition;

     event clk_Ready_chart, start_Ready_chart, stop_Ready_chart;
     event stop_Regulating_state, will_exit_Regulating_state;
     boolean maintainSpeed_interval;

     event trigger_maintainSpeed1, trigger_maintainSpeed2, trigger_maintainSpeed3;
     event trigger_stopRegulating1;
     event trigger_giveSpeed1, trigger_giveSpeed2;
     code_sender sent_giveSpeed_caller1, sent_giveSpeed_caller2;
   end;


process startRegulating =
   ( ? event start_startRegulating;
       integer speed; code_sender received_giveSpeed_caller;
     ! event end_startRegulating;
       event trigger_maintainSpeed, trigger_stopRegulating, trigger_giveSpeed;
       code_sender sent_giveSpeed_caller;
   )
   (| trigger_giveSpeed := start_startRegulating
    | sent_giveSpeed_caller := #startRegulating when trigger_giveSpeed
    | waited_speed := speed when (received_giveSpeed_caller = #startRegulating)
    | speed_request_interval := DEF_INTERVAL{false}(start_startRegulating, ^waited_speed)
    | speed_request_interval ^= start_startRegulating ^+ speed
    | cSpeed := waited_speed when speed_request_interval
    | cSpeed_threshold := cSpeed >= 50
    | case cSpeed_threshold in
        {true}:
           (| updateOrderedSpeedDisplay(when cSpeed_threshold,cSpeed when cSpeed_threshold)
            | updateDisplay(when cSpeed_threshold,"ON")
            | updateOrder(when cSpeed_threshold,cSpeed when cSpeed_threshold)
            | trigger_maintainSpeed := when cSpeed_threshold
            |)
        {false}:
           (| trigger_stopRegulating := when (not cSpeed_threshold)
            |)
      end
    | end_startRegulating := ^cSpeed
    |)
   where
     integer waited_speed, cSpeed;
     boolean speed_request_interval;
     boolean cSpeed_threshold;
   end;


process stopRegulating =
   ( ? event start_stopRegulating;
     ! event end_stopRegulating;
   )
   (| updateOrderedSpeedDisplay(start_stopRegulating,0)
    | updateDisplay(start_stopRegulating,"OFF")
    | end_stopRegulating := start_stopRegulating
    |);


process suspendRegulating =
   ( ? event start_suspendRegulating;
     ! event end_suspendRegulating;
   )
   (| updateDisplay(start_suspendRegulating,"STDBY")
    | end_suspendRegulating := start_suspendRegulating
    |);


process reinstateRegulating =
   ( ? event start_reinstateRegulating;
     ! event end_reinstateRegulating;
       event trigger_maintainSpeed;
   )
   (| updateDisplay(start_reinstateRegulating,"ON")
    | trigger_maintainSpeed := start_reinstateRegulating
    | end_reinstateRegulating := start_reinstateRegulating
    |);


process maintainSpeed =
   ( ? event start_maintainSpeed;
       integer speed; code_sender received_giveSpeed_caller;
     ! event end_maintainSpeed;
       event trigger_giveSpeed;
       code_sender sent_giveSpeed_caller;
   )
   (| trigger_giveSpeed := start_maintainSpeed
    | sent_giveSpeed_caller := #maintainSpeed when trigger_giveSpeed
    | waited_speed := speed when (received_giveSpeed_caller = #maintainSpeed)
    | speed_request_interval := DEF_INTERVAL{false}(start_maintainSpeed, ^waited_speed)
    | speed_request_interval ^= start_maintainSpeed ^+ speed
    | cSpeed := waited_speed when speed_request_interval
    | deltaTorque := calculate(^cSpeed,cSpeed)
    | setDeltaTorque(^cSpeed,deltaTorque)
    | end_maintainSpeed := ^cSpeed
    |)
   where
     integer waited_speed, cSpeed;
     boolean speed_request_interval;
     dreal deltaTorque;
   end;


process initRegulating =
   ( ? event start_initRegulating;
     ! event end_initRegulating;
   )
   (| updateDisplay(start_initRegulating,"OFF")
    | end_initRegulating := start_initRegulating
    |);


process disableRegulating =
   ( ? event start_disableRegulating;
     ! event end_disableRegulating
   )
   (| updateOrderedSpeedDisplay(start_disableRegulating,0)
    | updateDisplay(start_disableRegulating,"---")
    | end_disableRegulating := start_disableRegulating
    |);

use General;
use A_fifo;

end;