Layer2_MMS_SW_SPARK behavioural specification of F_FC

UseCaseDevelopment/Layer2_MMS_SW_SPARK/external.ads

 with Types; use Types;
 
-package External with Abstract_State =>
-  ((From_GS with External => Async_Writers),
-   (From_CP with External => Async_Writers),
-   (From_P_P with External => Async_Writers)) is
+package External with Abstract_State => (State with External => Async_Writers) is
 
    ------------------------------------------------------
    -- Ground-based Mission Preparation and Supervision --
@@ -11,23 +8,23 @@ package External with Abstract_State =>
 
    function Navigation_Parameters return Navigation_Parameters_Type with
      Volatile_Function,
-     Global => From_GS;
+     Global => State;
 
    function Navigation_Mode return Navigation_Mode_Type with
      Volatile_Function,
-     Global => From_GS;
+     Global => State;
 
    function Navigation_Option return Navigation_Option_Type with
      Volatile_Function,
-     Global => From_GS;
+     Global => State;
 
    function Go return Boolean with
      Volatile_Function,
-     Global => From_GS;
+     Global => State;
 
    function Emergency_Landing return Boolean with
      Volatile_Function,
-     Global => From_GS;
+     Global => State;
 
    --------------------------------------------------
    -- AV-based Mission Preparation (Control Panel) --
@@ -35,27 +32,27 @@ package External with Abstract_State =>
 
    function On_OFF_Push_Button return Boolean with
      Volatile_Function,
-     Global => From_CP;
+     Global => State;
 
    function Start_Push_Button return Boolean with
      Volatile_Function,
-     Global => From_CP;
+     Global => State;
 
    function Mode_Switch return Navigation_Mode_Type with
      Volatile_Function,
-     Global => From_CP;
+     Global => State;
 
    function Bay_Switch return Bay_Switch_Type with
      Volatile_Function,
-     Global => From_CP;
+     Global => State;
 
    function Payload_Mass return Payload_Mass_Type with
      Volatile_Function,
-     Global => From_CP;
+     Global => State;
 
    function USB_Key return Navigation_Parameters_Type with
      Volatile_Function,
-     Global => From_CP;
+     Global => State;
 
    -------------------------
    -- Physical Parameters --
@@ -63,14 +60,14 @@ package External with Abstract_State =>
 
    function P return Distance_Type with
      Volatile_Function,
-     Global => From_P_P;
+     Global => State;
 
    function P_Dot return Speed_Type with
      Volatile_Function,
-     Global => From_P_P;
+     Global => State;
 
    function Q return Angle_Type with
      Volatile_Function,
-     Global => From_P_P;
+     Global => State;
 
 end External;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-data.ads

+with Types; use Types;
+
+package MMS.F_PT.Data is
+
+   Payload_Mass_Grid  : Payload_Mass_Grid_Type (1 .. 10); -- ??? bounds
+
+end MMS.F_PT.Data;

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

