Layer2_MMS_SW_SPARK update parameter data items

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

@@ -79,25 +79,29 @@ package MMS.F_PT.F_CM.Output is
      renames MMS.F_PT.F_CM.Input.Mode_Switch;
 
    function Bay_Switch return Bay_Switch_Type
-     renames MMS.F_PT.F_CM.Input.Bay_Switch; 
+     renames MMS.F_PT.F_CM.Input.Bay_Switch;
+   
+   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
      renames MMS.F_PT.F_CM.Input.Payload_Mass;
    
-   function USB_Key return Navigation_Parameters_Type
-     renames MMS.F_PT.F_CM.Input.USB_Key;
-   
    -------------
    -- To F_FC --
    -------------
 
-   function P return Distance_Type
-     renames MMS.F_PT.F_CM.Input.P;
+   function P return Current_Range_Type;
+   --  From MMS.F_PT.F_CM.Input.P, conversion needed
    
-   function P_Dot return Speed_Type
-     renames MMS.F_PT.F_CM.Input.P_Dot;
+   function P_Dot return Current_Speed_Type;
+   --  From MMS.F_PT.F_CM.Input.P_Dot, conversion needed
    
-   function Q return Altitude_Type
-     renames MMS.F_PT.F_CM.Input.Q;
+   function Q return Current_Altitude_Type;
+   --  From MMS.F_PT.F_CM.Input.Q, conversion needed
    
 end MMS.F_PT.F_CM.Output;

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

@@ -17,7 +17,7 @@ package MMS.F_PT.F_EM.Input is
    -- From F_CM --
    ---------------
    
-   function P_Dot return Speed_Type
+   function P_Dot return Current_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_fc-data.ads

+with MMS.F_PT.Data;
+
 package MMS.F_PT.F_FC.Data is
 
    --  ??? Types need to be precisely defined.
@@ -8,28 +10,34 @@ package MMS.F_PT.F_FC.Data is
 
    --  From 6.7.2.3
 
-   type Gain_Type is new Integer; --  ??? some bounds
-
-   type Gain_Triple is record
-      Kd : Gain_Type;
-      Kp : Gain_Type;
-      Ki : Gain_Type;
-   end record;
+   Flight_Domain_Mesh : Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100); -- ??? bounds
 
    function Climb_Gains
-     (Mass     : Payload_Mass_Type;
-      Altitude : Current_Altitude_Type;
-      Speed    : Current_Speed_Type) return Gain_Triple;
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
 
    function Cruise_Gains
-     (Mass     : Payload_Mass_Type;
-      Altitude : Current_Altitude_Type;
-      Speed    : Current_Speed_Type) return Gain_Triple;
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
 
    function Descent_Gains
-     (Mass     : Payload_Mass_Type;
-      Altitude : Current_Altitude_Type;
-      Speed    : Current_Speed_Type) return Gain_Triple;
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
 
    ---------------
    -- Constants --
@@ -37,15 +45,16 @@ package MMS.F_PT.F_FC.Data is
 
    --  From 6.7.3.2
 
-   Qdot_MinCl : Integer; --  in angle.s-1
-   Qdot_MaxCl : Integer; --  in angle.s-1
-   Q_MaxCl    : Integer; --  in angle.s-1
-   Qdot_MinCr : Integer; --  in angle.s-1
-   Q_MinCr    : Integer; --  in angle.s-1
-   Pdot_MaxCr : Integer; --  in angle.s-1
-   Qdot_MinDs : Integer; --  in angle.s-1
-   Qdot_MaxDs : Integer; --  in angle.s-1
-   Q_MaxDs    : Integer; --  in angle.s-1
+   Qdot_MinCl : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MaxCl : Angular_Speed_Type; --  in angle.s-1
+   Q_MaxCl    : Angle_Type; --  in angle
+   Qdot_MinCr : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MaxCr : Angular_Speed_Type; --  in angle.s-1
+   Q_MinCr    : Angle_Type; --  in angle
+   Pdot_MaxCr : Current_Speed_Type; --  in km/h
+   Qdot_MinDs : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MaxDs : Angular_Speed_Type; --  in angle.s-1
+   Q_MaxDs    : Angle_Type; --  in angle
 
    Escape_Time : Integer; --  in s
 

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

@@ -7,14 +7,17 @@ package MMS.F_PT.F_FC.Input is
    -- From F_CM --
    ---------------
 
