bad message

recherches/ALDLoverAB/algo/index.tex

@@ -2,100 +2,72 @@ We define $k$ as the id of the round \\
 the $getMax(proves)$ return $MAX({(\_, r) : \exists (\_, PROVE(r)) \in proves})$ \\
 $buffer$ a FIFO list with $buffer[front]$ returning the first element
 
-% \begin{algorithm}[H]
-% \DontPrintSemicolon
-% \SetAlgoLined
-% \KwIn{le message $m$}
-% \BlankLine
-% \While{true}{
-%   proves = READ() \\
-%   k = getMax(dump) + 1 \\
-%   APPEND(k || m) \\
-%   \If{PROVE(k)}{
-%     APPEND(k) \\
-%     return
-%   }
-% }
-% \caption{AB\_Broadcast}
-% \end{algorithm}
+
+\begin{algorithm}[H]
+  \DontPrintSemicolon
+  \SetAlgoLined
+  
+  $rcved = rcved \bigcup \{m\}$ \;
+  \textbf{upon} RB\_deliver(PROP, r, S) \textbf{from} j \;
+  prop[r][j] = S
+
+  \caption{\textbf{Upon} RB\_deliver(m)}
+\end{algorithm}
 
 \begin{algorithm}[H]
 \DontPrintSemicolon
 \SetAlgoLined
 \KwIn{le message $m$}
+
+\KwData{rcved = $\emptyset$ \;
+delivered = $\emptyset$ \;
+r = 0 \;}
+
 \BlankLine
-k\_max = getMax(READ()) \\
-\While{buffer $\neq [\emptyset] $}{
-  (i, m) = buffer[front] \\
-  \textbf{wait} PROVE(k\_max || m) = false \\
-  proves = READ() \\
-  \If{$((i, PROVE(k\_max || m)) \in proves) \wedge ((i, PROVE(k\_max)) \in proves)$}{
-    $buffer = buffer - \{(i, m)\}$
-  }
-}
-\BlankLine
+
+RB\_cast(m) \;
+$rcved = rcvd \bigcup \{m\}$ \;
+
 \While{true}{
-  proves = READ() \\
-  k = getMax(proves) + 1 \\
-  PROVE(k || m) \\
-  APPEND(k || m) \\
-  \If{PROVE(k)}{
-    APPEND(k) \\
-    return
+  $r = r+1$ \;
+  $RB\_cast(PROP, r, S)$ \;
+  PROVE(r) \;
+  APPEND(r) \;
+  proves = READ() \;
+  $winner^r = \{j : (j, PROVE(r)) \in proves\}$ \;
+  \textbf{wait until} $(\forall j \in winner^k: prop[r][j])$ \;
+  \If{$\exists j \in winner^k : m \in prop[r][j]$}{
+    break \;
   }
 }
+
 \caption{AB\_Broadcast}
 \end{algorithm}
 
-$proves_r = {(i, r) : \forall i, \exists (i, PROVE(r)) \in proves}$ \\
-$proves_r^i = ((i, r) : \exists (i, PROVE(r)) \in proves)$ ?? NULL \\
-
-% $proves_r \subseteq proves$ s.a. $\forall PROVE(x) \in proves_r$, x is in the form $r || m$ with $m$ who cannot be empty \\
-% $proves_r^i$ is the $PROVE(r || m )$ operation submited by the process i if exist \\
-
 \begin{algorithm}[H]
   \DontPrintSemicolon
   \SetAlgoLined
-  buffer = $[\emptyset]$ \\
-  k = 0 \\
-  \BlankLine
+
+  r\_prev = 0 \;
   \While{true}{
-    proves = READ() \\
-    k\_max = getMax(proves) \\
-    \For{r=k+1 \emph{\KwTo} k\_max}{
-      APPEND(r)\\
-      \For{i = 1 \emph{\KwTo} $|P|$}{
-        \If{$(\exists m : \exists(i, PROVE(r || m)) \in proves)$}{
-          \uIf{$(\exists(i, PROVE(r)) \in proves)$} {
-            AB\_Recv(m)
-          }
-          \Else{
-            $buffer = buffer \cup \{(i, m)\}$
-          }
-        }
-      }
+    proves = READ() \;
+    $r\_max = MAX(\{r : \exists i, (i, PROVE(r)) \in proves\})$ \; 
+    \For{$r = r\_prev + 1 \textbf{to} r\_max$}{
+      APPEND(r) \;
+      proves = READ() \;
+      $winner^k = \{j : (j, PROVE(r)) \in proves \}$ \;
+      $\textbf{wait until} (\forall j \in winner^k : prop[r][j] \neq \emptyset)$ \;
+      $M^r = (\bigcup_{j \in winner^k} prop[r][j]) \setminus delivered$ \;
+      
+      \tcc*{we assume $M^r$ as an ordered list s.a. $\forall m_1, m_2, if m_1 < m_2$, $m_1$ appears before $m_2$ in $M^r$}
+
+      \BlankLine
+      
+      \ForEach{$m \in M^r$}{
+        $delivered = delivered \bigcup \{m\}$ \;
+        AB\_deliver(m) \;
+      } 
     }
   }
 \caption{AB\_Listen}
-\end{algorithm}
-  
-% \begin{algorithm}[H]
-%   \DontPrintSemicolon
-%   \SetAlgoLined
-%   \BlankLine
-%   \While{true}{
-%     proves = READ() \\
-%     k\_max = getMax(proves) \\
-%     \For{r=k+1 \emph{\KwTo} k\_max}{
-%       APPEND(r)\\
-%       $proves_r$ = \{$\forall i, PROVE(r)_i \in READ()$\} \\
-%       \For{i = 1 \emph{\KwTo} $|P|$}{
-%         \If{$\exists PROVE(r)_i \in proves_r$}{
-%           AB\_Recv($m$ s.t. $PROVE(r || m) \in proves$)
-%         }
-%       }
-%     }
-%   }
-  
-%   \caption{AB\_Listen}
-% \end{algorithm}
+\end{algorithm}