module NODE (TYPES, CONSTANTS, CHANNELS, COUNTER) is

process NODE [RECEIVE_BLOCK_PROPOSAL: BLOCK, COMMIT_PROPOSED_BLOCK: COMMIT,
              COMMIT_EMPTY_BLOCK: COMMIT, SYNC: SYNCHRONIZE, SET_BIT: SET_BIT,
              PROPAGATE: PROPAGATE, SELF_PROPAGATE: SELF_PROPAGATE,
              TALLY: TALLY, P_IN, P_OUT, P_ZERO, P_ONE: PROBABILISTIC]
             (ID: PID) is
   par SELF_PROPAGATE, TALLY in
      N [...] (ID)
   ||
      COUNTER [...] (ID)
   end par
end process

process N [RECEIVE_BLOCK_PROPOSAL: BLOCK, COMMIT_PROPOSED_BLOCK: COMMIT,
           COMMIT_EMPTY_BLOCK: COMMIT, SYNC: SYNCHRONIZE, SET_BIT: SET_BIT,
           PROPAGATE: PROPAGATE, SELF_PROPAGATE: SELF_PROPAGATE,
           TALLY: TALLY, P_IN, P_OUT, P_ZERO, P_ONE: PROBABILISTIC]
          (ID: PID) is
   var B, V: BIT, K0, K1: NAT, M: MORALITY in
      loop
         RECEIVE_BLOCK_PROPOSAL (?V);
         if NAT (ID) <= H then
            M := HONEST
         elsif V = 1 then
            M := MALICIOUS
         else
            M := DISGUISED
         end if;
         FLIP_COIN [...] (ID, 0, ?B, P_H);  -- result of graded consensus phase
         loop L in
            -- Coin-Fixed-To-0 step
            BROADCAST [...] (ID, B, M, ?K0, ?K1);
            if K0 >= T then
               COMMIT_PROPOSED_BLOCK;
               break L
            end if;
            FIX_COIN [...] (ID, 1, ?B, BIT (K1 >= T));
            -- Coin-Fixed-To-1 step
            BROADCAST [...] (ID, B, M, ?K0, ?K1);
            if K1 >= T then
               COMMIT_EMPTY_BLOCK;
               break L
            end if;
            FIX_COIN [...] (ID, 2, ?B, not (BIT (K0 >= T)));
            -- Coin-Genuinely-Flipped step
            BROADCAST [...] (ID, B, M, ?K0, ?K1);
            if K0 >= T then
               FIX_COIN [...] (ID, 0, ?B, 0)
            elsif K1 >= T then
               FIX_COIN [...] (ID, 0, ?B, 1)
            else
               FLIP_COIN [...] (ID, 0, ?B, 0.5 of PROB)  -- fair coin tossing
            end if
         end loop
      end loop
   end var
end process

process FIX_COIN [SET_BIT: SET_BIT]
                 (ID: PID, S: STEP, out var B: BIT, NEW_B: BIT) is
   B := NEW_B;
   SET_BIT (ID, S, B)
end process

process FLIP_COIN [SET_BIT: SET_BIT, P_ZERO, P_ONE: PROBABILISTIC]
                  (ID: PID, S: STEP, out var B: BIT, P: PROB) is
   alt
      P_ZERO (ID, P);
      B := 0
   []
      P_ONE (ID, 1_MINUS (P));
      B := 1
   end alt;
   SET_BIT (ID, S, B)
end process

process BROADCAST [SYNC: SYNCHRONIZE, PROPAGATE: PROPAGATE,
                   SELF_PROPAGATE: SELF_PROPAGATE, TALLY: TALLY,
                   P_IN, P_OUT: PROBABILISTIC]
                  (ID: PID, in var B: BIT, M: MORALITY, out K0, K1: NAT) is
   B := B or BIT (M = MALICIOUS);
   SYNC (BEGIN);
   alt
      P_IN (ID, P_V);
      PROPAGATE (ID, B);
      SELF_PROPAGATE (ID, B)
   []
      P_OUT (ID, 1_MINUS (P_V))
   end alt;
   SYNC (END);
   TALLY (ID, ?K0 where K0 <= N, ?K1 where K1 <= N)
end process

end module