Beginning of development of F_MM

UseCaseData/Layer2_MMS_SW_SPARK/default.gpr

+project Default is
+
+   package Compiler is
+      for Switches ("Ada") use ("-g", "-O2");
+   end Compiler;
+
+end Default;

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

-with MMS.F_PT.F_EM.Data;
+private with MMS.F_PT.F_EM.Data;
 
 package MMS.F_PT.F_EM.Behavior with SPARK_Mode is
       

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

 with Types; use Types;
 
-package MMS.F_PT.F_EM.Data is
+private
+package MMS.F_PT.F_EM.Data with SPARK_Mode is
 
    ---------------
    -- Constants --
@@ -8,7 +9,9 @@ package MMS.F_PT.F_EM.Data is
    
    --  From 6.8.4
    
-   Primary_Initial_Capacity   : Energy_Level_Type;
-   Secondary_Initial_Capacity : Energy_Level_Type;
+   Primary_Initial_Capacity   : Energy_Level_Type 
+     with Part_Of => Private_State;
+   Secondary_Initial_Capacity : Energy_Level_Type
+     with Part_Of => Private_State; 
 
 end MMS.F_PT.F_EM.Data;

UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_em.ads

 with Types; use Types;
 
-package MMS.F_PT.F_EM with Abstract_State => (Private_State, Output_State) is
+package MMS.F_PT.F_EM with 
+  SPARK_Mode,
+  Abstract_State => 
+  (Private_State,
+   Output_State) 
+is
    pragma Elaborate_Body (MMS.F_PT.F_EM);
-   
 end MMS.F_PT.F_EM;

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

