Improve proof time of feature test

Ref. eng/recordflux/RecordFlux#1803

tests/feature/fsm_comprehension_on_sequence/config.yml

@@ -2,9 +2,10 @@ output:
   - Channel
 sequence: |
   State: Start
-  State: Process
+  State: Process_1
   Read Channel: 4 0 2 1 1
   State: Send_1
+  State: Process_2
   Read Channel: 5 0 9 1 0 1 2 1 0 2 2 3
   State: Send_2
 proof:

tests/feature/fsm_comprehension_on_sequence/generated/rflx-test-s-fsm.ads

@@ -28,7 +28,7 @@ is
 
    type Channel is (C_Channel);
 
-   type State is (S_Start, S_Process, S_Send_1, S_Send_2, S_Final);
+   type State is (S_Start, S_Process_1, S_Send_1, S_Process_2, S_Send_2, S_Final);
 
    type Private_Context is private;
 

tests/feature/fsm_comprehension_on_sequence/generated/rflx-test-s-fsm_allocator.adb

@@ -29,8 +29,6 @@ is
       S.Slot_Ptr_6 := M.Slot_6'Unrestricted_Access;
       S.Slot_Ptr_7 := M.Slot_7'Unrestricted_Access;
       S.Slot_Ptr_8 := M.Slot_8'Unrestricted_Access;
-      S.Slot_Ptr_9 := M.Slot_9'Unrestricted_Access;
-      S.Slot_Ptr_10 := M.Slot_10'Unrestricted_Access;
    end Initialize;
 
    procedure Finalize (S : in out Slots) with
@@ -46,8 +44,6 @@ is
       S.Slot_Ptr_6 := null;
       S.Slot_Ptr_7 := null;
       S.Slot_Ptr_8 := null;
-      S.Slot_Ptr_9 := null;
-      S.Slot_Ptr_10 := null;
    end Finalize;
 
 end RFLX.Test.S.FSM_Allocator;

tests/feature/fsm_comprehension_on_sequence/generated/rflx-test-s-fsm_allocator.ads

@@ -30,8 +30,6 @@ is
          Slot_6 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
          Slot_7 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
          Slot_8 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
-         Slot_9 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
-         Slot_10 : aliased RFLX_Types.Bytes (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095) := (others => 0);
       end record;
 
    subtype Slot_Ptr_Type_4096 is RFLX_Types.Bytes_Ptr with
@@ -56,8 +54,6 @@ is
          Slot_Ptr_6 : Slot_Ptr_Type_4096;
          Slot_Ptr_7 : Slot_Ptr_Type_4096;
          Slot_Ptr_8 : Slot_Ptr_Type_4096;
-         Slot_Ptr_9 : Slot_Ptr_Type_4096;
-         Slot_Ptr_10 : Slot_Ptr_Type_4096;
       end record;
 
    function Initialized (S : Slots) return Boolean is
@@ -68,9 +64,7 @@ is
       and S.Slot_Ptr_5 /= null
       and S.Slot_Ptr_6 /= null
       and S.Slot_Ptr_7 /= null
-      and S.Slot_Ptr_8 /= null
-      and S.Slot_Ptr_9 /= null
-      and S.Slot_Ptr_10 /= null);
+      and S.Slot_Ptr_8 /= null);
 
    function Uninitialized (S : Slots) return Boolean is
      (S.Slot_Ptr_1 = null
@@ -80,9 +74,7 @@ is
       and S.Slot_Ptr_5 = null
       and S.Slot_Ptr_6 = null
       and S.Slot_Ptr_7 = null
-      and S.Slot_Ptr_8 = null
-      and S.Slot_Ptr_9 = null
-      and S.Slot_Ptr_10 = null);
+      and S.Slot_Ptr_8 = null);
 
    procedure Initialize (S : out Slots; M : Memory) with
      Post =>
@@ -100,8 +92,6 @@ is
       and S.Slot_Ptr_5 /= null
       and S.Slot_Ptr_6 /= null
       and S.Slot_Ptr_7 /= null
-      and S.Slot_Ptr_8 /= null
-      and S.Slot_Ptr_9 /= null
-      and S.Slot_Ptr_10 /= null);
+      and S.Slot_Ptr_8 /= null);
 
 end RFLX.Test.S.FSM_Allocator;

tests/feature/fsm_comprehension_on_sequence/test.rfi

@@ -3,5 +3,5 @@ Machine:
     Buffer_Size:
       Default: 4096
       Local:
-        Process:
+        Process_1:
           Option_Types: 8096

tests/feature/fsm_comprehension_on_sequence/test.rflx

@@ -15,14 +15,13 @@ package Test is
          Options'Append (Universal::Option'(Option_Type => Universal::OT_Null));
          Options'Append (Universal::Option'(Option_Type => Universal::OT_Data, Length => 2, Data => [2, 3]));
       transition
-         goto Process
+         goto Process_1
       exception
          goto null
       end Start;
 
-      state Process is
+      state Process_1 is
          Option_Types : Universal::Option_Types;
-         Message_Options : Universal::Options;
       begin
          Option_Types := [for E in Options => E.Option_Type];
          Option_Types := [for E in Options if True => E.Option_Type];
@@ -31,24 +30,33 @@ package Test is
          Message_1 := Universal::Message'(Message_Type => Universal::MT_Option_Types,
                                           Length => Option_Types'Size / 8,
                                           Option_Types => Option_Types);
-         Message_Options := [for E in Options if E.Option_Type = Universal::OT_Data => E];
-         Message_2 := Universal::Message'(Message_Type => Universal::MT_Options,
-                                          Length => Message_Options'Size / 8,
-                                          Options => Message_Options);
-         Message_Options'Reset;
       transition
          goto Send_1
       exception
          goto null
-      end Process;
+      end Process_1;
 
       state Send_1 is
       begin
          Channel'Write (Message_1);
       transition
-         goto Send_2
+         goto Process_2
       end Send_1;
 
+      state Process_2 is
+         Message_Options : Universal::Options;
+      begin
+         Message_Options := [for E in Options if E.Option_Type = Universal::OT_Data => E];
+         Message_2 := Universal::Message'(Message_Type => Universal::MT_Options,
+                                          Length => Message_Options'Size / 8,
+                                          Options => Message_Options);
+         Message_Options'Reset;
+      transition
+         goto Send_2
+      exception
+         goto null
+      end Process_2;
+
       state Send_2 is
       begin
          Channel'Write (Message_2);