CONSTANTS LeaseSpan = 40 ReplyMax = 20
SPECIFICATION Spec
INVARIANTS TypeOK ProcessExclusion
PROPERTY Handoff