% \iffalse meta-comment
%
% File: temporal-logic.dtx
%
% Copyright (C) 2026 Dominik Schmid
%
% 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}
\usepackage{tabularray}
\begin{document}
  \DocInput{\jobname.dtx}
\end{document}
%</driver>
% \fi
%
% \title{temporal-logic}
% \author{Dominik Schmid}
% \date{Version 1.0}
%
% \maketitle
% \setlength{\parindent}{0ex}
% \tolerance=1
% \emergencystretch=\maxdimen
% \hyphenpenalty=10000
% \hbadness=10000
%
% \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{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.
%
%  The symbols come in two variants: A standalone version for mentioning logic
%  symbols in text without additional formula spacing and a formula version,
%  also providing additional parameters. 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 ``tl'' for \textit{temporal logic}. Standalone symbols, as
%  described in Sect.~\ref{sec:standalone_symbols}, are prefixed with
%  ``tlop''. Those prefixes are necessary to prevent name clashes with
%  built-in \LaTeX{} commands.
%
% \subsection{Package options}
%  \label{sec:options}
%  Each operator is available as a \emph{bold}, \emph{calligraphic}, and
%  \emph{symbolic} version (if available). Details are described in
%  sections~\ref{sec:future_ltl}--\ref{sec:additional_operators} The displayed
%  version can be switched by passing an optional package option:
%
%  \begin{function}{
%   displaymode=bold,
%   displaymode=caligraphic,
%   displaymode=symbol}
%   \begin{syntax}
%    Bold display mode
%    Caligraphic display mode
%    Symbol display mode (default)
%   \end{syntax}
%  \end{function}
%
%  For brevity, \texttt{displaymode=} can be omitted.
%
%  The superscripts and subscripts are automatically captured by
%  \texttt{mathrm} / \texttt{mathit}. To switch bewteen roman and italic
%  display, the \texttt{scriptmode} can be passed:
%
%  \begin{function}{
%   scriptmode=roman,
%   scriptmode=italic}
%   \begin{syntax}
%    Roman script mode (default)
%    Italic script mode
%   \end{syntax}
%  \end{function}
%
%  For brevity, \texttt{scriptmode=} can be omitted. This setting can be
%  locally overridden by capturing the individual parameters into another
%  \texttt{mathrm} / \texttt{mathit}.
%
% \subsection{Manual structure}
%  This manual is structured as follows. First, the symbols for \emph{Future
%  LTL} and \emph{Past LTL} are introduced 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}.
%  Additional operators are defined in Sect.~\ref{sec:additional_operators}.
%  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.
%
% \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}{
%   \tlnext,
%   \tlfinally,
%   \tleventually,
%   \tlglobally,
%   \tluntil,
%   \tlrelease,
%   \tlweakuntil,
%   \tlstrongrelease,
%   \tlmightyrelease}
%   \begin{syntax}
%    \cs{tlnext} \cs{varphi}
%    \cs{tlfinally} \cs{varphi}
%    \cs{tleventually} \cs{varphi}
%    \cs{tlglobally} \cs{varphi}
%    \cs{varphi} \cs{tluntil} \cs{psi}
%    \cs{psi} \cs{tlrelease} \cs{varphi}
%    \cs{varphi} \cs{tlweakuntil} \cs{psi}
%    \cs{psi} \cs{tlstrongrelease} \cs{varphi}
%    \cs{psi} \cs{tlmightyrelease} \cs{varphi}
%   \end{syntax}
%  \end{function}
%
%  \noindent
%  The symbols get rendered according to the selected display mode
%  (cf.~Sect.~\ref{sec:options}). The symbols and the common semantics of the
%  operators are listed below:
%
%  \vspace{\baselineskip}
%  \noindent
%  \begin{tblr}{
%   colspec={lcccX},
%   width=\textwidth,
%   rowsep={3pt}
%  }
%   \textbf{Command} &
%   \textbf{Bold} &
%   \textbf{Textual} &
%   \textbf{Symbolic} &
%   \textbf{Semantics}\\
%
%   \cs{tlnext} &
%   $\tlboldnext \varphi$ &
%   $\tlletternext \varphi$ &
%   $\tlsymbnext \varphi$ &
%   $\varphi$ must hold at the next state.\\
%
%   {\cs{tlfinally} \\ \cs{tleventually}} &
%   {$\tlboldfinally \varphi$} &
%   {$\tlletterfinally \varphi$} &
%   {$\tlsymbfinally \varphi$} &
%   $\varphi$ must hold at least once in the future.\\
%
%   \cs{tlglobally}   &
%   $\tlboldglobally \varphi$ &
%   $\tlletterglobally \varphi$ &
%   $\tlsymbglobally \varphi$ &
%   $\varphi$ must hold from now for the entire trace.\\
%
%   \cs{tluntil} &
%   $\varphi \tlbolduntil \psi$ &
%   $\varphi \tlletteruntil \psi$ &
%   $\varphi \tlsymbuntil \psi$ &
%   $\varphi$ must hold at least until $\psi$ holds, which must hold at the
%   current or a future position.\\
%
%   \cs{tlrelease} &
%   $\psi \tlboldrelease \varphi$ &
%   $\psi \tlletterrelease \varphi$ & $\psi \tlsymbrelease \varphi$ &
%   $\varphi$ must hold until and including the point where $\psi$ first
%   becomes true. If $\psi$ never becomes true, $\varphi$ must remain true
%   for the entire trace.\\
%
%   \cs{tlweakuntil} &
%   $\varphi \tlboldweakuntil \psi$ &
%   $\varphi \tlletterweakuntil \psi$ & $\varphi \tlsymbweakuntil \psi$ &
%   $\varphi$ must hold at least until $\psi$ holds. If $\psi$ never
%   becomes true, $\phi$ must remain true for the entire trace.\\
%
%   {\cs{tlstrongrelease} \\ \cs{tlmightyrelease}} &
%   $\psi \tlboldstrongrelease \varphi$ &
%   $\psi \tlletterstrongrelease \varphi$ &
%   $\psi \tlsymbstrongrelease \varphi$ &
%   $\varphi$ must hold until and including the point where $\psi$ first
%   becomes true, which must hold at the current or a future position.\\
%  \end{tblr}
%
% \clearpage
% \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}{
%   \tlyesterday,
%   \tlprevious,
%   \tlonce,
%   \tlhistorically,
%   \tlsince,
%   \tlbackto,
%   \tlweaksince,
%   \tltrigger}
%   \begin{syntax}
%    \cs{tlyesterday} \cs{varphi}
%    \cs{tlprevious} \cs{varphi}
%    \cs{tlonce} \cs{varphi}
%    \cs{tlhistorically} \cs{varphi}
%    \cs{varphi} \cs{tlsince} \cs{psi}
%    \cs{psi} \cs{backto} \cs{varphi}
%    \cs{varphi} \cs{tlweaksince} \cs{psi}
%    \cs{psi} \cs{tltrigger} \cs{varphi}
%   \end{syntax}
%  \end{function}
%
%  \vspace{\baselineskip}
%  \noindent
%  \begin{tblr}{
%   colspec={lcccX},
%   width=\textwidth,
%   rowsep={3pt}
%  }
%   \textbf{Command} &
%   \textbf{Bold} &
%   \textbf{Textual} &
%   \textbf{Symbolic} &
%   \textbf{Semantics}\\
%
%   {\cs{tlyesterday} \\ \cs{tlprevious}} &
%   $\tlboldyesterday \varphi$ &
%   $\tlletteryesterday \varphi$ &
%   $\tlsymbyesterday \varphi$ &
%   $\varphi$ must have held at the previous state.\\
%
%   \cs{tlonce} &
%   $\tlboldonce \varphi$ &
%   $\tlletteronce \varphi$  &
%   $\tlsymbonce \varphi$  &
%   $\varphi$ must have held at least once in the past.\\
%
%   \cs{tlhistorically} &
%   $\tlboldhistorically \varphi$ &
%   $\tlletterhistorically \varphi$  &
%   $\tlsymbhistorically \varphi$ &
%   $\varphi$ must have held until now for the entire past trace.\\
%
%   \cs{tlsince} &
%   $\varphi \tlboldsince \psi$ &
%   $\tllettersince \varphi$  &
%   $\tllettersince \varphi$ &
%   $\varphi$ must have held since $\psi$ has held, which must have held at
%   the current or a past state.\\
%
%   \cs{tlbackto} &
%   $\psi \tlboldbackto \varphi$ &
%   $\tlletterbackto \varphi$  &
%   $\tlsymbbackto \varphi$  &
%   $\varphi$ must have held since and including the point where $\psi$ was
%   true the last time. If $\psi$ never was true, $\varphi$ must have been
%   true for the entire past trace.\\
%
%   \cs{tlweaksince} &
%   $\varphi \tlboldweaksince \psi$ &
%   $\tlletterweaksince \varphi$  &
%   $\tlsymbweaksince \varphi$ &
%   $\varphi$ must have held since $\psi$ has held. If $\psi$ never was true,
%   $\varphi$ must have been true for the entire past trace.\\
%
%   \cs{tltrigger} &
%   $\psi \tlboldtrigger \varphi$ &
%   $\tllettertrigger \varphi$  & $\tlsymbtrigger \varphi$ &
%   $\varphi$ must have held since and including the point where $\psi$ was
%   true the last time, which must have held at the current or a past state.\\
%  \end{tblr}
%
% \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{full MTL}, or simply \emph{MTL}.
%  \begin{function}{
%   \tlnext,
%   \tlfinally,
%   \tleventually,
%   \tlglobally,
%   \tluntil,
%   \tlrelease,
%   \tlweakuntil,
%   \tlstrongrelease,
%   \tlmightyrelease,
%   \tlyesterday,
%   \tlprevious,
%   \tlonce,
%   \tlhistorically,
%   \tlsince,
%   \tlbackto,
%   \tlweaksince,
%   \tltrigger}
%   \begin{syntax}
%    \begin{tabular}{lc}
%     \cs{tlnext}\oarg{Interval} & $\tlnext[[0,1]]$\\
%     \cs{tlfinally}\oarg{Interval} & $\tlfinally[[0,1]]$\\
%     \cs{tleventually}\oarg{Interval} & $\tleventually[[0,1]]$\\
%     \cs{tlglobally}\oarg{Interval} & $\tlglobally[[0,1]]$\\
%     \cs{tluntil}\oarg{Interval} & $\tluntil[[0,1]]$\\
%     \cs{tlrelease}\oarg{Interval} & $\tlrelease[[0,1]]$\\
%     \cs{tlweakuntil}\oarg{Interval} & $\tlweakuntil[[0,1]]$\\
%     \cs{tlstrongrelease}\oarg{Interval} & $\tlstrongrelease[[0,1]]$\\
%     \cs{tlmightyrelease}\oarg{Interval} & $\tlmightyrelease[[0,1]]$\\
%     \cs{tlyesterday}\oarg{Interval} & $\tlyesterday[[0,1]]$\\
%     \cs{tlprevious}\oarg{Interval} & $\tlprevious[[0,1]]$\\
%     \cs{tlonce}\oarg{Interval} & $\tlonce[[0,1]]$\\
%     \cs{tlhistorically}\oarg{Interval} & $\tlhistorically[[0,1]]$\\
%     \cs{tlsince}\oarg{Interval} & $\tlsince[[0,1]]$\\
%     \cs{tlbackto}\oarg{Interval} & $\tlbackto[[0,1]]$\\
%     \cs{tlweaksince}\oarg{Interval} & $\tlweaksince[[0,1]]$\\
%     \cs{tltrigger}\oarg{Interval} & $\tltrigger[[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. Unmatched brackets can be
%  generated using an extra group: \cs{tlnext[\{[0,$\infty$)\}]} $\implies
%  \tlnext[{[0,\infty)}]$.
%
% \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}{
%   \tlminprevalence,
%   \tlpastminprevalence,
%   \tlmaxprevalence,
%   \tlpastmaxprevalence,
%   \tlbind}
%   \begin{syntax}
%    \begin{tabular}{lc}
%     \cs{tlminprevalence}\marg{Percentage}\oarg{Interval} &
%     $\tlminprevalence{0.8}[[0,1]]$\\
%
%     \cs{tlpastminprevalence}\marg{Percentage}\oarg{Interval} &
%     $\tlpastminprevalence{0.8}[[0,1]]$\\
%
%     \cs{tlmaxprevalence}\marg{Percentage}\oarg{Interval} &
%     $\tlmaxprevalence{0.8}[[0,1]]$\\
%
%     \cs{tlpastmaxprevalence}\marg{Percentage}\oarg{Interval} &
%     $\tlpastmaxprevalence{0.8}[[0,1]]$\\
%
%     \cs{tlbind}\marg{Valuation}\marg{Variable} &
%     $\tlbind{v.id}{i}$\\
%    \end{tabular}
%   \end{syntax}
%  \end{function}
%
%  \noindent
%  The symbols only have a symbolic representation and get rendered
%  independent from the selected display mode (cf.~Sect.~\ref{sec:options}).
%  The symbols and the semantics of the operators are listed below:
%
%  \vspace{\baselineskip}
%  \noindent
%  \begin{tblr}{
%   colspec={lcX},
%   width=\textwidth,
%   rowsep={3pt}
%  }
%   \textbf{Command} &
%   \textbf{Symbolic} &
%   \textbf{Semantics}\\
%
%   \cs{tlminprevalence} &
%   $\tlminprevalence{p}[I] \varphi$ & $\varphi$ must hold in at least
%   fraction $p$ of the future states in the interval $I$.\\
%
%   \cs{tlpastminprevalence} &
%   $\tlpastminprevalence{p}[I] \varphi$ & $\varphi$ must have held in at
%   least fraction $p$ of the past states in the interval $I$.\\
%
%   \cs{tlmaxprevalence} &
%   $\tlmaxprevalence{p}[I] \varphi$ & $\varphi$ must hold in at most
%   fraction $p$ of the future states in the interval $I$.\\
%
%   \cs{tlpastmaxprevalence} &
%   $\tlpastmaxprevalence{p}[I] \varphi$ & $\varphi$ must have held in at
%   most fraction $p$ of the past states in the interval $I$.\\
%
%   \cs{tlbind} &
%   $\tlbind{v.id}{i}$ &
%   Saves the valuation $v.\mathrm{id}$ to the variable $i$ for later use in
%   a nested formula, where $v$ already has a new value.
%  \end{tblr}
%
%  \noindent
%  \emph{minPrevalence} and \emph{maxPrevalence} take the desired percentage
%  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.
%
% \clearpage
% \subsection{Additional operators}
%  \label{sec:additional_operators}
%  For convenience, the package contains four additional operators:
%
%  \begin{function}{
%   \tlrise,
%   \tlfall,
%   \tlprophecy,
%   \tlhistory}
%   \begin{syntax}
%    \cs{tlrise} \cs{varphi}
%    \cs{tlfall} \cs{varphi}
%    \cs{tlprophecy} \cs{varphi}
%    \cs{tlhistory} \cs{varphi}
%   \end{syntax}
%  \end{function}
%
%  \noindent
%  The symbols only have a symbolic representation and get rendered
%  independent from the selected display mode (cf.~Sect.~\ref{sec:options}).
%  The symbols and the semantics of the operators are listed below:
%
%  \vspace{\baselineskip}
%  \noindent
%  \begin{tblr}{
%   colspec={lcX},
%   width=\textwidth,
%   rowsep={3pt}
%  }
%   \textbf{Command} &
%   \textbf{Symbolic} &
%   \textbf{Semantics}\\
%
%   \cs{tlrise} &
%   $\tlrise \varphi$ &
%   Holds when $\varphi$ becomes true, i.e. $\varphi$ holds at this time but
%   did not hold in the immediate past.\\
%
%   \cs{tlfall} &
%   $\tlfall \varphi$ &
%   Holds when $\varphi$ becomes false, i.e. $\varphi$ does not hold at this
%   time but held in the immediate past.\\
%
%   \cs{tlprophecy} &
%   $\tlprophecy \varphi$ &
%   Holds when there exists a first moment in the future where $\varphi$
%   holds, and the moment is in the interval.\\
%
%   \cs{tlhistory} &
%   $\tlhistory \varphi$ &
%   Holds when there exists a last moment in the past where $\varphi$ held,
%   and the moment is in the interval.
%  \end{tblr}
%
% \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 $\varphi$ should directly
%  follow the symbol:
%  \begin{syntax}
%   \begin{tabular}{ll}
%    \cs{tleventually}\cs{varphi} & $\tleventually \varphi$\\
%    \cs{tlglobally}[[0,1]]\cs{varphi} & $\tlglobally[[0,1]] \varphi$
%   \end{tabular}
%  \end{syntax}
%
%  \noindent The binary symbols like \emph{until} should be used with two
%  formulas $\varphi$ and $\psi$ directly before and after the symbol:
%  \begin{syntax}
%   \begin{tabular}{ll}
%    \cs{varphi}\cs{tluntil}\cs{psi} & $\varphi \tluntil \psi$\\
%    \cs{varphi}\cs{tluntil}[[0,1]]\cs{psi} & $\varphi \tluntil[[0,1]] \psi$
%   \end{tabular}
%  \end{syntax}
%
%  \noindent
%  The \emph{CMFTBL} operators may be used as the unary ones:
%  \begin{syntax}
%   \begin{tabular}{ll}
%    \cs{tlminprevalence}\{0.8\}\cs{varphi} &
%    $\tlminprevalence{0.8} \varphi$\\
%
%    \cs{tlpastmaxprevalence}\{0.8\}[[0,1]]\cs{varphi} &
%    $\tlmaxprevalence{0.8}[[0,1]] \varphi$\\
%
%    \cs{tlbind}\{v.id\}\{i\}\cs{varphi} &
%    $\tlbind{v.id}{i} \varphi$
%   \end{tabular}
%  \end{syntax}
%
% \clearpage
% \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}{
%   \tlopnext,
%   \tlopfinally,
%   \tlopeventually,
%   \tlopglobally,
%   \tlopuntil,
%   \tloprelease,
%   \tlopweakuntil,
%   \tlopstrongrelease,
%   \tlopmightyrelease,
%   \tlyesterday,
%   \tlprevious,
%   \tlonce,
%   \tlhistorically,
%   \tlsince,
%   \tlbackto,
%   \tlweaksince,
%   \tltrigger,
%   \tlopminprevalence,
%   \tloppastminprevalence,
%   \tlopmaxprevalence,
%   \tloppastmaxprevalence,
%   \tlopbind,
%   \tloprise,
%   \tlopfall,
%   \tlopprophecy,
%   \tlophistory}
%   \begin{syntax}
%    \begin{tabular}{lc}
%     \cs{tlopnext} & $\tlopnext$\\
%     \cs{tlopfinally} & $\tlopfinally$\\
%     \cs{tlopeventually} & $\tlopeventually$\\
%     \cs{tlopglobally} & $\tlopglobally$\\
%     \cs{tlopuntil} & $\tlopuntil$\\
%     \cs{tloprelease} & $\tloprelease$\\
%     \cs{tlopweakuntil} & $\tlopweakuntil$\\
%     \cs{tlopstrongrelease} & $\tlopstrongrelease$\\
%     \cs{tlopmightyrelease} & $\tlopmightyrelease$\\
%     \cs{tlopyesterday} & $\tlopyesterday$\\
%     \cs{tlopprevious} & $\tlopprevious$\\
%     \cs{tloponce} & $\tloponce$\\
%     \cs{tlophistorically} & $\tlophistorically$\\
%     \cs{tlopsince} & $\tlopsince$\\
%     \cs{tlopbackto} & $\tlopbackto$\\
%     \cs{tlopweaksince} & $\tlopweaksince$\\
%     \cs{tloptrigger} & $\tloptrigger$\\
%     \cs{tlopminprevalence\{\}} & $\tlopminprevalence{}$\\
%     \cs{tloppastminprevalence\{\}} & $\tloppastminprevalence{}$\\
%     \cs{tlopmaxprevalence\{\}} & $\tlopmaxprevalence{}$\\
%     \cs{tloppastmaxprevalence\{\}} & $\tloppastmaxprevalence{}$\\
%     \cs{tlopbind\{\}\{\}} & $\tlopbind{}{}$\\
%     \cs{tloprise} & $\tloprise$\\
%     \cs{tlopfall} & $\tlopfall$\\
%     \cs{tlopprophecy} & $\tlopprophecy$\\
%     \cs{tlophistory} & $\tlophistory$\\
%    \end{tabular}
%   \end{syntax}
%  \end{function}
%
% \section{Dependencies}
%  The package loads the following dependencies:
%  \begin{itemize}
%   \item \emph{expl3} For \LaTeX 3 support.
%   \item \emph{l3keys2e} For package option parsing.
%   \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}
%  \normalsize
%
% \clearpage
% \section{License}
% \begin{center}
%  Copyright (C) 2026\\
%  Dominik Schmid\\[\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}
% \clearpage
% \section{Sourcecode}
%  \label{sec:sourcecode}
% \end{documentation}
% \begin{implementation}
%    \begin{macrocode}
% <*package>