-   function P return Distance_Type
+   function P return Current_Range_Type
      renames MMS.F_PT.F_CM.Output.P;
    
-   function P_Dot return Speed_Type
+   function P_Dot return Current_Speed_Type
      renames MMS.F_PT.F_CM.Output.P_Dot;
    
-   function Q return Altitude_Type
+   function Q return Current_Altitude_Type
      renames MMS.F_PT.F_CM.Output.Q;
+   
+   function Payload_Mass return Payload_Mass_Type
+     renames MMS.F_PT.F_CM.Output.Payload_Mass;
       
    ---------------
    -- From F_MM --

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc.ads

 package MMS.F_PT.F_FC is
 
-   
+   type Flight_Cell_Center_Type is record
+      Speed    : Current_Speed_Type;
+      Altitude : Current_Altitude_Type;
+   end record;
 
-end MMS.F_PT.F_FC;
\ No newline at end of file
+   type Flight_Speed_Center is new Positive;
+   type Flight_Altitude_Center is new Positive;
+
+   type Flight_Domain_Mesh_Type is array
+     (Flight_Speed_Center range <>, Flight_Altitude_Center range <>)
+     of Flight_Cell_Center_Type;
+
+   type Gain_Type is new Integer; --  ??? some bounds
+
+   type Gain_Triple is record
+      Kd : Gain_Type;
+      Kp : Gain_Type;
+      Ki : Gain_Type;
+   end record;
+
+end MMS.F_PT.F_FC;

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

+with MMS.F_PT.Data;
+
 package MMS.F_PT.F_MM.Data is
 
    --------------------------
@@ -6,41 +8,64 @@ package MMS.F_PT.F_MM.Data is
 
    --  From 6.6.2.3
 
-   function Viability_Amode_initial
-     (Payload_Mass    : Payload_Mass_Type;
-      Distance        : Current_Range_Type;
-      Navigation_Mode : Navigation_Mode_Type;
-      Altitude        : Current_Altitude_Type;
-      Speed           : Current_Speed_Type)
-      return Energy_Level_Type;
-
-   function Viability_Amode_cruise
-     (Payload_Mass    : Payload_Mass_Type;
-      Distance        : Current_Range_Type;
-      Navigation_Mode : Navigation_Mode_Type;
-      Altitude        : Current_Altitude_Type;
-      Speed           : Current_Speed_Type)
-      return Energy_Level_Type;
-
-   function Viability_RPmode_initial
-     (Payload_Mass    : Payload_Mass_Type;
-      Distance        : Current_Range_Type;
-      Navigation_Mode : Navigation_Mode_Type;
-      Altitude        : Current_Altitude_Type;
-      Speed           : Current_Speed_Type)
-      return Energy_Level_Type;
-
-   function Viability_RPmode_cruise
-     (Payload_Mass    : Payload_Mass_Type;
-      Distance        : Current_Range_Type;
-      Navigation_Mode : Navigation_Mode_Type;
-      Altitude        : Current_Altitude_Type;
-      Speed           : Current_Speed_Type)
-      return Energy_Level_Type;
+   Amode_Initial_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_Amode_Initial
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre => M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in Amode_Initial_Domain_Mesh'Range (1)
+     and then A in Amode_Initial_Domain_Mesh'Range (2)
+     and then S in Amode_Initial_Domain_Mesh'Range (3);
+
+   Amode_Cruise_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_Amode_Cruise
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre =>  M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in Amode_Cruise_Domain_Mesh'Range (1)
+     and then A in Amode_Cruise_Domain_Mesh'Range (2)
+     and then S in Amode_Cruise_Domain_Mesh'Range (3);
+
+   RPmode_Initial_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_RPmode_Initial
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre =>  M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in RPmode_Initial_Domain_Mesh'Range (1)
+     and then A in RPmode_Initial_Domain_Mesh'Range (2)
+     and then S in RPmode_Initial_Domain_Mesh'Range (3);
+
+   RPmode_Cruise_Domain_Mesh : Viability_Domain_Mesh_Type
+     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+
+   function Viability_RPmode_Cruise
+     (M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center) return Energy_Level_Type
+   with Pre =>  M in MMS.F_PT.Data.Payload_Mass_Grid'Range
+     and then D in RPmode_Cruise_Domain_Mesh'Range (1)
+     and then A in RPmode_Cruise_Domain_Mesh'Range (2)
+     and then S in RPmode_Cruise_Domain_Mesh'Range (3);
 
    --  From 6.6.4 Mission termination control
 
