Ada.Real_Time.Time_First

Ada.Real_Time.Time_First

[Simon Wright]

I opened an issue[1] on Cortex GNAT RTS, saying

   You’d expect Ada.Real_Time.Time_First to be quite a long time before
   any possible value of Ada.Real_Time.Clock; but in fact the system
   starts with Clock equal to Time_First.

On the other hand, 

I had written

   Last_Flight_Command_Time : Ada.Real_Time.Time
     := Ada.Real_Time.Time_First;

   ...
   
   Quad_Is_Flying :=
     Ada.Real_Time.To_Duration (Now - Last_Flight_Command_Time)
       < In_Flight_Time_Threshold;

but Now - Last_Flight_Command_Time is going to be quite small, to start
with, so Quad_Is_Flying is going to be True when it shouldn't be.

The workround I used was 

   Quad_Is_Flying :=
     Last_Flight_Command_Time /= Ada.Real_Time.Time_First
       and then
     Ada.Real_Time.To_Duration (Now - Last_Flight_Command_Time)
       < In_Flight_Time_Threshold;

In other words, I was using Time_First as a flag to indicate that
Last_Flight_Command_Time was invalid.

What would your standard pattern for this sort of problem be?
Esepecially considering that if I make Time_First a large negative
number I'll get the opposite problem, e.g. predicting ahead for a very
large interval, possibly even leading to numeric overflows.

I'm thinking of a Time type with the concept of validity, possibly built
round

   type Time (Valid : Boolean := False) is record
      case Valid is
         when True  => Value : Ada.Real_Time.Time;
         when False => null;
      end case;
   end record;

 and addition, etc with appropriate preconditions.

(not so sure about the discriminated record, might be more trouble than
it's worth)

[1] https://github.com/simonjwright/cortex-gnat-rts/issues/33

Re: Ada.Real_Time.Time_First

[Dmitry A. Kazakov]

On 2020-12-09 13:30, Simon Wright wrote:
> I opened an issue[1] on Cortex GNAT RTS, saying
> 
>     You’d expect Ada.Real_Time.Time_First to be quite a long time before
>     any possible value of Ada.Real_Time.Clock; but in fact the system
>     starts with Clock equal to Time_First.
> 
> On the other hand,
> 
> I had written
> 
>     Last_Flight_Command_Time : Ada.Real_Time.Time
>       := Ada.Real_Time.Time_First;
> 
>     ...
>     
>     Quad_Is_Flying :=
>       Ada.Real_Time.To_Duration (Now - Last_Flight_Command_Time)
>         < In_Flight_Time_Threshold;
> 
> but Now - Last_Flight_Command_Time is going to be quite small, to start
> with, so Quad_Is_Flying is going to be True when it shouldn't be.
> 
> The workround I used was
> 
>     Quad_Is_Flying :=
>       Last_Flight_Command_Time /= Ada.Real_Time.Time_First
>         and then
>       Ada.Real_Time.To_Duration (Now - Last_Flight_Command_Time)
>         < In_Flight_Time_Threshold;
> 
> In other words, I was using Time_First as a flag to indicate that
> Last_Flight_Command_Time was invalid.
> 
> What would your standard pattern for this sort of problem be?
> Esepecially considering that if I make Time_First a large negative
> number I'll get the opposite problem, e.g. predicting ahead for a very
> large interval, possibly even leading to numeric overflows.

I would use Next_Time instead of Last_Time:

    Next_Flight_Command_Time : Time := Time_First;
begin
    loop
       Now := Clock;
       if Now >= Next_Flight_Command_Time then
          Fire_All_Rockets;
          Next_Flight_Command_Time :=
             Next_Flight_Command_Time + In_Flight_Time_Threshold;
       end if;
    end loop;
exception
    when Constraint_Error => -- the End of Times!
       Put_Line ("Thank you for you cooperation!");
       Fire_Death_Star;
       Self_Destroy;
end;

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada.Real_Time.Time_First

[Niklas Holsti]

On 2020-12-09 14:30, Simon Wright wrote:
> I opened an issue[1] on Cortex GNAT RTS, saying
> 
>     You’d expect Ada.Real_Time.Time_First to be quite a long time before
>     any possible value of Ada.Real_Time.Clock; but in fact the system
>     starts with Clock equal to Time_First.


I don't see any reason for expecting Time_First to be far in the past 
relative to program start. In fact, RM D.8(19) says "For example, [the 
start of Time] can correspond to the time of system initialization".

