\documentclass{tlp}

\usepackage{booktabs}
\usepackage{dsfont}
\usepackage{wrapfig} 
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{multirow}
\usepackage{multicol}
\usepackage{xspace}
\usepackage{xcolor}
\definecolor{linkcolor}{RGB}{52,59,144}
\usepackage[hidelinks, colorlinks=true, allcolors=linkcolor]{hyperref}
\usepackage{url}
\renewcommand\UrlFont{\color{linkcolor}\rmfamily}

\usepackage{comment}    % comment out blocks of latex
\usepackage{hyperref}

\usepackage{listings}

\usepackage[most]{tcolorbox}
\usepackage{enumitem}


\definecolor{noteColor1} {rgb}{  1,  0,  0} %
\definecolor{noteColor2} {rgb}{  1,0.5,  0} %
\definecolor{noteColor13}{rgb}{0.9,0.2,  0} 
\definecolor{noteColor3} {rgb}{0.8,0.8,  0}
\definecolor{noteColor4} {rgb}{  1,  0,0.6}
\definecolor{noteColor5} {rgb}{  1,  0,  1} %
\definecolor{noteColor6} {rgb}{  0,0.8,  0} %
\definecolor{noteColor7} {rgb}{  0,0.8,0.6} %
\definecolor{noteColor8} {rgb}{  0,0.8,0.8} %
\definecolor{noteColor9} {rgb}{0.5,0.8,  0} %
\definecolor{noteColor10}{rgb}{  0,  0,  1} %
\definecolor{noteColor11}{rgb}{0.5,  0,  1} %
\definecolor{noteColor12}{rgb}{  0,0.5,  1} %


\definecolor{maroon}{rgb}{0.5,0,0}
\definecolor{darkgreen}{rgb}{0,0.5,0}
\definecolor{mildgreen}{rgb}{0,0.8,0}
\definecolor{lightblue}{rgb}{0.3,0.3,1}
\definecolor{lightgrey}{rgb}{0.97,0.97,0.97}
\definecolor{grey}{rgb}{0.65,0.65,0.65}

\lstnewenvironment{lstlistingwolinenum}{
    \lstset{
        basicstyle=\ttfamily\footnotesize,
        frame=lrtb,
        breaklines=true
    }
}{}
\lstnewenvironment{lstlistingwlinenum}{
    \lstset{
        basicstyle=\ttfamily\footnotesize,
        frame=lrtb,
        breaklines=true,
        numbers=left,
        numbersep=0.5em,
        xleftmargin=1.5em,
        framexleftmargin=1.5em,
        stepnumber=1
    }
}{}



