diff --git a/report/sections/02-How_it_works.tex b/report/sections/02-How_it_works.tex
index 16a76a5cff2d31ae1ed027da22baa56fb09f5975..84c34957eca22b5f8fe6187a7709b41a3bbed00e 100644
--- a/report/sections/02-How_it_works.tex
+++ b/report/sections/02-How_it_works.tex
@@ -8,21 +8,12 @@ All reported in this section (unless stated differently) is referenced by the bo
 
 The Global Positioning System (GPS) is the only positioning system that provides an absolute measure and is available worldwide. This is achieved using a constellation of space vehicles (SV) whose position is known with an high grade of accuracy and that is designed in such a way that at least five of them are visible at any time in every point over the world. 
 
-Any device able to listen to the signals broadcasted by the satellites can retrieve (i) their position and (ii) its distance from those: performing specific computations over this information it will be able to locate itself. We call such device a \textbf{GPS receiver}. The cited computation is called \emph{trilateration}, and it requires to listen to at least three satellites at the same time since the spatial coordinates to be determied are three. 
+Any device able to listen to the signals broadcasted by the satellites can retrieve (i) their position and (ii) its distance from those: performing specific computations over this information it will be able to locate itself. We call such device a \textbf{GPS receiver}. The cited computation is called \emph{trilateration}, and it theoretically requires to listen to at least three satellites at the same time since the spatial coordinates to be determied are three. 
 
-From a technological perspective the measure of the distance from the satellites is based on a time difference, and it assumes that the time reference is the same for the SV and the receiver. Since this is apparently not true for devices that do not contain atomic clocks -- i.e. most of the commonly used GPS receivers -- another constraint must be introduced. This is done in order to be able to treat also the receiver time offset as an unknown variable. For this reason at least four satellites must be visible to be able to position the receiver. In case the receiver can listen to more than four satellites those can still be used to improve accuracy.
+From a technological perspective the measure of the distance from the satellites is based on a time difference, and it assumes that the time reference is the same for the SV and the receiver. Since this is apparently not true for devices that do not contain atomic clocks -- i.e. most of the commonly used GPS receivers -- another constraint must be introduced. This is done in order to be able to treat also the receiver time offset as an unknown variable. For this reason at least four satellites must be visible to be able to position the receiver. In case the receiver can listen to more than four satellites those can also be used to improve accuracy.
 
 It shall be underlined moreover that the receiver only needs to listen to the SVs and it doesn't need to send any message.
 
-\subsection{Positioning the satellites}
-The position of the SVs can be retrieved from a set of parameters that describe their orbit around the earth. Since the orbits are not fixed in time due to trajectory corrections, collision avoidance or other uncertainties and disturbances such parameters need to be continuously updated. To make those parameters always available the satellites broadcast them toward the earth surface. 
-
-Two kind of data are broadcast and can be used for SV positioning: \emph{almanac data} or \emph{ephemeris data}. The former are a subset of the latter (7 parameters out of 15) and are valid for several months while the latter are valid for 30 minutes after they are broadcast. Being apparently less precise the achivable precision with only the almanac data is around one order of magnitude less when used for positioning. The difference in time validity allows on the other side that satellites are able to share such information betwen each other and therefore each of them transmits the almanac data for every satellite. The ephemeris data of each satellite are instead transmitted only by the SV itself. In practice almanac data are mainly used by the receiving devices to know which SVs will be visible at a certain point in time and speed up the tracking phase, the ephemeris data are instead the ones actually used for the positioning.
-
-The ephemeris data are fully repeated every 30 seconds by each SV. They are exact at the beginning of each of those half-minute cycles and are considered to be valid for 30 minutes. With those the receiver is able to achieve a precision of the order of meters in the positioning.
-
-Since there are stations around the world that listen at the satellites and make the ephemeris data available in the internet devices that are also connected to the internet, instead of listening to the satellites can retrieve the ephemeris data from the web. This avoids the bottleneck of the GPS transmission channel which has a capacity of 50bit/s and is at the basis of the 30 seconds that are necessary for retrieving them. Such intenet-connected implementation of the GPS positioning system is called \textbf{Assisted-GPS}.
-
 \subsection{GPS signal modulation and multiplexing}
 The GPS signal sent by the satellites is modulated using the Binary Phase Shift Key (BPSK) technique that includes the bit information in a $180^0$ phase shift of the carrier wave. This means that the carrier is transmitted ``as is'' or in counter-phase according to whether a 0 or 1 is being transmitted, an example is shown in figure~\ref{fig:bpsk}. 
 
