handouts/graphs.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Sun, 28 Sep 2025 14:03:59 +0100
changeset 991 b4b97704815b
parent 989 84401da2e277
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
497
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
\documentclass{article}
989
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     2
\usepackage{tikz}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     3
\usepackage{pgf}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     4
\usepackage{pgfplots}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     5
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     6
\pgfplotsset{compat=1.15}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     7
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     8
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
     9
%% DATA for the graphs: first x coordinate, second y coordinate
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    10
\begin{filecontents}{re-python2.data}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    11
1 0.033
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    12
5 0.036
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    13
10 0.034
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    14
15 0.036
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    15
18 0.059
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    16
19 0.084
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    17
20 0.141
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    18
21 0.248
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    19
22 0.485
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    20
23 0.878
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    21
24 1.71
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    22
25 3.40
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    23
26 7.08
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    24
27 14.12
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    25
28 26.69
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    26
\end{filecontents}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    27
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    28
\begin{filecontents}{re-java.data}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    29
5  0.00298
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    30
10  0.00418
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    31
15  0.00996
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    32
16  0.01710
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    33
17  0.03492
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    34
18  0.03303
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    35
19  0.05084
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    36
20  0.10177
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    37
21  0.19960
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    38
22  0.41159
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    39
23  0.82234
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    40
24  1.70251
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    41
25  3.36112
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    42
26  6.63998
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    43
27  13.35120
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    44
28  29.81185
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    45
\end{filecontents}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    46
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    47
\begin{filecontents}{re3a.data}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    48
1 0.00003
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    49
500001 0.22527
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    50
1000001 0.62752
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    51
1500001 0.88485
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    52
2000001 1.39815
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    53
2500001 1.68619
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    54
3000001 1.94957
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    55
3500001 2.15878
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    56
4000001 2.59918
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    57
4500001 5.90679
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    58
5000001 13.11295
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    59
5500001 19.15376
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    60
6000001 40.16373
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    61
\end{filecontents}
84401da2e277 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 497
diff changeset
    62
497
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
\begin{document}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
\section*{Benchmarks for $(a^*)^* b$ and $a^{?\{n\}} a^{\{n\}}$}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
\mbox{}\bigskip
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
\begin{center}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
$(a^*)^* \cdot b$ and strings $\underbrace{a\ldots a}_{n}$\medskip\\
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
\begin{tabular}{@{}cc@{}}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
\raisebox{5mm}{
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
\begin{tikzpicture}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
\begin{axis}[
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
    xlabel={$n$},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
    x label style={at={(1.05,0.0)}},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
    ylabel={time in secs},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
    enlargelimits=false,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
    xtick={0,5,...,30},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
    xmax=33,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
    ymax=35,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
    ytick={0,5,...,30},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
    scaled ticks=false,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
    axis lines=left,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
    width=5cm,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
    height=5cm, 
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
    legend entries={Java, Python},  
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
    legend pos=north west,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
    legend cell align=left]
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
\end{axis}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
\end{tikzpicture}}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
&
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
\begin{tikzpicture}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
  \begin{axis}[
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
    xlabel={$n$},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
    x label style={at={(1.1,0.0)}},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
    ylabel={time in secs},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
    enlargelimits=false,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
    ymax=35,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
    ytick={0,5,...,30},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
    axis lines=left,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
    width=6.5cm,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
    height=5cm,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
    legend entries={Derivative matcher},  
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
    legend pos=north east,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
    legend cell align=left]
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
\end{axis}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
\end{tikzpicture}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
\end{tabular}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
\end{center}\bigskip
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
\begin{center}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
$a^{?\{n\}} \cdot a^{\{n\}}$ and strings $\underbrace{a\ldots a}_{n}$\medskip\\
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
\begin{tabular}{@{}cc@{}}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
\begin{tikzpicture}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
\begin{axis}[
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
    xlabel={$n$},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
    x label style={at={(1.05,0.0)}},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
    ylabel={\small time in secs},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
    enlargelimits=false,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
    xtick={0,5,...,30},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
    xmax=33,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
    ymax=35,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
    ytick={0,5,...,30},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
    scaled ticks=false,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
    axis lines=left,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
    width=5cm,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
    height=5cm, 
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
    legend entries={Python,Ruby},  
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
    legend pos=north west,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
    legend cell align=left]
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
\addplot[brown,mark=triangle*, mark options={fill=white}] table {re-ruby.data};  
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
\end{axis}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
\end{tikzpicture}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
&
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
\begin{tikzpicture}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
  \begin{axis}[
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
    xlabel={$n$},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
    x label style={at={(1.1,0.05)}},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
    ylabel={\small time in secs},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
    enlargelimits=false,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
    xtick={0,2500,...,11000},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
    xmax=12000,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
    ymax=35,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
    ytick={0,5,...,30},
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
    scaled ticks=false,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
    axis lines=left,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
    width=6.5cm,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
    height=5cm,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
    legend entries={Derivative matcher},  
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
    legend pos=north east,
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
    legend cell align=left]
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
\end{axis}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
\end{tikzpicture}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
\end{tabular}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
\end{center}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
\end{document}
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
%%% Local Variables: 
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
%%% mode: latex
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
%%% TeX-master: t
aa88ac9be3c0 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
%%% End: