Include file:

#include "mcrl2/utilities/execution_timer.h
class mcrl2::utilities::execution_timer

Simple timer to time the CPU time used by a piece of code.

Example usage: execution_timer timer(“test_tool”, “/path/to/file”) timer.start(“hint”) … (execute some code here) … timer.finish(“hint”) will output the following to the file “/path/to/file”, or standard error if filename is empty, assuming that the time between start and finish is n seconds (with precision of 2 decimal places).tool: test_tool timing: hint: nNote that this is an output format that can immediately be parsed using YAML (

Protected attributes

std::string mcrl2::utilities::execution_timer::m_filename

name of the file to write timings to

std::map<std::string, timing> mcrl2::utilities::execution_timer::m_timings

collection of timings

std::string mcrl2::utilities::execution_timer::m_tool_name

name of the tool we are timing

Protected member functions

void write_report(std::ostream &s)

Write the report to an output stream.


  • s The output stream to which the report is written.

Public member functions

execution_timer(const std::string &tool_name = "", std::string const &filename = "")

Constructor of a simple execution timer.


  • tool_name Name of the tool that does the measurements
  • filename Name of the file to which the measurements are written
void finish(const std::string &timing_name)

Finish a measurement with a hint.


  • timing_name Name of the measurment being finished

Pre: A start(timing_name) was executed before

Post: The current time has been recorded as end time of timing_name

void report()

Write all timing information that has been recorded.

Timing information is written to the filename that was provided in the constructor. If no filename was provided (i.e. the filename is empty) the information is written to standard error. The output is in YAML compatible format.

void start(const std::string &timing_name)

Start measurement with a hint.


  • timing_name Name of the measurement being started

Pre: No start(timing_name) has occurred before

Post: The current time has been recorded as starting time of timing_name