module CONSENSUS is

------------------------------------------------------------------------------

-- This file describes a consensus algorithm that proceeds in several
-- rounds to decide a boolean value.

-- At each round, each process accepts (on gate INPUT) an estimation
-- EST of type bool and provides either a new estimation (on gate
-- OUTPUT), or a decision value (on gate DEC). The estimation produced
-- at round n is taken as input estimation at round n+1. The initial
-- estimation is provided by the environment.

-- More precisely, each round is divided in two 'broadcast-gathering'
-- phases:

-- In the first phase, each process broadcasts its estimation towards
-- the other processes (via gate SEND), and gathers the estimations
-- sent by the other processes (via gate RECV).

-- In the second phase, broadcast/gathering is repeated with an
-- auxiliary value deduced from estimations gathered in the first
-- phase.

-- At last, from gathered auxiliary values, each process can decide
-- whether providing a new estimation for a new round, or a final
-- decision value.

------------------------------------------------------------------------------

type TRISTATE is
   BOTTOM, TOPTRUE, TOPFALSE
   with ==, <>
end type

------------------------------------------------------------------------------

function BOOL (T: TRISTATE): bool is
   case T in
      TOPTRUE -> return true
    | TOPFALSE -> return false
    | BOTTOM -> raise UNEXPECTED
   end case
end function

------------------------------------------------------------------------------

channel COMMUNICATIONS is
   (ID: nat, TO: nat, ROUND: nat, PHASE: nat, ESTIMATION: bool),
   (ID: nat, TO: nat, ROUND: nat, PHASE: nat, AUX: TRISTATE)
   -- ID is the source process identifier
   -- TO is the target process identifier
   -- PHASE is either 1 or 2
   -- AUX is an auxiliary value computed from the estimations
end channel

------------------------------------------------------------------------------

channel DECISIONS is
   (ID: nat, AUX: bool)
   -- ID is a process identifier
   -- AUX is an auxiliary value computed from the estimations
end channel

------------------------------------------------------------------------------

channel INPUTS is
   (ID: nat, ESTIMATION: bool)
   -- ID is a process identifier
end channel

------------------------------------------------------------------------------

channel OUTPUTS is
   (ROUND: nat, ID: nat, ESTIMATION: bool)
   -- ID is a process identifier
end channel

------------------------------------------------------------------------------

-- Meaning of process parameters hereafter:
--    - NB_PROC is the total number of processes
--    - NB_FAULTS is the number of potentially faulty processes
--    - ID is the identifier of the current process
--    - ROUND is the current round
--    - MAX_ROUND is the maximal number of rounds for simulation

function CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND: nat): bool is
   return (NB_FAULTS < NB_PROC)
          -- the Ben-Or paper even assumes that 5 * NB_FAULTS < NB_PROC
          and
          (1 <= ID) and (ID <= NB_PROC)
          and
          (1 <= ROUND) and (ROUND <= MAX_ROUND)
end function

------------------------------------------------------------------------------

-- INPUT_VALUES starts the protocol for process ID: initial estimation
-- is received on gate INPUT.

process INPUT_VALUES [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                      INPUT: INPUTS, OUTPUT: OUTPUTS]
                     (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND: nat) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   var EST: bool in
      INPUT (ID, ?EST);
      CONSENSUS [SEND, RECV, DEC, INPUT, OUTPUT]
                (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND, EST)
   end var
end process

------------------------------------------------------------------------------

-- CONSENSUS is the main recursive process. Each recursive call to
-- CONSENSUS models one round of the protocol for process ID.

process CONSENSUS [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                   INPUT: INPUTS, OUTPUT: OUTPUTS]
                  (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND: nat, EST: bool) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   BROADCAST_PHASE_1 [SEND, RECV, DEC, INPUT, OUTPUT]
                     (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND, EST)
end process

------------------------------------------------------------------------------

-- BROADCAST_PHASE_1 broadcasts the current process estimation until
-- all processes have been reached.

process BROADCAST_PHASE_1 [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                           INPUT: INPUTS, OUTPUT: OUTPUTS]
                          (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND: nat,
                           EST: bool) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   var TO: nat in
      for TO := 1 while TO <= NB_PROC by TO := TO + 1 loop
         if TO <> ID then
            -- If TO is a different process than ID (don't send a message to
            -- myself), send the estimation and then continue
            SEND (ID, TO, ROUND, 1 of nat, EST)
         end if
      end loop
   end var;
   -- Broadcast is complete: start gathering
   GATHERING_PHASE_1 [SEND, RECV, DEC, INPUT, OUTPUT]
                     (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND, EST)
end process

------------------------------------------------------------------------------

-- GATHERING_PHASE_1 collects estimations broadcast by NB_PROC - NB_FAULTS
-- other processes. This ensures that gathering will not deadlock since at
-- most NB_FAULTS processes might be down.

process GATHERING_PHASE_1 [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                           INPUT: INPUTS, OUTPUT: OUTPUTS]
                          (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND: nat,
                           in var EST: bool) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   var NB_FALSE, NB_TRUE: nat in
      -- NB_FALSE is the number of gathered estimations with value FALSE
      -- NB_TRUE is the number of gathered estimations with value TRUE
      NB_FALSE := 0;
      NB_TRUE := 0;
      loop L in
         if EST then
            NB_TRUE := NB_TRUE + 1
         else
            NB_FALSE := NB_FALSE + 1
         end if;
         if (NB_FALSE + NB_TRUE) == (NB_PROC - NB_FAULTS) then
             break L
         end if;
         assert (NB_FALSE + NB_TRUE) < (NB_PROC - NB_FAULTS);
         var FROM: nat in
            RECV (?FROM, ID, ROUND, 1 of nat, ?EST) where FROM <> ID
         end var
      end loop;
      COMPUTE_AUX_VALUE [SEND, RECV, DEC, INPUT, OUTPUT]
                (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND, NB_FALSE, NB_TRUE)
   end var
