plot.tex

%% A standalone LaTeX file used to generate LaTeX plots for the benchmarks.
%% Requires PGFPlots (minimum version 1.17).
%% Rather than using this file directly, we compile plots with it by
%% redefining \timeout, \benchmono and \benchmod to the appropriate times and files,
%% and then write the output to a particular file.
%% The command ends up being something like:
%% TIMEOUT=7200 MOD=results/mod.dat MONO=results/mono.dat \
%%   pdflatex -jobname plot.pdf -halt-on-error -output-directory results \
%%   "\newcommand\timeout{$TIMEOUT}\newcommand\benchmod{$MOD}\newcommand\benchmono{$MONO}\input{plot.tex}"
%% See Makefile for how this is done.
%% In order for this to work, the \benchmod file must contain the columns "n", "wall", "med" and "99p".
%% The \benchmono file must contain the columns "n" and "total".
\documentclass[tikz]{standalone}
\usepackage{etoolbox} % command-line flag
\usepackage{mathptmx}  % times roman, including math (where possible)
\usepackage{siunitx} % SI units
\usepackage{pgfplots} % plots
\usepackage{pgfplotstable} % tables
\usepackage{xspace}
\pgfplotsset{compat=1.17}
\usepgfplotslibrary{units} % units
% style for timeout lines
\tikzstyle{timeout line} = [mark=none,black,dashed,samples=2,domain=20:2000]
\tikzstyle{timeout node} = [pos=0.2,yshift=-5pt,font=\it]

\newcommand{\ms}{\textsf{Ms}\xspace}
\newcommand{\sysshort}{\textsf{Tp}\xspace}

\pgfplotscreateplotcyclelist{cute}{
    {blue,mark=pentagon},
    {orange,mark=triangle},
    {green,mark=square},
    {red,mark=diamond},
}

\providecommand\timeout{7200.0} % fallback definitions
\providecommand\benchmono{mono.dat}
\providecommand\benchmod{mod.dat}
\pgfplotstableread{\benchmono}\mtbl
\pgfplotstableread{\benchmod}\tbl
% don't forget to divide the results by 1000 to get them in seconds
\begin{document}
\begin{tikzpicture}
    \begin{axis}[
            thick,
            grid=major,
            xlabel=Nodes,
            ylabel={Verification time},
            xmin=0,
            ymode=log,
            y unit=\si{\second},
            cycle list name=cute,
            legend style={
                    at={(1.35,0.98)},
                    anchor=north east,
                }
        ]
	\addplot table[x=n, y expr=\thisrow{wall}/1000]{\tbl};
	\addlegendentry{\sysshort}
	\addplot table[x=n, y expr=\thisrow{med}/1000]{\tbl};
	\addlegendentry{\sysshort median}
	\addplot table[x=n, y expr=\thisrow{99p}/1000]{\tbl};
	\addlegendentry{\sysshort $99^{th}$ p.}
	\addplot table[x=n, y expr=\thisrow{total}/1000]{\mtbl};
	\addlegendentry{\ms}
        \addplot[timeout line] {\timeout} node [timeout node] {t/o};
      \end{axis}
    \end{tikzpicture}
\end{document}