Layer2_MMS_SW_SPARK: update F_FC after answers on #28

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc-behavior-guarantees.adb

@@ -24,12 +24,13 @@ package body MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
          Propulsion_Braking_Mutual_Exclusion;
 
          Reference_Trajectory_Computation;
-         Gain_Scheduling;
 
          if Engine_State = PROPULSION then
+            Gain_Scheduling;
             Propulsion_Control;
             State.Braking_Torque := 0.0;
          elsif Engine_State = BRAKING then
+            Gain_Scheduling;
             Braking_Control;
             State.Propulsion_Torque := 0.0;
          else

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

@@ -412,64 +412,94 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    -- Reference Trajectory Computation --
    --------------------------------------
 
+   function Use_Set_Point_Altitude return Boolean is
+     (Running_State = LANDING or else Selected_Option = ALTITUDE)
+   with Pre => On_State = RUNNING;
+
    function Set_Point_Altitude return Current_Altitude_Type with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING;
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
 
    function Intermediate_Set_Point_Altitude return Current_Altitude_Type with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING;
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
 
    function Close_To_Set_Point_Altitude return Boolean with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING;
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
    --  True if we are close enough to the set point. Used to avoid Zeno effect.
 
    function Intermediate_Set_Point_Altitude_Reached return Boolean with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING and then Already_Running;
+     Pre    => On_State = RUNNING
+     and then Already_Running
+     and then not Operating_Mode_Changed
+     and then not Operating_Point_Changed
+     and then Use_Set_Point_Altitude;
    --  True if we have reached the previous intermediate set point.
 
+   function Use_Set_Point_Speed return Boolean is
+     (Running_State = LANDING or else Selected_Option = SPEED)
+   with Pre => On_State = RUNNING;
+
    function Set_Point_Speed return Current_Speed_Type with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING;
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Speed;
 
    function Intermediate_Set_Point_Speed return Current_Speed_Type with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING;
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Speed;
 
    function Close_To_Set_Point_Speed return Boolean with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING;
+     Pre    => On_State = RUNNING
+     and then Use_Set_Point_Speed;
    --  True if we are close enough to the set point. Used to avoid Zeno effect.
 
    function Intermediate_Set_Point_Speed_Reached return Boolean with
      Global => (Input    => Trajectory_State,
-                Proof_In => (Private_State,
+                Proof_In => (Input_State,
+                             Private_State,
                              Operating_Mode_State,
                              Mutual_Exclusion_State)),
-     Pre    => On_State = RUNNING and then Already_Running;
+     Pre    => On_State = RUNNING
+     and then Already_Running
+     and then not Operating_Mode_Changed
+     and then not Operating_Point_Changed
+     and then Use_Set_Point_Speed;
    --  True if we have reached the previous intermediate set point.
 
    function Set_Point_Distance return Current_Range_Type with
@@ -505,8 +535,11 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
           and then Set_Point_Speed = 0
           and then Set_Point_Distance = Mission_Range
         else
-          (Set_Point_Altitude = Operating_Point.Altitude
+          (case Selected_Option is
-           and then Set_Point_Speed = Operating_Point.Speed))
+                 when ALTITUDE =>
+                   Set_Point_Altitude = Operating_Point.Altitude,
+                 when SPEED =>
+                   Set_Point_Speed = Operating_Point.Speed))
 
      --  Instead of giving the true set-point to propulsion control, it gives
      --  half of the change amplitude. When current intermediate set-point is
@@ -515,25 +548,29 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
      --  Module is reset by any operating point change.
 
      and then
+       (if Use_Set_Point_Speed then
           Intermediate_Set_Point_Speed =
           (if not Already_Running
            or else Operating_Point_Changed
+           or else Operating_Mode_Changed
            or else (Intermediate_Set_Point_Speed_Reached
                     and then not Close_To_Set_Point_Speed)
            then
              (Set_Point_Speed + Current_Speed) / 2
            elsif Close_To_Set_Point_Speed then Set_Point_Speed
-           else Intermediate_Set_Point_Speed'Old)
+           else Intermediate_Set_Point_Speed'Old))
 
      and then
+       (if Use_Set_Point_Altitude then
           Intermediate_Set_Point_Altitude =
           (if not Already_Running
            or else Operating_Point_Changed
+           or else Operating_Mode_Changed
            or else (Intermediate_Set_Point_Altitude_Reached
                     and then not Close_To_Set_Point_Altitude)
            then (Set_Point_Altitude + Current_Altitude) / 2
            elsif Close_To_Set_Point_Altitude then Set_Point_Altitude
-           else Intermediate_Set_Point_Altitude'Old)
+           else Intermediate_Set_Point_Altitude'Old))
 
     --  Changes in the operating point provoque termination of the current
     --  cruise phase and activate a transient climb or descent phase to
@@ -585,7 +622,8 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
                            Private_State,
                            Mutual_Exclusion_State),
                 In_Out => Gain_Scheduling_State),
-     Pre    => On_State = RUNNING,
+     Pre    => On_State = RUNNING
+     and then Engine_State in BRAKING | PROPULSION,
      Post   =>
 
    --  1. Assembling mission profile.
@@ -631,20 +669,38 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
           Extract_Gain_Triple_For_Neighbours.Neighbours (I) =
          (case Flight_Phase is
           when CLIMB   =>
-           Data.Climb_Gains
+            (if Engine_State = PROPULSION then
+               Data.Climb_Propulsion_Gains
                  (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
                   A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
-             S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S),
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+             else
+               Data.Climb_Braking_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)),
           when CRUISE  =>
-           Data.Cruise_Gains
+            (if Engine_State = PROPULSION then
+               Data.Cruise_Propulsion_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+             else
+               Data.Cruise_Braking_Gains
                  (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
                   A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
-             S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S),
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)),
           when DESCENT =>
-           Data.Descent_Gains
+            (if Engine_State = PROPULSION then
+               Data.Descent_Propulsion_Gains
+                 (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
+                  A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)
+             else
+               Data.Descent_Braking_Gains
                  (M => Nearest_Neighbours.Neighbours (I).Mission_Profile.M,
                   A => Nearest_Neighbours.Neighbours (I).Mission_Profile.A,
-             S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S)))
+                  S => Nearest_Neighbours.Neighbours (I).Mission_Profile.S))))
 
    --  4. Compute MP's gain triple by interpolation of its neighbours
    --     Set appropriate value to Interpolated_Gain_Triple.
