Layer2_MMS_SW_SPARK behavioural specification of F_EL

UseCaseDevelopment/Layer2_MMS_SW_SPARK/DESIGN.txt

@@ -50,6 +50,10 @@ ACTIVITIES:
       Guarantee A: Not translated (linked with weather conditions)
       Guarantees B, C: Not translated (linked with actual embedded energy which is not measurable)
 
+    - MMS.F_EL:
+      7.3.2:
+      Guarantees A, B: Not tranlated (linked to weather conditions)
+
   * Verifications:
     The SPARK toolset can be used to check that:
     - Ada contracts are consistent. If it is a case by case contract, SPARK can check that all cases are covered and that no two cases can apply to the same inputs. If some properties or some information can only be checked in some cases, these cases can be expressed as preconditions on property or information functions and SPARK will check that they are always used in valid context.

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el-behavior.ads

@@ -0,0 +1,37 @@
+with Types; use Types;
+
+package MMS.F_EL.Behavior with SPARK_Mode is
+   
+   ------------
+   -- Inputs --
+   ------------
+
+   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;
+   
+   ----------------------
+   -- Estimated Values --
+   ----------------------
+
+   function Q_Dot return Angular_Speed_Type with Global => Private_State;
+   
+   ---------------------------------------
+   -- Behavioural Specification of F_EL --
+   ---------------------------------------
+
+   procedure Read_Inputs with
+   --  Read values of inputs once and for all and update the current state
+     Global => (In_Out => Private_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); 
+
+end MMS.F_EL.Behavior;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el-data.ads

@@ -1,13 +0,0 @@
-with Types; use Types;
-
-package MMS.F_EL.Data is
-
-   ---------------
-   -- Constants --
-   ---------------
-
-   --  From 7.3.2
-
-   Max_Touch_Speed : constant := 0.5; --  in m.s
-
-end MMS.F_EL.Data;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el-output.ads

@@ -6,14 +6,14 @@ package MMS.F_EL.Output is
    -- To MMS --
    ------------
    
-   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_PT --
    -------------
    
-   function Mission_Abort return Boolean;
+   function Mission_Abort return Boolean with Global => Output_State;
 
 end MMS.F_EL.Output;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el-state.ads

@@ -0,0 +1,4 @@
+private
+package MMS.F_EL.State is
+
+end MMS.F_EL.State;

UseCaseDevelopment/Layer2_MMS_SW_SPARK/mms-f_el.ads

@@ -1,7 +1,4 @@
-with Types; use Types;
-
-package MMS.F_EL is
-
-   
+package MMS.F_EL with Abstract_State => (Private_State, Output_State) is
+   pragma Elaborate_Body (MMS.F_EL);
 
 end MMS.F_EL;