Layer2_MMS_SW_SPARK: update after answers on #28

UseCaseDevelopment/Layer2_MMS_SW_SPARK/external.ads

@@ -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_Option with
+   function USB_Key return USB_Key_Type_Option with
      Volatile_Function,
      Global => State;
 

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

@@ -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_Option
+   function USB_Key return USB_Key_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

@@ -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_Option
+   function USB_Key return USB_Key_Type_Option
      renames MMS.F_PT.F_CM.Input.USB_Key; 
 
    ----------------------

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

@@ -8,12 +8,6 @@ package MMS.F_PT.F_FC.Behavior.Guarantees with SPARK_Mode is
    -- 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
      (On_State = RUNNING
       and then Engine_State in Braking_State_Type);

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

@@ -37,11 +37,13 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
    -----------------------------------
 
    procedure Run with
-     Post =>
+     Pre  => State_Invariant,
+     Post => State_Invariant
 
       --  6.6.3.A Viability guarantee: no take-off if energy aboard is
       --  incompatible with mission completion.
 
+      and then
        (if In_Take_Off_State and then not In_Take_Off_State'Old then
           Initial_Energy_Test_Succeeded)
 
@@ -69,7 +71,7 @@ package MMS.F_PT.F_MM.Behavior.Guarantees with SPARK_Mode is
           and then Mission_Parameters_Defined
         then
           USB_Key_Present
-        and then Operating_Mode = Operating_Mode_From_CP
+        and then Operating_Mode_From_Parameters = Operating_Mode_From_USB_Key
         and then Navigation_Parameters = Navigation_Parameters_From_USB_Key);
 
 end MMS.F_PT.F_MM.Behavior.Guarantees;

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

@@ -28,11 +28,9 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
    function Payload_Mass_Given return Boolean with
      Pre => Power_On;
-   --  ???  Should we assume that Payload_Mass is always given after takeoff?
-   --  same question for usb key
 
    function Payload_Mass return Payload_Mass_Type with
-     Pre => Power_On;
+     Pre => Power_On and then Payload_Mass_Given;
 
    function Navigation_Mode_From_CP return Navigation_Mode_Type with
      Pre => Power_On;
@@ -43,8 +41,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    function Navigation_Mode_From_GS return Navigation_Mode_Type with
      Pre => Power_On and then Navigation_Mode_From_GS_Received;
 
-   function Operating_Mode_From_CP return Navigation_Option_Type with
-     Pre => Power_On;
+   function Operating_Mode_From_USB_Key return Navigation_Option_Type with
+     Pre => Power_On and then USB_Key_Present;
 
    function Operating_Mode_From_GS_Received return Boolean with
      Pre => Power_On;
@@ -89,7 +87,8 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    function Mission_Parameters_Defined return Boolean is
      (USB_Key_Present
       or else (Navigation_Mode_From_CP = RP
-               and then Navigation_Parameters_From_GS_Received))
+               and then Navigation_Parameters_From_GS_Received
+               and then Operating_Mode_From_GS_Received))
    with
    Pre  => Power_On;
 
@@ -121,6 +120,12 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      Pre    => Power_State = ON
      and then On_State = ABORTED;
 
+   function State_Invariant return Boolean is
+     (Power_On = (Power_State = On)
+      and then (if Power_State = On and then On_State = RUNNING then
+                     Init_Completed));
+   --  Global assumptions, should be maintained by the task main loop.
+
    -----------------------------
    -- Properties and Entities --
    -----------------------------
@@ -128,8 +133,13 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
    function Navigation_Mode return Navigation_Mode_Type with
      Pre    => Power_On;
 
+   function Operating_Mode_From_Parameters return Navigation_Option_Type with
+     Pre    => Power_On
+     and then Mission_Parameters_Defined;
+
    function Operating_Mode return Navigation_Option_Type with
-     Pre    => Power_On;
+     Pre    => Power_On
+     and then Mission_Parameters_Defined;
 
    function Navigation_Parameters return Navigation_Parameters_Type
    with Pre => Power_On
@@ -180,11 +190,24 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
      and then Running_State = FLIGHT
      and then Current_Flight_Phase = CRUISE;
 
