Layer2_MMS_SW_SPARK: continue the specification of F_MM

UseCaseDevelopment/Layer2_MMS_SW_SPARK/external.ads

@@ -6,15 +6,15 @@ package External with Abstract_State => (State with External => Async_Writers) i
    -- Ground-based Mission Preparation and Supervision --
    ------------------------------------------------------
 
-   function Navigation_Parameters return Navigation_Parameters_Type with
+   function Navigation_Parameters return Navigation_Parameters_Type_Option with
      Volatile_Function,
      Global => State;
 
-   function Navigation_Mode return Navigation_Mode_Type with
+   function Navigation_Mode return Navigation_Mode_Type_Option with
      Volatile_Function,
      Global => State;
 
-   function Navigation_Option return Navigation_Option_Type with
+   function Navigation_Option return Navigation_Option_Type_Option with
      Volatile_Function,
      Global => State;
 
@@ -50,7 +50,7 @@ package External with Abstract_State => (State with External => Async_Writers) i
      Volatile_Function,
      Global => State;
 
-   function USB_Key return Navigation_Parameters_Type with
+   function USB_Key return Navigation_Parameters_Type_Option with
      Volatile_Function,
      Global => State;
 

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

@@ -11,13 +11,13 @@ package MMS.F_PT.F_CM.Input is
    -- From F_PT --
    ---------------
 
-   function Navigation_Parameters return Navigation_Parameters_Type 
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
      renames MMS.F_PT.Input.Navigation_Parameters;
 
-   function Navigation_Mode return Navigation_Mode_Type
+   function Navigation_Mode return Navigation_Mode_Type_Option
      renames MMS.F_PT.Input.Navigation_Mode;
    
-   function Navigation_Option return Navigation_Option_Type
+   function Navigation_Option return Navigation_Option_Type_Option
      renames MMS.F_PT.Input.Navigation_Option;
 
    function Go return Boolean
@@ -41,7 +41,7 @@ package MMS.F_PT.F_CM.Input is
    function Payload_Mass return Payload_Mass_Type
      renames MMS.F_PT.Input.Payload_Mass;
    
-   function USB_Key return Navigation_Parameters_Type
+   function USB_Key return Navigation_Parameters_Type_Option
      renames MMS.F_PT.Input.USB_Key;
    
    function P return Distance_Type

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

@@ -59,13 +59,13 @@ package MMS.F_PT.F_CM.Output is
    -- To F_MM --
    -------------
 
-   function Navigation_Parameters return Navigation_Parameters_Type 
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
      renames MMS.F_PT.F_CM.Input.Navigation_Parameters;
 
-   function Navigation_Mode return Navigation_Mode_Type
+   function Navigation_Mode return Navigation_Mode_Type_Option
      renames MMS.F_PT.F_CM.Input.Navigation_Mode;
    
-   function Navigation_Option return Navigation_Option_Type
+   function Navigation_Option return Navigation_Option_Type_Option
      renames MMS.F_PT.F_CM.Input.Navigation_Option;
 
    function Go return Boolean
@@ -86,7 +86,7 @@ package MMS.F_PT.F_CM.Output is
    function Bay_Switch return Bay_Switch_Type
      renames MMS.F_PT.F_CM.Input.Bay_Switch;
    
-   function USB_Key return Navigation_Parameters_Type
+   function USB_Key return Navigation_Parameters_Type_Option
      renames MMS.F_PT.F_CM.Input.USB_Key; 
 
    ----------------------

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

@@ -35,7 +35,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    -- Estimated Values --
    ----------------------
 
-   function Q_Dot return Angular_Speed_Type with Global => Private_State;
+   function Q_Dot return Speed_Type with Global => Private_State;
 
    ------------
    -- States --

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

@@ -47,15 +47,15 @@ package MMS.F_PT.F_FC.Data with SPARK_Mode is
 
    --  From 6.7.3.2
 
-   Qdot_MinCl : constant Angular_Speed_Type; --  in angle.s-1
-   Qdot_MaxCl : constant Angular_Speed_Type; --  in angle.s-1
+   Qdot_MinCl : constant Speed_Type; --  in angle.s-1
+   Qdot_MaxCl : constant Speed_Type; --  in angle.s-1
    Q_MaxCl    : constant Angle_Type; --  in angle
-   Qdot_MinCr : constant Angular_Speed_Type; --  in angle.s-1
-   Qdot_MaxCr : constant Angular_Speed_Type; --  in angle.s-1
+   Qdot_MinCr : constant Speed_Type; --  in angle.s-1
+   Qdot_MaxCr : constant Speed_Type; --  in angle.s-1
    Q_MinCr    : constant Angle_Type; --  in angle