\ProvidesExplPackage
 {temporal-logic}
 { 2026-01-06 }
 { v1.1 }
 { Symbols for Temporal Logics }

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

\ExplSyntaxOn

\msg_new:nnn { temporallogic } { multiple-display-modes }
{ Multiple~display~mode~options~given;~using~the~last~one. }

\msg_new:nnn { temporallogic } { multiple-script-modes }
{ Multiple~script~mode~options~given;~using~the~last~one. }

\int_new:N \g_temporallogic_display_mode_int
\int_new:N \g_temporallogic_script_mode_int
\int_new:N \g_temporallogic_display_mode_count_int
\int_new:N \g_temporallogic_script_mode_count_int
\int_const:Nn \c_temporallogic_display_mode_bold     { 1 }
\int_const:Nn \c_temporallogic_display_mode_letter   { 2 }
\int_const:Nn \c_temporallogic_display_mode_symbolic { 3 }
\int_const:Nn \c_temporallogic_script_mode_roman     { 1 }
\int_const:Nn \c_temporallogic_script_mode_italic    { 2 }

\keys_define:nn { temporallogic }
{
    displaymode .choice:,

    displaymode / bold .code:n =
    {
        \int_gset:Nn \g_temporallogic_display_mode_int
        { \c_temporallogic_display_mode_bold }
        \int_gincr:N \g_temporallogic_display_mode_count_int
    },

    displaymode / letter .code:n =
    {
        \int_gset:Nn \g_temporallogic_display_mode_int
        { \c_temporallogic_display_mode_letter }
        \int_gincr:N \g_temporallogic_display_mode_count_int
    },

    displaymode / symbolic .code:n =
    {
        \int_gset:Nn \g_temporallogic_display_mode_int
        { \c_temporallogic_display_mode_symbolic }
        \int_gincr:N \g_temporallogic_display_mode_count_int
    },

    % default
    displaymode .initial:n = symbolic,

    % short forms
    bold      .meta:n = { displaymode = bold },
    letter    .meta:n = { displaymode = letter },
    symbolic  .meta:n = { displaymode = symbolic },

    scriptmode .choice:,
    scriptmode / roman .code:n =
    {
        \int_gset:Nn \g_temporallogic_script_mode_int
        { \c_temporallogic_script_mode_roman }
        \int_gincr:N \g_temporallogic_script_mode_count_int
    },
    scriptmode / italic .code:n =
    {
        \int_gset:Nn \g_temporallogic_script_mode_int
        { \c_temporallogic_script_mode_italic }
        \int_gincr:N \g_temporallogic_script_mode_count_int
    },
    scriptmode .initial:n = roman,

    % short forms
    roman  .meta:n = { scriptmode = roman },
    italic .meta:n = { scriptmode = italic },
}