-   function Take_Off_Over return Boolean with
+   function Current_Altitude_Close_Enough_To_ref_TakeOff return Boolean with
+     Global => Input_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;
+   --  Return True if Current_Altitude is close enough to Speed_ref_TakeOff
+
+   function Take_Off_Over return Boolean is
+     (if Operating_Mode = ALTITUDE then
+         Current_Altitude_Close_Enough_To_ref_TakeOff
+      else Current_Speed_Close_Enough_To_ref_TakeOff)
+   with
      Pre => Power_On
      and then Power_State = ON
      and then On_State = RUNNING
-     and then Running_State = TAKE_OFF;
+     and then Running_State = TAKE_OFF
+     and then Mission_Parameters_Defined;
 
    function Descent_Over return Boolean with
      Pre => Power_On
@@ -216,8 +239,33 @@ 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 => (Output => Input_State,
-                Input  => External.State);
+     Global => (In_Out => Input_State,
+                Input  => (External.State, Private_State)),
+     Post =>
+
+   --  Only update inputs when new values are received.
+
+     (if USB_Key_Present'Old then USB_Key_Present)
+     and then (if Navigation_Parameters_From_GS_Received'Old
+               then Navigation_Parameters_From_GS_Received)
+     and then (if Operating_Mode_From_GS_Received'Old
+               then Operating_Mode_From_GS_Received)
+
+   --  Information from CP can only be changed before take-off.
+
+     and then (if Power_State = On and then On_State = RUNNING
+               then Navigation_Mode_From_CP = Navigation_Mode_From_CP'Old
+               and then Payload_Bay_Closed = Payload_Bay_Closed'Old
+               and then Payload_Mass_Given = Payload_Mass_Given'Old
+               and then
+                 (if Payload_Mass_Given then Payload_Mass = Payload_Mass'Old)
+               and then
+                 (if USB_Key_Present then
+                      USB_Key_Present'Old
+                  and then Navigation_Parameters_From_USB_Key =
+                    Navigation_Parameters_From_USB_Key'Old
+                  and then Operating_Mode_From_USB_Key =
+                    Operating_Mode_From_USB_Key'Old));
 
    procedure Write_Outputs with
    --  Compute values of outputs from the current state
@@ -259,15 +307,27 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
 
       else Navigation_Mode_From_GS)
 
-     and then Operating_Mode =
-       (if Navigation_Mode = A
+     and then
+         (if Mission_Parameters_Defined then
+
+            Operating_Mode_From_Parameters =
+              (if Navigation_Mode_From_CP = A
                or else not Operating_Mode_From_GS_Received
-        then Operating_Mode_From_CP
+               then Operating_Mode_From_USB_Key
                else Operating_Mode_From_GS)
 
-     and then
-         (if Mission_Parameters_Defined then
-            Navigation_Parameters =
+              --  During take-off, the most energy efficient mode is computed once and
+          --  for all from the viability tables.
+
+          and then 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)
+
+          and then Navigation_Parameters =
             (if Navigation_Mode_From_CP = A
              or else not Navigation_Parameters_From_GS_Received
              then Navigation_Parameters_From_USB_Key
@@ -289,21 +349,36 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
        and then Power_State = ON
        and then On_State in INIT | RUNNING,
 
-     --  F_MM ensures freeze of the operating point once landing is activated.
-
      Post   =>
-         (if Power_State = ON
-           and then On_State = RUNNING
+
+         --  F_MM ensures freeze of the operating point once landing is
+         --  activated.
+
+         (if On_State = RUNNING
            and then Running_State = LANDING
           then Operating_Point = Operating_Point'Old
+
+          --  Take-Off preset operating point (Altitude_ref_TakeOff and
+          --  Speed_ref_TakeOff) (see #28).
+
+          elsif On_State = RUNNING
+           and then Running_State = TAKE_OFF
+          then Operating_Point =
+              Operating_Point_Type'(Altitude => Data.Altitude_ref_TakeOff,
+                                    Speed    => Data.Speed_ref_TakeOff)
+
+          --  During flight, RP mode enables modification of the operating
+          --  point.
+
           else Operating_Point = Operating_Point_From_Navigation_Parameters)
 
          --  RP mode enables modification of range parameter before take-off.
 
     and then
        (if Navigation_Mode = RP
-        then Mission_Range = Mission_Range'Old
-        else Mission_Range = Mission_Range_From_Navigation_Parameters);
+           and then On_State = INIT
+        then Mission_Range = Mission_Range_From_Navigation_Parameters
+        else Mission_Range = Mission_Range'Old);
 
    ------------------------------
    --  Mission_Viability_Logic --
@@ -519,6 +594,9 @@ package MMS.F_PT.F_MM.Behavior with SPARK_Mode is
                    Viability_Logic_State,
                    Mission_Termination_State),
                 In_Out => Private_State),
+     Pre            =>
+       (if Power_On and then Power_State = On and then On_State = RUNNING then
+          Init_Completed),
      Contract_Cases =>
        (not Power_On
         =>
@@ -702,8 +780,8 @@ private
    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_USB_Key return Navigation_Option_Type is
+     (State.Input_USB_Key.Content.Navigation_Option);
 
    function Operating_Mode_From_GS_Received return Boolean is
      (State.Input_Navigation_Option.Present);
@@ -721,7 +799,7 @@ private
      (State.Input_USB_Key.Present);
 
    function Navigation_Parameters_From_USB_Key return Navigation_Parameters_Type is
-     (State.Input_USB_Key.Content);
+     (State.Input_USB_Key.Content.Navigation_Parameters);
 
    function Mission_Abort_Received return Boolean is
      (State.Input_Mission_Abort);
@@ -763,9 +841,6 @@ private
    function Aborted_For_Energy_Reasons return Boolean is
      (State.Aborted_For_Energy_Reasons);
 
-   function Take_Off_Over return Boolean is (True);
-   -- ??? When is take off over?
-
    function Descent_Over return Boolean is
      (State.Descent_Over);
 
@@ -775,6 +850,9 @@ private
    function Navigation_Mode return Navigation_Mode_Type is
      (State.Navigation_Mode);
 
+   function Operating_Mode_From_Parameters return Navigation_Option_Type is
+     (State.Operating_Mode_From_Parameters);
+
    function Operating_Mode return Navigation_Option_Type is
      (State.Operating_Mode);
 

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

@@ -74,5 +74,6 @@ package MMS.F_PT.F_MM.Data is
 
    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;

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

@@ -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_Option
+   function USB_Key return USB_Key_Type_Option
      renames MMS.F_PT.F_CM.Output.USB_Key;
    
    -----------------------

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

@@ -26,7 +26,7 @@ package MMS.F_PT.F_MM.State is
 
    Input_Payload_Mass : Payload_Mass_Type with Part_Of => Input_State;
 
-   Input_USB_Key : Navigation_Parameters_Type_Option with
+   Input_USB_Key : USB_Key_Type_Option with
      Part_Of => Input_State;
 
    Input_Mission_Abort : Boolean with Part_Of => Input_State;
@@ -65,6 +65,9 @@ package MMS.F_PT.F_MM.State is
    Navigation_Mode : Navigation_Mode_Type with
      Part_Of => Navigation_Parameter_State;
 
+   Operating_Mode_From_Parameters : Navigation_Option_Type with
+     Part_Of => Navigation_Parameter_State;
+
    Operating_Mode : Navigation_Option_Type with
      Part_Of => Navigation_Parameter_State;
 

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-f_mm.adb

@@ -37,6 +37,7 @@ SPARK_Mode,
                        Aborted_For_Energy_Reasons),
                     Navigation_Parameter_State =>
                       (Navigation_Mode,
+                       Operating_Mode_From_Parameters,
                        Operating_Mode,
                        Navigation_Parameters),
                     Operating_Point_State =>

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt-input.ads

@@ -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_Option
+   function USB_Key return USB_Key_Type_Option
      renames MMS.Input.USB_Key;
    
    function P return Distance_Type

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_pt.ads

@@ -12,6 +12,8 @@ package MMS.F_PT is
    
    type Energy_Level_Type is range 0 .. 500; -- in kj
 
+   subtype Speed_Or_Altitude is Navigation_Option_Type range SPEED .. ALTITUDE;
+   
    type Operating_Point_Type is record
       Altitude : Current_Altitude_Type; -- ??? which altitude type
       Speed    : Current_Speed_Type; --  ??? which speed type

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-input.ads

@@ -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_Option
+   function USB_Key return USB_Key_Type_Option
      renames External.USB_Key;
 
    -------------------------

UseCaseDevelopment/Layer2_MMS_SW_SPARK/types.ads

@@ -47,6 +47,20 @@ package Types is
       end case;
    end record;
 
+   type USB_Key_Type is record
+      Navigation_Parameters : Navigation_Parameters_Type;
+      Navigation_Option     : Navigation_Option_Type;
+   end record;
+
+   type USB_Key_Type_Option (Present : Boolean := False) is record
+      case Present is
+      when True  =>
+         Content : USB_Key_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