From 431062666fbd43b9fb7ab2c9781a02819ced3499 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Mon, 23 Nov 2020 23:04:51 +0100 Subject: [PATCH] Use math where appropriate in description of clock partitioning --- chapters/synchronous.tex | 74 +++++++++++++++------------------------- 1 file changed, 28 insertions(+), 46 deletions(-) diff --git a/chapters/synchronous.tex b/chapters/synchronous.tex index 9922492dc..a2c527ceb 100644 --- a/chapters/synchronous.tex +++ b/chapters/synchronous.tex @@ -854,25 +854,16 @@ \subsection{Flattening of Model}\label{flattening-of-model} array and matrix equations and records don't not need to be expanded if they have the same clock. \end{nonnormative} -Furthermore, each non-trivial expression (non-literal, non-constant, -non-parameter, non-variable), expr\textsubscript{i}, appearing as first -argument of a clock conversion operator (except \lstinline!hold! and \lstinline!backSample!) -is recursively replaced by a -unique variable, v\textsubscript{i}, and the equation v\textsubscript{i} -= expr\textsubscript{i} is added to the equation set. +Furthermore, each non-trivial expression (non-literal, non-constant, non-parameter, non-variable), $\mathit{expr}_{i}$, appearing as first argument of a clock conversion operator (except \lstinline!hold! and \lstinline!backSample!) is recursively replaced by a unique variable, $v_{i}$, and the equation $v_{i} = \mathit{expr}_{i}$ is added to the equation set. \subsection{Connected Components of the Equations and Variables Graph}\label{connected-components-of-the-equations-and-variables-graph} -Consider the set E of equations and the set V of unknown variables (not -constants and parameters) in a flattened model, i.e.\ M = \textless{}E, -V\textgreater{}. The partitioning is described in terms of an undirected -graph \textless{}N,~F\textgreater{} with the nodes N being the set of -equations and variables, N = E + V. The set \lstinline!incidence(e)! for an equation -\lstinline!e! in E is a subset of V, in general, the unknowns which lexically appear -in e. There is an edge in F of the graph between an equation, e, and a -variable, v, if v = incidence(e): +Consider the set $E$ of equations and the set $V$ of unknown variables (not constants and parameters) in a flattened model, i.e., $M = \left\langle E,\, V \right\rangle$. +The partitioning is described in terms of an undirected graph $\left\langle N,\, F \right\rangle$ with the nodes $N$ being the set of equations and variables, $N = E \cup V$. +The set $\operatorname{incidence}(e)$ for an equation $e$ in $E$ is a subset of $V$, in general, the unknowns which lexically appear in $e$. +There is an edge in $F$ of the graph between an equation, $e$, and a variable, $v$, if $v \in \operatorname{incidence}(e)$: \begin{equation*} -F = \{(e, v) : e \in E, v \in \text{\lstinline!incidence!}(e)\} +F = \{(e, v) : e \in E, v \in \operatorname{incidence}(e)\} \end{equation*} A set of clock partitions is the \emph{connected components} (Wikipedia, @@ -888,25 +879,21 @@ \subsection{Base-clock Partitioning}\label{base-clock-partitioning} The base-clock partitioning is performed with base-clock inference which uses the following incidence definition: -\lstinline!incidence(e)! = +$\operatorname{incidence}(e)$ = \begin{list}{}{\setlength{\leftmargin}{2em}\setlength{\topsep}{-\parskip}} \item -the \emph{unknown} variables, as well as variables \lstinline!x! in \lstinline!der(x)!, \lstinline!pre(x)!, and \lstinline!previous(x)!, which lexically appear in \lstinline!e! +the \emph{unknown} variables, as well as variables \lstinline!x! in \lstinline!der(x)!, \lstinline!pre(x)!, and \lstinline!previous(x)!, which lexically appear in $e$ \begin{list}{}{\setlength{\leftmargin}{2em}\setlength{\topsep}{-\parskip}} \item -except as first argument of base-clock conversion operators: \lstinline!sample! and \lstinline!hold! and \lstinline!Clock(condition, startInterval)!. +except as first argument of base-clock conversion operators: \lstinline!sample! and \lstinline!hold! and \lstinline!Clock(condition=$\ldots$, startInterval=$\ldots$)!. \end{list} \end{list}\vspace{\parskip}% Compensate for removal of \parskip from \topset. -The resulting set of connected components, is the partitioning of the -equations and variables, B\textsubscript{i} = -\textless{}E\textsubscript{i}, V\textsubscript{i}\textgreater{}, -according to base-clocks and continuous-time partitions. +The resulting set of connected components, is the partitioning of the equations and variables, $B_{i} = \left\langle E_{i},\, V_{i} \right\rangle$, according to base-clocks and continuous-time partitions. The base clock partitions are identified as \firstuse{clocked} or as \firstuse{continuous-time partitions} according to the following properties: -A variable u in \lstinline!sample(u)!, a variable y in y = -\lstinline!hold(ud)!, and a variable b in \lstinline!Clock(b, startInterval)! where b is of \lstinline!Boolean! type is in a continuous-time partition. +A variable \lstinline!u! in \lstinline!sample(u)!, a variable \lstinline!y! in \lstinline!y = hold(ud)!, and a variable \lstinline!b! in \lstinline!Clock(b, startInterval=$\ldots$)! where the \lstinline!Boolean! \lstinline!b! is in a continuous-time partition. Correspondingly, variables \lstinline!u! and \lstinline!y! in \lstinline!y = sample(uc)!, @@ -914,13 +901,12 @@ \subsection{Base-clock Partitioning}\label{base-clock-partitioning} \lstinline!y = superSample(u)!, \lstinline!y = shiftSample(u)!, \lstinline!y = backSample(u)!, -\lstinline!y = previous(u)!, are in a clocked partition. Equations in a clocked -when clause are also in a clocked partition. -Other partitions where none of the variables in the partition are -associated with any of the operators above have an unspecified partition -kind and are considered continuous-time partitions. +\lstinline!y = previous(u)!, +are in a clocked partition. +Equations in a clocked when clause are also in a clocked partition. +Other partitions where none of the variables in the partition are associated with any of the operators above have an unspecified partition kind and are considered continuous-time partitions. -All continuous-time partitions are collected together and form \emph{the} continuous-time partition. +All continuous-time partitions are collected together and form \firstuse{the continuous-time partition}. \begin{example} \begin{lstlisting}[language=modelica] @@ -965,33 +951,29 @@ \subsection{Sub-clock Partitioning}\label{sub-clock-partitioning} \cref{base-clock-partitioning}, the sub-clock partitioning is performed with sub-clock inference which uses the following incidence definition: -\lstinline!incidence(e)! = +$\operatorname{incidence}(e)$ = \begin{list}{}{\setlength{\leftmargin}{2em}\setlength{\topsep}{-\parskip}} \item -the \emph{unknown} variables, as well as variables \lstinline!x! in \lstinline!der(x)!, \lstinline!pre(x)!, and \lstinline!previous(x)!, which lexically appear in e +the \emph{unknown} variables, as well as variables \lstinline!x! in \lstinline!der(x)!, \lstinline!pre(x)!, and \lstinline!previous(x)!, which lexically appear in $e$ \begin{list}{}{\setlength{\leftmargin}{2em}\setlength{\topsep}{-\parskip}} \item except as first argument of sub-clock conversion operators: \lstinline!subSample!, \lstinline!superSample!,\linebreak[4] \lstinline!shiftSample!, \lstinline!backSample!, \lstinline!noClock!, and \lstinline!Clock! with first argument of \lstinline!Boolean! type. \end{list} \end{list}\vspace{\parskip}% Compensate for removal of \parskip from \topset. -The resulting set of connected components, is the partitioning of the -equations and variables, S\textsubscript{ij} = -\textless{}E\textsubscript{ij}, V\textsubscript{ij}\textgreater{}, -according to sub-clocks. +The resulting set of connected components, is the partitioning of the equations and variables, $S_{ij} = \left\langle E_{ij},\, V_{ij} \right\rangle$, according to sub-clocks. -The resulting sets of equations and variables shall be possible to solve separately, -meaning that systems of equations cannot involve different sub-clocks. +The resulting sets of equations and variables shall be possible to solve separately, meaning that systems of equations cannot involve different sub-clocks. It can be noted that: - -$E_{ij} \bigcap E_{kl} = \emptyset~ \forall i\ne{}k, j\ne{}l$ - -$ V_{ij} \bigcap V_{kl} = \emptyset~ \forall i\ne{}k, j\ne{}l$ - -$V = \bigcup V_{ij}$ - -$E = \bigcup E_{ij}$ +\begin{equation*} +\begin{aligned} +E_{ij} \bigcap E_{kl} &= \emptyset,\, \forall i\ne{}k, j\ne{}l \\ +V_{ij} \bigcap V_{kl} &= \emptyset,\, \forall i\ne{}k, j\ne{}l \\ +V &= \bigcup V_{ij} \\ +E &= \bigcup E_{ij} +\end{aligned} +\end{equation*} \begin{example} After sub-clock partitioning of the example from \cref{base-clock-partitioning}, the following partitions are identified: