SPECIFICATION Spec
CONSTANTS
  Variant = "gated"
  MaxHuman = 2
INVARIANTS
  TypeOK
  LiveResolver
  ResolverConsistent
  AtMostOnce
  LedgerComplete
CHECK_DEADLOCK FALSE