Clean up non-normative content in statemachines.tex

chapters/statemachines.tex

@@ -1,6 +1,7 @@
 \chapter{State Machines}\doublelabel{state-machines}
 
-{[}\emph{This chapter defines language elements to define clocked state
+\begin{nonnormative}
+This chapter defines language elements to define clocked state
 machines. These state machines have a similar modeling power as
 Statecharts (Harel 1987) and have the important feature that at one
 clock tick, there is only one assignment to every variable (for example,
@@ -10,41 +11,40 @@ \chapter{State Machines}\doublelabel{state-machines}
 and deactivate clocked equations and blocks at a clock tick. An
 efficient implementation will only evaluate the equations and blocks
 that are active at the current clock tick. With other Modelica language
-elements, this important feature cannot be defined.}
+elements, this important feature cannot be defined.
 
-\emph{The semantics of the state machines defined in this chapter is
+The semantics of the state machines defined in this chapter is
 inspired by mode automata and is basically the one from Lucid Synchrone
 3.0 (Pouzet 2006). Note, safety critical control software in aircrafts
 is often defined with such kind of state machines. The following
-properties are different to Lucid Synchrone 3.0:}
-
+properties are different to Lucid Synchrone 3.0:
 \begin{itemize}
 \item
-  \emph{Lucid Synchrone has two kinds of transitions: \emph{strong} and
+  Lucid Synchrone has two kinds of transitions: \emph{strong} and
   \emph{weak} transitions. Strong transitions are executed before the
   actions of a state are evaluated and weak transitions are executed
   after the actions of a state are evaluated. This can lead to
   surprising behavior, because the actions of a state are skipped if it
   is activated by a weak transition and exited by a true strong
-  transition.\\
+  transition.
+
   For this reason, the state machines in this chapter use \emph{immediate}
   (= the same as \emph{strong}) and \emph{delayed} transitions. Delayed
   transitions are \emph{immediate} transitions where the condition is
-  automatically delayed with an implicit \textbf{previous}(..). }
+  automatically delayed with an implicit \lstinline!previous(..)!.
 \item
-  \emph{Parallel state machines can be explicitly synchronized with a
+  Parallel state machines can be explicitly synchronized with a
   language element (similarly as parallel branches in Sequential
   Function Charts). This often occurring operation can also be defined
   in Statecharts or in Lucid Synchrone state machines but only
-  indirectly with appropriate conditions on transitions.}
+  indirectly with appropriate conditions on transitions.
 \item
-  \emph{Modelica blocks can be used as states. They might contain
+  Modelica blocks can be used as states. They might contain
   clocked or clocked discretized continuous-time equations (in the
   latter case, the equations are integrated between the previous and the
-  next clock tick, if the corresponding state is active).}
+  next clock tick, if the corresponding state is active).
 \end{itemize}
-
-{]}
+\end{nonnormative}
 
 \section{Transitions}\doublelabel{transitions}
 
@@ -67,18 +67,18 @@ \section{Transitions}\doublelabel{transitions}
 \end{tabular}
 &
 Arguments \lstinline!from! and \lstinline!to! are block instances and \lstinline!condition! is a
-Boolean argument. The optional arguments \lstinline!immediate!, \lstinline!reset!, and
-\lstinline!synchronize! are of type Boolean, have parametric variability and a
+\lstinline!Boolean! argument. The optional arguments \lstinline!immediate!, \lstinline!reset!, and
+\lstinline!synchronize! are of type \lstinline!Boolean!, have parametric variability and a
 default of \textbf{true, true, false} respectively. The optional
-argument \lstinline!priority! is of type Integer, has parametric variability and
+argument \lstinline!priority! is of type \lstinline!Integer!, has parametric variability and
 a default of 1.
 
 This operator defines a transition from instance \lstinline!from! to instance
 \lstinline!to!. The \lstinline!from! and \lstinline!to! instances become states of a state
 machine. The transition fires when condition = \textbf{true} if
