Layer_2_MMS_SW_SPARK: use dimension system for floating-point units

Some units in types.ads are defined as floating-point types and others
as signed integer types. Start using the dimension system in GNAT on
floating-point units. Next step is to see if there is a benefit in using
floating-point types instead of signed integer types for the input and
output types, so that we can use the standard dimension system. Otherwise,
we could use a signed integer type with the Dimension_System aspect as
the root type for all these signed integer types.

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

+with System.Dim.Mks; use all type System.Dim.Mks.Mks_Type;
+
 with MMS.F_PT.F_FC.Data;
 with External;
 with Types; use Types;
@@ -252,7 +254,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
         and then not Emergency_Landing
         and then
           (if Running_State = LANDING then
-              not (P_Dot = 0.0 and then Q_Dot = 0.0))
+              not (P_Dot = Zero_Speed and then Q_Dot = Zero_Speed))
         and then not In_Safety_Envelope
         and then Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time
         =>
@@ -263,7 +265,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
         and then not Emergency_Landing
         and then
           (if Running_State = LANDING then
-              not (P_Dot = 0.0 and then Q_Dot = 0.0))
+              not (P_Dot = Zero_Speed and then Q_Dot = Zero_Speed))
         and then
           (if Running_State = FLIGHT then not Start_Landing)
         and then
@@ -305,7 +307,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
         On_State = RUNNING
         and then not Emergency_Landing
         and then Running_State = LANDING
-        and then P_Dot = 0.0 and then Q_Dot = 0.0
+        and then P_Dot = Zero_Speed and then Q_Dot = Zero_Speed
         =>
           On_State = COMPLETE,
 

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

@@ -104,15 +104,15 @@ private
    Flight_Domain_Mesh : constant Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100) :=
      (others => (others => <>));
 
-   Qdot_MinCl : constant Speed_Type := 0.0;
-   Qdot_MaxCl : constant Speed_Type := 0.0;
+   Qdot_MinCl : constant Speed_Type := Zero_Speed;
+   Qdot_MaxCl : constant Speed_Type := Zero_Speed;
    Q_MaxCl    : constant Angle_Type := 0.0;
-   Qdot_MinCr : constant Speed_Type := 0.0;
-   Qdot_MaxCr : constant Speed_Type := 0.0;
+   Qdot_MinCr : constant Speed_Type := Zero_Speed;
+   Qdot_MaxCr : constant Speed_Type := Zero_Speed;
    Q_MinCr    : constant Angle_Type := 0.0;
-   Pdot_MaxCr : constant Speed_Type := 0.0;
-   Qdot_MinDs : constant Speed_Type := 0.0;
-   Qdot_MaxDs : constant Speed_Type := 0.0;
+   Pdot_MaxCr : constant Speed_Type := Zero_Speed;
+   Qdot_MinDs : constant Speed_Type := Zero_Speed;
+   Qdot_MaxDs : constant Speed_Type := Zero_Speed;
    Q_MaxDs    : constant Angle_Type := 0.0;
 
    Escape_Time : constant Time_Type := 0;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/types.ads

+with System.Dim.Mks; use System.Dim; use all type System.Dim.Mks.Mks_Type;
+
 package Types is
 
    ----------------------------------
@@ -65,11 +67,13 @@ package Types is
 
    type Payload_Mass_Type is new Integer range 0 .. 98; -- in kg
 
-   type Distance_Type is new Float; -- type of P, unit and bounds ???
+   subtype Distance_Type is Mks.Length; -- type of P, unit and bounds ???
+
+   subtype Speed_Type is Mks.Speed; -- type of P_Dot and Q_Dot, in angle.s-1, bounds ???
 
-   type Speed_Type is new Float; -- type of P_Dot and Q_Dot, in angle.s-1, bounds ???
+   Zero_Speed : constant Speed_Type := 0.0*Mks.m*Mks.s**(-1);
 
-   type Angle_Type is new Float; -- type of Q, unit and bounds ???
+   subtype Angle_Type is Mks.Angle; -- type of Q, unit and bounds ???
 
    type Rotactor_Type is range 0 .. 9;