module TYPES (BIT) is  -- the BIT type is imported from a predefined library

type PID is  -- node identifiers
   range 1...4 of NAT
   with <>, last
end type

type STEP is  -- steps of BBA* consensus protocol in [Chen-Micali-19]
   0,  -- congruent-to-0-modulo-3 step
   1,  -- congruent-to-1-modulo-3 step
   2   -- congruent-to-2-modulo-3 step
end type

type TAG is  -- synchronization tags
   BEGIN,
   END
end type

type MORALITY is  -- honesty values of nodes
   HONEST,
   MALICIOUS,
   DISGUISED  -- honest behavior of a malicious node
   with =
end type

type PROB is  -- probability
   P: REAL where 0.0 <= P and P <= 1.0
end type

function 1_MINUS (P: PROB): PROB is  -- complement of a probability
   return PROB (1.0 - REAL (P))
end function

end module