+   Glide_Distance_Domain_Mesh : Glide_Domain_Mesh_Type (1 .. 100); -- ??? bounds
+
    function Glide_Distance
-     (Altitude : Current_Altitude_Type) return Current_Range_Type;
+     (AI : Glide_Altitude_Center) return Current_Range_Type
+   with Pre => AI in Glide_Distance_Domain_Mesh'Range;
 
 end MMS.F_PT.F_MM.Data;

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

@@ -31,7 +31,7 @@ package MMS.F_PT.F_MM.Input is
      renames MMS.F_PT.F_CM.Output.Mode_Switch;
 
    function Bay_Switch return Bay_Switch_Type
-     renames MMS.F_PT.F_CM.Output.Bay_Switch; 
+     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;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.ads

 package MMS.F_PT.F_MM is
 
-   
+   type Viability_Cell_Center_Type is record
+      Distance     : Current_Range_Type;
+      Altitude     : Current_Altitude_Type;
+      Speed        : Current_Speed_Type;
+   end record;
 
-end MMS.F_PT.F_MM;
\ No newline at end of file
+   type Viability_Distance_Center is new Positive;
+   type Viability_Altitude_Center is new Positive;
+   type Viability_Speed_Center is new Positive;
+
+   type Viability_Domain_Mesh_Type is array
+     (Viability_Distance_Center range <>,
+      Viability_Altitude_Center range <>,
+      Viability_Speed_Center range <>)
+     of Viability_Cell_Center_Type;
+
+   type Glide_Altitude_Center is new Positive;
+
+   type Glide_Domain_Mesh_Type is array
+     (Glide_Altitude_Center range <>) of Current_Altitude_Type;
+
+end MMS.F_PT.F_MM;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt.ads

 package MMS.F_PT is
-
    
+   type Current_Range_Type is range 1 .. 1_000_000; -- in meters
+   
+   type Current_Speed_Type is range 1 .. 500;  -- in km/h
+   
+   type Current_Altitude_Type is range -200 .. 1_000; -- in meters
+   
+   type Angle_Type is new Float; -- in Angle bounds???
+   
+   type Angular_Speed_Type is new Float; -- in Angle.s-1 bounds???
+   
+   type Estimated_Total_Mass_Type is delta 0.1 range 5.0 .. 10.0; -- in kg ???
+   
+   type Energy_Level_Type is range 0 .. 500; -- in kj
+   
+   type Operating_Point_Type is record
+      Altitude : Current_Altitude_Type; -- ??? which altitude type
+      Speed    : Current_Speed_Type; --  ??? which speed type
+   end record;
+
+   type Payload_Mass_Center is new Positive;
+
+   type Payload_Mass_Grid_Type is array (Payload_Mass_Center range <>)
+     of Payload_Mass_Type;
 
-end MMS.F_PT;
\ No newline at end of file
+end MMS.F_PT;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms.ads

@@ -39,7 +39,7 @@ package MMS is
    
    type Bay_Switch_Type is (OPEN, CLOSED);
    
-   type Payload_Mass_Type is delta 0.1 range 1.0 .. 5.0; -- ??? in kg
+   type Payload_Mass_Type is new Integer range 0 .. 98; -- in kg
 
    type Distance_Type is new Float; -- in n.m
    
@@ -47,7 +47,7 @@ package MMS is
    
    type Altitude_Type is new Float; -- in ft
    
-   type Rotactor_Type is range 1 .. 9;
+   type Rotactor_Type is range 0 .. 9;
    
    type CP_Switches_Type is record
       Power      : Boolean;
@@ -75,19 +75,4 @@ package MMS is
    end record;
    
    type Torque_Type is delta 0.0001 range -10.0E6 .. 10.0E6; -- ???
-   
-   type Current_Range_Type is range 1 .. 1_000_000; -- in meters
-   
-   type Current_Speed_Type is range 1 .. 500;  -- in km/h
-   
-   type Current_Altitude_Type is range -200 .. 1_000; -- in meters
-   
-   type Estimated_Total_Mass_Type is delta 0.1 range 5.0 .. 10.0; -- in kg ???
-   
-   type Energy_Level_Type is range 0 .. 500; -- in kj
-   
-   type Operating_Point_Type is record
-      Altitude : Current_Altitude_Type; -- ??? which altitude type
-      Speed    : Current_Speed_Type; --  ??? which speed type
-   end record;
 end MMS;