SPECIFICATION Spec
INVARIANT Safety
CHECK_DEADLOCK FALSE
CONSTANTS
    MaxTriggers = 2