+with MMS.F_PT.F_MM.Input; use MMS.F_PT.F_MM.Input;
+with MMS.F_PT.F_MM.State; use MMS.F_PT.F_MM.State;
+
+package body MMS.F_PT.F_MM.Behavior with SPARK_Mode is
+
+   ----------------------------------------------
+   -- Mission_Range_From_Navigation_Parameters --
+   ----------------------------------------------
+
+   function Mission_Range_From_Navigation_Parameters
+      return Current_Range_Type
+   is
+   begin
+      return Current_Range_Type (State.Navigation_Parameters.Distance) * 1852;
+   end Mission_Range_From_Navigation_Parameters;
+
+   ------------------------------------------------
+   -- Operating_Point_From_Navigation_Parameters --
+   ------------------------------------------------
+
+   function Operating_Point_From_Navigation_Parameters
+      return Operating_Point_Type
+   is
+      Operating_Point_Altitude : Current_Altitude_Type;
+      Operating_Point_Speed    : Current_Speed_Type;
+   begin
+      --  Convert from ft to meters
+      Operating_Point_Altitude := Current_Altitude_Type
+        (Float (State.Navigation_Parameters.Altitude) * 0.3048);
+
+      --  Convert from k.t to km/h
+      Operating_Point_Speed := Current_Speed_Type
+        (Float (State.Navigation_Parameters.Speed) * 1.853);
+
+      return Operating_Point_Type'(Altitude => Operating_Point_Altitude,
+                                   Speed    => Operating_Point_Speed);
+   end Operating_Point_From_Navigation_Parameters;
+
+   --------------------------------------------------
+   -- Current_Altitude_Close_Enough_To_ref_TakeOff --
+   --------------------------------------------------
+
+   function Current_Altitude_Close_Enough_To_ref_TakeOff
+      return Boolean
+   is
+   begin
+      --  ??? Consider that we are close enough when we reach the ref
+      return State.Input_Current_Altitude >= Data.Altitude_Ref_TakeOff;
+   end Current_Altitude_Close_Enough_To_ref_TakeOff;
+
+   -----------------------------------------------
+   -- Current_Speed_Close_Enough_To_ref_TakeOff --
+   -----------------------------------------------
+
+   function Current_Speed_Close_Enough_To_ref_TakeOff
+      return Boolean
+   is
+   begin
+      --  ??? Consider that we are close enough when we reach the ref
+      return State.Input_Current_Speed >= Data.Speed_Ref_TakeOff;
+   end Current_Speed_Close_Enough_To_ref_TakeOff;
+
+   -----------------------
+   -- Emergency_Landing --
+   -----------------------
+
+   function Emergency_Landing
+      return Boolean
+   is
+   begin
+      return State.Output_Emergency_Landing;
+   end Emergency_Landing;
+
+   ------------------------------
+   -- Mission_Aborted_Signaled --
+   ------------------------------
+
+   function Mission_Aborted_Signaled
+      return Boolean
+   is
+   begin
+      return State.Output_Mission_Aborted;
+   end Mission_Aborted_Signaled;
+
+   --------------------------------
+   -- Mission_Cancelled_Signaled --
+   --------------------------------
+
+   function Mission_Cancelled_Signaled
+      return Boolean
+   is
+   begin
+      return State.Output_Mission_Cancelled;
+   end Mission_Cancelled_Signaled;
+
+   -----------------
+   -- Read_Inputs --
+   -----------------
+
+   procedure Read_Inputs
+   is
+   begin
+      if not (Power_State = On and then On_State = RUNNING) then
+         Input_Navigation_Parameters := Navigation_Parameters;
+
+         if Navigation_Mode_From_GS_Received then
+            Input_Navigation_Mode := Navigation_Mode;
+         end if;
+
+         Input_Mode_Switch := Mode_Switch;
+         Input_Navigation_Option := Navigation_Option;
+         Input_Bay_Switch := Bay_Switch;
+         Input_Payload_Mass := Payload_Mass;
+
+         if USB_Key_Present then
+            Input_USB_Key := USB_Key;
+         end if;
+      end if;
+
+      Input_Go := Go;
+      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_Current_Range := Current_Range;
+      Input_Current_Speed := Current_Speed;
+      Input_Current_Altitude := Current_Altitude;
+      Input_Current_Flight_Phase := Current_Flight_Phase;
+      Input_Energy_Level := Energy_Level;
+   end Read_Inputs;
+
+   -------------------
+   -- Write_Outputs --
+   -------------------
+
+   procedure Write_Outputs is
+      Is_Mission_Aborted : constant Boolean :=
+                             (Power_State = On and then On_State = ABORTED);
+      Is_Mission_Cancelled : constant Boolean :=
+                               (Power_State = ON
+                                and then On_State = INIT
+                                and then Init_State = CANCELLED);
+   begin
+      State.Output_Emergency_Landing := Is_Mission_Aborted;
+      State.Output_Mission_Aborted := Is_Mission_Aborted;
+
+      State.Output_Mission_Cancelled := Is_Mission_Cancelled;
+   end Write_Outputs;
+
+   -------------------------------------------------------
+   -- Management_Of_Navigation_Modes_Options_Parameters --
+   -------------------------------------------------------
+
+   procedure Management_Of_Navigation_Modes_Options_Parameters
+   is
+   begin
+      --  Set the navigation mode
+
+      State.Navigation_Mode :=
+        (if Navigation_Mode_From_CP = A
+         or else not Navigation_Mode_From_GS_Received
+         then Navigation_Mode_From_CP
+         else Navigation_Mode_From_GS);
+
+      --  Set the operating mode from parameters
+
+      if Mission_Parameters_Defined then
+         State.Operating_Mode_From_Parameters :=
+           (if Navigation_Mode_From_CP = A
+            or else not Operating_Mode_From_GS_Received
+            then Operating_Mode_From_USB_Key
+            else Operating_Mode_From_GS);
+      end if;
+
+      --  Set the operating mode
+
+      State.Operating_Mode :=
+        (if Operating_Mode_From_Parameters = ENERGY
+         and then Power_State = ON
+         and then On_State = RUNNING
+         and then Running_State = TAKE_OFF
+         then Data.Energy_Mode_Ref_TakeOff
+         else Operating_Mode_From_Parameters);
+
+      --  Set the navigation parameters
+
+      State.Navigation_Parameters :=
+        (if Navigation_Mode_From_CP = A
+         or else not Navigation_Parameters_From_GS_Received
+         then Navigation_Parameters_From_USB_Key
+         else Navigation_Parameters_From_GS);
+   end Management_Of_Navigation_Modes_Options_Parameters;
+
+   ---------------------------------------
+   -- Operating_Point_Update_Management --
+   ---------------------------------------
+
+   procedure Operating_Point_Update_Management is
+   begin
+      -- Set the operating point
+
+      if On_State = RUNNING and then Running_State = TAKE_OFF then
+         State.Operating_Point :=
+           Operating_Point_Type'(Altitude => Data.Altitude_Ref_TakeOff,
+                                 Speed    => Data.Speed_Ref_TakeOff);
+      elsif not (On_State = RUNNING and then Running_State = LANDING) then
+         State.Operating_Point := Operating_Point_From_Navigation_Parameters;
+      end if;
+
+      --  Set the mission range
+
+      if Navigation_Mode = RP and then On_State = INIT Then
+         State.Mission_Range := Mission_Range_From_Navigation_Parameters;
+      end if;
+   end Operating_Point_Update_Management;
+
+   ---------------------
+   -- Mission_Profile --
+   ---------------------
+
+   function Mission_Profile
+      return Mission_Profile_Type
+   is
+   begin
+      return State.Mission_Profile;
+   end Mission_Profile;
+
+   -------------------------------------
+   -- Appropriate_Tabulating_Function --
+   -------------------------------------
+
+   function Appropriate_Tabulating_Function
+      return Viability_Domain_Mesh_Type
+   is
+   begin
+      if On_State = INIT and then Navigation_Mode = A then
+         return Data.Amode_Initial_Domain_Mesh;
+      elsif On_State = INIT and then Navigation_Mode = RP then
+         return Data.RPmode_Initial_Domain_Mesh;
+      elsif Navigation_Mode = A Then
+         return Data.Amode_Cruise_Domain_Mesh;
+      else
+         return Data.RPmode_Cruise_Domain_Mesh;
+      end if;
+   end Appropriate_Tabulating_Function;
+
+   -----------------------------
+   -- Distance_With_Neighbour --
+   -----------------------------
+
+   function Distance_With_Neighbour
+     (Neighbour : Mission_Profile_Type)
+      return Mission_Profile_Distance_Type
+   is
+   begin
+      return Mission_Profile_Distance_Type
+        (abs (Neighbour.Distance - State.Mission_Profile.Distance));
+      --  ??? not clear how the distance is computed
+   end Distance_With_Neighbour;
+
+   ------------------------
+   -- Nearest_Neighbours --
+   ------------------------
+
+   function Nearest_Neighbours
+      return Neighbour_Mission_Profiles
+   is
+      Viability_Domain_Mesh : constant Viability_Domain_Mesh_Type :=
+                                Appropriate_Tabulating_Function;
+      M                     : Payload_Mass_Center :=
+                                F_PT.Data.Payload_Mass_Grid'First;
+      D                     : Viability_Distance_Center :=
+                                Viability_Domain_Mesh'First (1);
+      A                     : Viability_Altitude_Center :=
+                                Viability_Domain_Mesh'First (2);
+      S                     : Viability_Speed_Center :=
+                                Viability_Domain_Mesh'First (3);
+      Neighbours_Arr        : Neighbour_Mission_Profile_Array_Type (1 .. 6);
+      Last                  : Num_Of_Neighbours := 1;
+   begin
+      --  Search for in Payload Mass Grid
+      while M < F_PT.Data.Payload_Mass_Grid'Last
+        and then F_PT.Data.Payload_Mass_Grid (M) < Mission_Profile.Mass
+      loop
+         M := M + 1;
+      end loop;
+
+      --  Search in the Distance dimension
+      while D < Viability_Domain_Mesh'Last (1)
+        and then
+          Viability_Domain_Mesh (D, A, S).Distance < Mission_Profile.Distance
+      loop
+         D := D + 1;
+      end loop;
+
+      --  Search in the Altitude dimension
+      while A < Viability_Domain_Mesh'Last (2)
+        and Then
+          Viability_Domain_Mesh (D, A, S).Altitude < Mission_Profile.Altitude
+      loop
+         A := A + 1;
+      end loop;
+
+      --  Search in the Speed dimension
+      while S < Viability_Domain_Mesh'Last (3)
+        and then
+          Viability_Domain_Mesh (D, A, S).Speed < Mission_Profile.Speed
+      loop
+         S := S + 1;
+      end loop;
+
+      --  Construct the list of neighbours
+
+      declare
+         Min_M : constant Payload_Mass_Center := Payload_Mass_Center'Max
+           (F_PT.Data.Payload_Mass_Grid'First, M - 1);
+         Min_D : constant Viability_Distance_Center :=
+                   Viability_Distance_Center'Max
+                     (Viability_Domain_Mesh'First (1), D);
+         Min_A : constant Viability_Altitude_Center :=
+                   Viability_Altitude_Center'Max
+                     (Viability_Domain_Mesh'First (2), A);
+         Min_S : constant Viability_Speed_Center :=
+                   Viability_Speed_Center'Max
+                     (Viability_Domain_Mesh'First (3), S);
+         Neighbor_MP      : Neighbour_Mission_Profile_Type;
+         Neighbor_Center  : Viability_Cell_Center_Type;
+      begin
+         for M_Idx in Min_M .. M loop
+            for D_Idx in Min_D .. D loop
+               for A_Idx in Min_A .. A loop
+                  for S_Idx in Min_S .. S loop
+
+                     Neighbor_MP.Mission_Profile :=
+                       Center_Mission_Profile_Type'
+                         (M => M_Idx,
+                          D => D_Idx,
+                          A => A_Idx,
+                          S => S_Idx);
+
+                     Neighbor_Center := Viability_Domain_Mesh
+                       (D_Idx, A_Idx, S_Idx);
+
+                     Neighbor_MP.Distance := Distance_With_Neighbour
+                       (Mission_Profile_Type'
+                          (Mass     => F_PT.Data.Payload_Mass_Grid (M_Idx),
+                           Distance => Neighbor_Center.Distance,
+                           Altitude => Neighbor_Center.Altitude,
+                           Speed    => Neighbor_Center.Speed));
+
+                     Neighbours_Arr (Last) := Neighbor_MP;
+
+                     Last := Last + 1;
+                  end loop;
+               end loop;
+            end loop;
+         end loop;
+      end;
+
+      --  ??? How many neighboors should we give? See issue #31
+      return Neighbours_MPs : Neighbour_Mission_Profiles (Last - 1) do
+         for Idx in Neighbours_Arr'First .. Last - 1 loop
+            Neighbours_MPs.Neighbours (Idx) := Neighbours_Arr (Idx);
+         end loop;
+      end return;
+   end Nearest_Neighbours;
+
+   -----------------------------------------
+   -- Extract_Energy_Level_For_Neighbours --
+   -----------------------------------------
+
+   function Extract_Energy_Level_For_Neighbours
+     (Neighbours : Neighbour_Mission_Profiles) return Energy_Levels
+     with SPARK_Mode => Off
+   is
+      type Viability_Table_Function_Type is access
+        function
+          (M : Payload_Mass_Center;
+           D : Viability_Distance_Center;
+           A : Viability_Altitude_Center;
+           S : Viability_Speed_Center) return Energy_Level_Type;
+
+      Neighbours_Profiles : constant Neighbour_Mission_Profile_Array_Type :=
+                              Neighbours.Neighbours;
+      Neighbours_Energy_Levels : Energy_Levels (Neighbours_Profiles'Length);
+      Viability_Table_Function : Viability_Table_Function_Type;
+   begin
+      --  Choose the appropriated viability table function
+      if On_State = INIT and then Navigation_Mode = A then
+         Viability_Table_Function := Data.Viability_Amode_Initial'Access;
+      elsif On_State = INIT and then Navigation_Mode = RP then
+         Viability_Table_Function := Data.Viability_RPmode_Initial'Access;
+      elsif Navigation_Mode = A Then
+         Viability_Table_Function := Data.Viability_Amode_Cruise'Access;
+      else
+         Viability_Table_Function := Data.Viability_RPmode_Cruise'Access;
+      end if;
+
+      for I in Neighbours_Energy_Levels.Neighbours'Range loop
+         Neighbours_Energy_Levels.Neighbours (I) :=
+           Viability_Table_Function
+             (M => Neighbours_Profiles (I).Mission_Profile.M,
+              D => Neighbours_Profiles (I).Mission_Profile.D,
+              A => Neighbours_Profiles (I).Mission_Profile.A,
+              S => Neighbours_Profiles (I).Mission_Profile.S);
+      end loop;
+
+      return Neighbours_Energy_Levels;
+   end Extract_Energy_Level_For_Neighbours;
+
+   -------------------------------
+   -- Interpolated_Energy_Level --
+   -------------------------------
+
+   function Interpolated_Energy_Level
+      return Energy_Level_Type
+   is
+      Neighbours_MPs         : constant Neighbour_Mission_Profiles :=
+                                 Nearest_Neighbours;
+      Neighbours             : constant Neighbour_Mission_Profile_Array_Type :=
+                                 Neighbours_MPs.Neighbours;
+      Neighbours_Energy_Lvls : constant Energy_Level_Array_Type :=
+                                   Extract_Energy_Level_For_Neighbours
+                                   (Neighbours_MPs).Neighbours;
+      Int_Energy_Level       : Float := 0.0;
+      K                      : Num_Of_Neighbours :=
+                                 Neighbours_Energy_Lvls'First;
+   begin
+      --  ??? Not sure about the inverse distance interpolation formula
+      for J in Neighbours'Range loop
+         Int_Energy_Level := Int_Energy_Level +
+           Float (Neighbours_Energy_Lvls (K)) /
+             Float (Neighbours (J).Distance);
+         K := K + 1;
+      end loop;
+
+      return Energy_Level_Type (Int_Energy_Level);
+   end Interpolated_Energy_Level;
+
+   -----------------------------
+   -- Mission_Viability_Logic --
+   -----------------------------
+
+   procedure Mission_Viability_Logic
+   is
+   begin
+      State.Mission_Profile := Mission_Profile_Type'
+        (Mass     => Payload_Mass,
+         Distance => Current_Range,
+         Altitude => Current_Altitude,
+         Speed    => Current_Speed);
+   end Mission_Viability_Logic;
+
+   -------------------------------------
+   -- Initial_Mission_Viability_Logic --
+   -------------------------------------
+
+   procedure Initial_Mission_Viability_Logic
+   is
+      Cur_Energy_Level : constant Energy_Level_Type := Energy_Level;
+      Int_Energy_Level : constant Energy_Level_Type :=
+                           Interpolated_Energy_Level;
+   begin
+      if Navigation_Mode = A then
+         State.Initial_Energy_Compatible_With_Mission :=
+           Int_Energy_Level * 13 / 10 >= Cur_Energy_Level;
+      else
+         State.Initial_Energy_Compatible_With_Mission :=
+           Int_Energy_Level * 11 / 10 >= Cur_Energy_Level;
+      end if;
+   end Initial_Mission_Viability_Logic;
+
+   ---------------------------------------
+   -- In_Flight_Mission_Viability_Logic --
+   ---------------------------------------
+
+   procedure In_Flight_Mission_Viability_Logic
+   is
+   begin
+      --  ??? Include the safety margin here
+      State.In_Flight_Energy_Compatible_With_Mission :=
+        Energy_Level >= Interpolated_Energy_Level;
+   end In_Flight_Mission_Viability_Logic;
+
+   ----------------------------
+   -- Current_Glide_Distance --
+   ----------------------------
+
+   function Current_Glide_Distance
+      return Current_Range_Type
+   is
+      A           : Glide_Altitude_Center :=
+                      Data.Glide_Distance_Domain_Mesh'First;
+      Current_Alt : constant Current_Altitude_Type := Current_Altitude;
+   begin
+      while A <= Data.Glide_Distance_Domain_Mesh'Last
+        and then Data.Glide_Distance_Domain_Mesh (A) < Current_Alt
+      loop
+         A := A + 1;
+      end loop;
+
+      return Data.Glide_Distance (A);
+   end Current_Glide_Distance;
+
+   ---------------------------------
+   -- Mission_Termination_Control --
+   ---------------------------------
+
+   procedure Mission_Termination_Control
+   is
+   begin
+      State.Descent_Over :=
+        Mission_Range - Current_Range < Current_Glide_Distance;
+   end Mission_Termination_Control;
+
+   -------------------
+   -- Update_States --
+   -------------------
+
+   procedure Update_States
+   is
+   begin
+      --  Generated stub: replace with real body!
+      pragma Compile_Time_Warning (Standard.True, "Update_States unimplemented");
+      raise Program_Error with "Unimplemented procedure Update_States";
+   end Update_States;
+
+end MMS.F_PT.F_MM.Behavior;

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

@@ -10,7 +10,7 @@
 
 with Types; use Types;
 with External;
-with MMS.F_PT.F_MM.Data;
+private with MMS.F_PT.F_MM.Data;
 private with MMS.F_PT.F_MM.State;
 with MMS.F_PT.Data;
 
@@ -148,7 +148,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    function Mission_Range_From_Navigation_Parameters
      return Current_Range_Type
    with Global =>
-       (Input => Operating_Point_State, Proof_In => Input_State),
+       (Input => Navigation_Parameter_State, Proof_In => Input_State),
      Pre => Power_On
      and then Mission_Parameters_Defined;
    --  Fetch distance from Navigation_Parameters and do the appropriate
@@ -157,7 +157,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    function Operating_Point_From_Navigation_Parameters
      return Operating_Point_Type
    with Global =>
-       (Input => Operating_Point_State, Proof_In => Input_State),
+       (Input => Navigation_Parameter_State, Proof_In => Input_State),
      Pre => Power_On
      and then Mission_Parameters_Defined;
    --  Fetch altitude and speed from Navigation_Parameters and do the
@@ -191,11 +191,11 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      and then Current_Flight_Phase = CRUISE;
 
    function Current_Altitude_Close_Enough_To_ref_TakeOff return Boolean with
-     Global => Input_State;
+     Global => (Input => (Input_State, Viability_Logic_State));
    --  Return True if Current_Altitude is close enough to Altitude_ref_TakeOff
 
    function Current_Speed_Close_Enough_To_ref_TakeOff return Boolean with
-     Global => Input_State;
+     Global => (Input => (Input_State, Viability_Logic_State));
    --  Return True if Current_Altitude is close enough to Speed_ref_TakeOff
 
    function Take_Off_Over return Boolean is
@@ -233,6 +233,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    function Mission_Cancelled_Signaled return Boolean with
      Global => Output_State;
 
+private
+
    ---------------------------------------
    -- Behavioural Specification of F_MM --
    ---------------------------------------
@@ -292,8 +294,10 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    procedure Management_Of_Navigation_Modes_Options_Parameters with
    --  Compute the value of Navigation_Mode / Options / Parameters (see 6.9.4)
 
-     Global => (Input  => (Input_State, Private_State),
-                Output => Navigation_Parameter_State),
+     Global => (Input  => (Input_State,
+                           Private_State,
+                           Data.Energy_Mode_Ref_TakeOff),
+                In_Out => Navigation_Parameter_State),
      Pre    => Power_On,
      Post   => Navigation_Mode =
 
@@ -342,7 +346,10 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
 
      Global => (Input  =>
-                  (Input_State, Private_State, Navigation_Parameter_State),
+                  (Private_State,
+                   Navigation_Parameter_State,
+                   Data.Altitude_Ref_TakeOff,
+                   Data.Speed_Ref_TakeOff),
                 In_Out => Operating_Point_State),
      Pre    => Power_On
        and then Mission_Parameters_Defined
@@ -389,7 +396,9 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
    function Appropriate_Tabulating_Function return Viability_Domain_Mesh_Type
    with
-     Global => Viability_Logic_State;
+       Global => (Input => (Private_State,
+                            Viability_Logic_State,
+                            Navigation_Parameter_State));
 
    function Distance_With_Neighbour
      (Neighbour : Mission_Profile_Type) return Mission_Profile_Distance_Type
@@ -398,9 +407,12 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    --  Compute the distance between Mission_Profile and its Neighbour.
 
    function Nearest_Neighbours return Neighbour_Mission_Profiles with
-    Global => Viability_Logic_State;
+     Global => (Input => (Private_State,
+                          Viability_Logic_State,
+                          Navigation_Parameter_State));
 
-   function Extract_Energy_Level_For_Neighbours return Energy_Levels
+   function Extract_Energy_Level_For_Neighbours
+     (Neighbours : Neighbour_Mission_Profiles) return Energy_Levels
    with
     Global => Viability_Logic_State;
 
@@ -414,7 +426,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
                   (Input_State,
                    Private_State,
                    Navigation_Parameter_State,
-                   Operating_Point_State),
+                   Operating_Point_State,
+                   MMS.F_PT.Data.Payload_Mass_Grid),
                  In_Out => Viability_Logic_State),
      Pre    => Power_State = ON,
      Post   =>
@@ -476,11 +489,13 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
    --  4. Extracting energy level for the neighbours.
 
-   and then Extract_Energy_Level_For_Neighbours.Size =
+   and then Extract_Energy_Level_For_Neighbours (Nearest_Neighbours).Size =
        Nearest_Neighbours.Size
    and then
-       (for all I in 1 .. Extract_Energy_Level_For_Neighbours.Size =>
-          Extract_Energy_Level_For_Neighbours.Neighbours (I) =
+       (for all I In
+          1 .. Extract_Energy_Level_For_Neighbours (Nearest_Neighbours).Size =>
+              Extract_Energy_Level_For_Neighbours
+          (Nearest_Neighbours).Neighbours (I) =
          (if On_State = INIT and then Navigation_Mode = A
           then Data.Viability_Amode_Initial
             (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
@@ -538,7 +553,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    --  Compute the value of In_Flight_Energy_Compatible_With_Mission. It should
    --  be repeated at a periodic rate of F_Viability.
    --  Set In_Flight_Energy_Compatible_With_Mission to True if Energy_Level is
-   --  at least the Interpolated_Energy_Level plus an enery margin. When
+   --  at least the Interpolated_Energy_Level plus an energy margin. When
    --  EstimatedTotalMass increases, and even more so if it increases quickly,
    --  F_MM applies greater safety margins (see #17).
 
@@ -589,6 +604,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    procedure Update_States with
      Global => (Input  =>
                   (Input_State,
+                   Output_State,
                    Navigation_Parameter_State,
                    Operating_Point_State,
                    Viability_Logic_State,
@@ -753,8 +769,6 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
           Power_State = ON
         and then On_State = On_State'Old);
 
-private
-
    ----------------------------
    --  Definitions of Inputs --
    ----------------------------

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

@@ -2,6 +2,7 @@ with MMS.F_PT.Data;
 
 with Types; use Types;
 
+private
 package MMS.F_PT.F_MM.Data is
 
    --------------------------
@@ -11,7 +12,8 @@ package MMS.F_PT.F_MM.Data is
    --  From 6.6.2.3
 
    Amode_Initial_Domain_Mesh : Viability_Domain_Mesh_Type
-     (1 .. 100, 1 .. 100, 1 .. 100); -- ??? bounds
+     (1 .. 100, 1 .. 100, 1 .. 100)
+     with Part_Of => Viability_Logic_State; -- ??? bounds
 
    function Viability_Amode_Initial
      (M : Payload_Mass_Center;
@@ -24,7 +26,8 @@ package MMS.F_PT.F_MM.Data is
      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
+     (1 .. 100, 1 .. 100, 1 .. 100)
+     with Part_Of => Viability_Logic_State; -- ??? bounds
 
    function Viability_Amode_Cruise
      (M : Payload_Mass_Center;
@@ -37,7 +40,8 @@ package MMS.F_PT.F_MM.Data is
      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
+     (1 .. 100, 1 .. 100, 1 .. 100)
+     with Part_Of => Viability_Logic_State; -- ??? bounds
 
    function Viability_RPmode_Initial
      (M : Payload_Mass_Center;
@@ -50,7 +54,8 @@ package MMS.F_PT.F_MM.Data is
      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
+     (1 .. 100, 1 .. 100, 1 .. 100)
+     with Part_Of => Viability_Logic_State; -- ??? bounds
 
    function Viability_RPmode_Cruise
      (M : Payload_Mass_Center;
@@ -64,7 +69,8 @@ package MMS.F_PT.F_MM.Data is
 
    --  From 6.6.4 Mission termination control
 
-   Glide_Distance_Domain_Mesh : Glide_Domain_Mesh_Type (1 .. 100); -- ??? bounds
+   Glide_Distance_Domain_Mesh : Glide_Domain_Mesh_Type (1 .. 100)
+     with Part_Of => Mission_Termination_State; -- ??? bounds
 
    function Glide_Distance
      (AI : Glide_Altitude_Center) return Current_Range_Type
@@ -72,8 +78,8 @@ package MMS.F_PT.F_MM.Data is
 
    --  Issue #28
 
-   Altitude_ref_TakeOff    : Current_Altitude_Type;
-   Speed_ref_TakeOff       : Current_Speed_Type;
-   Energy_Mode_ref_TakeOff : Speed_Or_Altitude;
+   Altitude_Ref_TakeOff    : Current_Altitude_Type;
+   Speed_Ref_TakeOff       : Current_Speed_Type;
+   Energy_Mode_Ref_TakeOff : Speed_Or_Altitude;
 
 end MMS.F_PT.F_MM.Data;

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

@@ -93,6 +93,9 @@ package MMS.F_PT.F_MM.State is
    In_Flight_Energy_Compatible_With_Mission : Boolean with
      Part_Of => Viability_Logic_State;
 
+   Mission_Profile : Mission_Profile_Type with
+     Part_Of => Viability_Logic_State;
+
    -------------------------------
    -- Mission_Termination_State --
    -------------------------------

UseCaseData/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.adb

@@ -45,7 +45,8 @@ SPARK_Mode,
                        Operating_Point),
                     Viability_Logic_State =>
                       (Initial_Energy_Compatible_With_Mission,
-                       In_Flight_Energy_Compatible_With_Mission),
+                       In_Flight_Energy_Compatible_With_Mission,
+                       Mission_Profile),
                     Mission_Termination_State =>
                       (Descent_Over))
 is

UseCaseData/Layer2_MMS_SW_SPARK/mms-output.ads

@@ -40,8 +40,10 @@ package MMS.Output is
    -- Physical Parameters --
    -------------------------
    
-   function Propulsion_Torque return Torque_Type;
+   function Propulsion_Torque return Torque_Type
+     renames MMS.F_PT.Output.Propulsion_Torque;
    
-   function Braking_Torque return Torque_Type;
+   function Braking_Torque return Torque_Type
+     renames MMS.F_PT.Output.Braking_Torque;
    
 end MMS.Output;

UseCaseData/Layer2_MMS_SW_SPARK/types.ads

@@ -8,7 +8,7 @@ package Types with SPARK_Mode is
 
    type Speed_Input_Type is range 1 .. 250; -- in k.t
 
-   type Altitude_Input_Type is range -500 .. 3000; -- in ft
+   type Altitude_Input_Type is range -500 .. 3_000; -- in ft
 
    type Navigation_Parameters_Type is record
       Distance : Distance_Input_Type;