Fix ambiguities and typos (first step)

UseCaseData/Layer2_MMS_SW_SPARK/external.ads

@@ -46,7 +46,11 @@ package External with Abstract_State => (State with External => Async_Writers) i
      Volatile_Function,
      Global => State;
 
-   function Payload_Mass return Payload_Mass_Type with
+   function Rotactor_1 return Rotactor_Type with
+     Volatile_Function,
+     Global => State;
+
+   function Rotactor_2 return Rotactor_Type with
      Volatile_Function,
      Global => State;
 

UseCaseData/Layer2_MMS_SW_SPARK/mms-f_el-output.ads

@@ -6,8 +6,6 @@ package MMS.F_EL.Output is
    -- To MMS --
    ------------
    
-   function Propulsion_Torque return Torque_Type with Global => Output_State;
-   
    function Braking_Torque return Torque_Type with Global => Output_State;
    
    -------------

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

@@ -38,8 +38,11 @@ package MMS.F_PT.F_CM.Input is
    function Bay_Switch return Bay_Switch_Type
      renames MMS.F_PT.Input.Bay_Switch; 
 
-   function Payload_Mass return Payload_Mass_Type
-     renames MMS.F_PT.Input.Payload_Mass;
+   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 USB_Key return USB_Key_Type_Option
      renames MMS.F_PT.Input.USB_Key;

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