\usepackage{adjustbox}
\usepackage{relsize}
%\usepackage[dvipsnames]{xcolor}
% custom colors
\definecolor{PrologPredicate}{RGB}{0,0,200}
\definecolor{PrologVar}      {RGB}{145,032,039}
%%%\definecolor{PrologComment}  {RGB}{169,082,044}
\definecolor{PrologComment}  {RGB}{0,170,0}
\definecolor{PrologOther}    {rgb}{0.2,0.2,0.2}
\definecolor{PrologString}   {RGB}{070,120,200}
\usepackage{listings} 
\usepackage{textcomp}
\newcommand{\code}{\lstinline[style=MyInline]}
%%%%%%% LATEX-NOTE: the environment of \code{} must be in the same
%%%%%%% line. Otherwise its behaviour is incorrect
\lstdefinestyle{MyInline}
{
  basicstyle = \relsize{-0.5}\ttfamily\color{PrologPredicate},
  escapechar = @,
  escapeinside = {-<}{>-},
  breaklines = true,
  breakatwhitespace=true,
  upquote = true,
  literate =
  {?-}{{?-\,}}3
  {:-}{{:-\,}}3
  {.=.}{{\,\#=\,}}3
  {.<.}{{\,\#<\,}}3
  {.>.}{{\,\#>\,}}3
  {.=<.}{{\,\#=<\,}}4
  {.>=.}{{\,\#>=\,}}4
}
\lstdefinestyle{MySCASP}
{
    numbersep=0.5em,    % added by OV
    xleftmargin=0.35cm,  % OV
    %%%xleftmargin=0.5cm,
    numberstyle=\tiny,
    numbers=left,
    stepnumber=1,
  mathescape = true,
  escapechar = @,
  escapeinside = {-<}{>-},
  keywords = {},
  upquote = true,
  basicstyle = \ttfamily\relsize{-.5}\color{PrologPredicate},
  basewidth = 0.47em,
%  moredelim = {**[is][\color{PrologOther}]{&(}{&)}},
  moredelim = {*[s][\color{PrologVar}]{(}{)}},
  moredelim = {*[s][\color{PrologString}]{'}{'}},
  moredelim = {*[s][\color{PrologOther}]{:-}{.}},
  commentstyle = \mdseries\color{PrologComment},
  escapebegin=\color{PrologVar},
  morecomment=[l]\%,
  literate     =
  {|}{{|}}2
%  {&.}{{.}}0
  {.=.}{{\,\#=\,}}3
  {.<.}{{\,\#<\,}}3
  {.>.}{{\,\#>\,}}3
  {.=<.}{{\,\#=<\,}}4
  {.>=.}{{\,\#>=\,}}4
}
%

\usepackage{ntheorem}
   

\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
{
\theoremindent=.5cm
\theoremheaderfont{\kern-.5cm\normalfont\slshape}
\theorembodyfont{\normalfont}
\theoremseparator{.}
\theoremprework{\setlength\parindent{0cm}}
\newtheorem{example}{Example}
}


\newcommand{\scasp}[0]{s(CASP)}
\newcommand{\clingo}[0]{\textsc{Clingo}}
\newcommand{\hilite}[0]{\textsc{HiLiTE}}
\newcommand{\midas}[0]{MIDAS}
\newcommand{\myurl}[1]{\href{http://#1}{\nolinkurl{#1}}}
\newcommand{\version}{0.24.04.04\xspace}

\newcommand{\var}[1]{$\mathtt{#1}$}

\sloppy


% color box for showing implementation of a~requirement
% use like this "\begin{reqCodeBox}{*name_of_requirement*}"
\newtcolorbox{reqCodeBox}[3][0.6em]{%
    title={#3},
    colframe=black!75,
    enhanced,
    breakable,
    left=2pt, right=0pt, top=-6pt, bottom=-6pt, boxsep=0pt, boxrule=0.25pt, arc=2pt,
    bottomsep at break=6pt,
    topsep at break=6pt,
    coltitle=white, 
    detach title,
    overlay unbroken and first={
    % xshift=-1.9em  +  width=3.8em
    \node[xshift=-#2/2,yshift=-#1] at (frame.north east) {%
        \begin{tcolorbox}[enhanced, coltitle=white, colback=black!75, width=#2, left=0pt, right=0pt, top=1pt, bottom=1pt, boxsep=1pt, boxrule=0pt, arc=2pt]\textcolor{white}{#3}\end{tcolorbox}
        };
    }
}
\newtcolorbox{codeBox}{%
    colframe=black!75,
    enhanced,
    breakable,
    left=2pt, right=0pt, top=-6pt, bottom=-6pt, boxsep=0pt, boxrule=0.25pt, arc=2pt,
    bottomsep at break=6pt,
    topsep at break=6pt,
    coltitle=white, 
    detach title,
}
\newtcolorbox{enumBox}{%
    colframe=black!75,
    enhanced,
    breakable,
    left=2pt, right=2pt, top=0pt, bottom=0pt, boxsep=2pt, boxrule=0.25pt, arc=2pt,
    bottomsep at break=0pt,
    topsep at break=0pt,
    coltitle=white, 
    detach title,
}

\setlength{\skip\footins}{1.5em} % TODO !!

%===========================================================================================================
%=====================        TITLE / ABSTRACT / AUTHORS / ...        ======================================
%===========================================================================================================
\begin{document}

\jnlPage{X}{Y}
\jnlDoiYr{2024}
\doival{10.1017/xxxxx}

\title[
  SUPPLEMENTARY MATERIAL        % RIGHT TITLE
]
{ % FIRST PAGE TITLE
  SUPPLEMENTARY MATERIAL FOR:\\
  Early Validation of High-level System Requirements with Event Calculus and Answer Set Programming%
}
\lefttitle{
  SUPPLEMENTARY MATERIAL         % LEFT TITLE
}


\begin{authgrp}
%%%\vspace{-0.5em}
    % TODO should look like this:
    %%%\author{\sn{Vasicek} \gn{Ondrej}$^1$}
    %%%\affiliation{$^1$Brno University of Technology, Brno, Czech Republic}
    %%% ...

    %%%% Much shorter version:
    \author{%
               \sn{Va\v{s}\'{i}\v{c}ek}, \gn{Ond\v{r}ej}$^1$    \hfill      % main PhD first
               \sn{Arias},               \gn{Joaquin}$^2$       \hfill      % others alphabetical
               \sn{Fiedor},              \gn{Jan}$^{1,7}$       \hfill     
               \sn{Gupta},               \gn{Gopal}$^3$                  \\
        \hfill \sn{Hall},                \gn{Brendan}$^4$       \hfill     
               \sn{K\v{r}ena},           \gn{Bohuslav}$^1$      \hfill     
               \sn{Larson},              \gn{Brian}$^5$         \hfill ~ \\
        \hfill \sn{Varanasi},            \gn{Sarat Chandra}$^6$ \hfill     
               \sn{Vojnar},              \gn{Tom\'{a}\v{s}}$^{1,8}$ \hfill ~   
    }
    \vspace{.5em}
    \affiliation{%
        $^1$Brno University of Technology, CZ \hspace{.2cm}  %
        $^2$Universidad Rey Juan Carlos, ES \hspace{.2cm}    %
        $^3$UT Dallas, USA \hspace{.2cm}         %
        $^4$Ardent Innovation Labs, USA \hspace{.2cm}
        $^5$Multitude Corp., USA\hspace{.2cm}                        % Multitude Corporation, USA, Minesota, Chief Technical Officer
        $^6$GE Aerospace Research, USA \hspace{.2cm}       %
        $^7$Honeywell International s.r.o., CZ \hspace{.2cm}        %
        $^8$Masaryk University, CZ
    }
\vspace{-1em} % TODO
\end{authgrp}

%%%\history{\sub{xx xx xxxx;} \rev{xx xx xxxx;} \acc{xx xx xxxx}}%%%\vspace{-0.5em}}  % TODO

\maketitle



%===========================================================================================================
%=====================        SECTIONS        ==============================================================
%===========================================================================================================

\renewcommand\thesection{Appendix~\Alph{section}}
\renewcommand\thesubsection{\Alph{section}.\arabic{subsection}}

\renewcommand{\thetable}{\Alph{section}\arabic{table}}

\renewcommand{\thetable}{\Alph{section}\arabic{table}}




%===========================================================================================================
%%%\vspace{-0.5em}
\section{Additional Details for Sections from the Paper}
\label{appendix:a}
This appendix contains further details which did not fit into the paper. In particular, a description of how we fixed an overdose issue in the PCA pump specification in Section~\ref{apx:overdose-fix}, an example of decoupling the trigger and effects for an event in Section~\ref{apx:decopuling-example}, and a~full version of a~table of experiments (instead of a~shortened version) in Section~\ref{apx:full-table}.

    %-------------------------------------------------------------------------------------------------------
    %%%\vspace{-0.5em}
    \subsection{Fixing the Overdose Error in the PCA Pump Requirements}
    \label{apx:overdose-fix}
    %\ref*{sec:overdose}
    [Section~4.2.2] discussed an overdose error that we have discovered in the requirements specification of the PCA pump.
    %
    In this section, we discuss how we fixed the model in order to remove this issue.
    
    One option to fix the overdose issue is to introduce the missing overdose protection measure for basal delivery, as was the original intention defined in the exception cases
    in the specification.
    %
    This solution would prevent harm to the patient, however, it could allow an early spike of boluses only to cause a~max dose warning during subsequent basal delivery, which leads to loss of therapy and requires the attention of a~clinician.
    %
    Further, adding a~triggered event which can halt basal delivery based on the maximum safe dose, in a~similar way as what is already included for a~clinician-requested bolus, would cause a~significant increase in solving complexity and would turn basal delivery into a~self-ending trajectory.
    
    Therefore, we propose a~different, preemptive approach.
    %
    When the pump reasons about denying a~bolus, it should consider that (at least) basal delivery will follow under normal operation by \emph{assuming a~max dose window full of basal delivery}.
    %
    The actual amount of extra drug delivered via boluses is then added on top of the assumption.
    %
    The overdose protection measure defined for clinician-requested boluses needs to be modified in a~similar fashion.
    %
    In this way, there is no need for an overdose protection measure during basal delivery because the preemptive nature of handling boluses will not allow such situation, assuming that the max dose is defined such that basal delivery by itself (without any boluses) will not cause an overdose.
    %    
    Further, the preemptive denial of a~bolus should raise the max dose warning only for cases where the overdose would occur immediately after or during the bolus, not for cases where the overdose was preemptively prevented (i.e., only raise a~warning in cases when even the original model would).
    %
    This approach is what our ``fixed'' model of the PCA pump currently uses.
    %
    The two versions of the model can be found in \href{https://github.com/ovasicek/pca-pump-ec-artifacts/blob/master/model-original.pl}{model-original.pl} and \href{https://github.com/ovasicek/pca-pump-ec-artifacts/blob/master/model-fixed.pl}{model-fixed.pl}.

    \newcommand{\EXC}{E{\smaller{}x}C}
    
    
    %%%\vspace{-0.5em}
    \subsection{Example for the Decoupling of Event Triggers and Effects}
    \label{apx:decopuling-example}
    In [Section~5.5], we discussed a multi-run approach for mitigating increases in reasoning complexity caused by certain triggered events.
    %
    The approach is based on decoupling the trigger of the event from the effects of the event.
    %
    In this section, we provide a code demonstration of how the decoupling is done.
    %
    Given some event \code{alarm}, which is a triggered event which can only be triggered up to once per narrative, it can have effects on some fluents via \code{initiates}/\code{terminates} and on other events via triggering their occurrence.
    %
    The original code for the \code{alarm} event and its effects might look like this:
    %%%\vspace{-0.5em}
    \begin{codeBox}
    \begin{lstlisting}[style=MySCASP]
event(alarm).
happens(alarm, T) :- some_trigger_rule(T).  % event trigger
terminates(alarm, some_fluent, T).          % effect on fluents
happens(alarm_response_event, T) :-         % effect on other events
  happens(alarm, T).  
    \end{lstlisting}
    \end{codeBox}
    %%%\vspace{-0.4em}
    %
    \noindent In order to decouple the effects of the \code{alarm} event from its trigger, we replace the above code with the following code:
    %%%\vspace{-0.5em}
    \begin{codeBox}
    \begin{lstlisting}[style=MySCASP]
event(alarm).                               % original event
happens(alarm, T) :- some_trigger_rule(T).  % original event trigger

event(alarm_EFFECT).                        % new effect event
terminates(alarm_EFFECT, some_fluent, T).   % decoupled effect on fluents
happens(alarm_response_event, T) :-         % decoupled effect on other events
  happens(alarm_EFFECT, T).

happens(alarm_EFFECT,T):-                   % option to undo decoupling
  full_alarm_reasoning_enabled,
  happens(alarm,T).
    \end{lstlisting}
    \end{codeBox}
    %%%\vspace{-0.4em} 
    %
    \noindent We introduce a new \code{alarm_EFFECT} event and move all the effects of the original \code{alarm} event to this new event (lines~4-7).
    %
    The new event has no trigger rule, and the original event now has no effects.
    %
    We also include an option to undo the decoupling in order to re-enable full reasoning (lines~9-11) via a configuration fact \code{full_alarm_reasoning_enabled}, which is not defined by default.
    
    For each narrative, we can either choose to ignore reasoning about the \code{alarm} event entirely (when it is deemed not relevant), or we can use the multi-run approach, or we can re-enable the full (slow) reasoning.
    %
    For this particular example, the multi-run approach would consist of two runs.
    %
    The first run would use the query \code{?- happens(alarm,T).}
    %
    If the query fails, then the \code{alarm} event does not occur in the particular narrative and, thus, is not relevant.
    %
    If the query succeeds, then we introduce a new fact \code{happens(alarm_EFFECT,t)}., where \code{t} is the binding for \code{T} from the result of the query.
    %
    The second run of reasoning, then uses any query of interest while taking into account the new fact which might have been introduced in the previous run.

    In the case of decoupling multiple events, e.g., \code{E1} and \code{E2}, one needs to consider if one of the decoupled events has any impact on the occurrence of the other decoupled event.
    %
    If the occurrence of \code{E1} influences the occurrence of \code{E2} in any way, then we need to use three runs in the multi-run approach.
    %
    The first run queries the occurrence of \code{E1} and introduces the appropriate fact, the second run then queries the occurrence of \code{E2} while already considering the effects of \code{E1} via the new fact, and the third run then runs any query of interest while taking into account facts introduced by both of the prior runs.

    %%-------------------------------------------------------------------------------------------------------
    %\ref*{t:simulation-queries}
    %%%\vspace{-0.5em}
    \subsection{Full Version of [Table~1]}
    \label{apx:full-table}
    %\ref*{t:simulation-queries}
    %\ref*{sec:simulation-comparison}
    [Section~4.1.1] presented [Table~1], which was a~shortened version due to space constraints and due to limited value of presenting execution times of every UC/\EXC{}.
    %
    We include the full version in Table~\ref{apx:t:simulation-queries-full}.
    %
    \newcommand{\uclink}[2]{\href{https://github.com/ovasicek/pca-pump-ec-artifacts/blob/master/narratives_and_queries/#1.pl}{#2}}
    %%%\vspace{-1em}
    \begin{table}%[h]
        \centering
        %%\vspace{-0.5em}
        \small
        \caption{Full results of simulation of relevant use cases and exception cases}
        \vspace{0.2em}
        \begin{tabular}{lllcr} \toprule
                                      & \textbf{Use Case Name}    & \textbf{Variant}         & \textbf{Result} & \textbf{Time(s.)} \\%& Memory [MB] \\
          \midrule
          \uclink{uc1}  {UC1}         & Normal Operation          & no variants              & OK              &    1.69           \\%& 27.63       \\             
          \uclink{uc2}  {UC2}         & Patient-Requested Bolus   & no variants              & OK              &    3.17           \\%& 27.92       \\             
          \uclink{uc3a} {UC3a}        & Clinician-Requested Bolus & not suspend              & OK              &    2.84           \\%& 27.91       \\             
          \uclink{uc3b} {UC3b}        & Clinician-Requested Bolus & suspended and resumed    & OK              &   37.13           \\%& 29.69       \\             
          \uclink{uc7a} {UC7a}        & Resume Infusion           & after basal delivery     & OK              &    1.92           \\%& 27.65       \\             
          \uclink{uc7b} {UC7b}        & Resume Infusion           & after patient bolus      & OK              &    3.83           \\%& 27.88       \\            
          \uclink{uc7c} {UC7c}        & Resume Infusion           & after clinician bolus    & OK              &    3.56           \\%& 27.91       \\ 
          \midrule
          \uclink{ec1}  {\EXC{}1}     & Bolus Request Too Soon    & no variants              & OK              &    2.72           \\%& 27.91       \\
          \uclink{ec7a} {\EXC{}7a}    & Over-Flow Rate Alarm      & defined in \EXC{} step 1 & FAIL            &    1.87           \\%& 27.91       \\
          \uclink{ec7b} {\EXC{}7b}    & Over-Flow Rate Alarm      & defined in \EXC{} step 1 & FAIL            &    1.87           \\%& 27.82       \\
          \uclink{ec7c} {\EXC{}7c}    & Over-Flow Rate Alarm      & defined in \EXC{} step 1 & FAIL            &    2.17           \\%& 27.89       \\
          \uclink{ec7d} {\EXC{}7d}    & Over-Flow Rate Alarm      & defined in \EXC{} step 1 & FAIL            &    4.62           \\%& 27.90       \\
          \uclink{ec7e} {\EXC{}7e}    & Over-Flow Rate Alarm      & defined in \EXC{} step 1 & FAIL            &    1.53           \\%& 27.60       \\
          \uclink{ec7f} {\EXC{}7f}    & Over-Flow Rate Alarm      & defined in \EXC{} step 1 & FAIL            &    4.24           \\%& 27.90       \\
          \uclink{ec8a} {\EXC{}8a}    & Under-Flow Rate Alarm     & basal delivery           & OK              &    1.56           \\%& 27.59       \\
          \uclink{ec8b} {\EXC{}8b}    & Under-Flow Rate Alarm     & defined in \EXC{} step 1 & FAIL            &    2.19           \\%& 27.67       \\
          \uclink{ec8c} {\EXC{}8c}    & Under-Flow Rate Alarm     & defined in \EXC{} step 1 & FAIL            &    2.15           \\%& 27.66       \\
          \uclink{ec9a} {\EXC{}9a}    & Pump Overheating          & during basal delivery    & OK              &    1.68           \\%& 27.61       \\
          \uclink{ec9b} {\EXC{}9b}    & Pump Overheating          & during patient bolus     & OK              &    2.88           \\%& 27.93       \\
          \uclink{ec9c} {\EXC{}9c}    & Pump Overheating          & during clinician bolus   & OK              &    2.31           \\%& 27.90       \\
          \uclink{ec10a}{\EXC{}10a}   & Downstream Occlusion      & during basal delivery    & OK              &    1.67           \\%& 27.64       \\
          \uclink{ec10b}{\EXC{}10b}   & Downstream Occlusion      & during patient bolus     & OK              &    3.15           \\%& 27.89       \\
          \uclink{ec10c}{\EXC{}10c}   & Downstream Occlusion      & during clinician bolus   & OK              &    2.32           \\%& 27.90       \\
          \uclink{ec11a}{\EXC{}11a}   & Upstream Occlusion        & during basal delivery    & OK              &    1.66           \\%& 27.60       \\
          \uclink{ec11b}{\EXC{}11b}   & Upstream Occlusion        & during patient bolus     & OK              &    3.10           \\%& 27.90       \\
          \uclink{ec11c}{\EXC{}11c}   & Upstream Occlusion        & during clinician bolus   & OK              &    2.35           \\%& 27.90       \\
          \uclink{ec12a}{\EXC{}12a}   & Air-in-line Embolism      & during basal delivery    & OK              &    1.66           \\%& 27.62       \\
          \uclink{ec12b}{\EXC{}12b}   & Air-in-line Embolism      & during patient bolus     & OK              &    2.91           \\%& 27.92       \\
          \uclink{ec12c}{\EXC{}12c}   & Air-in-line Embolism      & during clinician bolus   & OK              &    2.31           \\%& 27.90       \\
          \uclink{ec13a}{\EXC{}13a}   & Maximum Safe Dose         & during basal delivery    & FAIL            &   25.62           \\%& 28.62       \\
          \uclink{ec13b}{\EXC{}13b}   & Maximum Safe Dose         & during patient bolus     & OK              &   31.61           \\%& 28.74       \\
          \uclink{ec13c}{\EXC{}13c}   & Maximum Safe Dose         & during clinician bolus   & OK              &   53.45           \\%& 30.05       \\
          \uclink{ec20a}{\EXC{}20a}   & Reservoir Low             & during basal delivery    & FAIL            &    1.99           \\%& 27.58       \\
          \uclink{ec20b}{\EXC{}20b}   & Reservoir Low             & during patient bolus     & FAIL            &    7.95           \\%& 27.92       \\
          \uclink{ec20c}{\EXC{}20c}   & Reservoir Low             & during clinician bolus   & FAIL            &    5.07           \\%& 27.91       \\
          \uclink{ec21} {\EXC{}21}    & Reservoir Empty           & no variants              & OK              &   40.99           \\%& 28.04       \\
          \bottomrule
        \end{tabular}
        \label{apx:t:simulation-queries-full}
    \end{table}



\end{document}