@@ -35,9 +26,9 @@ The GPS signal sent by the satellites is modulated using the Binary Phase Shift
  \end{center}
 \end{figure}
 
-The signals from the different satellites are multiplexed on the same carrier frequency using Code Division Multiple Access (CDMA), more precisely Direct Sequence Spread Spectrum (DSSS) technique is used. In this methodology the data (in our case the ephemeris and almanac data) are trasmitted overlapped with another signal at much higher simbol rate. Therefore the data are considered a \emph{baseband} signal while the latter is referred to as a \emph{spreading} waveform, meaning that the former can be considered at almost zero frequency with respect to the other signals (the carrier and the spreading sequence). The spreading sequence is a periodic signal and is completely known by the receivers, it is the ``key'' that the receivers will use for distinguishing the signals from the different sources. In the GPS system sequences of PseudoRandom Noise called \emph{golden codes} are used as spreading signals: those deterministic codes have the property of looking like white noises (so to have null correlation with themself) and are not correlated with each other. As we will see in section~\ref{sec:receiverSegment} both those properties are crucial for the GPS system to actually work.
+The signals from the different satellites are multiplexed on the same carrier frequency using Code Division Multiple Access (CDMA), more precisely Direct Sequence Spread Spectrum (DSSS) technique is used. In this methodology the data (in our case the ephemeris and almanac data) are trasmitted overlapped with another signal at much higher simbol rate. The data are therefore considered a \emph{baseband} signal while the latter is referred to as a \emph{spreading} waveform, meaning that the former can be considered at almost zero frequency with respect to the other signals (the carrier and the spreading sequence). The spreading sequence is a periodic signal and is completely known by the receivers, it is the ``key'' that the receivers will use for distinguishing the signals from the different sources. In the GPS system sequences of PseudoRandom Noise called \emph{golden codes} are used as spreading signals: those deterministic codes have the property of looking like white noises (so to have null correlation with themself) and are not correlated with each other. As we will see in section~\ref{sec:receiverSegment} both those properties are crucial for the GPS system to actually work.
 
-The GPS signal sent by each satellite has therefore three components: the carrier, the localization data and the PRN sequence. As we can see in figure~\ref{fig:dsss}. The signal is broadcast in parallel on different band frequencies L1 (1575.42 MHz) and L2 (1227.60 MHz).
+The GPS signal sent by each satellite has therefore three components: the carrier, the localization data and the PRN sequence, a grsficsl example of this is shown in figure~\ref{fig:dsss}. The signal is broadcast in parallel on different band frequencies L1 (1575.42 MHz) and L2 (1227.60 MHz).
 
 \begin{figure}[htb]
  \begin{center}
@@ -48,9 +39,18 @@ The GPS signal sent by each satellite has therefore three components: the carrie
  \end{center}
 \end{figure}
 
+\subsection{Positioning the satellites}
+The position of the SVs can be retrieved from a set of parameters that describe their orbit around the earth. Since the orbits are not fixed in time due to trajectory corrections, collision avoidance or other uncertainties and disturbances, such parameters need to be continuously updated. To make those parameters always available the satellites broadcast them toward the earth surface. 
+
+Two kind of data are broadcast and can be used for SV positioning: \emph{almanac data} or \emph{ephemeris data}. The former are a subset of the latter (7 parameters out of 15) and are valid for several months while the latter are valid for 30 minutes after they are broadcast. Being apparently less precise the achivable precision with only the almanac data is around one order of magnitude less when used for positioning. The difference in time validity allows on the other side that satellites are able to share such information betwen each other and therefore each of them transmits the almanac data for every satellite. The ephemeris data of each satellite are instead transmitted only by the SV itself. In practice almanac data are mainly used by the receiving devices to know which SVs will be visible at a certain point in time and speed up the tracking phase, the ephemeris data are instead the ones actually used for the positioning.
+
+The ephemeris data are fully repeated every 30 seconds by each SV. They are exact at the beginning of each of those half-minute cycles and are considered to be valid for 30 minutes. With those the receiver is able to achieve a precision of the order of meters in the positioning.
+
+Since there are stations around the world that listen at the satellites and make the ephemeris data available in the internet devices that are also connected to the internet, instead of listening to the satellites can retrieve the ephemeris data from the web. This avoids the bottleneck of the GPS transmission channel which has a capacity of 50bit/s and is at the basis of the 30 seconds that are necessary for retrieving them. Such intenet-connected implementation of the GPS positioning system is called \textbf{Assisted-GPS}.
+
 \subsection{Measuring the distance from the satellites}
 \label{measuring_distance}
-The distance between the receiving device and the satellites is determined measuring the time it takes for the microwave signal generated by the satellite to reach the receiver. Since both the SVs and the receivers know exactly the PRN code this can be done measuring the phase shift with which such signal is received by the device. The sender and the receiver generate the same signal with the same time reference: assumming that the clocks of the receiver and of the SV are synchronized the phase delay of the signal received by the GPS device will be equivalent to the distance divided by the speed of light. This way the receiver only needs to measure how much it has to delay the PRN code (generating the so-called \emph{replica code}) in order to measure the distance from the SV, a graphical representaiton of this is shown in figure~\ref{fig:phase_delay}. As a consequence the bit rate of the PRN code defines the maximum resolution achivable with this technology.
+The distance between the receiving device and the satellites is determined measuring the time it takes for the microwave signal generated by the satellite to reach the receiver. Since both the SVs and the receivers know exactly the PRN code this can be done measuring the phase shift (i.e. the delay) with which such signal is received by the device. The sender and the receiver generate the same signal with the same time reference: assumming that the clocks of the receiver and of the SV are synchronized the phase delay of the signal received by the GPS device will be equivalent to the distance divided by the speed of light. This way the receiver only needs to measure how much it has to delay the PRN code (generating the so-called \emph{replica code}) in order to measure the distance from the SV, a graphical representaiton of this is shown in figure~\ref{fig:phase_delay}. As a consequence the bit rate of the PRN code defines the maximum resolution achivable with this technology.
 
 Since the atomic clocks of the different satellites are deisgned to be extremely stable and precise they can be considered synchronized (they are also corrected on a regulard basis), this way the only one extra variable as to be introduced to compensate for the non-synchronization is the receiver's clock.
 
@@ -67,12 +67,12 @@ Since the atomic clocks of the different satellites are deisgned to be extremely
 \label{sec:receiverSegment}
 A GPS receiver listens to the satellite signals through an antenna. The device must then decode the signal to identify the visible satellites, locate them and retrieve the distance from those. Since the satellites and the receivers are moving with respect to each other there will also be a distortion in the signal frequencies due to the doppler effect. This implies that for decoding the GPS signal for a given satellite the receiver must perform a two-dimensional search: in frequency and phase. The device will generate the replica code and distorce it in both frequency and phase shift it until it correlates with the GPS signal received from the antenna. This is why the correlation properties of the golden codes are so critical. First since they look like white-noises they will not correlate to themselfes unless they have the same phase shift. Second they do not correlate with each other avoiding the risk of not distinguishing the signal from different satellites.
 
-Once frequency and phase are tracked two information are directly accessible: (i) the phase as described in section~\ref{measuring_distance} allows to retrieve the ranging data (i.e. the distance) from the satellite, (ii) the frequency instead since its shift is directly related to the relative speed betwen the receiver and the satellite and the satellite's speed is known from the ephemeris data can be used to directly measure the speed.
+Once frequency and phase are tracked two information are directly accessible: the ranging data and the speed of the receiver. The ranging data are computed from the phase as described in section~\ref{measuring_distance} from the phase shift. The speed instead can be computed from the relative speed measured with the doppler frequency and the satellite speed that is known from the ephemeris data.
 
-It must be recalled that also the location data are sent by the satellite and those, according to whether a 0 or 1 is being trasmitted, can turn the PRN code into its complement (in the sense of logical negation) or leave it as it is. Depending on whether the replica code or its complement correlates with the signal itself the receiver is able to tell if a 0 or 1 is being transmitted. This relies on the fact that the location data are transmitted at much lower frequency (a baseband signal) with respect the spreading waveform and therefore don't interfere.
+It must be recalled that also the location data are sent by the satellite and those, according to whether a 0 or 1 is being trasmitted, can turn the PRN code into its complement (in the sense of logical negation) or leave it as it is. Depending on whether the replica code or its complement correlates with the signal itself the receiver is able to tell if a 0 or 1 is being transmitted. This exploits the fact that the location data are transmitted at much lower frequency (a baseband signal) with respect the spreading waveform and therefore don't interfere.
 
 \subsection{The receiver technologies}
