------------------------------------------------------------------------------
-- Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
-- This work is free. You can redistribute it and/or modify it under the
-- terms of the Do What The Fuck You Want To Public License, Version 2,
-- as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);
------------------------------------------------------------------------------
--
-- SPARK Proof Analysis Tool
--
-- S.P.A.T. - Stopwatch for performance measurements.
--
------------------------------------------------------------------------------
limited private with Ada.Real_Time;
package SPAT.Stop_Watch is
type T (<>) is tagged limited private;
---------------------------------------------------------------------------
-- Create
--
-- Initializes a stop watch instance and returns it.
---------------------------------------------------------------------------
function Create return T;
---------------------------------------------------------------------------
-- Reset
--
-- Resets the stop watch.
---------------------------------------------------------------------------
procedure Reset (This : in out T);
---------------------------------------------------------------------------
-- Start
--
-- Starts a new lap measurement.
---------------------------------------------------------------------------
procedure Start (This : in out T);
---------------------------------------------------------------------------
-- Elapsed
--
-- Returns the time since the last start of measurement.
---------------------------------------------------------------------------
function Elapsed (This : in T) return String;
---------------------------------------------------------------------------
-- Elapsed_Total
--
-- Returns the time since the clock was reset.
---------------------------------------------------------------------------
function Elapsed_Total (This : in T) return String;
private
type T is tagged limited
record
Start_Time : Ada.Real_Time.Time;
Lap_Time : Ada.Real_Time.Time;
end record;
end SPAT.Stop_Watch;