Layer2_MMS_SW_SPARK: take into account answers for #22

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

@@ -21,6 +21,16 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
      Global => Private_State,
      Pre    => Mission_State = RUNNING;
 
+   function Operating_Point return Operating_Point_Type with
+     Global => Private_State;
+
+   --------------------------
+   -- Properties on Inputs --
+   --------------------------
+
+   function Operating_Point_Changed return Boolean with
+     Global => Private_State;
+
    ----------------------
    -- Estimated Values --
    ----------------------
@@ -36,9 +46,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    function Mission_State return Mission_State_Type with
      Global => Private_State;
 
-   type Phase_State_Type is (CLIMB, CRUISE, DESCENT);
+   function Flight_Phase_State return Flight_Phase_Type with
-
-   function Phase_State return Phase_State_Type with
      Global => Private_State,
      Pre    => Mission_State = RUNNING;
 
@@ -56,7 +64,7 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    --  From 6.7.3.2
 
    function In_Safety_Envelope return Boolean is
-     (case Phase_State is
+     (case Flight_Phase_State is
          when CLIMB   =>
             Q_Dot in MMS.F_PT.F_FC.Data.Qdot_MinCl .. MMS.F_PT.F_FC.Data.Qdot_MaxCl
               and Q < MMS.F_PT.F_FC.Data.Q_MaxCl,
@@ -70,10 +78,13 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    with Pre => Mission_State = RUNNING;
 
    function Time_Since_In_Safety_Escape return Time_Type with
-     Global => Private_State;
+     Global => Private_State,
+     Pre    => (Mission_State = RUNNING and then not In_Safety_Envelope)
+     or else Mission_State = ABORTED;
 
    function Fast_Evolving_Safety_Escape return Boolean with
-     Global => Private_State;
+     Global => Private_State,
+     Pre    => Mission_State = RUNNING and then not In_Safety_Envelope;
 
    function Time_Since_Stopped return Time_Type with
      Global => Private_State,
@@ -86,7 +97,9 @@ package MMS.F_PT.F_FC.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,
-                Input  => External.State);
+                Input  => External.State),
+     Post   => Operating_Point_Changed =
+       (Operating_Point'Old /= Operating_Point);
 
    procedure Write_Outputs with
    --  Compute values of outputs from the current state
@@ -96,6 +109,9 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    procedure Run with
      Global         => (In_Out => Private_State),
      Contract_Cases =>
+
+       --  ??? All these are guesses...
+
        (Mission_State = INIT
         and then Start_Take_Off
         =>
@@ -124,8 +140,20 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
           Mission_State = Mission_State'Old),
 
      Post           =>
-       (if In_Safety_Envelope'Old then Time_Since_In_Safety_Escape = 0
+
-        else Time_Since_In_Safety_Escape > Time_Since_In_Safety_Escape'Old)
+       --  Changes in the operating point provoque termination of the current
+       --  cruise phase and activate a transient climb or descent phase to
+       --  capture the new operating point (see 6.6.4 4. Cruise).
+
+       (if Operating_Point_Changed then Flight_Phase_State in CLIMB | DESCENT)
+
+       --  Time_Since_In_Safety_Escape is the number of seconds since the first
+       --  occurrence of safety escapes.
+
+       and then
+       (if not In_Safety_Envelope then
+          (if In_Safety_Envelope'Old then Time_Since_In_Safety_Escape = 0
+           else Time_Since_In_Safety_Escape > Time_Since_In_Safety_Escape'Old))
 
         --  6.7.4 Propulsion braking mutual exclusion
 
@@ -133,8 +161,10 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
        (if Mission_State = RUNNING and then Mission_State'Old = RUNNING then
           (case Engine_State'Old is
            when PROPULSION   =>
-             (if Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Hazard_Duration
+             (if not In_Safety_Envelope
-                or else Fast_Evolving_Safety_Escape
+              and then
+                (Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Hazard_Duration
+                 or else Fast_Evolving_Safety_Escape)
               then Engine_State = WAITING_BRAK
                 and then Time_Since_Stopped = 0
               else Engine_State = PROPULSION),
@@ -146,8 +176,9 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
               else Engine_State = BRAKING),
 
            when WAITING_PROP =>
-             (if Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Hazard_Duration
+             (if not In_Safety_Envelope
-                or else Fast_Evolving_Safety_Escape
+              and then (Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Hazard_Duration
+                        or else Fast_Evolving_Safety_Escape)
               then Engine_State = BRAKING
               elsif Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration
               then Engine_State = PROPULSION

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

@@ -2,7 +2,7 @@ with MMS.F_PT.Data;
 
 with Types; use Types;
 
-package MMS.F_PT.F_FC.Data is
+package MMS.F_PT.F_FC.Data with SPARK_Mode is
 
    --  ??? Types need to be precisely defined.
 
@@ -12,7 +12,7 @@ package MMS.F_PT.F_FC.Data is
 
    --  From 6.7.2.3
 
-   Flight_Domain_Mesh : Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100); -- ??? bounds
+   Flight_Domain_Mesh : constant Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100); -- ??? bounds
 
    function Climb_Gains
      (S : Flight_Speed_Center;
@@ -47,28 +47,58 @@ package MMS.F_PT.F_FC.Data is
 
    --  From 6.7.3.2
 
-   Qdot_MinCl : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MinCl : constant Angular_Speed_Type; --  in angle.s-1
-   Qdot_MaxCl : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MaxCl : constant Angular_Speed_Type; --  in angle.s-1
-   Q_MaxCl    : Angle_Type; --  in angle
+   Q_MaxCl    : constant Angle_Type; --  in angle
-   Qdot_MinCr : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MinCr : constant Angular_Speed_Type; --  in angle.s-1
-   Qdot_MaxCr : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MaxCr : constant Angular_Speed_Type; --  in angle.s-1
-   Q_MinCr    : Angle_Type; --  in angle
+   Q_MinCr    : constant Angle_Type; --  in angle
-   Pdot_MaxCr : Speed_Type; --  in km/h
+   Pdot_MaxCr : constant Speed_Type; --  in km/h
-   Qdot_MinDs : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MinDs : constant Angular_Speed_Type; --  in angle.s-1
-   Qdot_MaxDs : Angular_Speed_Type; --  in angle.s-1
+   Qdot_MaxDs : constant Angular_Speed_Type; --  in angle.s-1
-   Q_MaxDs    : Angle_Type; --  in angle
+   Q_MaxDs    : constant Angle_Type; --  in angle
 
-   Escape_Time : Time_Type; --  in s
+   Escape_Time : constant Time_Type; --  in s
 
    --  From 6.7.4
 
-   Commutation_Duration : Time_Type; --  in s
+   Commutation_Duration : constant Time_Type; --  in s
-   Hazard_Duration      : Time_Type; --  in s
+   Hazard_Duration      : constant Time_Type; --  in s
 
-   Recovery_Speed : Integer; --  in m.s
+   Recovery_Speed : constant Integer; --  in m.s
 
-   J0 : Integer; --  in kg.m2
+   J0 : constant Integer; --  in kg.m2
-   L  : Integer; --  in m
+   L  : constant Integer; --  in m
-   M0 : Integer; --  in kg
+   M0 : constant Integer; --  in kg
+
+private
+   pragma SPARK_Mode (Off);
+
+   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
+
+   Escape_Time : constant Time_Type := 0; --  in s
+
+   --  From 6.7.4
+
+   Commutation_Duration : constant Time_Type := 0; --  in s
+   Hazard_Duration      : constant Time_Type := 0; --  in s
+
+   Recovery_Speed : constant Integer := 0; --  in m.s
+
+   J0 : constant Integer := 0; --  in kg.m2
+   L  : constant Integer := 0; --  in m
+   M0 : constant Integer := 0; --  in kg
 
 end MMS.F_PT.F_FC.Data;

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

@@ -24,4 +24,6 @@ package MMS.F_PT.F_FC.Output is
    
    function Current_Altitude return Current_Altitude_Type with Global => Output_State;
    
+   function Current_Flight_Phase return Flight_Phase_Type with Global => Output_State;
+   
 end MMS.F_PT.F_FC.Output;

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

@@ -16,15 +16,16 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
        and then On_State = RUNNING
        and then Running_State = TAKE_OFF);
 
-   function Energy_Check_Succeed return Boolean is
+   function Initial_Energy_Check_Succeeded return Boolean is
      (Power_State = ON
       and then On_State = INIT
       and then Energy_Compatible_With_Mission);
 
-   function Energy_Check_Fail return Boolean is
+   function In_Flight_Energy_Check_Failed return Boolean is
      (Power_State = ON
       and then On_State = RUNNING
-      and then Running_State = CRUISE
+      and then Running_State = FLIGHT
+      and then Current_Flight_Phase = CRUISE
       and then not Energy_Compatible_With_Mission);
 
    function Mission_Cancelled return Boolean is
@@ -42,7 +43,7 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
       --  incompatible with mission completion.
 
       (if In_Take_Off_State and then not In_Take_Off_State'Old then
-         Energy_Check_Succeed'Old)
+         Initial_Energy_Check_Succeeded'Old)
 
       --  6.6.3.B Any mission cancellation is signaled to CP and GS.
 
@@ -55,6 +56,6 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
 
       and then
        (if Mission_Cancelled and then not Mission_Cancelled'Old then
-           Energy_Check_Fail'Old);
+           In_Flight_Energy_Check_Failed'Old);
 
 end MMS.F_PT.F_MM.Behavior.Guarantees;

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

@@ -45,6 +45,12 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    function Current_Altitude return Current_Altitude_Type with
      Global => Private_State;
 
+   function Current_Flight_Phase return Flight_Phase_Type with
+     Global => Private_State,
+     Pre    => Power_State = ON
+     and then On_State = RUNNING
+     and then Running_State = FLIGHT;
+
    -----------------------------------------
    -- States of the automaton in Figure 3 --
    -----------------------------------------
@@ -60,7 +66,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      Global => Private_State,
      Pre    => Power_State = ON;
 
-   type Running_State_Type is (TAKE_OFF, CLIMB, CRUISE, DESCENT, LANDING);
+   type Running_State_Type is (TAKE_OFF, FLIGHT, LANDING);
 
    function Running_State return Running_State_Type with
      Global => Private_State,
@@ -111,7 +117,8 @@ 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 = DESCENT;
+     and then Running_State = FLIGHT
+     and then Current_Flight_Phase = DESCENT;
 
    function Landed return Boolean is
      (Current_Speed = 0 and Current_Altitude = 0)
@@ -121,19 +128,6 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      and then On_State = RUNNING
      and then Running_State = LANDING;
 
-   function Operating_Point_Changed return Boolean with
-     Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State = RUNNING
-     and then (Running_State in CLIMB | CRUISE | DESCENT)
-     and then Navigation_Mode = RP;
-
-   function Cruise_Altitude_Reached return Boolean with
-     Global => Private_State,
-     Pre => Power_State = ON
-     and then On_State = RUNNING
-     and then (Running_State in CLIMB | DESCENT);
-
    ----------------
    -- Properties --
    ----------------
@@ -142,7 +136,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      Global => Private_State,
      Pre => Power_State = ON
      and then On_State in INIT | RUNNING
-     and then (if On_State = RUNNING then Running_State = CRUISE);
+     and then (if On_State = RUNNING then
+                 Running_State = FLIGHT and then Current_Flight_Phase = CRUISE);
 
    function Mission_Parameters_Defined return Boolean is
      (USB_Key_Present
@@ -205,11 +200,9 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
      Global         => (In_Out => Private_State),
      Post           =>
-       Operating_Point_Changed = (Operating_Point /= Operating_Point'Old)
 
        --  RP mode enables modification of range parameter before take-off.
 
-     and then
        (if not (Power_State'Old = ON
                 and then On_State'Old = INIT
                 and then Navigation_Mode'Old = RP)
@@ -296,7 +289,7 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
         =>
           Power_State = ON
         and then On_State = RUNNING
-        and then Running_State = CLIMB,
+        and then Running_State = FLIGHT,
 
         Power_State = ON
         and then On_State = RUNNING
@@ -311,7 +304,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
         Power_State = ON
         and then On_State = RUNNING
-        and then Running_State = CRUISE
+        and then Running_State = FLIGHT
+        and then Current_Flight_Phase = CRUISE
         and then Power_On
         and then not Mission_Abort_Received
         and then not Energy_Compatible_With_Mission
@@ -323,7 +317,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
         Power_State = ON
         and then On_State = RUNNING
-        and then Running_State = DESCENT
+        and then Running_State = FLIGHT
+        and then Current_Flight_Phase = DESCENT
         and then Power_On
         and then not Mission_Abort_Received
         and then Descent_Over
@@ -334,49 +329,17 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
         Power_State = ON
         and then On_State = RUNNING
-        and then (Running_State in CLIMB | CRUISE | DESCENT)
+        and then Running_State = FLIGHT
-        and then Power_On
-        and then not Mission_Abort_Received
-        and then Navigation_Mode = RP
-        and then
-          (if Running_State = CRUISE then Energy_Compatible_With_Mission)
-        and then
-          (if Running_State = DESCENT then not Descent_Over)
-        and then Operating_Point_Changed
-        =>
-          Power_State = ON
-        and then On_State = RUNNING
-        and then (Running_State in CLIMB | DESCENT),
-
-        Power_State = ON
-        and then On_State = RUNNING
-        and then (Running_State in CLIMB | DESCENT)
-        and then Power_On
-        and then not Mission_Abort_Received
-        and then (if Navigation_Mode = RP then not Operating_Point_Changed)
-        and then (if Running_State = DESCENT then not Descent_Over)
-        and then Cruise_Altitude_Reached
-        =>
-          Power_State = ON
-        and then On_State = RUNNING
-        and then Running_State = CRUISE,
-
-        Power_State = ON
-        and then On_State = RUNNING
-        and then (Running_State in CLIMB | DESCENT | CRUISE)
         and then Power_On
         and then not Mission_Abort_Received
         and then
-          (if Running_State = CRUISE then Energy_Compatible_With_Mission)
+          (if Current_Flight_Phase = CRUISE then Energy_Compatible_With_Mission)
-        and then (if Navigation_Mode = RP then not Operating_Point_Changed)
         and then
-          (if Running_State in CLIMB | DESCENT then
+          (if Current_Flight_Phase = DESCENT then not Descent_Over)
-                 not Cruise_Altitude_Reached)
-        and then (if Running_State = DESCENT then not Descent_Over)
         =>
           Power_State = ON
         and then On_State = RUNNING
-        and then Running_State = Running_State'Old,
+        and then Running_State = FLIGHT,
 
         Power_State = ON
         and then On_State = RUNNING

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

@@ -64,6 +64,9 @@ package MMS.F_PT.F_MM.Input is
    function Current_Altitude return Current_Altitude_Type
      renames MMS.F_PT.F_FC.Output.Current_Altitude;
    
+   function Current_Flight_Phase return Flight_Phase_Type
+     renames MMS.F_PT.F_FC.Output.Current_Flight_Phase;
+   
    ---------------
    -- From F_EM --
    ---------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt.ads

@@ -22,4 +22,6 @@ package MMS.F_PT is
    type Payload_Mass_Grid_Type is array (Payload_Mass_Center range <>)
      of Payload_Mass_Type;
 
+   type Flight_Phase_Type is (CLIMB, CRUISE, DESCENT);
+
 end MMS.F_PT;