-Until some years ago due to performance limitations of processors the processing of the GPS signal was performed with embedded circuits, hence not programmable: a GPS receiver was just a set of circuits that would listen to the satellites and provide the position as output. Nowadays it is possible to digitalize the GPS signal (after downconverting it to lower frequencies) and decode it with programs written in high level languages, allowing for more degrees of freedom when implementing a GPS receiver. This is called software-based GPS receiver, as opposed to the previous hardware-based ones. According to this the components of a software-based GPS receiver are: the antenna, a down-converter\footnote{The down converter lowers the frequency spectrum of the signal making it managable by the A/D converter.}, an A/D converter and a sufficiently performing processor programmable in high-level language.
+Until some years ago due to performance limitations of processors the processing of the GPS signal was performed with embedded circuits, hence not programmable: a GPS receiver was just a set of circuits that would listen to the satellites and provide the position as output. Nowadays it is possible to digitalize the GPS signal (after downconverting it to lower frequencies) and decode it with programs written in high level languages, allowing for more degrees of freedom when implementing a GPS receiver. This technology is called software-based GPS receiver, as opposed to the previous hardware-based ones. According to this the components of a software-based GPS receiver are: the antenna, a down-converter\footnote{The down converter lowers the frequency spectrum of the signal making it managable by the A/D converter.}, an A/D converter and a sufficiently performing processor programmable in high-level language.
 
 %\subsection{Other aspects taken into account in GPS devices}
 %\textcolor{red}{NOT SURE IF TO INCLUDE THIS}
diff --git a/report/sections/03-Modeling.tex b/report/sections/03-Modeling.tex
index 2f0a43bb856c42842b19b7fca7a2858f73f64677..39582abd148554627deb2d3753691c2c63f75c4b 100644
--- a/report/sections/03-Modeling.tex
+++ b/report/sections/03-Modeling.tex
@@ -13,52 +13,50 @@ The following sections discuss the choices for the inputs and outputs for the mo
 
 \subsection{Input definition}
 \label{sec:input-def}
-The sensor interacts with the user (in obth the cases that it is a human or an application running on the same device) receiving ON/OFF control signals. This signal must therefore be considered when modeling a GPS sensor.
+The sensor interacts with the user (in both the cases that it is a human or an application running on the same device) receiving ON/OFF control signals. This signal must therefore be considered when modeling a GPS sensor.
 
 Once turned on the sensor listens to the signals broadcasted by the different satellites. If we neglect distinguishing the different satellites this can be captured by an integer representing the number of visible satellites. 
 
 %Another modeling approach could be to capture instead whether each of the satellites is visible or not. 
-Modeling indepentendtly the different satellites would increase the complexity of the model but provide quite marginal improvement in the descriptive power. This because the dynamics with which the device listens to the different SVs are strongly synchronized. Whenever the sensor is fetching the frequency, phase or ephemeris data it can be done in parallel for all of the visible satellites. Not distinguishing between the different satellites doesn't allow to simulate precisely how long it will take to get those information since the dynamics of fetching of each of the satellites cannot be captured\footnote{Also other corner cases will not be captured by the model because of this simplifying assumption: such cases are mainly related to the fact that the loss of connection with some satellite is not coordinated instead.\textcolor{red}{AN EXAMPLE OF THIS SHOULD BE MADE AFTER THE MODEL IS PRESENTED: the problem arises when the same satellte disappears and come back fast enough that the device should still have ephemeris data available. Another case is when a extra satellite is seen but not tracked, if after that another satellite is no more visible then the ephemeris data are of the previous satellite but this is not recognized by the model since the number of visible satellites is the same as before.}}. On the other side this can be replaced with rigorous worst-case analysis or probabilistic modeling with bounded errors with respect to a precise model. Also it should be considered that we are interested in the behavior of the overall device, not in the tracking of the single satellite.
+Modeling indepentendtly the different satellites would increase the complexity of the model but provide quite marginal improvement in the descriptive power. This because the dynamics with which the device listens to the different SVs are strongly synchronized. Whenever the sensor is fetching the frequency, phase or ephemeris data it can do it in parallel for all of the visible satellites. Not distinguishing between the different satellites doesn't allow to simulate precisely how long it will take to get this information since the dynamics of fetching of each of the satellite's signal cannot be captured. On the other side this can be replaced with rigorous worst-case analysis or probabilistic modeling with bounded errors with respect to a precise model. Also the loss of connection with the different satellites, which is apparently not synchronized, cannot be represented becxause of not distinguishing the different satellites. Since the interest here is modelling the behavior of the overall device, it is sufficient to detect when not enough satellites are tracked and it can be neglected which of the satellites is actually tracked.
+
+%\textcolor{red}{AN EXAMPLE OF THIS SHOULD BE MADE AFTER THE MODEL IS PRESENTED: the problem arises when the same satellte disappears and come back fast enough that the device should still have ephemeris data available. Another case is when a extra satellite is seen but not tracked, if after that another satellite is no more visible then the ephemeris data are of the previous satellite but this is not recognized by the model since the number of visible satellites is the same as before.}
 
 All of this is apparently arguable and it should be re-considered for the specific use case.
 
