Adding rollback/mismatch detection when updating last sequence number

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 1016f55929b995f84d5fd8ea9c1021c76fa68499..9d10557f1d3fea49b852f7552ba7405b2405e346 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -310,6 +310,15 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
 \If{$s_t = \emptyset$}\r
        \State $MS_s[id_s] = s_s$  \Comment{First occurrence}\r
 \Else\r
+       \If{$id_s = id_{self}$}\r
+               \If{$s_t \neq s_s$}\Comment{Check for mismatch on $s$}\r
+                       \State \Call{Error}{'Mismatch on $s$ for $id_{self}$'}\r
+               \EndIf\r
+       \Else\r
+               \If{$s_t > s_s$}\Comment{Check for rollback on $s$}\r
+                       \State \Call{Error}{'Rollback on $s$ for $id_s$'}\r
+               \EndIf\r
+       \EndIf\r
        \State $MS_S[id_s] \gets max(s_t, s_s)$\r
 \EndIf\r
 \State \Return{$MS_s$}\r