Contrariwise, it could be useful to know that Clock actually starts from 
Time_First, because I have often needed a "Start_Time" object that 
records the Clock at the start of the program, and it would be much 
simpler to use Time_First, if Time_First is known to equal the initial 
Clock.

>     Quad_Is_Flying :=
>       Ada.Real_Time.To_Duration (Now - Last_Flight_Command_Time)
>         < In_Flight_Time_Threshold;


If Time_First, as the initial value of Last_Flight_Command_Time, would 
really be in the far past compared to Now, that computation risks 
overflowing the range of Duration, which may be as small as one day 
(86_400 seconds), RM 9.6(27).

> The workround I used was
> 
>     Quad_Is_Flying :=
>       Last_Flight_Command_Time /= Ada.Real_Time.Time_First
>         and then
>       Ada.Real_Time.To_Duration (Now - Last_Flight_Command_Time)
>         < In_Flight_Time_Threshold;
> 
> In other words, I was using Time_First as a flag to indicate that
> Last_Flight_Command_Time was invalid.


Even that can still overflow Duration, if more than one day can pass 
since the last flight command.

> What would your standard pattern for this sort of problem be?
> Esepecially considering that if I make Time_First a large negative
> number I'll get the opposite problem, e.g. predicting ahead for a very
> large interval, possibly even leading to numeric overflows.


You have two problems: your assumption about Time_First (or perhaps it's 
not an assumption, if you make your own RTS) and the possible overflow 
of Duration.

To indicate an invalid Last_Flight_Command_Time, I would either use a 
discriminated type wrapping a Time value that depends on a Valid 
discriminant, as you suggested, or just have a Boolean flag, say 
Flight_Commands_Given that is initially False. I would use the 
discriminated type only if there is more than one such variable or 
object in the program.

For the overflow, I suggest changing the comparison to

    Now < Last_Flight_Command_Time
          + To_Time_Span (In_Flight_Time_Threshold)

assuming that Last_Flight_Command_Time is valid in the sense we are 
discussing. That will overflow only when Last_Flight_Command_Time 
approaches Time_Last, and the program is likely to fail then anyway.


> [1] https://github.com/simonjwright/cortex-gnat-rts/issues/33

Re: Ada.Real_Time.Time_First

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> I would use Next_Time instead of Last_Time:
>
>    Next_Flight_Command_Time : Time := Time_First;
> begin
>    loop
>       Now := Clock;
>       if Now >= Next_Flight_Command_Time then
>          Fire_All_Rockets;
>          Next_Flight_Command_Time :=
>  

Great idea; the name isn't right in my context, but the method applies
very well. (It's the time by which the next flight command has to have
been given before we decide we're not flying any more. I plead that (a)
this logic seems not to be our Earth logic, (b) it's a translation from
someone's C, (c) the original code has a comment expressing doubt)

Re: Ada.Real_Time.Time_First

[Simon Wright]

Niklas Holsti <niklas.holsti@tidorum.invalid> writes:

> On 2020-12-09 14:30, Simon Wright wrote:
>> I opened an issue[1] on Cortex GNAT RTS, saying
>>     You’d expect Ada.Real_Time.Time_First to be quite a long time
>>     before any possible value of Ada.Real_Time.Clock; but in fact the
>>     system starts with Clock equal to Time_First.
>
>
> I don't see any reason for expecting Time_First to be far in the past
> relative to program start. In fact, RM D.8(19) says "For example, [the 
> start of Time] can correspond to the time of system initialization".
>
> Contrariwise, it could be useful to know that Clock actually starts
> from Time_First, because I have often needed a "Start_Time" object
> that records the Clock at the start of the program, and it would be
> much simpler to use Time_First, if Time_First is known to equal the
> initial Clock.

OK, I'll back out that last commit!

> To indicate an invalid Last_Flight_Command_Time, I would either use a
> discriminated type wrapping a Time value that depends on a Valid 
> discriminant, as you suggested, or just have a Boolean flag, say
> Flight_Commands_Given that is initially False. I would use the 
> discriminated type only if there is more than one such variable or
> object in the program.

Yes.

> For the overflow, I suggest changing the comparison to
>
>    Now < Last_Flight_Command_Time
>          + To_Time_Span (In_Flight_Time_Threshold)
>
> assuming that Last_Flight_Command_Time is valid in the sense we are
> discussing. That will overflow only when Last_Flight_Command_Time 
> approaches Time_Last, and the program is likely to fail then anyway.

This conversation has been very valuable, particularly in the case of
other similar tests. I suspect, though, that "are we still flying?" is a
question that'll take more thinking to resolve!

>> [1] https://github.com/simonjwright/cortex-gnat-rts/issues/33