Small changes in client reading slots part - to be verified by Thomas

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 450d91372294752d9a4a83a1d42d9e8765d737a7..99840ea6a23bdb5305c19e81cbeef878b7804878 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -259,8 +259,6 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \EndProcedure\r
 \end{algorithmic}\r
 \r
-\note{Don't include ``such that'' in the argument of a function...}\r
-\r
 \begin{algorithmic}[1]\r
 \Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
 \State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
@@ -269,8 +267,8 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
-\If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
+\Function{ValidPrevHmac}{$s_s,DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
+\If{$s_s = 0 \land hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
        \State \Return $true$\r
 \Else\r
        \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
@@ -278,8 +276,6 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \EndFunction\r
 \end{algorithmic}\r
 \r
-\note{So if a slot has a null previous hmac, everything is fine?  What if it isn't the first slot?}\r
-\r
 \begin{algorithmic}[1]\r
 \Function{GetQueSta}{$Dat_s$}\r
 \State $DE_s \gets GetDatEnt(DE_s)$\r
@@ -309,7 +305,7 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{GetColRes}{$Dat_s$}\Comment{At most 2 $cr$ entries in a slot}\r
+\Function{GetColRes}{$Dat_s$} %\Comment{At most 2 $cr$ entries in a slot}\r
 \State $DE_s \gets GetDatEnt(Dat_s)$\r
 \State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
        de_s \in D \land de_s = cr$\r
@@ -319,15 +315,16 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
        \State $\tuple{s_{ret},id_{ret}} \r
        \gets \emptyset$\r
 \EndIf\r
-\State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
-       de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
-\If{$de_{r_{cr}} \neq \emptyset$}\r
-       \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
-\Else\r
-       \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r
-       \gets \emptyset$\r
-\EndIf\r
-\State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
+%\State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+%      de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
+%\If{$de_{r_{cr}} \neq \emptyset$}\r
+%      \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
+%\Else\r
+%      \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r
+%      \gets \emptyset$\r
+%\EndIf\r
+%\State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
+\State \Return{$\{\tuple{s_{ret},id_{ret}}\}$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
@@ -442,7 +439,7 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
        \EndIf\r
        \State $DE_g \gets GetDatEnt(Dat_g)$\r
        \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$\r
-       \If{$\neg \Call{ValidPrevHmac}{DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
+       \If{$\neg \Call{ValidPrevHmac}{s_g,DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
                \State \Call{ReportError}{'Invalid previous HMAC value'}\r
        \EndIf\r
        \State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$\r
@@ -462,10 +459,11 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
        \If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
        \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
        \EndIf\r
-       \State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r
-       \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
+       %\State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r
+    %  \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
+       \State $\{\tuple{s_e,id_e}\} \gets \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
        \State $\Call{CheckCollision}{MS,SM,\tuple{s_e,id_e}}$\Comment{From normal slot}\r
-       \State $\Call{CheckCollision}{MS,SM,\tuple{s_f,id_f}}$\Comment{From reinsertion}\r
+       %\State $\Call{CheckCollision}{MS,SM,\tuple{s_f,id_f}}$\Comment{From reinsertion}\r
        \State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
        \State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
 \EndFor\r