-The input choice for the model here presented are therefore: (i) the control signal that turns ON and OFF the antenna and (ii) the number of visible satellites. Modeling the tracking of each of the satellites individually would instead require to include whether each of the satellites is visible or not and the time reference for the broadcast of the ephemeris data of each of the satellites.
+The inputs choice for the model here presented is therefore: (i) the control signal that turns ON and OFF the antenna and (ii) the number of visible satellites\footnote{Modeling the tracking of each of the satellites individually would instead require including whether each of the satellites is visible or not and also the time reference for the broadcast of the ephemeris data for each of the satellites.}.
 
 \subsection{Output definition}
-What we want to capture with this model are the position measure and the power consumption, here we discuss and define them individually.
+What we want to capture with this model are the position availability and the power consumption, here we discuss and define them individually.
 
 \subsubsection{Modeling the position availability and accuracy}
 \label{sec:modelingThePosition}
-As stated before what we want to capture are the availability of the position information and the power consumption. It would be very useful to have a model of the accuracy of the positioning as well, but this is strongly related to the specific use cases. Accuracy of positioning depends on the number of visible satellites and the quality of the signal that is received from those satellites, but defining rigorously the relation between those and the actual accuracy is not straight forward. For instance having two satellites that are very close to each other might not make much difference from having only one of those, or capturing how the clouds (or other structures around the device) might deteriorate the satellite signal is apparently very complex. Those considerations make defining a general model with still a managable complexity rarely (if not ever) feasible. 
+As stated before what we want to capture are the availability of the position information and the power consumption. It would be very useful to have a model of the accuracy of the positioning as well, but this is a very complex problem and is strongly related to the specific use cases. Accuracy of positioning depends on the number of visible satellites, their positioning in the sky and the quality of signal transmission. Both modeling those phenomena and defining rigorously they can affect the accuracy is not straight forward. For instance having two satellites that are very close to each other might not make much difference from having only one of those, or capturing how the clouds (or other structures around the device) might deteriorate the satellite signal is apparently very complex. Those considerations make defining a general model with still a managable complexity rarely (if not ever) feasible. 
 
-If we neglect the quality of the signals received and how the satellites are distributed in the visible sky we can define the requirements over accuracy as a minimum number of satellites to be used for positioning --- which as said in section~\ref{sec:how_it_works} cannot be less than 4. The output can then be a boolean defining whether the position is available or not. This is apparently incomplete but valid in general cases with good sky visibility and not degenerate distributions of the SVs (which is avoided in most cases by the constellation design). If this approach is shown to be insufficient further extensions of this model could be investigated: for instance distinguishing the different satellites could allow for probabilistic modeling of the quality of the signal --- still leaving the problem of modeling how does this affect the quality of positioning though.
+If we neglect the quality of the signals received and how the satellites are distributed in the visible sky we can define the accuracy requirements as a minimum number of satellites to be used for positioning --- which as stated in section~\ref{sec:how_it_works} cannot be less than 4. The output can then be defined as a boolean that is true when enough satellites are tracked and therefore the position is available or false otherwise. This is apparently incomplete but valid in general cases with good sky visibility and not degenerate distributions of the SVs (which is avoided in most cases by the constellation design)\footnote{If this approach is shown to be insufficient further extensions of this model could be investigated: for instance distinguishing the different satellites could allow for probabilistic modeling of the quality of the signal --- still leaving the problem of modeling how does this affect the quality of positioning though.}.
 
 \subsubsection{Modeling the power consumption}
