texlive[72575] Master: temporal-logic (17oct24)
commits+karl at tug.org
commits+karl at tug.org
Thu Oct 17 21:23:54 CEST 2024
Revision: 72575
https://tug.org/svn/texlive?view=revision&revision=72575
Author: karl
Date: 2024-10-17 21:23:53 +0200 (Thu, 17 Oct 2024)
Log Message:
-----------
temporal-logic (17oct24)
Modified Paths:
--------------
trunk/Master/tlpkg/bin/tlpkg-ctan-check
trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc
Added Paths:
-----------
trunk/Master/texmf-dist/doc/latex/temporal-logic/
trunk/Master/texmf-dist/doc/latex/temporal-logic/README.md
trunk/Master/texmf-dist/doc/latex/temporal-logic/temporal-logic-doc.pdf
trunk/Master/texmf-dist/source/latex/temporal-logic/
trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.dtx
trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.ins
trunk/Master/texmf-dist/tex/latex/temporal-logic/
trunk/Master/texmf-dist/tex/latex/temporal-logic/temporal-logic.sty
trunk/Master/tlpkg/tlpsrc/temporal-logic.tlpsrc
Added: trunk/Master/texmf-dist/doc/latex/temporal-logic/README.md
===================================================================
--- trunk/Master/texmf-dist/doc/latex/temporal-logic/README.md (rev 0)
+++ trunk/Master/texmf-dist/doc/latex/temporal-logic/README.md 2024-10-17 19:23:53 UTC (rev 72575)
@@ -0,0 +1,29 @@
+# Latex package for Temporal Logic Operators
+
+## Overview
+
+The package defines functions for rendering the temporal operators defined in
+the **Linear Temporal Logic** (_LTL_), **Metric Temporal Logic** (_MTL_), **Metric First-order
+Temporal Logic** (_MFOTL_), and **Counting Metric First-order Temporal Binding Logic** (_CMFTBL_). The package
+defines various functions with variants in order to include or omit optional
+parameters to the operators like the optional interval.
+
+## Build the package
+
+If you want to generate the necessary `.sty` file and the documentation for this
+package you can do this with the following steps:
+
+1. Generate `.sty` file from `.ins` file with the command:
+ `latex temporal-logic.ins`
+2. Generate documentation with the command:
+ `latexmk -pdf temporal-logic.dtx`
+
+## Copyright and License
+
+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.
Property changes on: trunk/Master/texmf-dist/doc/latex/temporal-logic/README.md
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Added: trunk/Master/texmf-dist/doc/latex/temporal-logic/temporal-logic-doc.pdf
===================================================================
(Binary files differ)
Index: trunk/Master/texmf-dist/doc/latex/temporal-logic/temporal-logic-doc.pdf
===================================================================
--- trunk/Master/texmf-dist/doc/latex/temporal-logic/temporal-logic-doc.pdf 2024-10-17 19:23:22 UTC (rev 72574)
+++ trunk/Master/texmf-dist/doc/latex/temporal-logic/temporal-logic-doc.pdf 2024-10-17 19:23:53 UTC (rev 72575)
Property changes on: trunk/Master/texmf-dist/doc/latex/temporal-logic/temporal-logic-doc.pdf
___________________________________________________________________
Added: svn:mime-type
## -0,0 +1 ##
+application/pdf
\ No newline at end of property
Added: trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.dtx
===================================================================
--- trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.dtx (rev 0)
+++ trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.dtx 2024-10-17 19:23:53 UTC (rev 72575)
@@ -0,0 +1,593 @@
+% \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 at 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 at tu-dortmund.de}
+% {dominik.schmid at 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}
\ No newline at end of file
Property changes on: trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.dtx
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Added: trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.ins
===================================================================
--- trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.ins (rev 0)
+++ trunk/Master/texmf-dist/source/latex/temporal-logic/temporal-logic.ins 2024-10-17 19:23:53 UTC (rev 72575)
@@ -0,0 +1,52 @@
+\iffalse meta-comment
+
+File: temporal-logic.ins
+
+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 at tu-dortmund.de>.
+
+This work consists of the files temporal-logic.dtx, temporal-logic.ins,
+and the derived file temporal-logic.sty.
+
+\fi
+
+\input l3docstrip.tex
+
+\askforoverwritefalse
+
+\preamble
+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 at tu-dortmund.de>.
+
+This work consists of the files temporal-logic.dtx, temporal-logic.ins,
+and the derived file temporal-logic.sty.
+\endpreamble
+
+\postamble
+\endpostamble
+
+\generate{\file{temporal-logic.sty} {\from{temporal-logic.dtx} {package}}}
+
+\endbatchfile
Added: trunk/Master/texmf-dist/tex/latex/temporal-logic/temporal-logic.sty
===================================================================
--- trunk/Master/texmf-dist/tex/latex/temporal-logic/temporal-logic.sty (rev 0)
+++ trunk/Master/texmf-dist/tex/latex/temporal-logic/temporal-logic.sty 2024-10-17 19:23:53 UTC (rev 72575)
@@ -0,0 +1,215 @@
+%%
+%% This is file `temporal-logic.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% temporal-logic.dtx (with options: `package')
+%% 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 at tu-dortmund.de>.
+%%
+%% This work consists of the files temporal-logic.dtx, temporal-logic.ins,
+%% and the derived file temporal-logic.sty.
+
+\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 }
+}
+%%
+%%
+%% End of file `temporal-logic.sty'.
Property changes on: trunk/Master/texmf-dist/tex/latex/temporal-logic/temporal-logic.sty
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Modified: trunk/Master/tlpkg/bin/tlpkg-ctan-check
===================================================================
--- trunk/Master/tlpkg/bin/tlpkg-ctan-check 2024-10-17 19:23:22 UTC (rev 72574)
+++ trunk/Master/tlpkg/bin/tlpkg-ctan-check 2024-10-17 19:23:53 UTC (rev 72575)
@@ -825,7 +825,7 @@
tamethebeast tango tangocolors tangramtikz tap tapir tasks
tblr-extras tcldoc tcolorbox tdclock tds tdsfrmath
technics technion-thesis-template ted telprint
- templates-fenn templates-sommer templatetools tempora
+ templates-fenn templates-sommer templatetools tempora temporal-logic
tengwarscript
tensind tensor termcal termcal-de termes-otf termlist termmenu termsim
testhyphens testidx
Modified: trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc
===================================================================
--- trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc 2024-10-17 19:23:22 UTC (rev 72574)
+++ trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc 2024-10-17 19:23:53 UTC (rev 72575)
@@ -256,6 +256,7 @@
depend synproof
depend t-angles
depend tablor
+depend temporal-logic
depend tensind
depend tensor
depend tex-ewd
Added: trunk/Master/tlpkg/tlpsrc/temporal-logic.tlpsrc
===================================================================
More information about the tex-live-commits
mailing list.