-   Pdot_MaxCr : constant Speed_Type; --  in km/h
-   Qdot_MinDs : constant Angular_Speed_Type; --  in angle.s-1
-   Qdot_MaxDs : constant Angular_Speed_Type; --  in angle.s-1
+   Pdot_MaxCr : constant Speed_Type; --  in angle.s-1
+   Qdot_MinDs : constant Speed_Type; --  in angle.s-1
+   Qdot_MaxDs : constant Speed_Type; --  in angle.s-1
    Q_MaxDs    : constant Angle_Type; --  in angle
 
    Escape_Time : constant Time_Type; --  in s
@@ -77,28 +77,28 @@ private
    Flight_Domain_Mesh : constant Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100) :=
      (others => (others => <>));
 
-   Qdot_MinCl : constant Angular_Speed_Type := 0.0; --  in angle.s-1
-   Qdot_MaxCl : constant Angular_Speed_Type := 0.0; --  in angle.s-1
-   Q_MaxCl    : constant Angle_Type := 0.0; --  in angle
-   Qdot_MinCr : constant Angular_Speed_Type := 0.0; --  in angle.s-1
-   Qdot_MaxCr : constant Angular_Speed_Type := 0.0; --  in angle.s-1
-   Q_MinCr    : constant Angle_Type := 0.0; --  in angle
-   Pdot_MaxCr : constant Speed_Type := 0.0; --  in km/h
-   Qdot_MinDs : constant Angular_Speed_Type := 0.0; --  in angle.s-1
-   Qdot_MaxDs : constant Angular_Speed_Type := 0.0; --  in angle.s-1
-   Q_MaxDs    : constant Angle_Type := 0.0; --  in angle
+   Qdot_MinCl : constant Speed_Type := 0.0;
+   Qdot_MaxCl : constant Speed_Type := 0.0;
+   Q_MaxCl    : constant Angle_Type := 0.0;
+   Qdot_MinCr : constant Speed_Type := 0.0;
+   Qdot_MaxCr : constant Speed_Type := 0.0;
+   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;
+   Q_MaxDs    : constant Angle_Type := 0.0;
 
-   Escape_Time : constant Time_Type := 0; --  in s
+   Escape_Time : constant Time_Type := 0;
 
    --  From 6.7.4
 
-   Commutation_Duration : constant Time_Type := 0; --  in s
-   Hazard_Duration      : constant Time_Type := 0; --  in s
+   Commutation_Duration : constant Time_Type := 0;
+   Hazard_Duration      : constant Time_Type := 0;
 
-   Recovery_Speed : constant Integer := 0; --  in m.s
+   Recovery_Speed : constant Integer := 0;
 
-   J0 : constant Integer := 0; --  in kg.m2
-   L  : constant Integer := 0; --  in m
-   M0 : constant Integer := 0; --  in kg
+   J0 : constant Integer := 0;
+   L  : constant Integer := 0;
+   M0 : constant Integer := 0;
 
 end MMS.F_PT.F_FC.Data;

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