-A GPS device consumes power in two ways: (i) powering the antenna in order to listen to the signals from the satellites, (ii) performing the computation for the actual positioning. Experiments~\cite{bib:microsoft-leap} show that the overall power consumption of a GPS sensor is mainly related to the powering of the antenna since the GPS signal sent by the SV is not very strong good amplification of it must be performed, while the consumption due to the computation can with respect to the antenna be neglected.
+A GPS device consumes power in two ways: (i) powering the antenna, (ii) performing the computation for the positioning. Experiments~\cite{bib:microsoft-leap} show that the overall power consumption of a GPS sensor is mainly related to the powering of the antenna. The GPS signal sent by the SV is infact not very strong and good amplification of it must be performed. The power consumption related to the computations can therefore with respect to the antenna be neglected.
 
-The antenna doesn't present any relevant dynamics and consumes a constant amount of power when it is turned on. According to this the power consumption of the GPS sensor can be modeled as a prescribed constant value when the antenna is turned on or a null value when the antenna is off\footnote{Some power brusts are actually present at the start and stop of the sensor, those are not relevant with respect the overall consumption and can be neglected in a high-level analysis.}.
+The antenna doesn't present any relevant dynamics~\cite{bib:microsoft-leap} and consumes a constant amount of power when it is turned on. According to this the power consumption of the GPS sensor can be modeled as a prescribed constant value when the antenna is turned on or a null value when the antenna is off\footnote{Some power brusts are actually present at the start and stop of the sensor, those are not relevant with respect the overall consumption and can be neglected in a high-level analysis.}.
 
 \subsection{Modeling the Information Dynamics}
 \label{sec:info-dynamics}
-%\begin{itemize}
-%	\item Discuss the time to first fix and the expiration of ephemeris data and frequency and phase locking
-%	\item Discuss whether to model the single satellites or just the aggregated version
-%	\item Present the model
-%\end{itemize}
+% per il paper riscrivi definendo gli stati rilevanti (parti da quali informazioni sono necessarie --, acceso/spento, p&f tracciati e dati epfemeri -- e poi scarta le combinazioni non sensate) e poi le transizioni, sii piu' sistematico
 
-It is now defined when the sensor is consuming power, when it is not and how much it consumes. Now, for what concerns the \emph{cyber} domain we want to describe when the position is available in relation to when the sensor is consuming power. 
+It is now defined when the sensor is consuming power, when it is not and how much it consumes. Now, for what concerns the \emph{cyber} domain we want to describe when the position is available in relation to the defined inputs. 
 
-To locate the receiver two information for each satellite are required: (i) the position of the satellite and (ii) the ranging data. Those are respectively included in the ephemeris data and the phase shift of the signal of each satellite. Since to decode the signal and read the ephemeris data the device must first fetch the phase and frequency shift the retrieval of the two is connected, in the sense that the ephemeris data cannot be read without having first fetched frequency and phase. What is not correlated is instead how the different satellites stop being available and therefore the different information stop being useful. 
+To locate the receiver two information for each satellite are required: (i) the position of the visible satellites and (ii) the ranging data. Those are respectively encoded in the ephemeris data and the phase shift of the signal of each satellite. Since to decode the signal and read the ephemeris data the device must have fetched the phase and frequency shift the retrieval of the two is connected. This means for example that the ephemeris data cannot be read without having first fetched frequency and phase.
 
-The phase and frequency are instead lost as soon as the antenna is turned off and the device will have to perform a new search when the antenna is turned on again. In~\cite{bib:microsoft-leap} an algorithm that exploits previous knowledge of frequency and phase shift for improving the speed of fetching the signal has been proposed: this can be done under the assumption that the device has not moved too far away and relative speed has not changed too much from last positioning\footnote{In the discussed work the authors have only simulated what could be the improvement in performance with this method, so there has not been real testing of it.}.
+The phase and frequency are lost as soon as the antenna is turned off or a satellite is no more visible: in those cases the device has to perform a new search when the antenna is turned on again or when the satellite is visible again respectively. In~\cite{bib:microsoft-leap} an algorithm that exploits previous knowledge of frequency and phase shift for improving the speed of fetching the signal has been proposed: this can be done under the assumption that the device has not moved too far away and relative speed has not changed too much from last positioning\footnote{In the discussed work the authors have only simulated what could be the improvement in performance using this method, so there has not been real testing of it.}.
 
