Feature request: transition between states due to timeout

[mgrojo]

There should be a way to leave a state due to a timeout transition. For example, if a state machine for a client is defined, a timeout should be defined in a state in which the program is waiting for a response, but the response message is not received after a time. Ideally, the amount of time could be specified at run-time.

I haven't found a way to implement this through the state machines, and it seems to make sense for implementing the request-response model.

[senier]

Thanks for you suggestion, @mgrojo!

As you have noticed, we have ignored the whole topic of time so far in RecordFlux. My gut feeling is that introducing a notion of time and timeouts would require some design effort to make sure we also cover other potential use / corner cases. That being said, we don't have any concrete plans for any work in that direction.

Have you considered wrapping you message into a simple additional message which is handled in the read/write implementation of you channels? Here is what I'd do (the runtime configuration could either be done through user-defined functions or also as part of an outer message header):

package Handle_Timeout is

   type T is unsigned 8;
   type Status is (Valid => 1, Timeout => 2) with Size => 8;

   type Message is
      message
         F : T;
      end message;

   type Result is
      message
         Status : Status;
         Data : Message;
      end message;

   generic
      X : Channel with Readable;
   machine S is
      M : Result;
   begin
      state Read is
      begin
         X'Read (M);
      transition
         goto Retry
            if M'Valid and M.Status = Timeout
         goto null
            if M'Valid and M.Status = Valid
         goto null
      exception
         goto null
      end Read;

      state Retry is
      begin
      transition
         goto Read
      end Retry;
   end S;

end Handle_Timeout;

Your implementation would then set the Status field accordingly:

with RFLX.Handle_Timeout.S.FSM;
with RFLX.RFLX_Types;

procedure Run is
   package FSM renames RFLX.Handle_Timeout.S.FSM;
   package Types renames RFLX.RFLX_Types;
   use type Types.Index;
   Ctx : FSM.Context;
   Buffer : Types.Bytes (Types.Index'First .. Types.Index'First + 100);
   Retries : Natural := 3;
begin
   FSM.Initialize (Ctx);
   while FSM.Active (Ctx) loop
      for C in FSM.Channel'Range
      loop
         if FSM.Needs_Data (Ctx, C) then
            if Retries > 0 then
               Buffer (Buffer'First) := 2; -- Timeout
               Retries := Retries - 1;
            else
               Buffer (Buffer'First) := 1; -- Valid
            end if;
            FSM.Write (Ctx, C, Buffer);
         end if;
      end loop;
      FSM.Run (Ctx);
   end loop;
   FSM.Finalize (Ctx);
end Run;

Running the state machine with debug enabled then give the expected output:

$./out/run 
State: Read
State: Retry
State: Read
State: Retry
State: Read
State: Retry
State: Read
$

While having this in the formal spec would arguably be nicer, you can keep the additional overhead low if you make the outer message simple.

[mgrojo]

Thanks. I will investigate that approach.

Running the state machine with debug enabled then give the expected output:

I didn't know about that. I guess it is through this switch to rflx generate

  --debug {built-in,external}
                        enable adding of debug output to generated code

It seems useful.

[senier]

I didn't know about that. I guess it is through this switch to rflx generate

  --debug {built-in,external}
                        enable adding of debug output to generated code

Exactly. built-in will generate debug code right away using Ada.Text_IO. With external you could provide a custom implementation (if, say, you're on an embedded target with custom serial output functions).