timer: support for walltime

* spot/misc/timer.hh: here.

spot/misc/timer.hh

@@ -33,7 +33,7 @@
 # include <sys/times.h>
 #endif
 #include <ctime>
-
+#include <chrono>
 
 namespace spot
 {
@@ -96,6 +96,7 @@ namespace spot
     {
       SPOT_ASSERT(!running);
       running = true;
+      wall_start_ = std::chrono::high_resolution_clock::now();
 #ifdef SPOT_HAVE_TIMES
       struct tms tmp;
       times(&tmp);
@@ -112,6 +113,9 @@ namespace spot
     void
     stop()
     {
+      auto end = std::chrono::high_resolution_clock::now();
+      wall_cumul_ = std::chrono::duration_cast
+        <std::chrono::milliseconds>(end - wall_start_).count();
 #ifdef SPOT_HAVE_TIMES
       struct tms tmp;
       times(&tmp);
@@ -194,10 +198,23 @@ namespace spot
       return running;
     }
 
+    /// \brief Return cumulative wall time
+    ///
+    /// When using multithreading the cpu time is not
+    /// relevant and we have to deal with wall time to have an
+    /// effective timer
+    std::chrono::milliseconds::rep
+    walltime() const
+    {
+      return wall_cumul_;
+    }
+
   protected:
     time_info start_;
     time_info total_;
     bool running;
+    std::chrono::high_resolution_clock::time_point wall_start_;
+    std::chrono::milliseconds::rep wall_cumul_;
   };
 
   // This function declared here must be implemented in each file