\ProcessKeysOptions { temporallogic }

\int_compare:nNnT { \g_temporallogic_display_mode_count_int } > { 2 }
{
    \msg_warning:nn { temporallogic } { multiple-display-modes }
}

\int_compare:nNnT { \g_temporallogic_script_mode_count_int } > { 2 }
{
    \msg_warning:nn { temporallogic } { multiple-script-modes }
}



\cs_new:Nn \__temporal_logic_op_sup_sub:Nnn {
      \ensuremath {
        #1
        \int_case:nnF { \g_temporallogic_script_mode_int }
        {
            {
                \c_temporallogic_script_mode_roman}  {
                    \tl_if_empty:nF { #2 } { \c_math_superscript_token
                        { \,\mathrm{#2} } }
                    \tl_if_empty:nF { #3 } { \c_math_subscript_token
                        { \,\mathrm{#3} } }
            }
            {
                \c_temporallogic_script_mode_italic} {
                    \tl_if_empty:nF { #2 } { \c_math_superscript_token
                        { \,\mathit{#2} } }
                    \tl_if_empty:nF { #3 } { \c_math_subscript_token
                        { \,\mathit{#3} } }
                }
            }{}
        \,
      }
}
\cs_generate_variant:Nn \__temporal_logic_op_sup_sub:Nnn { cnn }

\cs_new:Nn \__temporal_logic_op_sup:Nn
{ \__temporal_logic_op_sup_sub:Nnn { #1 } { #2 } {} }
\cs_generate_variant:Nn \__temporal_logic_op_sup:Nn { cn }

\cs_new:Nn \__temporal_logic_op_sub:Nn
{ \__temporal_logic_op_sup_sub:Nnn { #1 } { } { #2 } }
\cs_generate_variant:Nn \__temporal_logic_op_sub:Nn { cn }

\cs_new:Nn \__temporal_logic_op:N
{ \__temporal_logic_op_sup_sub:Nnn { #1 } { } { } }
\cs_generate_variant:Nn \__temporal_logic_op:N { c }

\dim_new:N \__temporal_logic_fht_dim
\cs_new:Nn \__temporal_logic_ex: { \dim_use:N \__temporal_logic_fht_dim }

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



\ProvideDocumentCommand \tldisplaymode {} {
    \int_case:nnF { \g_temporallogic_display_mode_int }
    {
        {\c_temporallogic_display_mode_bold}     { Bold }
        {\c_temporallogic_display_mode_letter}   { Letter }
        {\c_temporallogic_display_mode_symbolic} { Symbolic }
    }{}
}
\ProvideDocumentCommand \tlscriptmode {} {
    \int_case:nnF { \g_temporallogic_script_mode_int }
    {
        {\c_temporallogic_script_mode_roman}  { Roman }
        {\c_temporallogic_script_mode_italic} { Italic }
    }{}
}



% Next
\DeclareMathOperator { \tlboldnext } {
    \ensuremath\mathbf{X}
}
\DeclareMathOperator { \tlletternext } {
    \ensuremath\mathcal{X}
}
\DeclareMathOperator { \tlsymbnext } {
    \__temporal_logic_render_op:n {
        \draw
        (.5*\EX, .5*\EX)
        circle
        (.4*\EX);
    }
}
\ProvideDocumentCommand { \tlnext } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldnext }
            {\c_temporallogic_display_mode_letter}   { tlletternext }
            {\c_temporallogic_display_mode_symbolic} { tlsymbnext }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopnext } { } { \tlnext\! }



% Finally
\DeclareMathOperator { \tlboldfinally } {
    \ensuremath\mathbf{F}
}
\DeclareMathOperator { \tlletterfinally } {
    \ensuremath\mathcal{F}
}
\DeclareMathOperator { \tlsymbfinally } {
    \__temporal_logic_render_op:n {
        \draw
        (.5*\EX, 0) --
        (.2*\EX, .5*\EX) --
        (.5*\EX, \EX) --
        (.8*\EX, .5*\EX) --
        cycle;
    }
}
\ProvideDocumentCommand { \tlfinally } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldfinally }
            {\c_temporallogic_display_mode_letter}   { tlletterfinally }
            {\c_temporallogic_display_mode_symbolic} { tlsymbfinally }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopfinally } { } { \tlfinally\! }



% Eventually
\DeclareMathOperator { \tlboldeventually } { \tlboldfinally }
\DeclareMathOperator { \tllettereventually } { \tlletterfinally }
\DeclareMathOperator { \tlsymbeventually } { \tlsymbfinally }
\ProvideDocumentCommand { \tleventually } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldeventually }
            {\c_temporallogic_display_mode_letter}   { tllettereventually }
            {\c_temporallogic_display_mode_symbolic} { tlsymbeventually }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopeventually } { } { \tleventually\! }


% Globally
\DeclareMathOperator { \tlboldglobally } {
    \ensuremath\mathbf{G}
}
\DeclareMathOperator { \tlletterglobally } {
    \ensuremath\mathcal{G}
}
\DeclareMathOperator { \tlsymbglobally } {
    \__temporal_logic_render_op:n {
        \draw
        (.15*\EX, .15*\EX)
        rectangle
        (.85*\EX, .85*\EX);
    }
}
\ProvideDocumentCommand { \tlglobally } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldglobally }
            {\c_temporallogic_display_mode_letter}   { tlletterglobally }
            {\c_temporallogic_display_mode_symbolic} { tlsymbglobally }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopglobally } { } { \tlglobally\! }



% Until
\DeclareMathOperator { \tlbolduntil } {
    \medspace\ensuremath\mathbf{U}
}
\DeclareMathOperator { \tlletteruntil } {
    \medspace\ensuremath\mathcal{U}
}
\DeclareMathOperator { \tlsymbuntil } {
    \medspace\ensuremath\mathcal{U}
}
\ProvideDocumentCommand { \tluntil } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlbolduntil }
            {\c_temporallogic_display_mode_letter}   { tlletteruntil }
            {\c_temporallogic_display_mode_symbolic} { tlsymbuntil }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopuntil } { } { \negmedspace\tluntil\! }



% Release
\DeclareMathOperator { \tlboldrelease } {
    \medspace\ensuremath\mathbf{R}
}
\DeclareMathOperator { \tlletterrelease } {
    \medspace\ensuremath\mathcal{R}
}
\DeclareMathOperator { \tlsymbrelease } {
    \medspace\ensuremath\mathcal{R}
}
\ProvideDocumentCommand { \tlrelease } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldrelease }
            {\c_temporallogic_display_mode_letter}   { tlletterrelease }
            {\c_temporallogic_display_mode_symbolic} { tlsymbrelease }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tloprelease } { } { \negmedspace\tlrelease\! }



% Weak until
\DeclareMathOperator { \tlboldweakuntil } {
    \medspace\ensuremath\mathbf{W}
}
\DeclareMathOperator { \tlletterweakuntil } {
    \medspace\ensuremath\mathcal{W}
}
\DeclareMathOperator { \tlsymbweakuntil } {
    \medspace\ensuremath\mathcal{W}
}
\ProvideDocumentCommand { \tlweakuntil } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldweakuntil }
            {\c_temporallogic_display_mode_letter}   { tlletterweakuntil }
            {\c_temporallogic_display_mode_symbolic} { tlsymbweakuntil }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopweakuntil } { } { \negmedspace\tlweakuntil\! }



% Strong Release
\DeclareMathOperator { \tlboldstrongrelease } {
    \medspace\ensuremath\mathbf{M}
}
\DeclareMathOperator { \tlletterstrongrelease } {
    \medspace\ensuremath\mathcal{M}
}
\DeclareMathOperator { \tlsymbstrongrelease } {
    \medspace\ensuremath\mathcal{M}
}
\ProvideDocumentCommand { \tlstrongrelease } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldstrongrelease }
            {\c_temporallogic_display_mode_letter}   { tlletterstrongrelease }
            {\c_temporallogic_display_mode_symbolic} { tlsymbstrongrelease }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopstrongrelease } { }
{ \negmedspace\tlstrongrelease\! }



% Mighty Release
\DeclareMathOperator { \tlboldmightyrelease } { \tlboldstrongrelease }
\DeclareMathOperator { \tllettermightyrelease } { \tlletterstrongrelease }
\DeclareMathOperator { \tlsymbmightyrelease } { \tlsymbstrongrelease }
\ProvideDocumentCommand { \tlmightyrelease } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldmightyrelease }
            {\c_temporallogic_display_mode_letter}   { tllettermightyrelease }
            {\c_temporallogic_display_mode_symbolic} { tlsymbmightyrelease }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopmightyrelease } { }
{ \negmedspace\tlmightyrelease\! }