@@ -22,7 +22,7 @@ package MMS.F_PT.F_CM.Output is
       
    function CP_Displays return CP_Displays_Type is
      (CP_Displays_Type'
-        (Ready            => True, --  This register is not loaded at increment 1
+        (Ready            => True, --  This register is not loaded at increment 1 ???
          Cancelled        => MMS.F_PT.F_CM.Input.Mission_Cancelled,
          Complete         => MMS.F_PT.F_CM.Input.Mission_Complete,
          Aborted          => MMS.F_PT.F_CM.Input.Mission_Aborted,
@@ -89,7 +89,11 @@ package MMS.F_PT.F_CM.Output is
    function USB_Key return Navigation_Parameters_Type
      renames MMS.F_PT.F_CM.Input.USB_Key; 
 
-   function Payload_Mass_To_F_MM return Payload_Mass_Type
+   ----------------------
+   -- To F_MM and F_FC --
+   ----------------------
+
+   function Payload_Mass return Payload_Mass_Type
      renames MMS.F_PT.F_CM.Input.Payload_Mass;
    
    -------------
@@ -101,8 +105,5 @@ package MMS.F_PT.F_CM.Output is
    function P_Dot return Speed_Type renames MMS.F_PT.F_CM.Input.P_Dot;
    
    function Q return Angle_Type renames MMS.F_PT.F_CM.Input.Q;
-
-   function Payload_Mass_To_F_FC return Payload_Mass_Type
-     renames MMS.F_PT.F_CM.Input.Payload_Mass;
    
 end MMS.F_PT.F_CM.Output;

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

+package body MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
+
+   procedure Run is
+   begin
+      MMS.F_PT.F_FC.Behavior.Run;
+   end Run;
+
+end MMS.F_PT.F_FC.Behavior.Guarantees;

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

+with MMS.F_PT.F_FC.Data;
+with Types; use Types;
+
+package MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   -----------------------------------
+   -- High-Level Properties on F_FC --
+   -----------------------------------
+
+   subtype Propulsion_State_Type is Engine_State_Type
+   range PROPULSION .. WAITING_BRAK;
+
+   subtype Braking_State_Type is Engine_State_Type
+   range BRAKING .. WAITING_PROP;
+
+   function Engine_State_In_Braking return Boolean is
+     (Mission_State = RUNNING and then Engine_State in Braking_State_Type);
+
+   function Engine_State_In_Propulsion return Boolean is
+     (Mission_State = RUNNING and then Engine_State in Propulsion_State_Type);
+
+   -----------------------------------
+   -- High-Level Garantees for F_FC --
+   -----------------------------------
+
+   procedure Run with
+     Post =>
+
+     --  6.7.3.2.D Propulsion and  braking torque actions are in mutual
+     --  exclusion.
+
+     (if (Engine_State_In_Propulsion'Old and then Engine_State_In_Braking)
+      or else (Engine_State_In_Braking'Old and then Engine_State_In_Propulsion)
+      then Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration)
+
+     --  6.7.3.2.E In-flight mission concellation with remaining propulsion
+     --  capacity implies occurrence of safety excapes for more than
+     --  Escape_Time seconds.
+
+     and then
+       (if Mission_State = ABORTED and then Mission_State'Old /= ABORTED
+        then Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time);
+
+end MMS.F_PT.F_FC.Behavior.Guarantees;

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

 with MMS.F_PT.F_FC.Data;
-
+with External;
 with Types; use Types;
 
-package MMS.F_PT.F_FC.Behavior is
+package MMS.F_PT.F_FC.Behavior with SPARK_Mode is
+   pragma Unevaluated_Use_Of_Old (Allow);
 
    ------------
    -- Inputs --
    ------------
 
-   function P return Distance_Type;
-   function P_Dot return Speed_Type;
-   function Q return Angle_Type;
+   function P return Distance_Type with Global => Private_State;
+   function P_Dot return Speed_Type with Global => Private_State;
+   function Q return Angle_Type with Global => Private_State;
+
+   function Start_Take_Off return Boolean with
+     Global => Private_State,
+     Pre    => Mission_State = INIT;
+
+   function Start_Landing return Boolean with
+     Global => Private_State,
+     Pre    => Mission_State = RUNNING;
 
    ----------------------
    -- Estimated Values --
    ----------------------
 
-   function Q_Dot return Angular_Speed_Type;
+   function Q_Dot return Angular_Speed_Type with Global => Private_State;
 
    ------------
    -- States --
    ------------
 
+   type Mission_State_Type is (INIT, RUNNING, ABORTED, COMPLETE);
+
+   function Mission_State return Mission_State_Type with
+     Global => Private_State;
+
    type Phase_State_Type is (CLIMB, CRUISE, DESCENT);
 
-   function Phase_State return Phase_State_Type;
+   function Phase_State return Phase_State_Type with
+     Global => Private_State,
+     Pre    => Mission_State = RUNNING;
+
+   type Engine_State_Type is
+     (PROPULSION, WAITING_BRAK, BRAKING, WAITING_PROP);
+
+   function Engine_State return Engine_State_Type with
+     Global => Private_State,
+     Pre    => Mission_State = RUNNING;
 
    ----------------
    -- Properties --
@@ -43,6 +66,100 @@ package MMS.F_PT.F_FC.Behavior is
               and P_Dot < MMS.F_PT.F_FC.Data.Pdot_MaxCr,
          when DESCENT =>
             Q_Dot in MMS.F_PT.F_FC.Data.Qdot_MinDs .. MMS.F_PT.F_FC.Data.Qdot_MaxDs
-              and Q < MMS.F_PT.F_FC.Data.Q_MaxDs);
+              and Q < MMS.F_PT.F_FC.Data.Q_MaxDs)
+   with Pre => Mission_State = RUNNING;
+
+   function Time_Since_In_Safety_Escape return Time_Type with
+     Global => Private_State;
+
+   function Fast_Evolving_Safety_Escape return Boolean with
+     Global => Private_State;
+
+   function Time_Since_Stopped return Time_Type with
+     Global => Private_State,
+     Pre    => Mission_State = RUNNING;
+
+   ---------------------------------------
+   -- Behavioural Specification of F_FC --
+   ---------------------------------------
+
+   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);
+
+   procedure Write_Outputs with
+   --  Compute values of outputs from the current state
+     Global => (Input  => Private_State,
+                Output => Output_State);
+
+   procedure Run with
+     Global         => (In_Out => Private_State),
+     Contract_Cases =>
+       (Mission_State = INIT
+        and then Start_Take_Off
+        =>
+          Mission_State = RUNNING
+        and then Engine_State = PROPULSION,
+
+        Mission_State = INIT
+        and then not Start_Take_Off
+        =>
+          Mission_State = INIT,
+
+        Mission_State = RUNNING
+        and then Start_Landing
+        =>
+          Mission_State = COMPLETE,
+
+        Mission_State = RUNNING
+        and then not Start_Landing
+        =>
+          (if Time_Since_In_Safety_Escape > MMS.F_PT.F_FC.Data.Escape_Time then
+               Mission_State = ABORTED
+           else Mission_State = RUNNING),
+
+        (Mission_State in COMPLETE | ABORTED)
+        =>
+          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)
+
+        --  6.7.4 Propulsion braking mutual exclusion
+
+       and then
+       (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
+                or else Fast_Evolving_Safety_Escape
+              then Engine_State = WAITING_BRAK
+                and then Time_Since_Stopped = 0
+              else Engine_State = PROPULSION),
+
+           when BRAKING      =>
+             (if In_Safety_Envelope
+              then Engine_State = WAITING_PROP
+                and then Time_Since_Stopped = 0
+              else Engine_State = BRAKING),
+
+           when WAITING_PROP =>
+             (if 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
+              else Engine_State = WAITING_PROP
+                and then Time_Since_Stopped > Time_Since_Stopped'Old),
+
+           when WAITING_BRAK =>
+               (if In_Safety_Envelope
+                then Engine_State = PROPULSION
+                elsif Time_Since_Stopped > MMS.F_PT.F_FC.Data.Commutation_Duration
+                then Engine_State = BRAKING
+                else Engine_State = WAITING_BRAK
+                  and then Time_Since_Stopped > Time_Since_Stopped'Old)));
 
 end MMS.F_PT.F_FC.Behavior;

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

@@ -58,12 +58,12 @@ package MMS.F_PT.F_FC.Data is
    Qdot_MaxDs : Angular_Speed_Type; --  in angle.s-1
    Q_MaxDs    : Angle_Type; --  in angle
 
-   Escape_Time : Integer; --  in s
+   Escape_Time : Time_Type; --  in s
 
    --  From 6.7.4
 
-   Commutation_Duration : Integer; --  in s
-   Hazard_Duration      : Integer; --  in s
+   Commutation_Duration : Time_Type; --  in s
+   Hazard_Duration      : Time_Type; --  in s
 
    Recovery_Speed : Integer; --  in m.s
 

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

@@ -19,7 +19,7 @@ package MMS.F_PT.F_FC.Input is
      renames MMS.F_PT.F_CM.Output.Q;
    
    function Payload_Mass return Payload_Mass_Type
-     renames MMS.F_PT.F_CM.Output.Payload_Mass_To_F_FC;
+     renames MMS.F_PT.F_CM.Output.Payload_Mass;
       
    ---------------
    -- From F_MM --

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

@@ -2,26 +2,26 @@ with Types; use Types;
 
 package MMS.F_PT.F_FC.Output is
 
-   ----------------------
-   -- To F_CM and F_EM --
-   ----------------------
+   ---------------------
+   -- To F_CM or F_EM --
+   ---------------------
 
-   function Propulsion_Torque return Torque_Type;
+   function Propulsion_Torque return Torque_Type with Global => Output_State;
    
-   function Braking_Torque return Torque_Type;
+   function Braking_Torque return Torque_Type with Global => Output_State;
    
    -------------
    -- To F_MM --
    -------------
    
-   function Mission_Abort return Boolean; -- ??? not listed in F_FC outputs
+   function Mission_Abort return Boolean with Global => Output_State; -- ??? not listed in F_FC outputs
    
-   function Estimated_Total_Mass return Estimated_Total_Mass_Type;
+   function Estimated_Total_Mass return Estimated_Total_Mass_Type with Global => Output_State;
    
-   function Current_Range return Current_Range_Type;
+   function Current_Range return Current_Range_Type with Global => Output_State;
    
-   function Current_Speed return Current_Speed_Type;
+   function Current_Speed return Current_Speed_Type with Global => Output_State;
    
-   function Current_Altitude return Current_Altitude_Type;
+   function Current_Altitude return Current_Altitude_Type with Global => Output_State;
    
 end MMS.F_PT.F_FC.Output;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_fc.ads

 with Types; use Types;
 
-package MMS.F_PT.F_FC is
+package MMS.F_PT.F_FC with Abstract_State => (Private_State, Output_State) is
+   pragma Elaborate_Body (MMS.F_PT.F_FC);
 
    type Flight_Cell_Center_Type is record
       Speed    : Current_Speed_Type;
@@ -22,4 +23,6 @@ package MMS.F_PT.F_FC is
       Ki : Gain_Type;
    end record;
 
+   type Time_Type is new Integer; --  in s ??? some bounds
+
 end MMS.F_PT.F_FC;

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

@@ -36,7 +36,7 @@ package MMS.F_PT.F_MM.Input is
      renames MMS.F_PT.F_CM.Output.Bay_Switch;
 
    function Payload_Mass return Payload_Mass_Type
-     renames MMS.F_PT.F_CM.Output.Payload_Mass_To_F_MM;
+     renames MMS.F_PT.F_CM.Output.Payload_Mass;
    
    function USB_Key return Navigation_Parameters_Type
      renames MMS.F_PT.F_CM.Output.USB_Key;

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

 with Types; use Types;
 
-package MMS.F_PT.F_MM.Output with
-  Abstract_State => (To_F_CM, To_F_EL, To_F_FC)
-is
+package MMS.F_PT.F_MM.Output is
 
    -------------
    -- To F_CM --
-   --------------
+   -------------
    
-   function Mission_Cancelled return Boolean with Global => To_F_CM;
+   function Mission_Cancelled return Boolean with Global => Output_State;
    
-   function Mission_Complete return Boolean with Global => To_F_CM;
+   function Mission_Complete return Boolean with Global => Output_State;
    
-   function Mission_Aborted return Boolean with Global => To_F_CM;
+   function Mission_Aborted return Boolean with Global => Output_State;
    
    -------------
    -- To F_EL --
    --------------
 
-   function Emergency_Landing return Boolean with Global => To_F_EL;
+   function Emergency_Landing return Boolean with Global => Output_State;
    
    -------------
    -- To F_FC --
    -------------
    
-   function Start_Take_Off return Boolean with Global => To_F_FC;
+   function Start_Take_Off return Boolean with Global => Output_State;
    
-   function Start_Landing return Boolean with Global => To_F_FC;
+   function Start_Landing return Boolean with Global => Output_State;
 
-   function Operating_Point return Operating_Point_Type with Global => To_F_FC;
+   function Operating_Point return Operating_Point_Type with Global => Output_State;
    
-   function Operating_Mode return Navigation_Option_Type with Global => To_F_FC;
+   function Operating_Mode return Navigation_Option_Type with Global => Output_State;
    
-   function Mission_Range return Current_Range_Type with Global => To_F_FC;
+   function Mission_Range return Current_Range_Type with Global => Output_State;
    -- ??? which distance type
    
 end MMS.F_PT.F_MM.Output;

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;
+end MMS.F_PT.F_MM.State;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.ads

 with Types; use Types;
 
-package MMS.F_PT.F_MM is
+package MMS.F_PT.F_MM with Abstract_State => (Private_State, Output_State) is
+   pragma Elaborate_Body (MMS.F_PT.F_MM);
 
    type Viability_Cell_Center_Type is record
       Distance     : Current_Range_Type;