Use math where appropriate in description of clock partitioning

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,39 +879,34 @@ \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)!,
 \lstinline!y = subSample(u)!,
 \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: