small changes

paper/sections/03-model.tex

@@ -192,7 +192,7 @@ font=\footnotesize]
 % arrows from 2
 \draw [arr] (cs) to node [above] {\texttt{fetch\_freq\&phase}} (re);
 \draw [arr, in=60, out=120] (cs) to node [above, xshift=1mm] {\texttt{turn\_off}} (ni);
-\draw [arr, in=210, out=240] (cs) edge[loop] node [below, xshift=-6mm] {\texttt{lose\_visibility}} (cs);
+%\draw [arr, in=210, out=240] (cs) edge[loop] node [below, xshift=-6mm] {\texttt{lose\_visibility}} (cs);
 
 % arrows from 3
 \draw [arr] (re) to node [above] {\texttt{get\_ephemeris}} (pa); 
@@ -212,7 +212,7 @@ font=\footnotesize]
 \draw [arr, in=-45, out=0] (ws) to node [right, near start, xshift=1mm] {\texttt{fetch\_freq\&phase}} (pa);
 \draw [arr, in=285, out=135] (ws) to node [near end, above, xshift=13mm, yshift=-2mm] {\texttt{ephemeris\_expire}} (cs);
 \draw [arr, in=-10, out=190] (ws) to node [above] {\texttt{turn\_off}} (wsa);
-\draw [arr, in=-60, out=-30] (ws) edge[loop] node [below] {\texttt{lose\_visibility}} (ws);
+%\draw [arr, in=-60, out=-30] (ws) edge[loop] node [below] {\texttt{lose\_visibility}} (ws);
 
 % arrows from 6 - warm start available
 \draw [arr, in=170, out=10] (wsa) to node [above] {\texttt{turn\_on}} (ws);
@@ -238,7 +238,9 @@ Detecing data from more than 4 satellites improves the positioning
 accuracy. As for power consumption, the receiver always consumes a
 (negligible) idle power. On top of that, the sensor consumes
 additional power when its radio is turned on, which is precisely the
-cause of battery draining. \textcolor{red}{This power has been experimentally shown to be constant in time~\cite{bib:enloc-smartphones}~\cite{bib:microsoft-leap} and usually around 400mW.}. Our model needs to capture whether:
+cause of battery draining. This power has been experimentally shown to
+be constant in time~\cite{bib:enloc-smartphones, bib:microsoft-leap}
+and usually around 400mW. Our model needs to capture whether:
 \begin{enumerate}
   \item \emph{ephemeris data} are available or not;
   \item \emph{ranging data} are available or not;
@@ -284,9 +286,11 @@ fetched. We refer to this transition as
 causes: (i) the antenna is turned off (transition \texttt{turn\_off}),
 (ii) the number of visible satellites is less than the required
 one\footnote{Generally 4. Different applications may require a higher
-  number of satellites to improve positioning accuracy (\textcolor{red}{https://www.developerfusion.com/article/4652/writing-your-own-gps-applications-part-2/2/}).} (transition
-\texttt{lose\_visibility}). Lastly the antenna's state is controlled
-by the user with the events \texttt{turn\_on} and \texttt{turn\_off}.
+  number of satellites to improve positioning accuracy
+  (\url{https://www.developerfusion.com/article/4652/writing-your-own-gps-applications-part-2/2/}).}
+(transition \texttt{lose\_visibility}). Lastly the antenna's state is
+controlled by the user with the events \texttt{turn\_on} and
+\texttt{turn\_off}.
 
 The transitions can be divided in three categories: \emph{inputs},
 \emph{delays}, and \emph{disturbances}. The two transitions
@@ -328,13 +332,9 @@ properties that define it. For instance, if the antenna is off (states
 No Info \textcircled{\scriptsize 1} and Warm Start Available
 \textcircled{\scriptsize 6}), the automaton can accept the transition
 \texttt{turn\_on} and move to a different state, but cannot accept the
-transition \texttt{turn\_off}. \textcolor{red}{There are three exceptions,
-corresponding to the self-loops in Figure~\ref{fig:cyberDynamics}. In
-state Cold Start \textcircled{\scriptsize 2} and Warm Start
-\textcircled{\scriptsize 5}, the ranging data are not available. The
-transition \texttt{lose\_visibility}, that models the loss of ranging
-data, can be fired to capture the interruption of the ongoing
-acquisition process, that has to be restarted.}\todo{remove alro transitions from figure.} In state Position Available \textcircled{\scriptsize 4} the transition
+transition \texttt{turn\_off}. There is one exception, corresponding
+to the self-loop in Figure~\ref{fig:cyberDynamics}. In state Position
+Available \textcircled{\scriptsize 4} the transition
 \texttt{get\_ephemeris} can be fired to indicate an update of the
 ephemeris data before their expiration.