-immediate = \textbf{true} (this is called an \emph{immediate transition})
+immediate = \textbf{true} (this is called an \firstuse{immediate transition})
 or \textbf{previous}(condition) when immediate = \textbf{false} (this is
-called a \emph{delayed transition}). Argument \lstinline!priority! defines the
+called a \firstuse{delayed transition}). Argument \lstinline!priority! defines the
 priority of firing when several transitions could fire. In this case the
 transition with the smallest value of \lstinline!priority! fires. It is required
 that $\textrm{priority}\ge 1$ and that for all transitions from the same state, the
@@ -110,24 +110,24 @@ \section{Transitions}\doublelabel{transitions}
 operator returns \textbf{false}.
 
 It is an error if the instance is not a state of a state machine.\\ \hline
-\textbf{ticksInState()} & Returns the number of ticks of the clock of the state machine
+\lstinline!ticksInState()! & Returns the number of ticks of the clock of the state machine
 for which the currently active state has maintained its active state without interruption,
 i.e. without local or hierarchical transitions from this state.
 In the case of a self-transition to the currently active state or to an active enclosing state,
 the number is reset to one.
 This function can only be used in state machines.\\ \hline
-\textbf{timeInState()} & Returns the time duration as Real in {[}s{]}
+\lstinline!timeInState()! & Returns the time duration as \lstinline!Real! in {[}s{]}
 for which the currently active state has maintained its active state without interruption,
 i.e. without local or hierarchical transitions from this state.
 In the case of a self-transition to the currently active state or to an active enclosing state,
 the time is reset to zero.
 This function can only be used in state machines.\\ \hline
-
 \end{longtable}
+
 \begin{example}
-If there is a transition with immediate=false from
-state A1 to A2 and the condition is ticksInState() $\ge 5$, and A1 became
-active at 10ms, and the clock period is 1ms, then A1 will be active at
+If there is a transition with \lstinline!immediate=false! from
+state \lstinline!A1! to \lstinline!A2! and the condition is \lstinline!ticksInState() >= 5!, and \lstinline!A1! became
+active at 10ms, and the clock period is 1ms, then \lstinline!A1! will be active at
 10ms, 11ms, 12ms, 13ms, 14ms, and will be not active at 15 ms.
 \begin{lstlisting}[language=modelica]
   block State end State;
@@ -140,6 +140,7 @@ \section{Transitions}\doublelabel{transitions}
   transition(A1, A2, ticksInState() >= 5, immediate=false);
 \end{lstlisting}
 \end{example}
+
 \section{State Machine Graphics}\doublelabel{state-machine-graphics}
 
 \begin{nonnormative}
@@ -156,10 +157,10 @@ \section{State Machine Graphics}\doublelabel{state-machine-graphics}
 lines.
 \end{nonnormative}
 
-The annotation for graphics of \textbf{transition}() has the following
-structure: \textbf{annotation}(Line(\ldots{}), Text(\ldots{})); and for
-\textbf{initialState}(): \textbf{graphical-primitives}(Line(\ldots{})); with Line
-and Text annotations defined in \autoref{annotations}.
+The annotation for graphics of \lstinline!transition()! has the following
+structure: \lstinline[mathescape=true]!annotation(Line($\ldots$), Text($\ldots$))!; and for
+\lstinline!initialState()!: \emph{graphical-primitives}\lstinline[mathescape=true]!(Line($\ldots$))!; with \lstinline!Line!
+and \lstinline!Text! annotations defined in \autoref{annotations}.
 
 \begin{example}
 \begin{lstlisting}[language=modelica]
@@ -195,18 +196,17 @@ \section{State Machine Graphics}\doublelabel{state-machine-graphics}
 
 If the condition text is somewhat distant from the perpendicular line, a
 dimmed straight line joins the transition text and the perpendicular
-line {[} \emph{See the rightmost transition above.} {]}.
+line.  (See the rightmost transition above.)
 
 If \lstinline!reset=true!, a filled arrow head is used otherwise an open arrow head.
 For \lstinline!synchronize=true!, an inverse ``fork'' symbol is used in the