% Yesterday
\DeclareMathOperator { \tlboldyesterday } {
    \ensuremath\mathbf{Y}
}
\DeclareMathOperator { \tlletteryesterday } {
    \ensuremath\mathcal{Y}
}
\DeclareMathOperator { \tlsymbyesterday } {
    \__temporal_logic_render_op:n {
        \draw[fill]
        (.5*\EX, .5*\EX)
        circle
        (.4*\EX);
    }
}
\ProvideDocumentCommand { \tlyesterday } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldyesterday }
            {\c_temporallogic_display_mode_letter}   { tlletteryesterday }
            {\c_temporallogic_display_mode_symbolic} { tlsymbyesterday }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopyesterday } { } { \tlyesterday\! }



% Previous
\DeclareMathOperator { \tlboldprevious } { \tlboldyesterday }
\DeclareMathOperator { \tlletterprevious } { \tlletteryesterday }
\DeclareMathOperator { \tlsymbprevious } { \tlsymbyesterday }
\ProvideDocumentCommand { \tlprevious } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldprevious }
            {\c_temporallogic_display_mode_letter}   { tlletterprevious }
            {\c_temporallogic_display_mode_symbolic} { tlsymbprevious }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopprevious } { } { \tlprevious\! }


% Once
\DeclareMathOperator { \tlboldonce } {
    \ensuremath\mathbf{O}
}
\DeclareMathOperator { \tlletteronce } {
    \ensuremath\mathcal{O}
}
\DeclareMathOperator { \tlsymbonce } {
    \__temporal_logic_render_op:n {
        \draw[fill]
        (.5*\EX, 0) --
        (.2*\EX, .5*\EX) --
        (.5*\EX, \EX) --
        (.8*\EX, .5*\EX) --
        cycle;
    }
}
\ProvideDocumentCommand { \tlonce } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldonce }
            {\c_temporallogic_display_mode_letter}   { tlletteronce }
            {\c_temporallogic_display_mode_symbolic} { tlsymbonce }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tloponce } { } { \tlonce\! }



