Layer2_MMS_SW_SPARK add external volatile state for captors

UseCaseDevelopment/Layer2_MMS_SW_SPARK/external.ads

+with Types; use Types;
+
+package External with Abstract_State =>
+  ((From_GS with External => Async_Writers),
+   (From_CP with External => Async_Writers),
+   (From_P_P with External => Async_Writers)) is
+
+   ------------------------------------------------------
+   -- Ground-based Mission Preparation and Supervision --
+   ------------------------------------------------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type with
+     Volatile_Function,
+     Global => From_GS;
+
+   function Navigation_Mode return Navigation_Mode_Type with
+     Volatile_Function,
+     Global => From_GS;
+
+   function Navigation_Option return Navigation_Option_Type with
+     Volatile_Function,
+     Global => From_GS;
+
+   function Go return Boolean with
+     Volatile_Function,
+     Global => From_GS;
+
+   function Emergency_Landing return Boolean with
+     Volatile_Function,
+     Global => From_GS;
+
+   --------------------------------------------------
+   -- AV-based Mission Preparation (Control Panel) --
+   --------------------------------------------------
+
+   function On_OFF_Push_Button return Boolean with
+     Volatile_Function,
+     Global => From_CP;
+
+   function Start_Push_Button return Boolean with
+     Volatile_Function,
+     Global => From_CP;
+
+   function Mode_Switch return Navigation_Mode_Type with
+     Volatile_Function,
+     Global => From_CP;
+
+   function Bay_Switch return Bay_Switch_Type with
+     Volatile_Function,
+     Global => From_CP;
+
+   function Payload_Mass return Payload_Mass_Type with
+     Volatile_Function,
+     Global => From_CP;
+
+   function USB_Key return Navigation_Parameters_Type with
+     Volatile_Function,
+     Global => From_CP;
+
+   -------------------------
+   -- Physical Parameters --
+   -------------------------
+
+   function P return Distance_Type with
+     Volatile_Function,
+     Global => From_P_P;
+
+   function P_Dot return Speed_Type with
+     Volatile_Function,
+     Global => From_P_P;
+
+   function Q return Angle_Type with
+     Volatile_Function,
+     Global => From_P_P;
+
+end External;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el-data.ads

+with Types; use Types;
+
 package MMS.F_EL.Data is
 
    ---------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el-input.ads

 with MMS.Input;
 with MMS.F_PT.Output;
 
+with Types; use Types;
+
 package MMS.F_EL.Input is
 
    --------------
@@ -13,7 +15,7 @@ package MMS.F_EL.Input is
    function P_Dot return Speed_Type
      renames MMS.Input.P_Dot;
    
-   function Q return Altitude_Type
+   function Q return Angle_Type
      renames MMS.Input.Q;
    
    ---------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el-output.ads

+with Types; use Types;
+
 package MMS.F_EL.Output is
 
    ------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el.ads

+with Types; use Types;
+
 package MMS.F_EL is
 
    

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm-input.ads

@@ -3,6 +3,8 @@ with MMS.F_PT.F_MM.Output;
 with MMS.F_PT.F_FC.Output;
 with MMS.F_PT.F_EM.Output;
 
+with Types; use Types;
+
 package MMS.F_PT.F_CM.Input is
    
    ---------------
@@ -42,12 +44,6 @@ package MMS.F_PT.F_CM.Input is
    function USB_Key return Navigation_Parameters_Type
      renames MMS.F_PT.Input.USB_Key;
    
-   function Rotactor_1 return Rotactor_Type
-     renames MMS.F_PT.Input.Rotactor_1;
-   
-   function Rotactor_2 return Rotactor_Type
-     renames MMS.F_PT.Input.Rotactor_2;
-   
    function P return Distance_Type
      renames MMS.F_PT.Input.P;
    

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm-output.ads

 with MMS.F_PT.F_CM.Input;
 
+with Types; use Types;
+
 package MMS.F_PT.F_CM.Output is
 
    -------------
@@ -12,8 +14,11 @@ package MMS.F_PT.F_CM.Output is
          Mode       => MMS.F_PT.F_CM.Input.Mode_Switch,
          Bay        => MMS.F_PT.F_CM.Input.Bay_Switch,
          Start      => MMS.F_PT.F_CM.Input.Start_Push_Button,