-beginning of the arrow {[} \emph{See the rightmost transition above.}
-{]}.
+beginning of the arrow.  (See the rightmost transition above.)
 
 The value of the \lstinline!priority! attribute is prefixing the condition text
 followed by a colon if \lstinline!priority! \textgreater{} 1.
 
 The \lstinline!initialState! line has a filled arrow head and a bullet at the
-opposite end of the initial state {[} \emph{as shown above} {]}.
+opposite end of the initial state (as shown above).
 
 \section{State Machine Semantics}\doublelabel{state-machine-semantics}
 
@@ -226,16 +226,16 @@ \section{State Machine Semantics}\doublelabel{state-machine-semantics}
 The transitions are sorted with lowest priority number last in the
 array; and the priorities must be unique for each value of \lstinline!from!. The
 states are enumerated from 1 and up. The transition conditions are
-stored in a separate array c{[}:{]} since they are time varying.
-
-  The semantics model is a discrete-time system with inputs \{ c{[}:{]},
-  active, reset\} with t being an array corresponding to the inputs to the
-  transition operator, outputs \{activeState, activeReset,
-  activeResetStates{[}:{]}\} and states \{nextState, nextReset,
-  nextResetStates{[}:{]}\}. For a top level state machine, active is
-  always true. For sub-state machines, active is true only when the parent
-  state is active. For a top level state machine, reset is true at the
-  first activation only. For sub-state machine, reset is propagated from
+stored in a separate array \lstinline!c[:]! since they are time varying.
+
+The semantics model is a discrete-time system with inputs \{\lstinline!c[:]!,
+\lstinline!active!, \lstinline!reset!\} with \lstinline!t! being an array corresponding to the inputs to the
+transition operator, outputs \{\lstinline!activeState!, \lstinline!activeReset!,
+\lstinline!activeResetStates[:]!\} and states \{\lstinline!nextState!, \lstinline!nextReset!,
+\lstinline!nextResetStates[:]!\}. For a top level state machine, active is
+always true. For sub-state machines, active is true only when the parent
+state is active. For a top level state machine, reset is true at the
+first activation only. For sub-state machine, reset is propagated from
 the state machines higher up.
 
 \subsection{State Activation}\doublelabel{state-activation}
@@ -282,7 +282,7 @@ \subsection{State Activation}\doublelabel{state-activation}
 	for i in 1:size(t,1));
 \end{lstlisting}
 
-In a similar way, the Integer delayed is calculated as the index for a
+In a similar way, the \lstinline!Integer delayed! is calculated as the index for a
 potentially delayed transition, i.e. a transition taking place at the
 next clock tick. In this case the from-state needs to be equal to
 nextState:
@@ -358,7 +358,7 @@ \subsection{Activation handling}\doublelabel{activation-handling}
 
 The execution of a sub-state machine has to be suspended when its
 enclosing state is not active. This activation flag is given as a
-Boolean input \lstinline!active!. When this flag is true, the sub-state machine
+\lstinline!Boolean! input \lstinline!active!. When this flag is true, the sub-state machine
 maintains its previous state, by guarding the equations of the state
 variables \lstinline!nextState!, \lstinline!nextReset! and \lstinline!nextResetStates!.
 