@@ -19,14 +19,14 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
    function Initial_Energy_Check_Succeeded return Boolean is
      (Power_State = ON
       and then On_State = INIT
-      and then Energy_Compatible_With_Mission);
+      and then Initial_Energy_Compatible_With_Mission);
 
    function In_Flight_Energy_Check_Failed return Boolean is
      (Power_State = ON
       and then On_State = RUNNING
       and then Running_State = FLIGHT
       and then Current_Flight_Phase = CRUISE
-      and then not Energy_Compatible_With_Mission);
+      and then not In_Flight_Energy_Compatible_With_Mission);
 
    function Mission_Cancelled return Boolean is
       (Power_State = On

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

@@ -10,6 +10,9 @@
 
 with Types; use Types;
 with External;
+with MMS.F_PT.F_MM.Data;
+private with MMS.F_PT.F_MM.State;
+with MMS.F_PT.Data;
 
 package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    pragma Unevaluated_Use_Of_Old (Allow);
@@ -18,36 +21,60 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    -- Inputs --
    ------------
 
-   function Navigation_Mode_From_CP return Navigation_Mode_Type with
-     Global => Private_State;
+   function Power_On return Boolean;
+
+   function Payload_Bay_Closed return Boolean with
+     Pre => Power_State = ON
+     and then On_State = INIT;
+
+   function Payload_Mass_Given return Boolean with
+     Pre => Power_State = ON;
+   --  ???  Should we assume that Payload_Mass is always given after takeoff?
+
+   function Payload_Mass return Payload_Mass_Type with
+     Pre => Power_State = ON
+     and then Payload_Mass_Given;
+
+   function Navigation_Mode_From_CP return Navigation_Mode_Type;
+
+   function Navigation_Mode_From_GS_Received return Boolean;
 
    function Navigation_Mode_From_GS return Navigation_Mode_Type with
-     Global => Private_State;
+     Pre => Navigation_Mode_From_GS_Received;
 
-   function Operating_Point_From_GS_Received return Boolean with
-     Global => Private_State;
+   function Operating_Mode_From_CP return Navigation_Option_Type;
 
-   function Operating_Point_From_GS return Operating_Point_Type with
-     Global => Private_State;
+   function Operating_Mode_From_GS_Received return Boolean;
 
-   function USB_Key_Present return Boolean with
-     Global => Private_State;
+   function Operating_Mode_From_GS return Navigation_Option_Type with
+     Pre => Operating_Mode_From_GS_Received;
 
-   function Operating_Point_From_USB_Key return Operating_Point_Type with
-     Global => Private_State;
+   function Navigation_Parameters_From_GS_Received return Boolean;
 
-   function Current_Range return Current_Range_Type with
-     Global => Private_State;
+   function Navigation_Parameters_From_GS return Navigation_Parameters_Type with
+     Pre => Navigation_Parameters_From_GS_Received;
 
-   function Current_Speed return Current_Speed_Type with
-     Global => Private_State;
+   function USB_Key_Present return Boolean;
 
-   function Current_Altitude return Current_Altitude_Type with
-     Global => Private_State;
+   function Navigation_Parameters_From_USB_Key return Navigation_Parameters_Type
+   with
+     Pre => USB_Key_Present;
+
+   function Mission_Abort_Received return Boolean with
+     Pre => Power_State = ON;
+
+   function Start_Or_Go_Received return Boolean with
+     Pre => Power_State = ON
+     and then On_State = INIT;
+
+   function Current_Range return Current_Range_Type;
+
+   function Current_Speed return Current_Speed_Type;
+
+   function Current_Altitude return Current_Altitude_Type;
 
    function Current_Flight_Phase return Flight_Phase_Type with
-     Global => Private_State,
-     Pre    => Power_State = ON
+     Pre => Power_State = ON
      and then On_State = RUNNING
      and then Running_State = FLIGHT;
 
@@ -73,39 +100,11 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      Pre => Power_State = ON
      and then On_State = RUNNING;
 
-   function Navigation_Mode return Navigation_Mode_Type
-   is (if Navigation_Mode_From_CP = A then A
-       else Navigation_Mode_From_GS)
-   with
-     Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State in INIT | RUNNING;
-
-   function Operating_Mode return Navigation_Option_Type with
-     Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State = RUNNING
-     and then Navigation_Mode = RP;
-
-   -----------------------------------------
-   -- Guards of the automaton in Figure 3 --
-   -----------------------------------------
+   -----------------------------
+   -- Properties and Entities --
+   -----------------------------
 
-   function Power_On return Boolean with
-     Global => Private_State;
-
-   function Power_Off return Boolean with
-     Global => Private_State,
-     Post => Power_Off'Result = not Power_On;
-
-   function Mission_Abort_Received return Boolean with
-     Global => Private_State,
-     Pre => Power_State = ON;
-
-   function Start_Or_Go_Received return Boolean with
-     Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State = INIT;
+   function Power_Off return Boolean is (not Power_On);
 
    function Take_Off_Over return Boolean with
      Global => Private_State,
@@ -117,68 +116,86 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      Global => Private_State,
      Pre => Power_State = ON
      and then On_State = RUNNING
-     and then Running_State = FLIGHT
-     and then Current_Flight_Phase = DESCENT;
+     and then Running_State = FLIGHT;
 
    function Landed return Boolean is
      (Current_Speed = 0 and Current_Altitude = 0)
    with
-     Global => Private_State,
      Pre => Power_State = ON
      and then On_State = RUNNING
      and then Running_State = LANDING;
 
-   ----------------
-   -- Properties --
-   ----------------
+   function Mission_Range_From_Navigation_Parameters
+     return Current_Range_Type;
+--   with Pre => Mission_Parameters_Defined;
+   --  Fetch distance from State.Navigation_Parameters and do the appropriate
+   --  conversion.
+
+   function Operating_Point_From_Navigation_Parameters
+     return Operating_Point_Type;
+--   with Pre => Mission_Parameters_Defined;
+   --  Fetch altitude and speed from State.Navigation_Parameters and do the
+   --  appropriate conversions.
 
-   function Energy_Compatible_With_Mission return Boolean with
+   function Navigation_Mode return Navigation_Mode_Type with
      Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State in INIT | RUNNING
-     and then (if On_State = RUNNING then
-                 Running_State = FLIGHT and then Current_Flight_Phase = CRUISE);
+     Pre    => Power_State = ON
+     and then On_State in INIT | RUNNING;
 
-   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
+   function Operating_Mode return Navigation_Option_Type with
      Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State = INIT;
+     Pre    => Power_State = ON
+     and then On_State = RUNNING
+     and then Navigation_Mode = RP;
 
-   function Payload_Bay_Closed return Boolean with
+   function Initial_Energy_Compatible_With_Mission return Boolean with
      Global => Private_State,
      Pre => Power_State = ON
      and then On_State = INIT;
+  --   and then Mission_Parameters_Defined
+  --   and then Payload_Mass_Given;
 
-   function Mission_Cancellation_Signaled return Boolean with
-     Global => Private_State;
+   function In_Flight_Energy_Compatible_With_Mission return Boolean with
+     Global => Private_State,
+     Pre => Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = FLIGHT;
+ --    and then Current_Flight_Phase = CRUISE;
 
-   -------------
-   -- Outputs --
-   -------------
+   function Mission_Parameters_Defined return Boolean is
+     (USB_Key_Present
+      or else (Navigation_Mode_From_CP = RP
+               and then Navigation_Parameters_From_GS_Received));
 
    function Ready_For_Takeoff return Boolean is
      (Payload_Bay_Closed
+      and then Payload_Mass_Given
       and then Mission_Parameters_Defined
-      and then Energy_Compatible_With_Mission)
+      and then Initial_Energy_Compatible_With_Mission)
    with