-         Rotactor_1 => MMS.F_PT.F_CM.Input.Rotactor_1,
-         Rotactor_2 => MMS.F_PT.F_CM.Input.Rotactor_2));
+         Rotactor_1 => 
+            Rotactor_Type (MMS.F_PT.F_CM.Input.Payload_Mass / 10),
+         Rotactor_2 => 
+            Rotactor_Type (MMS.F_PT.F_CM.Input.Payload_Mass mod 10)));
+   --  ??? Rotactors are computed from payload mass, which one is which?
       
    function CP_Displays return CP_Displays_Type is
      (CP_Displays_Type'
@@ -83,12 +88,8 @@ package MMS.F_PT.F_CM.Output is
    
    function USB_Key return Navigation_Parameters_Type
      renames MMS.F_PT.F_CM.Input.USB_Key; 
-   
-   ----------------------
-   -- To F_MM and F_FC --
-   ----------------------
 
-   function Payload_Mass return Payload_Mass_Type
+   function Payload_Mass_To_F_MM return Payload_Mass_Type
      renames MMS.F_PT.F_CM.Input.Payload_Mass;
    
    -------------
@@ -100,5 +101,8 @@ package MMS.F_PT.F_CM.Output is
    function P_Dot return Speed_Type renames MMS.F_PT.F_CM.Input.P_Dot;
    
    function Q return Angle_Type renames MMS.F_PT.F_CM.Input.Q;
+
+   function Payload_Mass_To_F_FC return Payload_Mass_Type
+     renames MMS.F_PT.F_CM.Input.Payload_Mass;
    
 end MMS.F_PT.F_CM.Output;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_cm.ads

+with Types; use Types;
+
 package MMS.F_PT.F_CM is
 
    

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-data.ads

+with Types; use Types;
+
 package MMS.F_PT.F_EM.Data is
 
    ---------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-input.ads

 with MMS.F_PT.F_FC.Output;
 with MMS.F_PT.F_CM.Output;
 
+with Types; use Types;
+
 package MMS.F_PT.F_EM.Input is
 
    ---------------
@@ -17,7 +19,7 @@ package MMS.F_PT.F_EM.Input is
    -- From F_CM --
    ---------------
    
-   function P_Dot return Current_Speed_Type
+   function P_Dot return Speed_Type
      renames MMS.F_PT.F_CM.Output.P_Dot;
 
 end MMS.F_PT.F_EM.Input;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_em-output.ads

+with Types; use Types;
+
 package MMS.F_PT.F_EM.Output is
 
    -------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_em.ads

+with Types; use Types;
+
 package MMS.F_PT.F_EM is
 
    

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior.ads

 with MMS.F_PT.F_FC.Data;
 
+with Types; use Types;
+
 package MMS.F_PT.F_FC.Behavior is
 
    ------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-data.ads

 with MMS.F_PT.Data;
 
+with Types; use Types;
+
 package MMS.F_PT.F_FC.Data is
 
    --  ??? Types need to be precisely defined.

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-input.ads

 with MMS.F_PT.F_CM.Output;
 with MMS.F_PT.F_MM.Output;
 
+with Types; use Types;
+
 package MMS.F_PT.F_FC.Input is
 
    ---------------
@@ -17,7 +19,7 @@ package MMS.F_PT.F_FC.Input is
      renames MMS.F_PT.F_CM.Output.Q;
    
    function Payload_Mass return Payload_Mass_Type
-     renames MMS.F_PT.F_CM.Output.Payload_Mass;
+     renames MMS.F_PT.F_CM.Output.Payload_Mass_To_F_FC;
       
    ---------------
    -- From F_MM --

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-output.ads

+with Types; use Types;
+
 package MMS.F_PT.F_FC.Output is
 
    ----------------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc.ads

+with Types; use Types;
+
 package MMS.F_PT.F_FC is
 
    type Flight_Cell_Center_Type is record

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.adb

+with Types; use Types;
+
 package body MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
 
    procedure Run is

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior-guarantees.ads

@@ -2,6 +2,8 @@
 --  is used to verify in SPARK that high level guarantees on F_MM are implied
 --  by its behavioural specification.
 
+with Types; use Types;
+
 package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
    pragma Unevaluated_Use_Of_Old (Allow);
 

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior.ads

@@ -8,12 +8,38 @@
 --   - A single behaviour is specified for each case in the specification.
 --   - There is a behaviour is specified for every case in the specification.
 
+with Types; use Types;
+with External;
+with MMS.F_PT.F_MM.Output;
+
 package MMS.F_PT.F_MM.Behavior with
   SPARK_Mode,
   Abstract_State => State
 is
    pragma Unevaluated_Use_Of_Old (Allow);
 
+   ------------
+   -- Inputs --
+   ------------
+
+   function Navigation_Mode_From_CP return Navigation_Mode_Type with
+     Global => State;
+
+   function Navigation_Mode_From_GS return Navigation_Mode_Type with
+     Global => State;
+
+   function Operating_Point_From_GS_Received return Boolean with
+     Global => State;
+
+   function Operating_Point_From_GS return Operating_Point_Type with
+     Global => State;
+
+   function USB_Key_Present return Boolean with
+     Global => State;
+
+   function Operating_Point_From_USB_Key return Operating_Point_Type with
+     Global => State;
+
    -----------------------------------------
    -- States of the automaton in Figure 3 --
    -----------------------------------------
@@ -36,7 +62,10 @@ is
      Pre => Power_State = ON
      and then On_State = RUNNING;
 
-   function Navigation_Mode return Navigation_Mode_Type with
+   function Navigation_Mode return Navigation_Mode_Type
+   is (if Navigation_Mode_From_CP = A then A
+       else Navigation_Mode_From_GS)
+   with
      Global => State,
      Pre => Power_State = ON
      and then On_State in INIT | RUNNING;
@@ -95,7 +124,7 @@ is
      and then On_State = RUNNING
      and then Running_State = LANDING;
 
-   function Operating_Mode_Changed return Boolean with
+   function Operating_Point_Changed return Boolean with
      Global => State,
      Pre => Power_State = ON
      and then On_State = RUNNING
@@ -118,7 +147,11 @@ is
      and then On_State in INIT | RUNNING
      and then (if On_State = RUNNING then Running_State = CRUISE);
 
-   function Mission_Parameters_Defined return Boolean with
+   function Mission_Parameters_Defined return Boolean is
+     (USB_Key_Present
+      or else (Navigation_Mode_From_CP = RP
+               and then Operating_Point_From_GS_Received))
+   with
      Global => State,
      Pre => Power_State = ON
      and then On_State = INIT;
@@ -133,6 +166,10 @@ is
      Pre => Power_State = ON
      and then On_State = CANCELLED;
 
+   -------------
+   -- Outputs --
+   -------------
+
    function Mission_Cancellation_Signaled return Boolean with
      Global => State;
 
@@ -146,6 +183,14 @@ is
    -- Behavioural Specification of F_MM --
    ---------------------------------------
 
+   procedure Read_Inputs with
+     Global => (In_Out => State,
+                Input  => (External.From_GS, External.From_CP));
+
+   procedure Write_Outputs with
+     Global => (Input  => State,
+                Output => (Output.To_F_CM, Output.To_F_FC, Output.To_F_EL));
+
    procedure Run with
      Global         => (In_Out => State),
      Post           =>
@@ -162,7 +207,16 @@ is
 
      and then
        (if Navigation_Mode'Old = A
+        then Operating_Point = Operating_Point'Old)
+
+       --  Freeze the operating mode once landing is activated.
+
+     and then
+       (if Power_State'Old = ON
+        and then On_State'Old = RUNNING
+        and then Running_State = LANDING
         then Operating_Point = Operating_Point'Old),
+
      Contract_Cases =>
        (Power_State = OFF
         and then Power_Off
@@ -273,7 +327,7 @@ is
           (if Running_State = CRUISE then Energy_Compatible_With_Mission)
         and then
           (if Running_State = DESCENT then not Descent_Over)
-        and then Operating_Mode_Changed
+        and then Operating_Point_Changed
         =>
           Power_State = ON
         and then On_State = RUNNING
@@ -284,7 +338,7 @@ is
         and then (Running_State in CLIMB | DESCENT)
         and then Power_On
         and then not Mission_Abort_Received
-        and then (if Navigation_Mode = RP then not Operating_Mode_Changed)
+        and then (if Navigation_Mode = RP then not Operating_Point_Changed)
         and then (if Running_State = DESCENT then not Descent_Over)
         and then Cruise_Altitude_Reached
         =>
@@ -299,7 +353,7 @@ is
         and then not Mission_Abort_Received
         and then
           (if Running_State = CRUISE then Energy_Compatible_With_Mission)
-        and then (if Navigation_Mode = RP then not Operating_Mode_Changed)
+        and then (if Navigation_Mode = RP then not Operating_Point_Changed)
         and then
           (if Running_State in CLIMB | DESCENT then
                  not Cruise_Altitude_Reached)
@@ -337,4 +391,37 @@ is
           Power_State = ON
         and then On_State = On_State'Old);
 
+private
+
+   procedure Mission_Setup_Management with
+     Global => (In_Out => State),
+     Post => (if Payload_Bay_Closed
+              and then Mission_Parameters_Defined
+              and then Energy_Compatible_With_Mission
+              then Boarding_Completed);
+
+   procedure Operating_Point_Update_Management with
+     Global => (In_Out => State),
+     Contract_Cases =>
+       (Navigation_Mode_From_CP = A
+        or else not Operating_Point_From_GS_Received
+        =>
+          Operating_Point = Operating_Point_From_USB_Key,
+
+        Navigation_Mode_From_CP = RP
+        and then Operating_Point_From_GS_Received
+        and then Power_State = ON
+        and then On_State = RUNNING
+        and then Running_State = LANDING
+        =>
+          Operating_Point = Operating_Point'Old,
+
+        Navigation_Mode_From_CP = RP
+        and then Operating_Point_From_GS_Received
+        and then not (Power_State = ON
+          and then On_State = RUNNING
+          and then Running_State = LANDING)
+        =>
+          Operating_Point = Operating_Point_From_GS);
+
 end MMS.F_PT.F_MM.Behavior;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-data.ads

 with MMS.F_PT.Data;
 
+with Types; use Types;
+
 package MMS.F_PT.F_MM.Data is
 
    --------------------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-input.ads

@@ -3,6 +3,8 @@ with MMS.F_PT.F_FC.Output;
 with MMS.F_PT.F_EM.Output;
 with MMS.F_PT.Input;
 
+with Types; use Types;
+
 package MMS.F_PT.F_MM.Input is
    
    ---------------
@@ -34,7 +36,7 @@ package MMS.F_PT.F_MM.Input is
      renames MMS.F_PT.F_CM.Output.Bay_Switch;
 
    function Payload_Mass return Payload_Mass_Type
-     renames MMS.F_PT.F_CM.Output.Payload_Mass;
+     renames MMS.F_PT.F_CM.Output.Payload_Mass_To_F_MM;
    
    function USB_Key return Navigation_Parameters_Type
      renames MMS.F_PT.F_CM.Output.USB_Key;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-output.ads

-package MMS.F_PT.F_MM.Output is
+with Types; use Types;
+
+package MMS.F_PT.F_MM.Output with
+  Abstract_State => (To_F_CM, To_F_EL, To_F_FC)
+is
 
    -------------
    -- To F_CM --
    --------------
    
-   function Mission_Cancelled return Boolean;
+   function Mission_Cancelled return Boolean with Global => To_F_CM;
    
-   function Mission_Complete return Boolean;
+   function Mission_Complete return Boolean with Global => To_F_CM;
    
-   function Mission_Aborted return Boolean;
+   function Mission_Aborted return Boolean with Global => To_F_CM;
    
    -------------
    -- To F_EL --
    --------------
 
-   function Emergency_Landing return Boolean;
+   function Emergency_Landing return Boolean with Global => To_F_EL;
    
    -------------
    -- To F_FC --
    -------------
    
-   function Start_Take_Off return Boolean;
+   function Start_Take_Off return Boolean with Global => To_F_FC;
    
-   function Start_Landing return Boolean;
+   function Start_Landing return Boolean with Global => To_F_FC;
 
-   function Operating_Point return Operating_Point_Type;
+   function Operating_Point return Operating_Point_Type with Global => To_F_FC;
    
-   function Operating_Mode return Navigation_Option_Type;
+   function Operating_Mode return Navigation_Option_Type with Global => To_F_FC;
    
-   function Mission_Range return Current_Range_Type; -- ??? which distance type
+   function Mission_Range return Current_Range_Type with Global => To_F_FC;
+   -- ??? which distance type
    
 end MMS.F_PT.F_MM.Output;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.ads

+with Types; use Types;
+
 package MMS.F_PT.F_MM is
 
    type Viability_Cell_Center_Type is record

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-input.ads

 with MMS.Input;
 with MMS.F_EL.Output;
 
+with Types; use Types;
+
 package MMS.F_PT.Input is
 
    --------------
@@ -40,12 +42,6 @@ package MMS.F_PT.Input is
    function USB_Key return Navigation_Parameters_Type
      renames MMS.Input.USB_Key;
    
-   function Rotactor_1 return Rotactor_Type
-     renames MMS.Input.Rotactor_1;
-   
-   function Rotactor_2 return Rotactor_Type
-     renames MMS.Input.Rotactor_2;
-   
    function P return Distance_Type
      renames MMS.Input.P;
    

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-output.ads

 with MMS.F_PT.F_CM.Output;
 with MMS.F_PT.F_MM.Output;
   
+with Types; use Types;
+
 package MMS.F_PT.Output is
    
    -----------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt.ads

+with Types; use Types;
+
 package MMS.F_PT is
    
    type Current_Range_Type is range 1 .. 1_000_000; -- in meters

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-input.ads

+with Types; use Types;
+with External;
+
 package MMS.Input is
 
    ------------------------------------------------------
    -- Ground-based Mission Preparation and Supervision --
    ------------------------------------------------------
 
-   function Navigation_Parameters return Navigation_Parameters_Type;
+   function Navigation_Parameters return Navigation_Parameters_Type
+     renames External.Navigation_Parameters;
 
-   function Navigation_Mode return Navigation_Mode_Type;
+   function Navigation_Mode return Navigation_Mode_Type
+     renames External.Navigation_Mode;
 
-   function Navigation_Option return Navigation_Option_Type;
+   function Navigation_Option return Navigation_Option_Type
+     renames External.Navigation_Option;
 
-   function Go return Boolean;
+   function Go return Boolean renames External.Go;
 
-   function Emergency_Landing return Boolean;
+   function Emergency_Landing return Boolean renames External.Emergency_Landing;
 
    --------------------------------------------------
    -- AV-based Mission Preparation (Control Panel) --
    --------------------------------------------------
 
-   function On_OFF_Push_Button return Boolean;
-
-   function Start_Push_Button return Boolean;
-
-   function Mode_Switch return Navigation_Mode_Type;
+   function On_OFF_Push_Button return Boolean
+     renames External.On_OFF_Push_Button;
 
-   function Bay_Switch return Bay_Switch_Type;
+   function Start_Push_Button return Boolean
+     renames External.Start_Push_Button;
 
-   function Payload_Mass return Payload_Mass_Type;
+   function Mode_Switch return Navigation_Mode_Type
+     renames External.Mode_Switch;
 
-   function USB_Key return Navigation_Parameters_Type;
+   function Bay_Switch return Bay_Switch_Type
+     renames External.Bay_Switch;
 
-   function Rotactor_1 return Rotactor_Type;
+   function Payload_Mass return Payload_Mass_Type
+     renames External.Payload_Mass;
 
-   function Rotactor_2 return Rotactor_Type;
+   function USB_Key return Navigation_Parameters_Type
+     renames External.USB_Key;
 
    -------------------------
    -- Physical Parameters --
    -------------------------
 
-   function P return Distance_Type;
+   function P return Distance_Type renames External.P;
 
-   function P_Dot return Speed_Type;
+   function P_Dot return Speed_Type renames External.P_Dot;
 
-   function Q return Angle_Type;
+   function Q return Angle_Type renames External.Q;
 
 end MMS.Input;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-output.ads

 with MMS.F_PT.Output;
 
+with Types; use Types;
+
 package MMS.Output is
 
    -------------------------------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms.ads

@@ -16,65 +16,4 @@
 --        with a header specifying to which component(s) they are linked.
 
 package MMS is
-
-   ----------------------------------
-   -- Types for inputs and outputs --
-   ----------------------------------
-
-   type Distance_Input_Type is range 1 .. 100; -- in n.m
-   
-   type Speed_Input_Type is range 1 .. 250; -- in k.t
-   
-   type Altitude_Input_Type is range -500 .. 3000; -- in ft
-   
-   type Navigation_Parameters_Type is record
-      Distance : Distance_Input_Type;
-      Speed    : Speed_Input_Type;
-      Altitude : Altitude_Input_Type;
-   end record;
-   
-   type Navigation_Mode_Type is (RP, A);
-   
-   type Navigation_Option_Type is (SPEED, ALTITUDE, ENERGY);
-   
-   type Bay_Switch_Type is (OPEN, CLOSED);
-   
-   type Payload_Mass_Type is new Integer range 0 .. 98; -- in kg
-
-   type Distance_Type is new Float; -- type of P, unit and bounds ???
-   
-   type Speed_Type is new Float; -- type of P_Dot, unit and bounds ???
-   
-   type Angle_Type is new Float; -- type of Q, unit and bounds ???
-   
-   type Angular_Speed_Type is new Float; -- type of Q_Dot, unit and bounds ???
-   
-   type Rotactor_Type is range 0 .. 9;
-   
-   type CP_Switches_Type is record
-      Power      : Boolean;
-      Mode       : Navigation_Mode_Type;
-      Bay        : Bay_Switch_Type;
-      Start      : Boolean;
-      Rotactor_1 : Rotactor_Type;
-      Rotactor_2 : Rotactor_Type;
-   end record;
-
-   type Source_Type is range 1 .. 100;
-   
-   type CP_Displays_Type is record
-      Ready            : Boolean;
-      Cancelled        : Boolean;
-      Complete         : Boolean;
-      Aborted          : Boolean; -- ???
-      Primary_Source   : Source_Type;
-      Secondary_Source : Source_Type;
-   end record;
-      
-   type Propulsion_Energy_Type is record
-      Primary_Source_Capacity   : Source_Type;
-      Secondary_Source_Capacity : Source_Type;
-   end record;
-   
-   type Torque_Type is delta 0.0001 range -10.0E6 .. 10.0E6; -- ???
 end MMS;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/types.ads

+package Types is
+
+   ----------------------------------
+   -- Types for inputs and outputs --
+   ----------------------------------
+
+   type Distance_Input_Type is range 1 .. 100; -- in n.m
+
+   type Speed_Input_Type is range 1 .. 250; -- in k.t
+
+   type Altitude_Input_Type is range -500 .. 3000; -- in ft
+
+   type Navigation_Parameters_Type is record
+      Distance : Distance_Input_Type;
+      Speed    : Speed_Input_Type;
+      Altitude : Altitude_Input_Type;
+   end record;
+
+   type Navigation_Mode_Type is (RP, A);
+
+   type Navigation_Option_Type is (SPEED, ALTITUDE, ENERGY);
+
+   type Bay_Switch_Type is (OPEN, CLOSED);
+
+   type Payload_Mass_Type is new Integer range 0 .. 98; -- in kg
+
+   type Distance_Type is new Float; -- type of P, unit and bounds ???
+
+   type Speed_Type is new Float; -- type of P_Dot, unit and bounds ???
+
+   type Angle_Type is new Float; -- type of Q, unit and bounds ???
+
+   type Angular_Speed_Type is new Float; -- type of Q_Dot, unit and bounds ???
+
+   type Rotactor_Type is range 0 .. 9;
+
+   type CP_Switches_Type is record
+      Power      : Boolean;
+      Mode       : Navigation_Mode_Type;
+      Bay        : Bay_Switch_Type;
+      Start      : Boolean;
+      Rotactor_1 : Rotactor_Type;
+      Rotactor_2 : Rotactor_Type;
+   end record;
+
+   type Source_Type is range 1 .. 100;
+
+   type CP_Displays_Type is record
+      Ready            : Boolean;
+      Cancelled        : Boolean;
+      Complete         : Boolean;
+      Aborted          : Boolean; -- ???
+      Primary_Source   : Source_Type;
+      Secondary_Source : Source_Type;
+   end record;
+
+   type Propulsion_Energy_Type is record
+      Primary_Source_Capacity   : Source_Type;
+      Secondary_Source_Capacity : Source_Type;
+   end record;
+
+   type Torque_Type is delta 0.0001 range -10.0E6 .. 10.0E6; -- ???
+end Types;