% \iffalse meta-comment
%
% File: cmftbl.dtx
%
% Copyright (C) 2024 Dominik Schmid and Till Schallau
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3c
% of this license or (at your option) any later version.
% The latest version of this license is in
% http://www.latex-project.org/lppl.txt
% and version 1.3c or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status "maintained".
%
% The current maintainer of this work is Dominik Schmid
% <dominik.schmid@tu-dortmund.de>.
%
% This work consists of the files temporal-logic.dtx and temporal-logic.ins
% and the derived file temporal-logic.sty.
%
% \fi
%
% \iffalse
%<*driver>
\documentclass{l3doc}
\usepackage{temporal-logic}
\begin{document}
  \DocInput{\jobname.dtx}
\end{document}
%</driver>
% \fi
%
% \title{temporal-logic}
% \author{Dominik Schmid and Till Schallau}
% \date{Version 1.0}
%
% \maketitle
%
% \begin{documentation}
%
% \begin{abstract}
%  The \emph{temporal-logic} package defines functions for rendering temporal
%  operators defined in \emph{Linear Temporal Logic} (LTL)\footnote{Pnueli, A.
%  (1977). The temporal logic of programs. In: 18th Annual Symposium on
%  Foundations of Computer Science (SFCS 1977). IEEE.
%  \url{https://doi.org/10.1109/SFCS.1977.32}.}, \emph{Metric
%  Temporal Logic} (MTL)\footnote{Alur, R., Henzinger, T. A. (1993). Real-time
%  logics: Complexity and expressiveness. In: Proceedings of the Fifth Annual
%  Symposium on Logic in Computer Science (LICS 1990). Elsevier.
%  \url{https://doi.org/10.1006/inco.1993.1025}.}, \emph{Metric
%  First-order Temporal Logic} (MFOTL)\footnote{Basin, David, Klaedtke, Felix,
%  Müller, Samuel, and Zălinescu, Eugen. (2015). Monitoring Metric First-order
%  Temporal Properties. In: Journal of the ACM (J. ACM). Association for
%  Computing Machinery. \url{https://doi.org/10.1145/2699444}.}, and the
%  \emph{Counting Metric First-order Temporal Binding Logic}
%  (CMFTBL)\footnote{Schallau, T., Naujokat, S., Kullmann, F., Howar, F.
%  (2024). Tree-Based Scenario Classification. In: NASA Formal Methods (NFM
%  2024). Lecture Notes in Computer Science, vol 14627. Springer, Cham.
%  \url{https://doi.org/10.1007/978-3-031-60698-4\_15}.}. The package defines
%  various functions with variants in order to include or omit optional
%  parameters of the operators like the optional interval.
% \end{abstract}
%
% \clearpage
% \tableofcontents
% \clearpage
%
% \section{Introduction}
% \subsection{Counting Metric First-order Temporal Logic}
%  \emph{Counting Metric First-order Temporal Logic} (CMFTBL) argues about
%  finite traces of states. It is an extension of \emph{Metric First-order
%  Temporal Logic} (MFOTL), which itself is based on \emph{Metric Temporal
%  Logic} (MTL) and ultimately on \emph{Linear Temporal Logic} (LTL). All these
%  logics extend the base with further operators and features.
%
% \subsection{Basic usage}
%  This package defines the symbols used in Temporal logics as
%  \emph{MathOperators}. Therefore, the symbols, as well as the commands, have
%  to be used in math mode. To use normal text in the parameters \cs{mathrm}
%  or \cs{text} may be used to switch back to text mode.
%
%  The symbols come in two variants. A standalone version for mentioning logic
%  symbols in text without additional formula spacing is described in
%  Sect.~\ref{sec:standalone_symbols} and a formula version, also providing
%  additional parameters, is described in Sect.~\ref{sec:future_ltl} --
%  Sect.~\ref{sec:cmftbl_extension}. The formula version should always be
%  preferred over the standalone symbols in formulas as they provide
%  additional spaces and explicitly enforce the correct usage of superscript
%  and subscript via mandatory parameters. The naming scheme of the operators
%  is chosen such that each command reflects the name of the temporal operator
%  prefixed with a ``c'' for \textit{\underline{C}MFTBL}. Standalone symbols, as described
%  in Sect.~\ref{sec:standalone_symbols}, are prefixed with ``csymb''. Those
%  prefixes are necessary to prevent name clashes with built-in \LaTeX commands.
%
% \subsection{Manual structure}
%  This manual is structured as follows. First, the symbols for \emph{Future
%  LTL} and \emph{Past LTL} are introducted in Sect.~\ref{sec:future_ltl} and
%  Sect.~\ref{sec:past_ltl}. The additional intervals from \emph{MTL} are
%  described in Sect.~\ref{sec:mtl_extension}. The operators introduced
%  in \emph{MFOTL} and \emph{CMFTBL} are described in
%  Sect.~\ref{sec:mfotl_extension} and Sect.~\ref{sec:cmftbl_extension}.
%  Section~\ref{sec:usage} shows the usage of the symbols in formulas.
%  Section~\ref{sec:standalone_symbols} closes the
%  command definitions with the standalone symbols for usage in text.
%  Finally, Sect.~\ref{sec:operator_scaling} demonstrates the automatic scaling
%  of the operators.
%
% \subsection{Dependencies}
%   The package loads the following dependencies:
%   \begin{itemize}
%     \item \emph{expl3} For \LaTeX 3 support.
%     \item \emph{xparse} For parsing the mandatory and optional arguments.
%     \item \emph{amsmath} For symbol definitions.
%     \item \emph{tikz} For rendering of symbols.
%   \end{itemize}
%
% \clearpage
% \section{Symbol definitions}
% \subsection{Future LTL symbols}
% \label{sec:future_ltl}
%   \emph{Future LTL}, or simply \emph{LTL}, defines operators to argue about
%   the future. This includes the following operators.
% \begin{function}{
%   \ceventually,
%   \cglobally,
%   \cnext,
%   \cuntil}
%   \begin{syntax}
%   \begin{tabular}{lc}
%     \cs{ceventually} & $\ceventually$\\
%     \cs{cglobally}   & $\cglobally$\\
%     \cs{cnext}       & $\cnext$\\
%     \cs{cuntil}      & $\cuntil$\\
% \end{tabular}
% \end{syntax}
% \end{function}
%
%  \noindent The semantics of the operators are commonly defined as follows:
% \begin{itemize}
%   \item $\ceventually \phi$ expresses that $\phi$ must hold at least once in
%   the future.
%  \item $\cglobally \phi$ expresses that $\phi$ must hold from now for the
%   entire trace.
%  \item $\cnext \phi$ expresses that $\phi$ must hold at the next state.
%  \item $\phi \cuntil \psi$ expresses that $\phi$ must hold until $\psi$
%   holds.
% \end{itemize}
%
% \subsection{Past LTL symbols}
% \label{sec:past_ltl}
%  \emph{Past LTL} defines operators analogous to \emph{Future LTL} to argue
%  about the past. The symbols are identical but are filled solid black.
%  \begin{function}{ ,
%   \conce,
%   \chistorically,
%   \cprevious,
%   \csince}
%   \begin{syntax}
%   \begin{tabular}{lc}
%     \cs{conce}         & $\conce$\\
%     \cs{chistorically} & $\chistorically$\\
%     \cs{cprevious}     & $\cprevious$\\
%     \cs{csince}        & $\csince$\\
%   \end{tabular}
%   \end{syntax}
%  \end{function}
%
%  \noindent The semantics of the operators are commonly defined as follows:
%  \begin{itemize}
%   \item $\conce \phi$ expresses that $\phi$ must have held at least once
%   in the past.
%   \item $\chistorically \phi$ expresses that $\phi$ must have held until
%   now for the entire past trace.
%   \item $\cprevious \phi$ expresses that $\phi$ must have held at the previous
%   state.
%   \item $\phi \csince \psi$ expresses that $\phi$ must have held since $\psi$
%   has held.
%  \end{itemize}
%
% \clearpage
% \subsection{MTL extension}
% \label{sec:mtl_extension}
%  The \emph{Future LTL} and \emph{Past LTL} operators may be extended with an
%  optional interval to form \emph{MTL}.
%  \begin{function}{
%   \ceventually,
%   \conce,
%   \cglobally,
%   \chistorically,
%   \cnext,
%   \cprevious,
%   \cuntil,
%   \csince}
%   \begin{syntax}
%    \begin{tabular}{lc}
%     \cs{ceventually}\oarg{Interval} & $\ceventually[[0,1]]$\\
%     \cs{conce}\oarg{Interval} & $\conce[[0,1]]$\\
%     \cs{cglobally}\oarg{Interval} & $\cglobally[[0,1]]$\\
%     \cs{chistorically}\oarg{Interval} & $\chistorically[[0,1]]$\\
%     \cs{cnext}\oarg{Interval} & $\cnext[[0,1]]$\\
%     \cs{cprevious}\oarg{Interval} & $\cprevious[[0,1]]$\\
%     \cs{cuntil}\oarg{Interval} & $\cuntil[[0,1]]$\\
%     \cs{csince}\oarg{Interval} & $\csince[[0,1]]$\\
%   \end{tabular}
%  \end{syntax}
% \end{function}
%
%  \noindent The semantics of the intervals are commonly defined as follows:
%  The trace is only evaluated in the given interval. An empty interval is
%  considered to be $[0, \infty)$ for future and $(\infty, 0]$ for past
%  operators. The first component of the interval always indicates the earlier
%  state for both future and past operators.
%
% \subsection{MFOTL extension}
% \label{sec:mfotl_extension}
%  \emph{MFOTL} introduces the first-order quantifiers $\exists$ and $\forall$.
%  This package does not provide additional symbols, as the built-in ones
%  already contained in \LaTeX~may be used.
%
%  \begin{function}{
%   \exists,
%   \forall}
%   \begin{syntax}
%    \begin{tabular}{lc}
%     \cs{exists} & $\exists$\\
%     \cs{forall} & $\forall$\\
%    \end{tabular}
%   \end{syntax}
%  \end{function}
%
% \clearpage
% \subsection{CMFTBL extension}
% \label{sec:cmftbl_extension}
%  \emph{CMFTBL} extends \emph{MFOTL} by the operators \emph{minPrevalence},
%  \emph{maxPrevalence}, their past forms, and the \emph{bind} operator.
%
%  \begin{function}{
%   \cminprevalence,
%   \cpastminprevalence,
%   \cmaxprevalence,
%   \cpastmaxprevalence,
%   \cbind}
%   \begin{syntax}
%    \begin{tabular}{lc}
%     \cs{cminprevalence}\marg{Percentage}\oarg{Interval} &
%     $\cminprevalence{0.8}[[0,1]]$\\
%     \cs{cpastminprevalence}\marg{Percentage}\oarg{Interval} &
%     $\cpastminprevalence{0.8}[[0,1]]$\\
%     \cs{cmaxprevalence}\marg{Percentage}\oarg{Interval} &
%     $\cmaxprevalence{0.8}[[0,1]]$\\
%     \cs{cpastmaxprevalence}\marg{Percentage}\oarg{Interval} &
%     $\cpastmaxprevalence{0.8}[[0,1]]$\\
%     \cs{cbind}\marg{Valuation}\marg{Variable} &
%     $\cbind{v.id}{i}$\\
%    \end{tabular}
%   \end{syntax}
%  \end{function}
%
%  \noindent The semantics of the operators are defined as follows. Let $p$ be a
%  fraction of states in the interval $[0,1]$:
%  \begin{itemize}
%   \item $\cminprevalence{p}[I] \phi$ expresses that $\phi$ must hold in at
%   least fraction $p$ of the future states in the interval $I$.
%   \item $\cpastminprevalence{p}[I] \phi$ expresses that $\phi$ must have held
%   in at least fraction $p$ of the past states in the interval $I$.
%   \item $\cmaxprevalence{p}[I] \phi$ expresses that $\phi$ must hold in at
%   most fraction $p$ of the future states in the interval $I$.
%   \item $\cpastmaxprevalence{p}[I] \phi$ expresses that $\phi$ must have held
%   in at most fraction $p$ of the past states in the interval $I$.
%   \item $\cbind{v.id}{i}$ saves the valuation $v.id$ to the variable $i$ for
%   later use in a nested formula, where $v$ already has a new value.
%  \end{itemize}
%
%  \emph{minPrevalence} and \emph{maxPrevalence} take the desired precentage as
%  another mandatory parameter. These operators may only be defined on finite
%  traces since they argue about numbers of states. \emph{bind} has no optional
%  interval but two mandatory arguments: the value to bind and the target
%  variable.
%
% \section{Usage in formulas}
% \label{sec:usage}
%  The commands may be directly used in math mode to create composite formulas.
%  For the unary formulas, the term $\phi$ should directly follow the symbol:
%  \begin{syntax}
%   \begin{tabular}{ll}
%    \cs{ceventually}\cs{phi} & $\ceventually \phi$\\
%    \cs{cglobally}[[0,1]]\cs{phi} & $\cglobally[[0,1]] \phi$
%   \end{tabular}
%  \end{syntax}
%
%  \noindent The binary symbols \emph{until} and \emph{since} should be used
%  with two formulas $\phi$ and $\psi$ directly before and after the symbol:
%  \begin{syntax}
%   \begin{tabular}{ll}
%    \cs{phi}\cs{cuntil}\cs{psi} & $\phi \cuntil \psi$\\
%    \cs{phi}\cs{csince}[[0,1]]\cs{psi} & $\phi \csince[[0,1]] \psi$
%   \end{tabular}
%  \end{syntax}
%
% \noindent
% The new \emph{CMFTBL} operators my be used as the unary ones:
% \begin{syntax}
% \begin{tabular}{ll}
%   \cs{cminprevalence}\{0.8\}\cs{phi} &
%   $\cminprevalence{0.8} \phi$\\
%   \cs{cmaxprevalence}\{0.8\}[[0,1]]\cs{phi} &
%   $\cmaxprevalence{0.8}[[0,1]] \phi$\\
%   \cs{cbind}\{v.id\}\{i\}\cs{phi} &
%   $\cbind{v.id}{i} \phi$
% \end{tabular}
% \end{syntax}
%
% \section{Standalone symbols}
% \label{sec:standalone_symbols}
% The package defines all symbols as a standalone version as
% \emph{MathOperators} without additional spacing around for the usage in text.
%
% \begin{function}{
%   \csymbeventually,
%   \csymbonce,
%   \csymbglobally,
%   \csymbhistorically,
%   \csymbnext,
%   \csymbprevious,
%   \csymbuntil,
%   \csymbsince,
%   \csymbminprevalence,
%   \csymbpastminprevalence,
%   \csymbmaxprevalence,
%   \csymbpastmaxprevalence,
%   \csymbbind}
%   \begin{syntax}
%   \begin{tabular}{lc}
%     \cs{csymbeventually} & $\csymbeventually$\\
%     \cs{csymbonce} & $\csymbonce$\\
%     \cs{csymbglobally} & $\csymbglobally$\\
%     \cs{csymbhistorically} & $\csymbhistorically$\\
%     \cs{csymbnext} & $\csymbnext$\\
%     \cs{csymbprevious} & $\csymbprevious$\\
%     \cs{csymbuntil} & $\csymbuntil$\\
%     \cs{csymbsince} & $\csymbsince$\\
%     \cs{csymbminprevalence} & $\csymbminprevalence$\\
%     \cs{csymbpastminprevalence} & $\csymbpastminprevalence$\\
%     \cs{csymbmaxprevalence} & $\csymbmaxprevalence$\\
%     \cs{csymbpastmaxprevalence} & $\csymbpastmaxprevalence$\\
%     \cs{csymbbind} & $\csymbbind$
% \end{tabular}
% \end{syntax}
% \end{function}
%
% \section{Operator scaling}
% \label{sec:operator_scaling}
% The operators scale automatically with the current text size:\\[\baselineskip]
%
% \begin{tabular}{ll}
%   \Huge\cs{Huge} & \Huge$\ceventually[[0,1]] \phi$\\
%   \huge\cs{huge} & \huge$\ceventually[[0,1]] \phi$\\
%   \LARGE\cs{LARGE} & \LARGE$\ceventually[[0,1]] \phi$\\
%   \Large\cs{Large} & \Large$\ceventually[[0,1]] \phi$\\
%   \large\cs{large} & \large$\ceventually[[0,1]] \phi$\\
%   \normalsize\cs{normalsize} & \normalsize$\ceventually[[0,1]] \phi$\\
%   \small\cs{small} & \small$\ceventually[[0,1]] \phi$\\
%   \footnotesize\cs{footnotesize} & \footnotesize$\ceventually[[0,1]] \phi$\\
%   \scriptsize\cs{scriptsize} & \scriptsize$\ceventually[[0,1]] \phi$\\
%   \tiny\cs{tiny} & \tiny$\ceventually[[0,1]] \phi$
% \end{tabular}
%
% \normalsize
% \clearpage
%
% \section{License}
% \begin{center}
%   Copyright (C) 2024\\
%   Dominik Schmid and Till Schallau\\[\baselineskip]
%
%   This work may be distributed and/or modified under the conditions of the\\ %   \LaTeX~Project Public License, either version 1.3c of this license\\
%   or (at your option) any later version.\\[\baselineskip]
%
%   The latest version of this license is in
%   \url{http://www.latex-project.org/lppl.txt}\\
%   and version 1.3c or later is part of all distributions of
%   \LaTeX~version 2005/12/01 or later.\\[\baselineskip]
%
%   This work has the LPPL maintenance status ''maintained''.\\[\baselineskip]
%
%   The current maintainer of this work is\\
%   Dominik Schmid <\href{mailto:dominik.schmid@tu-dortmund.de}
%   {dominik.schmid@tu-dortmund.de>}.\\[\baselineskip]
%
%   This work consists of the files temporal-logic.dtx, temporal-logic.ins,\\
%   and the derived file temporal-logic.sty.
% \end{center}
% \section{Sourcecode}
% \label{sec:sourcecode}
% \end{documentation}
% \begin{implementation}
%    \begin{macrocode}
% <*package>
% <@@=cmftbl>

\RequirePackage{amsmath}
\RequirePackage{expl3}
\RequirePackage{xparse}
\RequirePackage{tikz}

\ProvidesExplPackage {temporal-logic} { 2024-10-17 } { v1.0 }{
  Symbols for Temporal Logics
}

\cs_new:Nn \__@@_op_sup_sub:Nnn {
      \ensuremath {
        #1
        \tl_if_empty:nF { #2 } { \c_math_superscript_token { \,#2 } }
        \tl_if_empty:nF { #3 } { \c_math_subscript_token { \,#3 } }
        \,
      }
}
\cs_generate_variant:Nn \__@@_op_sup_sub:Nnn { cnn }

\cs_new:Nn \__@@_op_sup:Nn { \__@@_op_sup_sub:Nnn { #1 } { #2 } {} }
\cs_generate_variant:Nn \__@@_op_sup:Nn { cn }

\cs_new:Nn \__@@_op_sub:Nn { \__@@_op_sup_sub:Nnn { #1 } { } { #2 } }
\cs_generate_variant:Nn \__@@_op_sub:Nn { cn }

\cs_new:Nn \__@@_op:N { \__@@_op_sup_sub:Nnn { #1 } { } { } }
\cs_generate_variant:Nn \__@@_op:N { c }

\dim_new:N \__@@_fht_dim
\cs_new:Nn \__@@_ex: { \dim_use:N \__@@_fht_dim }

\cs_new:Nn \__@@_render_op:n {
  \dim_set:Nn \__@@_fht_dim {\fontcharht\font`X}
  \tikz[execute~at~end~picture={
       \useasboundingbox (0, 0) rectangle (\__@@_ex:, \__@@_ex:);
  }]{
    \group_begin:
      \cs_set_eq:NN \EX \__@@_ex:
      #1
    \group_end:
  }
}

\DeclareMathOperator { \csymbeventually } {
  \__@@_render_op:n {
     \draw
       (.5*\EX, 0) --
       (.2*\EX, .5*\EX) --
       (.5*\EX, \EX) --
       (.8*\EX, .5*\EX) --
       cycle;
  }
}
\DeclareMathOperator { \csymbonce } {
  \__@@_render_op:n {
    \draw[fill]
    (.5*\EX, 0) --
    (.2*\EX, .5*\EX) --
    (.5*\EX, \EX) --
    (.8*\EX, .5*\EX) --
    cycle;
}
}
\DeclareMathOperator { \csymbglobally } {
  \__@@_render_op:n {
    \draw
    (.15*\EX, .15*\EX)
    rectangle
    (.85*\EX, .85*\EX);
  }
}
\DeclareMathOperator { \csymbhistorically } {
  \__@@_render_op:n {
    \draw[fill]
    (.15*\EX, .15*\EX)
    rectangle
    (.85*\EX, .85*\EX);
  }
}
\DeclareMathOperator { \csymbnext } {
  \__@@_render_op:n {
    \draw
    (.5*\EX, .5*\EX)
    circle
    (.4*\EX);
  }
}
\DeclareMathOperator { \csymbprevious } {
  \__@@_render_op:n {
    \draw[fill]
    (.5*\EX, .5*\EX)
    circle
    (.4*\EX);
  }
}
\DeclareMathOperator { \csymbuntil } {
  \ensuremath\mathcal{U}
}
\DeclareMathOperator { \csymbsince } {
  \ensuremath\mathcal{S}
}
\DeclareMathOperator { \csymbminprevalence } {
  \__@@_render_op:n {
    \draw
      (.1*\EX, .9*\EX) --
      (.9*\EX, .9*\EX) --
      (.5*\EX, .1*\EX) --
      cycle;
  }
}
\DeclareMathOperator { \csymbpastminprevalence } {
  \__@@_render_op:n {
    \draw[fill]
    (.1*\EX, .9*\EX) --
    (.9*\EX, .9*\EX) --
    (.5*\EX, .1*\EX) --
    cycle;
  }
}
\DeclareMathOperator { \csymbmaxprevalence } {
  \__@@_render_op:n {
    \draw
    (.1*\EX, .1*\EX) --
    (.9*\EX, .1*\EX) --
    (.5*\EX, .9*\EX) --
    cycle;
}
  }
\DeclareMathOperator { \csymbpastmaxprevalence } {
  \__@@_render_op:n {
    \draw[fill]
    (.1*\EX, .1*\EX) --
    (.9*\EX, .1*\EX) --
    (.5*\EX, .9*\EX) --
    cycle;
  }
}
\DeclareMathOperator { \csymbbind } {
  \__@@_render_op:n {
    \draw (.5*\EX, \EX) -- (.5*\EX, 0);
    \draw
      (.2*\EX, .3*\EX) ..
      controls (.4*\EX, .2*\EX) ..
      (.5*\EX, 0) ..
      controls (.6*\EX, .2*\EX) ..
      (.8*\EX, .3*\EX);
  }
}

\ProvideDocumentCommand { \ceventually } { O{} } {
  \__@@_op_sub:cn { csymbeventually } { #1 }
}
\ProvideDocumentCommand { \conce } { O{} } {
  \__@@_op_sub:cn { csymbonce } { #1 }
}
\ProvideDocumentCommand { \cglobally } { O{} } {
  \__@@_op_sub:cn { csymbglobally } { #1 }
}
\ProvideDocumentCommand { \chistorically } { O{} } {
  \__@@_op_sub:cn { csymbhistorically } { #1 }
}
\ProvideDocumentCommand { \cnext } { O{} } {
  \__@@_op_sub:cn { csymbnext } { #1 }
}
\ProvideDocumentCommand { \cprevious } { O{} } {
  \__@@_op_sub:cn { csymbprevious } { #1 }
}
\ProvideDocumentCommand { \cuntil } { O{} } {
  \__@@_op_sub:Nn { \;\csymbuntil } { #1 }
}
\ProvideDocumentCommand { \csince } { O{} } {
  \__@@_op_sub:Nn { \;\csymbsince } { #1 }
}
\ProvideDocumentCommand { \cminprevalence } { m O{} } {
  \__@@_op_sup_sub:cnn { csymbminprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \cpastminprevalence } { m O{} } {
  \__@@_op_sup_sub:cnn { csymbpastminprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \cmaxprevalence } { m O{} } {
  \__@@_op_sup_sub:cnn { csymbmaxprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \cpastmaxprevalence } { m O{} } {
  \__@@_op_sup_sub:cnn { csymbpastmaxprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \cbind } { m m } {
  \__@@_op_sup_sub:cnn { csymbbind } { #1 } { #2 }
}
% </package>
%    \end{macrocode}
% \end{implementation}