@@ -14,11 +14,8 @@ 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 => 
-            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?
+         Rotactor_1 => MMS.F_PT.F_CM.Input.Rotactor_1,
+         Rotactor_2 => MMS.F_PT.F_CM.Input.Rotactor_2));
       
    function CP_Displays return CP_Displays_Type is
      (CP_Displays_Type'
@@ -89,12 +86,11 @@ package MMS.F_PT.F_CM.Output is
    function USB_Key return USB_Key_Type_Option
      renames MMS.F_PT.F_CM.Input.USB_Key; 
    
-   ----------------------
-   -- To F_MM and F_FC --
-   ----------------------
+   function Rotactor_1 return Rotactor_Type
+     renames MMS.F_PT.F_CM.Input.Rotactor_1;
    
-   function Payload_Mass return Payload_Mass_Type
-     renames MMS.F_PT.F_CM.Input.Payload_Mass;
+   function Rotactor_2 return Rotactor_Type
+     renames MMS.F_PT.F_CM.Input.Rotactor_2;
    
    -------------
    -- To F_FC --

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

@@ -19,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_MM.Output.Payload_Mass;
       
    ---------------
    -- From F_MM --

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

@@ -16,8 +16,6 @@ package MMS.F_PT.F_FC.Output is
    
    function Mission_Abort return Boolean with Global => Output_State; -- ??? not listed in F_FC outputs
    
-   function Estimated_Total_Mass return Estimated_Total_Mass_Type with Global => Output_State;
-   
    function Current_Range return Current_Range_Type with Global => Output_State;
    
    function Current_Speed return Current_Speed_Type with Global => Output_State;

UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-behavior.adb

@@ -121,7 +121,8 @@ package body MMS.F_PT.F_MM.Behavior with SPARK_Mode is
       Input_On_OFF_Push_Button := On_OFF_Push_Button;
       Input_Start_Push_Button := Start_Push_Button;
       Input_Mission_Abort := Mission_Abort;
-      Input_Estimated_Total_Mass := Estimated_Total_Mass;
+      Input_Rotactor_1 := Rotactor_1;
+      Input_Rotactor_2 := Rotactor_2;
       Input_Current_Range := Current_Range;
       Input_Current_Speed := Current_Speed;
       Input_Current_Altitude := Current_Altitude;
@@ -140,11 +141,33 @@ package body MMS.F_PT.F_MM.Behavior with SPARK_Mode is
                                (Power_State = ON
                                 and then On_State = INIT
                                 and then Init_State = CANCELLED);
+      Is_Mission_Ready     : constant Boolean :=
+                               (Power_State = On
+                                and then On_State = INIT
+                                and then Init_State = READY);
+      Is_Start_Take_Off    : constant Boolean :=
+                               (Power_State = On
+                                and then On_State = RUNNING
+                                and then Running_State = TAKE_OFF);
+      Is_Start_Landing     : constant Boolean :=
+                               (Power_State = On
+                                and then On_State = RUNNING
+                                and then Running_State = Landing);
+
+      Payload_Mass         : constant Payload_Mass_Type :=
+                               Payload_Mass_Type
+                                 (Input_Rotactor_1 * 10 + Input_Rotactor_2);
    begin
       State.Output_Emergency_Landing := Is_Mission_Aborted;
       State.Output_Mission_Aborted := Is_Mission_Aborted;
-
       State.Output_Mission_Cancelled := Is_Mission_Cancelled;
+      State.Output_Mission_Ready := Is_Mission_Ready;
+      State.Output_Start_Take_Off := Is_Start_Take_Off;
+      State.Output_Start_Landing := Is_Start_Landing;
+      State.Output_Operating_Point := Operating_Point;
+      State.Output_Operating_Mode := Operating_Mode;
+      State.Output_Mission_Range := Mission_Range;
+      State.Output_Payload_Mass := Payload_Mass;
    end Write_Outputs;
 
    -------------------------------------------------------

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

@@ -410,6 +410,24 @@ private
      Global => (Input => (Private_State,
                           Viability_Logic_State,
                           Navigation_Parameter_State));
+   --  First hypothesis: nearest neighbours have the smallest distance with
+   --  Mission_profile
+   --
+   --  Post => Nearest_Neighbours'Result'Length = 2 * Nb_Of_Dimensions
+   --  for all Neighboor_Center of Nearest_Neighbours'Result =>
+   --  for all Center of Appropriate_Tabulating_Function =>
+   --  if Center not in Nearest_Neighboors'Result then
+   --     Distance_With_Neighbour (Neighboor_Center) < Distance_With_Neighbour (Center)
+   --  end if;
+   --
+   --  Second hypothesis: nearest neighbours has the smallest distance in only
+   --  one dimension with the Mission_Profile
+   --
+   --  Post => Nearest_Neighbours'Result'Length = 2 * Nb_Of_Dimensions
+   --  for all Neighboor_Center of Nearest_Neighbours'Result =>
+   --  Appropriate_Tabulating_Function (D, A, S).Distance <= Appropriate_Tabulating_Function (D - 1, A, S).Distance
+   --  and Appropriate_Tabulating_Function (D, A, S).Distance <= Appropriate_Tabulating_Function (D + 1, A, S).Distance
+
 
    function Extract_Energy_Level_For_Neighbours
      (Neighbours : Neighbour_Mission_Profiles) return Energy_Levels
@@ -750,6 +768,7 @@ private
         =>
           Power_State = ON
         and then On_State = COMPLETE,
+        -- ??? Should we verify that the distance
 
         Power_State = ON
         and then On_State = RUNNING

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

@@ -35,12 +35,15 @@ package MMS.F_PT.F_MM.Input is
    function Bay_Switch return Bay_Switch_Type
      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;
-   
    function USB_Key return USB_Key_Type_Option
      renames MMS.F_PT.F_CM.Output.USB_Key;
    
+   function Rotactor_1 return Rotactor_Type
+     renames MMS.F_PT.F_CM.Output.Rotactor_1;
+   
+   function Rotactor_2 return Rotactor_Type
+     renames MMS.F_PT.F_CM.Output.Rotactor_2;
+   
    -----------------------
    -- From F_FC or F_EL --
    -----------------------
@@ -52,9 +55,6 @@ package MMS.F_PT.F_MM.Input is
    -- From F_FC --
    ---------------
 
-   function Estimated_Total_Mass return Estimated_Total_Mass_Type
-     renames MMS.F_PT.F_FC.Output.Estimated_Total_Mass;
-   
    function Current_Range return Current_Range_Type
      renames MMS.F_PT.F_FC.Output.Current_Range;
    

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

@@ -9,14 +9,15 @@ package MMS.F_PT.F_MM.Output is
    function Mission_Cancelled return Boolean with Global => Output_State;
    
    function Mission_Complete return Boolean with Global => Output_State;
+   --  ??? To F_FC too?
    
    function Mission_Aborted return Boolean with Global => Output_State;
    
    function Ready_For_Takeoff return Boolean with Global => Output_State;
    
-   ----------------------
-   -- To F_EL and F_CM --
-   ----------------------
+   ----------------------------
+   -- To F_EL, F_CM and F_FC --
+   ----------------------------
 
    function Emergency_Landing return Boolean with Global => Output_State;
    
@@ -35,4 +36,6 @@ package MMS.F_PT.F_MM.Output is
    function Mission_Range return Current_Range_Type with Global => Output_State;
    -- ??? which distance type
    
+   function Payload_Mass return Payload_Mass_Type with Global => Output_State;
+   
 end MMS.F_PT.F_MM.Output;

UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm-state.ads

@@ -31,8 +31,9 @@ package MMS.F_PT.F_MM.State is
 
    Input_Mission_Abort : Boolean with Part_Of => Input_State;
 
-   Input_Estimated_Total_Mass : Estimated_Total_Mass_Type with
-     Part_Of => Input_State;
+   Input_Rotactor_1 : Rotactor_Type with Part_Of => Input_State;
+
+   Input_Rotactor_2 : Rotactor_Type with Part_Of => Input_State;
 
    Input_Current_Range : Current_Range_Type with Part_Of => Input_State;
 
@@ -112,6 +113,8 @@ package MMS.F_PT.F_MM.State is
 
    Output_Mission_Aborted : Boolean with Part_Of => Output_State;
 
+   Output_Mission_Ready : Boolean with Part_Of => Output_State;
+
    Output_Emergency_Landing : Boolean with Part_Of => Output_State;
 
    Output_Start_Take_Off : Boolean with Part_Of => Output_State;
@@ -124,4 +127,6 @@ package MMS.F_PT.F_MM.State is
 
    Output_Mission_Range : Current_Range_Type with Part_Of => Output_State;
 
+   Output_Payload_Mass : Payload_Mass_Type with Part_Of => Output_State;
+
 end MMS.F_PT.F_MM.State;

UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.adb

@@ -13,7 +13,8 @@ SPARK_Mode,
                        Input_Payload_Mass,
                        Input_USB_Key,
                        Input_Mission_Abort,
-                       Input_Estimated_Total_Mass,
+                       Input_Rotactor_1,
+                       Input_Rotactor_2,
                        Input_Current_Range,
                        Input_Current_Speed,
                        Input_Current_Altitude,
@@ -23,12 +24,14 @@ SPARK_Mode,
                       (Output_Mission_Cancelled,
                        Output_Mission_Complete,
                        Output_Mission_Aborted,
+                       Output_Mission_Ready,
                        Output_Emergency_Landing,
                        Output_Start_Take_Off,
                        Output_Start_Landing,
                        Output_Operating_Point,
                        Output_Operating_Mode,
-                       Output_Mission_Range),
+                       Output_Mission_Range,
+                       Output_Payload_Mass),
                     Private_State =>
                       (Power_State,
                        On_State,

UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-input.ads

@@ -36,8 +36,11 @@ package MMS.F_PT.Input is
    function Bay_Switch return Bay_Switch_Type
      renames MMS.Input.Bay_Switch; 
    
-   function Payload_Mass return Payload_Mass_Type
-     renames MMS.Input.Payload_Mass;
+   function Rotactor_1 return Rotactor_Type
+     renames MMS.Input.Rotactor_1;
+   
+   function Rotactor_2 return Rotactor_Type
+     renames MMS.Input.Rotactor_2;
    
    function USB_Key return USB_Key_Type_Option
      renames MMS.Input.USB_Key;

UseCaseData/Layer2_MMS_SW_SPARK/mms-input.ads

@@ -36,8 +36,11 @@ package MMS.Input is
    function Bay_Switch return Bay_Switch_Type
      renames External.Bay_Switch;
 
-   function Payload_Mass return Payload_Mass_Type
-     renames External.Payload_Mass;
+   function Rotactor_1 return Rotactor_Type
+     renames External.Rotactor_1;
+
+   function Rotactor_2 return Rotactor_Type
+     renames External.Rotactor_2;
 
    function USB_Key return USB_Key_Type_Option
      renames External.USB_Key;