% Historically
\DeclareMathOperator { \tlboldhistorically } {
    \ensuremath\mathbf{H}
}
\DeclareMathOperator { \tlletterhistorically } {
    \ensuremath\mathcal{H}
}
\DeclareMathOperator { \tlsymbhistorically } {
    \__temporal_logic_render_op:n {
        \draw[fill]
        (.15*\EX, .15*\EX)
        rectangle
        (.85*\EX, .85*\EX);
    }
}
\ProvideDocumentCommand { \tlhistorically } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldhistorically }
            {\c_temporallogic_display_mode_letter}   { tlletterhistorically }
            {\c_temporallogic_display_mode_symbolic} { tlsymbhistorically }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlophistorically } { } { \tlhistorically\! }



% Since
\DeclareMathOperator { \tlboldsince } {
    \medspace\ensuremath\mathbf{S}
}
\DeclareMathOperator { \tllettersince } {
    \medspace\ensuremath\mathcal{S}
}
\DeclareMathOperator { \tlsymbsince } {
    \medspace\ensuremath\mathcal{S}
}
\ProvideDocumentCommand { \tlsince } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldsince }
            {\c_temporallogic_display_mode_letter}   { tllettersince }
            {\c_temporallogic_display_mode_symbolic} { tlsymbsince }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopsince } { } { \negmedspace\tlsince\!}