@@ -656,15 +712,16 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
 
    function Propulsion_Altitude_Error return Current_Altitude_Type'Base is
      (Current_Altitude - Intermediate_Set_Point_Altitude)
-   with Pre => On_State = RUNNING;
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
 
    function Propulsion_Speed_Error return Current_Speed_Type'Base is
      (Current_Speed - Intermediate_Set_Point_Speed)
-   with Pre => On_State = RUNNING;
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Speed;
 
    function Propulsion_Error return Error_Type with
-     Global => (Proof_In => Private_State,
+     Global => Propulsion_State;
-                Input    => Propulsion_State);
    --  In Flight and maybe also Take-Off phase, should be
    --  Propulsion_Altitude_Error if Selected_Mode is ALTITUDE and
    --  Propulsion_Speed_Error otherwise, but I am confused about the units...
@@ -672,14 +729,12 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    --  see #29.
 
    function Propulsion_Integral_Error return Error_Type with
-     Global => (Proof_In => Private_State,
+     Global => Propulsion_State;
-                Input    => Propulsion_State);
+   --  Cumulative past Propulsion_Error during the last Ti seconds
-   --  Cumulative past error during the last Ti seconds
 
    function Propulsion_Derivative_Error return Error_Type with
-     Global => (Proof_In => Private_State,
+     Global => Propulsion_State;
-                Input    => Propulsion_State);
+   --  Propulsion_Error variation at current time
-   --  Error variation at current time
 
    procedure Propulsion_Control with
      Global => (Input  => (Input_State,
@@ -699,24 +754,27 @@ package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
    -- Braking Control --
    ---------------------
 
+   function Braking_Altitude_Error return Current_Altitude_Type'Base is
+     (Current_Altitude - Intermediate_Set_Point_Altitude)
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Altitude;
+
    function Braking_Speed_Error return Current_Speed_Type'Base is
-     (Current_Speed - Data.Recovery_Speed)
+     (Current_Speed - Intermediate_Set_Point_Speed)
-   with Pre => On_State = RUNNING;
+   with Pre => On_State = RUNNING
+     and then Use_Set_Point_Speed;
 
    function Braking_Error return Error_Type with
-     Global => (Proof_In => Private_State,
+     Global => Braking_State;
-                Input    => Braking_State);
+   --  Same as propulsion, see #28.
-   --  Should be Braking_Speed_Error, but I am confused about the units...
 
    function Braking_Integral_Error return Error_Type with
-     Global => (Proof_In => Private_State,
+     Global => Braking_State;
-                Input    => Braking_State);
+   --  Cumulative past Braking_Error during the last Ti seconds
-   --  Cumulative past error during the last Ti seconds
 
    function Braking_Derivative_Error return Error_Type with
-     Global => (Proof_In => Private_State,
+     Global => Braking_State;
-                Input    => Braking_State);
+   --  Braking_Error variation at current time
-   --  Error variation at current time
 
    procedure Braking_Control with
      Global => (Input  => (Input_State,

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

@@ -14,7 +14,7 @@ package MMS.F_PT.F_FC.Data with SPARK_Mode is
 
    Flight_Domain_Mesh : constant Flight_Domain_Mesh_Type (1 .. 100, 1 .. 100); -- ??? bounds
 
-   function Climb_Gains
+   function Climb_Propulsion_Gains
      (S : Flight_Speed_Center;
       A : Flight_Altitude_Center;
       M : Payload_Mass_Center) return Gain_Triple
@@ -23,7 +23,7 @@ package MMS.F_PT.F_FC.Data with SPARK_Mode is
      and then A in Flight_Domain_Mesh'Range (2)
      and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
 
-   function Cruise_Gains
+   function Cruise_Propulsion_Gains
      (S : Flight_Speed_Center;
       A : Flight_Altitude_Center;
       M : Payload_Mass_Center) return Gain_Triple
@@ -32,7 +32,34 @@ package MMS.F_PT.F_FC.Data with SPARK_Mode is
      and then A in Flight_Domain_Mesh'Range (2)
      and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
 
-   function Descent_Gains
+   function Descent_Propulsion_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Climb_Braking_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Cruise_Braking_Gains
+     (S : Flight_Speed_Center;
+      A : Flight_Altitude_Center;
+      M : Payload_Mass_Center) return Gain_Triple
+   with
+     Pre => S in Flight_Domain_Mesh'Range (1)
+     and then A in Flight_Domain_Mesh'Range (2)
+     and then M in MMS.F_PT.Data.Payload_Mass_Grid'Range;
+
+   function Descent_Braking_Gains
      (S : Flight_Speed_Center;
       A : Flight_Altitude_Center;
       M : Payload_Mass_Center) return Gain_Triple