-   Global => Private_State,
+   Global => (Private_State, Input_State),
    Pre  => Power_State = ON
      and then On_State = INIT;
+   --  ??? Should be sent to F_CM but the corresponding flag is disabled for
+   --  now...
 
-   function Emergency_Landing return Boolean with
+   function Emergency_Landing return Boolean is
+     (On_State = CANCELLED)
+   with
      Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State = CANCELLED;
+     Pre    => Power_State = ON;
+   --  ??? Should be ABORTED maybe?
 
    function Mission_Range return Current_Range_Type with
      Global => Private_State;
+   --  Pre => Mission_Parameters_Defined;
 
    function Operating_Point return Operating_Point_Type with
      Global => Private_State;
+   --  Pre => Mission_Parameters_Defined;
+
+   function Mission_Cancellation_Signaled return Boolean with
+     Global => Private_State;
 
    ---------------------------------------
    -- Behavioural Specification of F_MM --
@@ -186,7 +203,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
    procedure Read_Inputs with
    --  Read values of inputs once and for all and update the current state
-     Global => (In_Out => Private_State,
+     Global => (Output => Input_State,
                 Input  => External.State);
 
    procedure Write_Outputs with
@@ -198,7 +215,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    -- Do:
    --  - Compute the new state of the automaton
 
-     Global         => (In_Out => Private_State),
+     Global         => (In_Out => Private_State, Input => Input_State),
      Post           =>
 
        --  RP mode enables modification of range parameter before take-off.
@@ -206,7 +223,9 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
        (if not (Power_State'Old = ON
                 and then On_State'Old = INIT
                 and then Navigation_Mode'Old = RP)
-        then Mission_Range = Mission_Range'Old)
+        then Mission_Range = Mission_Range'Old
+        elsif Mission_Parameters_Defined
+        then Mission_Range = Mission_Range_From_Navigation_Parameters)
 
        --  RP mode enables modification of altitude and speed parameters at any
        --  time (but not at landing, it is frozen...).
@@ -308,7 +327,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
         and then Current_Flight_Phase = CRUISE
         and then Power_On
         and then not Mission_Abort_Received
-        and then not Energy_Compatible_With_Mission
+        and then not In_Flight_Energy_Compatible_With_Mission
         =>
           Power_State = ON
         and then On_State = CANCELLED
@@ -333,7 +352,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
         and then Power_On
         and then not Mission_Abort_Received
         and then
-          (if Current_Flight_Phase = CRUISE then Energy_Compatible_With_Mission)
+          (if Current_Flight_Phase = CRUISE then
+                 In_Flight_Energy_Compatible_With_Mission)
         and then
           (if Current_Flight_Phase = DESCENT then not Descent_Over)
         =>
@@ -371,23 +391,243 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
 private
 
+   ----------------------------
+   --  Definitions of Inputs --
+   ----------------------------
+
+   function Power_On return Boolean is
+     (State.Input_On_OFF_Push_Button);
+
+   function Payload_Bay_Closed return Boolean is
+     (State.Input_Bay_Switch = CLOSED);
+
+   function Payload_Mass_Given return Boolean is
+     (State.Input_Payload_Mass /= 99);
+
+   function Payload_Mass return Payload_Mass_Type is
+     (State.Input_Payload_Mass);
+
+   function Navigation_Mode_From_CP return Navigation_Mode_Type is
+     (State.Input_Mode_Switch);
+
+   function Navigation_Mode_From_GS_Received return Boolean is
+     (State.Input_Navigation_Mode.Present);
+
+   function Navigation_Mode_From_GS return Navigation_Mode_Type is
+     (State.Input_Navigation_Mode.Content);
+
+   function Operating_Mode_From_CP return Navigation_Option_Type is
+     (ALTITUDE); --  ??? what is the default operating mode in A mode?
+
+   function Operating_Mode_From_GS_Received return Boolean is
+     (State.Input_Navigation_Option.Present);
+
+   function Operating_Mode_From_GS return Navigation_Option_Type is
+     (State.Input_Navigation_Option.Content);
+
+   function Navigation_Parameters_From_GS_Received return Boolean is
+     (State.Input_Navigation_Parameters.Present);
+
+   function Navigation_Parameters_From_GS return Navigation_Parameters_Type is
+     (State.Input_Navigation_Parameters.Content);
+
+   function USB_Key_Present return Boolean is
+     (State.Input_USB_Key.Present);
+
+   function Navigation_Parameters_From_USB_Key return Navigation_Parameters_Type is
+     (State.Input_USB_Key.Content);
+
+   function Mission_Abort_Received return Boolean is
+     (State.Input_Mission_Abort);
+
+   function Start_Or_Go_Received return Boolean is
+     (State.Input_Go or State.Input_Start_Push_Button);
+
+   function Current_Range return Current_Range_Type is
+     (State.Input_Current_Range);
+
+   function Current_Speed return Current_Speed_Type is
+     (State.Input_Current_Speed);
+
+   function Current_Altitude return Current_Altitude_Type is
+     (State.Input_Current_Altitude);
+
+   function Current_Flight_Phase return Flight_Phase_Type is
+     (State.Input_Current_Flight_Phase);
+
+   -------------------
+   -- Tasks of F_MM --
+   -------------------
+
+   function Navigation_Parameters return Navigation_Parameters_Type is
+     (State.Navigation_Parameters);
+ --  with Pre => Mission_Parameters_Defined;
+
+   procedure Management_Of_Navigation_Mode with
+   --  Compute the value of Navigation_Mode / Options / Parameters (see 6.9.4)
+
+     Post   => Navigation_Mode =
+
+     --  In case of conflict on the navigation mode, CP prevails over GS.
+
+     (if Navigation_Mode_From_CP = A
+      or else not Navigation_Mode_From_GS_Received
+      then Navigation_Mode_From_CP
+
+     --  If CP states the mode to RC then GS can choose the navigation mode.
+
+      else Navigation_Mode_From_GS)
+
+     and then Operating_Mode =
+       (if Navigation_Mode = A
+        or else not Operating_Mode_From_GS_Received
+        then Operating_Mode_From_CP
+        else Operating_Mode_From_GS)
+
+     and then
+         (if Mission_Parameters_Defined then
+            Navigation_Parameters =
+              (if Navigation_Mode = A
+               or else not Navigation_Parameters_From_GS_Received
+               then Navigation_Parameters_From_USB_Key
+               else Navigation_Parameters_From_GS));
+
    procedure Operating_Point_Update_Management with
    --  Compute the value of Operating_Point
 
-     Global => (In_Out => Private_State),
-     Contract_Cases =>
-       (Navigation_Mode_From_CP = A
-        or else not Operating_Point_From_GS_Received
-        =>
-          Operating_Point = Operating_Point_From_USB_Key,
+     Pre    =>
+       Mission_Parameters_Defined
+       and then Power_State = ON
+       and then On_State in INIT | RUNNING,
 
-        Navigation_Mode_From_CP = RP
-        and then Operating_Point_From_GS_Received
-        =>
-          (if Power_State = ON
+     --  F_MM ensures freeze of the operating point once landing is activated.
+
+     Post   =>
+         (if Power_State = ON
            and then On_State = RUNNING
            and then Running_State = LANDING
-           then Operating_Point = Operating_Point'Old
-           else Operating_Point = Operating_Point_From_GS));
+          then Operating_Point = Operating_Point'Old
+          else Operating_Point = Operating_Point_From_Navigation_Parameters);
+
+   ------------------------------
+   --  Mission_Viability_Logic --
+   ------------------------------
+
+   function Mission_Profile return Mission_Profile_Type with
+   --  Assemble the mission profile
+
+     Pre  => Power_State = ON,
+   --  and then Mission_Parameters_Defined
+  --   and then Payload_Mass_Given,
+     Post => Mission_Profile'Result =
+        (Mass     => Payload_Mass,
+         Distance => Current_Range,
+         Altitude => Current_Altitude,
+         Speed    => Current_Speed);
+
+   function Appropriate_Tabulating_Function return Viability_Domain_Mesh_Type
+   --  Select the tabulated function corresponding to the navigation mode
+
+   with
+     Pre  => Power_State = ON
+     and then On_State in INIT | RUNNING,
+     Post => Appropriate_Tabulating_Function'Result =
+         (if On_State = INIT and then Navigation_Mode = A
+          then Data.Amode_Initial_Domain_Mesh
+          elsif On_State = INIT and then Navigation_Mode = RP
+          then Data.RPmode_Initial_Domain_Mesh
+          elsif Navigation_Mode = A
+          then Data.Amode_Cruise_Domain_Mesh
+          else Data.RPmode_Cruise_Domain_Mesh);
+
+   function Distance_With_Neighbour
+     (Neighbour : Mission_Profile_Type) return Mission_Profile_Distance_Type
+   with
+     Pre => Power_State = ON
+     and then On_State in INIT | RUNNING;
+   --  and then Mission_Parameters_Defined
+   --  and then Payload_Mass_Given;
+   --  Compute the distance between Mission_Profile and its Neighbour.
+
+   function Nearest_Neighbours return Neighbour_Mission_Profile_Array_Type with
+   --  Compute the nearest neighbous of Mission_Profile in
+   --  Appropriate_Tabulating_Function, and the distance of Mission_Profile to
+   --  its nearest neignbours.
+
+     Pre  => Power_State = ON
+     and then On_State in INIT | RUNNING,
+  --   and then Mission_Parameters_Defined
+  --   and then Payload_Mass_Given,
+     Post =>
+       (for all Neighbour_Center of Nearest_Neighbours'Result =>
+          Neighbour_Center.Mission_Profile.M in
+            MMS.F_PT.Data.Payload_Mass_Grid'Range
+        and then Neighbour_Center.Mission_Profile.D in
+          Appropriate_Tabulating_Function'Range (1)
+        and then Neighbour_Center.Mission_Profile.A in
+          Appropriate_Tabulating_Function'Range (2)
+        and then Neighbour_Center.Mission_Profile.S in
+          Appropriate_Tabulating_Function'Range (3)
+        and then Neighbour_Center.Distance =
+          Distance_With_Neighbour
+            (Mission_Profile_Type'
+               (Mass     =>
+                   MMS.F_PT.Data.Payload_Mass_Grid
+                     (Neighbour_Center.Mission_Profile.M),
+                Distance =>
+                  Appropriate_Tabulating_Function
+                    (Neighbour_Center.Mission_Profile.D,
+                     Neighbour_Center.Mission_Profile.A,
+                     Neighbour_Center.Mission_Profile.S).Distance,
+                Altitude =>
+                  Appropriate_Tabulating_Function
+                    (Neighbour_Center.Mission_Profile.D,
+                     Neighbour_Center.Mission_Profile.A,
+                     Neighbour_Center.Mission_Profile.S).Altitude,
+                Speed    =>
+                  Appropriate_Tabulating_Function
+                    (Neighbour_Center.Mission_Profile.D,
+                     Neighbour_Center.Mission_Profile.A,
+                     Neighbour_Center.Mission_Profile.S).Speed)));
+
+   function Extract_Energy_Level_For_Neighbour
+     (Neighbour : Center_Mission_Profile_Type) return Energy_Level_Type
+   --  Extract energy level for the neighbour.
+
+   with
+     Pre  => Power_State = ON
+     and then On_State in INIT | RUNNING,
+     Post => Extract_Energy_Level_For_Neighbour'Result =
+         (if On_State = INIT and then Navigation_Mode = A
+          then Data.Viability_Amode_Initial (M => Neighbour.M,
+                                             D => Neighbour.D,
+                                             A => Neighbour.A,
+                                             S => Neighbour.S)
+          elsif On_State = INIT and then Navigation_Mode = RP
+          then Data.Viability_RPmode_Initial (M => Neighbour.M,
+                                              D => Neighbour.D,
+                                              A => Neighbour.A,
+                                              S => Neighbour.S)
+          elsif Navigation_Mode = A
+          then Data.Viability_Amode_Cruise (M => Neighbour.M,
+                                            D => Neighbour.D,
+                                            A => Neighbour.A,
+                                            S => Neighbour.S)
+          else Data.Viability_RPmode_Cruise (M => Neighbour.M,
+                                             D => Neighbour.D,
+                                             A => Neighbour.A,
+                                             S => Neighbour.S));
+
+   procedure Mission_Viability_Logic with
+   --  Compute the value of Initial_Energy_Compatible_With_Mission and
+   --  In_Flight_Energy_Compatible_With_Mission.
+
+     Pre => Power_State = ON
+     and then On_State in INIT | RUNNING
+     and then (if On_State = INIT
+               then Mission_Parameters_Defined
+                 and then Payload_Mass_Given
+               else Running_State = FLIGHT
+                 and then Current_Flight_Phase = CRUISE);
 
 end MMS.F_PT.F_MM.Behavior;

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

@@ -11,13 +11,13 @@ package MMS.F_PT.F_MM.Input is
    -- From F_CM --
    ---------------
 
-   function Navigation_Parameters return Navigation_Parameters_Type 
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
      renames MMS.F_PT.F_CM.Output.Navigation_Parameters;
 
-   function Navigation_Mode return Navigation_Mode_Type
+   function Navigation_Mode return Navigation_Mode_Type_Option
      renames MMS.F_PT.F_CM.Output.Navigation_Mode;
    
-   function Navigation_Option return Navigation_Option_Type
+   function Navigation_Option return Navigation_Option_Type_Option
      renames MMS.F_PT.F_CM.Output.Navigation_Option;
 
    function Go return Boolean
@@ -38,7 +38,7 @@ package MMS.F_PT.F_MM.Input is
    function Payload_Mass return Payload_Mass_Type
      renames MMS.F_PT.F_CM.Output.Payload_Mass;
    
-   function USB_Key return Navigation_Parameters_Type
+   function USB_Key return Navigation_Parameters_Type_Option
      renames MMS.F_PT.F_CM.Output.USB_Key;
    
    -----------------------

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

 private
 package MMS.F_PT.F_MM.State is
-   V : Integer with Part_Of => Private_State;
+
+   -----------------
+   -- Input_State --
+   -----------------
+
+   Input_Navigation_Parameters : Navigation_Parameters_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Navigation_Mode : Navigation_Mode_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Navigation_Option : Navigation_Option_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Go : Boolean with Part_Of => Input_State;
+
+   Input_On_OFF_Push_Button : Boolean with Part_Of => Input_State;
+
+   Input_Start_Push_Button : Boolean with Part_Of => Input_State;
+
+   Input_Mode_Switch : Navigation_Mode_Type with Part_Of => Input_State;
+
+   Input_Bay_Switch : Bay_Switch_Type with Part_Of => Input_State;
+
+   Input_Payload_Mass : Payload_Mass_Type with Part_Of => Input_State;
+
+   Input_USB_Key : Navigation_Parameters_Type_Option with
+     Part_Of => Input_State;
+
+   Input_Mission_Abort : Boolean with Part_Of => Input_State;
+
+   Input_Estimated_Total_Mass : Estimated_Total_Mass_Type with
+     Part_Of => Input_State;
+
+   Input_Current_Range : Current_Range_Type with Part_Of => Input_State;
+
+   Input_Current_Speed : Current_Speed_Type with Part_Of => Input_State;
+
+   Input_Current_Altitude : Current_Altitude_Type with Part_Of => Input_State;
+
+   Input_Current_Flight_Phase : Flight_Phase_Type with Part_Of => Input_State;
+
+   Input_Energy_Level : Energy_Level_Type with Part_Of => Input_State;
+
+   -------------------
+   -- Private_State --
+   -------------------
+
+   Navigation_Mode : Navigation_Mode_Type with Part_Of => Private_State;
+
+   Operating_Mode : Navigation_Option_Type with Part_Of => Private_State;
+
+   Navigation_Parameters : Navigation_Parameters_Type with
+     Part_Of => Private_State;
+
+   Operating_Point : Operating_Point_Type with Part_Of => Private_State;
+
+   Initial_Energy_Compatible_With_Mission : Boolean with
+     Part_Of => Private_State;
+
+   In_Flight_Energy_Compatible_With_Mission : Boolean with
+     Part_Of => Private_State;
+
+   Descent_Over : Boolean with Part_Of => Private_State;
+
+   ------------------
+   -- Output_State --
+   ------------------
+
+   Output_Mission_Cancelled : Boolean with Part_Of => Output_State;
+
+   Output_Mission_Complete : Boolean with Part_Of => Output_State;
+
+   Output_Mission_Aborted : 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;
+
+   Output_Start_Landing : Boolean with Part_Of => Output_State;
+
+   Output_Operating_Point : Operating_Point_Type with Part_Of => Output_State;
+
+   Output_Operating_Mode : Navigation_Option_Type with Part_Of => Output_State;
+
+   Output_Mission_Range : Current_Range_Type with Part_Of => Output_State;
+
 end MMS.F_PT.F_MM.State;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.adb

+with MMS.F_PT.F_MM.State; use MMS.F_PT.F_MM.State;
+package body MMS.F_PT.F_MM with
+  SPARK_Mode,
+  Refined_State => (Input_State   => (Input_Navigation_Parameters,
+                                      Input_Navigation_Mode,
+                                      Input_Navigation_Option,
+                                      Input_Go,
+                                      Input_On_OFF_Push_Button,
+                                      Input_Start_Push_Button,
+                                      Input_Mode_Switch,
+                                      Input_Bay_Switch,
+                                      Input_Payload_Mass,
+                                      Input_USB_Key,
+                                      Input_Mission_Abort,
+                                      Input_Estimated_Total_Mass,
+                                      Input_Current_Range,
+                                      Input_Current_Speed,
+                                      Input_Current_Altitude,
+                                      Input_Current_Flight_Phase,
+                                      Input_Energy_Level),
+                    Output_State  => (Output_Mission_Cancelled,
+                                      Output_Mission_Complete,
+                                      Output_Mission_Aborted,
+                                      Output_Emergency_Landing,
+                                      Output_Start_Take_Off,
+                                      Output_Start_Landing,
+                                      Output_Operating_Point,
+                                      Output_Operating_Mode,
+                                      Output_Mission_Range),
+                    Private_State => (Navigation_Mode,
+                                      Operating_Mode,
+                                      Navigation_Parameters,
+                                      Operating_Point,
+                                      Initial_Energy_Compatible_With_Mission,
+                                      In_Flight_Energy_Compatible_With_Mission,
+                                      Descent_Over))
+is
+end MMS.F_PT.F_MM;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.ads

 with Types; use Types;
 
-package MMS.F_PT.F_MM with Abstract_State => (Private_State, Output_State) is
+package MMS.F_PT.F_MM with
+  SPARK_Mode,
+  Abstract_State => (Private_State, Output_State, Input_State)
+is
    pragma Elaborate_Body (MMS.F_PT.F_MM);
 
    type Viability_Cell_Center_Type is record
@@ -24,4 +27,28 @@ package MMS.F_PT.F_MM with Abstract_State => (Private_State, Output_State) is
    type Glide_Domain_Mesh_Type is array
      (Glide_Altitude_Center range <>) of Current_Altitude_Type;
 
+   type Mission_Profile_Type is record
+      Mass     : Payload_Mass_Type;
+      Distance : Current_Range_Type;
+      Altitude : Current_Altitude_Type;
+      Speed    : Current_Speed_Type;
+   end record;
+
+   type Center_Mission_Profile_Type is record
+      M : Payload_Mass_Center;
+      D : Viability_Distance_Center;
+      A : Viability_Altitude_Center;
+      S : Viability_Speed_Center;
+   end record;
+
+   type Mission_Profile_Distance_Type is new Natural;
+
+   type Neighbour_Mission_Profile_Type is record
+      Mission_Profile : Center_Mission_Profile_Type;
+      Distance        : Mission_Profile_Distance_Type;
+   end record;
+
+   type Neighbour_Mission_Profile_Array_Type is array (Positive range 1 .. 16)
+     of Neighbour_Mission_Profile_Type;
+
 end MMS.F_PT.F_MM;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-input.ads

@@ -9,13 +9,13 @@ package MMS.F_PT.Input is
    -- From MMS --
    --------------
 
-   function Navigation_Parameters return Navigation_Parameters_Type 
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
      renames MMS.Input.Navigation_Parameters;
 
-   function Navigation_Mode return Navigation_Mode_Type
+   function Navigation_Mode return Navigation_Mode_Type_Option
      renames MMS.Input.Navigation_Mode;
    
-   function Navigation_Option return Navigation_Option_Type
+   function Navigation_Option return Navigation_Option_Type_Option
      renames MMS.Input.Navigation_Option;
 
    function Go return Boolean
@@ -39,7 +39,7 @@ package MMS.F_PT.Input is
    function Payload_Mass return Payload_Mass_Type
      renames MMS.Input.Payload_Mass;
    
-   function USB_Key return Navigation_Parameters_Type
+   function USB_Key return Navigation_Parameters_Type_Option
      renames MMS.Input.USB_Key;
    
    function P return Distance_Type

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-input.ads

@@ -7,13 +7,13 @@ package MMS.Input is
    -- Ground-based Mission Preparation and Supervision --
    ------------------------------------------------------
 
-   function Navigation_Parameters return Navigation_Parameters_Type
+   function Navigation_Parameters return Navigation_Parameters_Type_Option
      renames External.Navigation_Parameters;
 
-   function Navigation_Mode return Navigation_Mode_Type
+   function Navigation_Mode return Navigation_Mode_Type_Option
      renames External.Navigation_Mode;
 
-   function Navigation_Option return Navigation_Option_Type
+   function Navigation_Option return Navigation_Option_Type_Option
      renames External.Navigation_Option;
 
    function Go return Boolean renames External.Go;
@@ -39,7 +39,7 @@ package MMS.Input is
    function Payload_Mass return Payload_Mass_Type
      renames External.Payload_Mass;
 
-   function USB_Key return Navigation_Parameters_Type
+   function USB_Key return Navigation_Parameters_Type_Option
      renames External.USB_Key;
 
    -------------------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/types.ads

@@ -16,22 +16,47 @@ package Types is
       Altitude : Altitude_Input_Type;
    end record;
 
+   type Navigation_Parameters_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : Navigation_Parameters_Type;
+      when False =>
+         null;
+      end case;
+   end record;
+
    type Navigation_Mode_Type is (RP, A);
 
+   type Navigation_Mode_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : Navigation_Mode_Type;
+      when False =>
+         null;
+      end case;
+   end record;
+
    type Navigation_Option_Type is (SPEED, ALTITUDE, ENERGY);
 
+   type Navigation_Option_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : Navigation_Option_Type;
+      when False =>
+         null;
+      end case;
+   end record;
+
    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 Speed_Type is new Float; -- type of P_Dot and Q_Dot, in angle.s-1, 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