-The ephemeris data are characterized by a well defined expiration time, 30 minutes after being collected they will be no more accurate enough to allow correct positioning and new data must be collected. 
+The ephemeris data are characterized by a well defined expiration time, 30 minutes after being collected they won't be accurate enough to allow correct positioning and new data must be collected. 
 
-When ephemeris data are not available -- for instance when it is started -- and the device must fetch the signal and wait to read them the procedure is called \textbf{cold start}. When instead Ephemeris data are available and the device must only fetch the signal in order to get the ranging data it is called \textbf{warm start}. Here, by analogy, we introduce the notation of \textbf{hot start}, to define when the innformation about previous ranging and frequency are exploited for improving the speed of signal fetching.
+When ephemeris data are not available -- for instance at the start up -- and the device must fetch the signal and wait to read them the procedure is called \textbf{cold start}. When instead Ephemeris data are available and the device must only fetch the signal in order to get the ranging data it is called \textbf{warm start}. Here, by analogy, we introduce the notation of \textbf{hot start}, to define when the innformation about previous ranging and frequency are exploited for improving the speed of signal fetching.
 
-The relation betwen those procedures can be described as a discrete system with states representing what the system is doing and transitions representing either when those information are acquired by the device or when they lose (or have lost) validity, plus of course the input events of turning on and off the antenna. 
+The relation betwen those procedures can be described as a discrete system with states representing what the system is doing and which information are available and transitions representing either when those information are acquired by the device or when they lose (or have lost) validity, plus of course the input events of turning on and off the antenna. 
 
-\textcolor{red}{consider putting those in tables with descriptions}
+%\textcolor{red}{consider putting those in tables with descriptions}
 
 The cited transitions are:
 \begin{itemize}
@@ -67,10 +65,13 @@ The cited transitions are:
 	\item fetch frequency and phase,
 	\item fetch frequency and phase quick (in case of hot start),
 	\item get ephemeris data,
-	\item ephemeris data expired (i.e. any of the scenarios in which the data are not available, both the case that they expired and that they have not been fetched yet) %\footnote{Note that even though the expiration of ephemeris data is expressed as the fact that the data are not valid any more, hence as a condition that lasts in time, not only as an event. It is in fact defiend as \texttt{sv\_ephemeris}<\texttt{required\_satellites}.},
+	\item ephemeris data expired, 
+	\item lose visibility,
 	\item lose hot start.
 \end{itemize}
 
+All the transitions are defined with respect the minimum number of required satellites. This means for example that \emph{lose visibility} will be triggered when the signal is not tracked for the prescribed minimum number of satellites, and not in general when one of the satellites is no more visible.
+
 The states instead are:
 \begin{itemize}
 	\item No Info,
@@ -83,9 +84,9 @@ The states instead are:
 	\item Warm Start Available.
 \end{itemize}
 
-As discussed in section~\ref{sec:modelingThePosition} we also want to include in the model the number of tracked satellites, we must therefore include in the model two integers: \texttt{sv\_tracked\_freq\_phase} and \texttt{sv\_tracked\_ephemeris}. The former describes the number of satellites for which frequency and phase are known and the latter the number of satellites for which ephemeris data are available. The number of tracked satellites (both for frequency and phase and for the ephemeris data) is set equal to the number of visible satellites respectively when the transitions \emph{fetch frequency and phase} and \emph{get ephemeris} are executed.
+The model includes also two integers: \texttt{sv\_tracked\_freq\_phase} and \texttt{sv\_tracked\_ephemeris}. The former describes the number of satellites for which frequency and phase are known and the latter the number of satellites for which ephemeris data are available. The number of tracked satellites (both for frequency and phase and for the ephemeris data) is set equal to the number of visible satellites respectively when the transitions \emph{fetch frequency and phase (quick)} and \emph{get ephemeris data} are executed.
 
-Due to the fact that we dont distinguis betwen the different satellites the numbers of tracked satellites visible satellites must be bounded by the number of visible sateliltes. This can be expressed with the equations:
+Both those numbers must be bounded by the number of visible sateliltes. While this is apparently always true for the state variable \texttt{sv\_tracked\_freq\_phase}, it is not for \texttt{sv\_tracked\_ephemeris}. A satellite might in fact not be visible for some minutes and the ephemeris data are still valid after the connection interruption. This limit cannot be overcome without distinguishing the different satellites, which, as stated previously, would increase the complexity of the model with marginal improvement in the descriptive power. Those bounds are expressed with the equations:
 
 \begin{equation}
 \begin{array}{l}
@@ -101,17 +102,17 @@ Due to the fact that we dont distinguis betwen the different satellites the numb
 \end{array}
 \end{equation}
 
-Along with the ephemeris data comes the necessity of representing the expiration time of those: we introduce therefore a real variable called \texttt{expiration\_time}. Since the acquisition is performed in parallel for all the satellites the expiration time will be the same for all the satellites and it is updated when the transition \emph{get ephemeris} is executed. The non-availability of the ephemeris data (expressed by the transition \emph{ephemeris data expired}) can happen in two ways: either the data are not available for enough of the visible satellites, either the expiration time has passed. This can be expressed with the followiong formula (where time represents the actual time):
+Along with the ephemeris data comes the necessity of representing the expiration time of those: we introduce therefore another state variable called \texttt{expiration\_time}. Since the acquisition is performed in parallel for all the satellites the expiration time will be the same for all the satellites currently tracked and it is updated (i.e. increased by 30 minutes) when the transition \emph{get ephemeris} is executed. 
 
-\begin{equation}
-\begin{array}{c}
-	(sv\_tracked\_ephemeris < required\_satellites)  \\
-	\lor \\
-	(expiration\_time < time) .
-\end{array}
-\end{equation}
+%\begin{equation}
+%\begin{array}{c}
+%	(sv\_tracked\_ephemeris < required\_satellites)  \\
+%	\lor \\
+%	(expiration\_time < time) .
+%\end{array}
+%\end{equation}
 
-We now need to define how the states and the transitions are connected, a possible representation of this is given in figure~\ref{fig:cyberDynamics}.
+A possible representation of the states and the transitions are connected is given in figure~\ref{fig:cyberDynamics}.
 %\footnote{In this representation it is assumed that after a \texttt{turn\_ON} signal no \texttt{turn\_OFF} signal will be received before the system is able to provide the position. This looks like a non desirable situation. The model could still easily be extended to include this case defining the following transitions (all triggered by the event \texttt{turn\_OFF}):
 
 %\begin{itemize}
@@ -143,10 +144,13 @@ font=\footnotesize]
 
 \draw [arr, bend right] (zero) to (ni); % arrows from beginning node
 \draw [arr] (ni) to node [above] {turn ON} (cs); % arrows from 1
-\draw [arr] (cs) to node [above] {fetch freq and phase} (re); % arrows from 2
+\draw [arr] (cs) to node [above] {fetch freq and phase} (re);
 \draw [arr, in=60, out=120] (cs) to node [above] {turn OFF} (ni);
-\draw [arr] (re) to node [above] {get ephemeris} (pa); % arrows from 3
+
+% arrows from 3
+\draw [arr] (re) to node [above] {get ephemeris} (pa); 
 \draw [arr, in=60, out=120] (re) to node [above] {turn OFF} (ni);
+\draw [arr, in=60, out=120] (re) to node [above] {lose visibility} (cs);
 
 % arrows from 4 - position available
 \draw [arr, in=60, out=120] (pa) to node [above]
diff --git a/report/sections/04-Examples.tex b/report/sections/04-Examples.tex
index 99518a53ec260ae560dc9b38a4dfdeb7bdc8a6b3..00ca14e685c604c9cb4be7c52541d55caaf1ba03 100644
--- a/report/sections/04-Examples.tex
+++ b/report/sections/04-Examples.tex
@@ -78,7 +78,7 @@ In this third scenario it is shown a possible way the number of visible satellit
  \begin{center}
   \includegraphics[width=0.70\columnwidth]{./img/control3.png}
   \caption{Turn\_ON signal and visible satellites for the antenna in simulation 3.
-           \label{fig:control2}
+           \label{fig:control3}
           }
  \end{center}
 \end{figure}
@@ -87,7 +87,7 @@ In this third scenario it is shown a possible way the number of visible satellit
  \begin{center}
   \includegraphics[width=0.70\columnwidth]{./img/position3.png}
   \caption{Availability of the position measure in simulation 3.
-           \label{fig:position2}
+           \label{fig:position3}
           }
  \end{center}
 \end{figure}