module Regulator =

type Regulator_states = enum (notReady, Ready);
type Regulator_Ready_states = enum (Stopped, Regulating, Suspended);

process Regulator_chart =
   ( ? event Tick;
       event ms;
       event CarStarter, OnOffReg, speedTooLow, pressAcceleratorPedal, releaseAcceleratorPedal, pressBrakePedal;
     ! Regulator_states Regulator_currentState;
       Regulator_Ready_states Ready_currentState;
   )
   (| (| case Regulator_currentState in
           {#notReady}:
              (| Regulator_nextState ::= #Ready when CarStarter
               | initRegulating(CarStarter)
               |)
           {#Ready}:
              (| Regulator_nextState ::= #notReady when CarStarter
               | disableRegulating(CarStarter)
               |)
           else
              (| Regulator_nextState ::= Regulator_currentState
               |)
         end
       | Regulator_currentState := Regulator_nextState $ init #notReady
       | Regulator_currentState ^= Tick
       |)
    | clk_Ready_chart := when (Regulator_currentState = #Ready)
    | start_Ready_chart := when (Regulator_nextState = #Ready) when (Regulator_currentState /= #Ready)
    | Ready_State ^= clk_Ready_chart ^+ start_Ready_chart
    | (| case Ready_State in
           {#Stopped}:
              (| Ready_newState ::= #Regulating when OnOffReg
               | (trigger_maintainSpeed1, trigger_stopRegulating) := startRegulating(OnOffReg)
               |)
           {#Regulating}:
              (| Ready_newState ::= (#Stopped when (speedTooLow default OnOffReg default pressBrakePedal default call_stopRegulating))
                                    default (#Suspended when pressAcceleratorPedal)
               | stopRegulating(speedTooLow default OnOffReg default pressBrakePedal default call_stopRegulating)
               | suspendRegulating(pressAcceleratorPedal)
               |)
           {#Suspended}:
              (| Ready_newState ::= (#Stopped when (speedTooLow default OnOffReg))
                                    default (#Regulating when releaseAcceleratorPedal)
               | stopRegulating(speedTooLow default OnOffReg)
               | trigger_maintainSpeed2 := reinstateRegulating(releaseAcceleratorPedal)
               |)
           else
              (| Ready_newState ::= Ready_State 
               |)
         end
       | Ready_newState ^= 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
       | (| (| start_Regulating_state := when (Ready_nextState = #Regulating) when (Ready_currentState /= #Regulating)
             | enter_Regulating_state := shift_event(start_Regulating_state, clk_Ready_chart)
             | clk_Regulating_state := when (Ready_currentState = #Regulating)
             | (counter, call_maintainSpeed) := topmod{500}(enter_Regulating_state)
             | counter ^= (enter_Regulating_state ^+ ms) ^* (enter_Regulating_state ^+ clk_Regulating_state)
             | maintainSpeed(call_maintainSpeed)
             |)
          | call_stopRegulating := shift_event(trigger_stopRegulating, clk_Ready_chart)
          |)
       |)
    |)
   where
     Regulator_states Regulator_nextState;
     event clk_Ready_chart, start_Ready_chart;
     Regulator_Ready_states Ready_State, Ready_newState, Ready_nextState;
     event trigger_stopRegulating, call_stopRegulating;
     event trigger_maintainSpeed1, trigger_maintainSpeed2, call_maintainSpeed;
     event start_Regulating_state, enter_Regulating_state, clk_Regulating_state;
     integer counter;
   end;


process startRegulating =
   ( ? event clk_startRegulating;
     ! event trigger_maintainSpeed, trigger_stopRegulating;
   )
   (| cSpeed := giveSpeed(clk_startRegulating)
    | cSpeed_threshold := cSpeed >= 50
    | case cSpeed_threshold in
        {true}:
           (| updateOrderedSpeedDisplay(clk_startRegulating,cSpeed when clk_startRegulating)
            | updateDisplay(clk_startRegulating,"ON")
            | updateOrder(clk_startRegulating,cSpeed)
            | trigger_maintainSpeed := true when cSpeed_threshold
            |)
        {false}:
           (| trigger_stopRegulating := true when (not cSpeed_threshold)
            |)
      end
    |)
   where
     integer cSpeed;
     boolean cSpeed_threshold;
   end;


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


process suspendRegulating =
   ( ? event clk_suspendRegulating;
     !
   )
   (| updateDisplay(clk_suspendRegulating,"STDBY")
    |);


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


process maintainSpeed =
   ( ? event clk_maintainSpeed;
     !
   )
   (| cSpeed := giveSpeed(clk_maintainSpeed)
    | deltaTorque := calculate(clk_maintainSpeed,cSpeed)
    | setDeltaTorque(clk_maintainSpeed,deltaTorque)
    |)
   where
     integer cSpeed;
     dreal deltaTorque;
   end;


process initRegulating =
   ( ? event clk_initRegulating;
     !
   )
   (| updateDisplay(clk_initRegulating,"OFF")
    |);


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

use General;

end;