end process

------------------------------------------------------------------------------

-- COMPUTE_AUX_VALUE computes an auxiliary value from the proportion
-- of FALSE and TRUE estimations. This value, used in the second phase
-- of the protocol, belongs to the set {TOPTRUE, TOPFALSE, BOTTOM}. It
-- is chosen as follows:
--
--   * TOPFALSE if the number of FALSE estimations gathered constitutes a
--     majority over all processes (including the potentially faulty ones).
--
--   * TOPTRUE if the number of TRUE estimations gathered constitutes a
--     majority over all processes (including the potentially faulty ones).
--
--   * BOTTOM otherwise.

-- Remark that different processes may have collected different sets
-- of estimations since not all estimations are (and can be safely)
-- collected. However, if a process chooses TOPTRUE (respectively
-- TOPFALSE) as auxiliary value, then no other process can choose
-- TOPFALSE (respectively TOPTRUE) at the same time, because there is
-- at most one majority.

process COMPUTE_AUX_VALUE [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                           INPUT: INPUTS, OUTPUT: OUTPUTS]
                          (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND,
                           NB_FALSE, NB_TRUE: nat) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   require (NB_FALSE + NB_TRUE) >= (NB_PROC - NB_FAULTS);
   var AUX: TRISTATE in
      if NB_FALSE >= ((NB_PROC div 2) + 1) then
         AUX := TOPFALSE
      elsif NB_TRUE >= ((NB_PROC div 2) + 1) then
         AUX := TOPTRUE
      else
         AUX := BOTTOM
      end if;
      BROADCAST_PHASE_2 [SEND, RECV, DEC, INPUT, OUTPUT] (NB_PROC, NB_FAULTS,
                                                   ID, ROUND, MAX_ROUND, AUX)
   end var
end process

------------------------------------------------------------------------------

-- BROADCAST_PHASE_2 broadcasts the auxiliary values, similarly to
-- phase 1.

process BROADCAST_PHASE_2 [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                           INPUT: INPUTS, OUTPUT: OUTPUTS]
                          (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND: nat,
                           AUX: TRISTATE) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   var TO: nat in
      for TO := 1 while TO <= NB_PROC by TO := TO + 1 loop
         if TO <> ID then
            -- If TO is a different process than ID (don't send a message to
            -- myself), send the estimation and then continue
            SEND (ID, TO, ROUND, 2 of nat, AUX)
         end if
      end loop
   end var;
   -- Broadcast is complete: start gathering
   GATHERING_PHASE_2 [SEND, RECV, DEC, INPUT, OUTPUT]
                     (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND, AUX)
end process

------------------------------------------------------------------------------

-- GATHERING_PHASE_2 gathers auxiliary values similarly to the first phase.

process GATHERING_PHASE_2 [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                           INPUT: INPUTS, OUTPUT: OUTPUTS]
                          (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND: nat,
                           in var AUX: TRISTATE) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   var NB_RECEIVED, NB_TOP: nat, NEW_AUX: TRISTATE in
      -- NB_RECEIVED: number of received messages
      -- NB_TOP: number of TOPFALSE or TOPTRUE received
      NB_RECEIVED := 1;
      NB_TOP := 0;
      NEW_AUX := AUX;
      loop L in
         if AUX <> BOTTOM then
            NB_TOP := NB_TOP + 1;
            NEW_AUX := AUX
         end if;
         if NB_RECEIVED == (NB_PROC - NB_FAULTS) then
             break L
         end if;
         assert NB_RECEIVED < (NB_PROC - NB_FAULTS);
         var FROM: nat in
            RECV (?FROM, ID, ROUND, 2 of nat, ?AUX) where FROM <> ID
         end var;
         NB_RECEIVED := NB_RECEIVED + 1
      end loop;
      -- NEW_AUX: new auxiliary value deduced from gathered auxiliary values
      NEW_ESTIMATION [SEND, RECV, DEC, INPUT, OUTPUT]
                  (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND, NB_TOP, NEW_AUX)
   end var
end process

------------------------------------------------------------------------------

-- NEW_ESTIMATION either computes a new estimation or decides the final value.

-- We can safely decide when we have collected more than NB_FAULTS
-- top values. The decided value is then the value carried by the TOP value.
-- Else, if we received at least one TOP value, we start next round
-- with the value it carried. Otherwise, we only received BOTTOM values.
-- In that case we randomly choose the new estimation.

process NEW_ESTIMATION [SEND, RECV: COMMUNICATIONS, DEC: DECISIONS,
                        INPUT: INPUTS, OUTPUT: OUTPUTS]
                       (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND, NB_TOP: nat,
                        NEW_AUX: TRISTATE) is
   require CONSTRAINTS (NB_PROC, NB_FAULTS, ID, ROUND, MAX_ROUND);
   if NB_TOP > NB_FAULTS then
      DEC (ID, BOOL (NEW_AUX));
      stop
   else
      var B: bool in
         if NB_TOP > 0 then
            B := BOOL (NEW_AUX);
            OUTPUT (ROUND, ID, B)
         else
            assert NB_TOP == 0;
            OUTPUT (ROUND, ID, ?B)
         end if;
         only if ROUND < MAX_ROUND then
            CONSENSUS [SEND, RECV, DEC, INPUT, OUTPUT] (NB_PROC, NB_FAULTS,
                                                 ID, ROUND + 1, MAX_ROUND, B)
         end if
      end var
   end if
end process

------------------------------------------------------------------------------

process MAIN is
   stop -- the main process will be provided by the SVL script
end process

------------------------------------------------------------------------------

end module