@@ -460,43 +460,42 @@ \subsection{Merging Connections to Multiple Outputs}\doublelabel{merging-connect
 
 \subsection{Example}\doublelabel{example}
 
-\emph{{[} Consider the following hierarchical state machine:}
+\begin{example}
+Consider the following hierarchical state machine:
 
 \includegraphics[width=5.34375in,height=5.72917in]{statemachine2}
 
-\emph{The model demonstrates the following properties:}
-
+The model demonstrates the following properties:
 \begin{itemize}
 \item
-  \emph{\lstinline!state1! is a meta state with two parallel state machines in it.}
+  \lstinline!state1! is a meta state with two parallel state machines in it.
 \item
-  \emph{\lstinline!stateA! declares \lstinline!v! as \lstinline!outer output!. \lstinline!state1! is on an intermediate
+  \lstinline!stateA! declares \lstinline!v! as \lstinline!outer output!. \lstinline!state1! is on an intermediate
   level and declares \lstinline!v! as \lstinline!inner outer output!, i.e. matches lower level
   \lstinline!outer v! by being \lstinline!inner! and also matches higher level \lstinline!inner v! by being
-  \lstinline!outer!. The top level declares \lstinline!v! as \lstinline!inner! and gives the start value.}
+  \lstinline!outer!. The top level declares \lstinline!v! as \lstinline!inner! and gives the start value.
 \item
-  \emph{\lstinline!count! is defined with a start value in \lstinline!state1!. It is reset when
-  a reset transition (v\textgreater{}=20) is made to \lstinline!state1!.}
+  \lstinline!count! is defined with a start value in \lstinline!state1!. It is reset when
+  a reset transition (v\textgreater{}=20) is made to \lstinline!state1!.
 \item
-  \emph{\lstinline!stateX! declares the local variable \lstinline!w! to be equal to \lstinline!v! declared
-  as \lstinline!inner input!.}
+  \lstinline!stateX! declares the local variable \lstinline!w! to be equal to \lstinline!v! declared
+  as \lstinline!inner input!.
 \item
-  \emph{\lstinline!stateY! declares a local counter \lstinline!j!. It is reset at start and as a
-  consequence of the reset transition (v\textgreater{}=20) to \lstinline!state1!:}
+  \lstinline!stateY! declares a local counter \lstinline!j!. It is reset at start and as a
+  consequence of the reset transition (v\textgreater{}=20) to \lstinline!state1!:
   When the reset transition ($v\ge 20$) fires, then the variables of the
   active states are reset immediately (so \lstinline!count! from \lstinline!state1!, and \lstinline!i!
   from \lstinline!stateX!). The variables of other states are only reset at the time
   instants when these states become active. So \lstinline!j! in \lstinline!StateY! is reset to
   0, when the transition \lstinline!stateX.i! \textgreater{} 20 fires (after \lstinline!state1!
   became active again, so after the reset transition $v\ge 20$).
 \item
-  \emph{Synchronizing the exit from the two parallel state machines of
+  Synchronizing the exit from the two parallel state machines of
   \lstinline!state1! is done by checking that \lstinline!stated! and \lstinline!stateY! are active using the
-  \lstinline!activeState! function.}
+  \lstinline!activeState! function.
 \end{itemize}
 
-\emph{The Modelica code (without annotations) is:}
-
+The Modelica code (without annotations) is:
 \begin{lstlisting}[language=modelica]
 block HierarchicalAndParallelStateMachine
   inner Integer v(start=0);
@@ -578,14 +577,14 @@ \subsection{Example}\doublelabel{example}
 end HierarchicalAndParallelStateMachine;
 \end{lstlisting}
 
-\emph{The behavior of the state machine can be seen in the plots of v:}
+The behavior of the state machine can be seen in the plots of \lstinline!v!:
 \begin{figure}[H]
 \includegraphics[width=4.16667in,height=2.91667in]{statemachineplot}
 \end{figure}
-\emph{The transition from \lstinline!state1! to \lstinline!state2! could have been done with a
-\lstinline!synchronize! transition with \lstinline!condition=true! instead. The semantically
-equivalent model is shown below:}
 
+The transition from \lstinline!state1! to \lstinline!state2! could have been done with a
+\lstinline!synchronize! transition with \lstinline!condition=true! instead. The semantically
+equivalent model is shown below:
 \begin{lstlisting}[language=modelica]
 block HierarchicalAndParallelStateMachine
   extends StateMachineSemantics(
@@ -697,3 +696,4 @@ \subsection{Example}\doublelabel{example}
   end if;
 end HierarchcialAndParallelStateMachine;
 \end{lstlisting}
+\end{example}