% Back to
\DeclareMathOperator { \tlboldbackto } {
    \medspace\ensuremath\mathbf{B}
}
\DeclareMathOperator { \tlletterbackto } {
    \medspace\ensuremath\mathcal{B}
}
\DeclareMathOperator { \tlsymbbackto } {
    \medspace\ensuremath\mathcal{B}
}
\ProvideDocumentCommand { \tlbackto } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldbackto }
            {\c_temporallogic_display_mode_letter}   { tlletterbackto }
            {\c_temporallogic_display_mode_symbolic} { tlsymbbackto }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopbackto } { } { \negmedspace\tlbackto\! }


% Weak Since
\DeclareMathOperator { \tlboldweaksince } {
    \medspace\ensuremath\mathbf{WS}
}
\DeclareMathOperator { \tlletterweaksince } {
    \medspace\ensuremath\mathcal{WS}
}
\DeclareMathOperator { \tlsymbweaksince } {
    \medspace\ensuremath\mathcal{WS}
}
\ProvideDocumentCommand { \tlweaksince } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldweaksince }
            {\c_temporallogic_display_mode_letter}   { tlletterweaksince }
            {\c_temporallogic_display_mode_symbolic} { tlsymbweaksince }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tlopweaksince } { } { \negmedspace\tlweaksince\! }



% Trigger
\DeclareMathOperator { \tlboldtrigger } {
    \medspace\ensuremath\mathbf{T}
}
\DeclareMathOperator { \tllettertrigger } {
    \medspace\ensuremath\mathcal{T}
}
\DeclareMathOperator { \tlsymbtrigger } {
    \medspace\ensuremath\mathcal{T}
}
\ProvideDocumentCommand { \tltrigger } { O{} } {
    \__temporal_logic_op_sub:cn {
        \int_case:nnF { \g_temporallogic_display_mode_int }
        {
            {\c_temporallogic_display_mode_bold}     { tlboldtrigger }
            {\c_temporallogic_display_mode_letter}   { tllettertrigger }
            {\c_temporallogic_display_mode_symbolic} { tlsymbtrigger }
        }{}
    } { #1 }
}
\ProvideDocumentCommand { \tloptrigger } { } { \negmedspace\tltrigger\! }



% Min-/Max prevalence
\DeclareMathOperator { \tlsymbminprevalence } {
    \__temporal_logic_render_op:n {
        \draw
        (.1*\EX, .9*\EX) --
        (.9*\EX, .9*\EX) --
        (.5*\EX, .1*\EX) --
        cycle;
    }
}
\DeclareMathOperator { \tlsymbpastminprevalence } {
    \__temporal_logic_render_op:n {
        \draw[fill]
        (.1*\EX, .9*\EX) --
        (.9*\EX, .9*\EX) --
        (.5*\EX, .1*\EX) --
        cycle;
    }
}
\DeclareMathOperator { \tlsymbmaxprevalence } {
    \__temporal_logic_render_op:n {
        \draw
        (.1*\EX, .1*\EX) --
        (.9*\EX, .1*\EX) --
        (.5*\EX, .9*\EX) --
        cycle;
    }
}
\DeclareMathOperator { \tlsymbpastmaxprevalence } {
    \__temporal_logic_render_op:n {
        \draw[fill]
        (.1*\EX, .1*\EX) --
        (.9*\EX, .1*\EX) --
        (.5*\EX, .9*\EX) --
        cycle;
    }
}
\ProvideDocumentCommand { \tlminprevalence } { m O{} } {
    \__temporal_logic_op_sup_sub:cnn { tlsymbminprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \tlpastminprevalence } { m O{} } {
    \__temporal_logic_op_sup_sub:cnn { tlsymbpastminprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \tlmaxprevalence } { m O{} } {
    \__temporal_logic_op_sup_sub:cnn { tlsymbmaxprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \tlpastmaxprevalence } { m O{} } {
    \__temporal_logic_op_sup_sub:cnn { tlsymbpastmaxprevalence } { #1 } { #2 }
}
\ProvideDocumentCommand { \tlopminprevalence } { m }
{ \tlminprevalence{#1}\! }
\ProvideDocumentCommand { \tloppastminprevalence } { m }
{ \tlpastminprevalence{#1}\! }
\ProvideDocumentCommand { \tlopmaxprevalence } { m }
{ \tlmaxprevalence{#1}\! }
\ProvideDocumentCommand { \tloppastmaxprevalence } { m }
{ \tlpastmaxprevalence{#1}\! }



% Bind
\DeclareMathOperator { \tlsymbbind } {
    \__temporal_logic_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 { \tlbind } { m m } {
    \__temporal_logic_op_sup_sub:cnn { tlsymbbind } { #1 } { #2 }
}
\ProvideDocumentCommand { \tlopbind } { m m } { \tlbind{ {#1} }{ {#2} } }



% Rise
\DeclareMathOperator { \tlsymbrise } {
    \__temporal_logic_render_op:n {
        \draw
        (.1*\EX, .1*\EX) --
        (.9*\EX, .9*\EX);
        \draw
        (.4*\EX, .9*\EX) --
        (.9*\EX, .9*\EX) --
        (.9*\EX, .4*\EX);
    }
}
\ProvideDocumentCommand { \tlrise } { O{} } {
    \__temporal_logic_op_sub:cn { tlsymbrise } { #1 }
}
\ProvideDocumentCommand { \tloprise } { } { \tlrise\! }



% Fall
\DeclareMathOperator { \tlsymbfall } {
    \__temporal_logic_render_op:n {
        \draw
        (.1*\EX, .9*\EX) --
        (.9*\EX, .1*\EX);
        \draw
        (.4*\EX, .1*\EX) --
        (.9*\EX, .1*\EX) --
        (.9*\EX, .6*\EX);
    }
}
\ProvideDocumentCommand { \tlfall } { O{} } {
    \__temporal_logic_op_sub:cn { tlsymbfall } { #1 }
}
\ProvideDocumentCommand { \tlopfall } { } { \tlfall\! }


% Prophecy
\DeclareMathOperator { \tlsymbprophecy } {
    \__temporal_logic_render_op:n {
        \draw
        (.1*\EX, .1*\EX) --
        (.1*\EX, .9*\EX) --
        (.9*\EX, .5*\EX) --
        cycle;
    }
}
\ProvideDocumentCommand { \tlprophecy } { O{} } {
    \__temporal_logic_op_sub:cn { tlsymbprophecy } { #1 }
}
\ProvideDocumentCommand { \tlopprophecy } { } { \tlprophecy\! }



% History
\DeclareMathOperator { \tlsymbhistory } {
    \__temporal_logic_render_op:n {
        \draw
        (.9*\EX, .1*\EX) --
        (.9*\EX, .9*\EX) --
        (.1*\EX, .5*\EX) --
        cycle;
    }
}
\ProvideDocumentCommand { \tlhistory } { O{} } {
    \__temporal_logic_op_sub:cn { tlsymbhistory } { #1 }
}
\ProvideDocumentCommand { \tlophistory } { } { \tlhistory\! }
\ExplSyntaxOff
% </package>
%    \end{macrocode}
% \end{implementation}