SPECIFICATION DSpec
INVARIANT DSafety
PROPERTY DEventuallyDone
CHECK_DEADLOCK FALSE
CONSTANT DetachedProfiles = {"none","imminent-permission","imminent-entry","resolving-permission","resolving-entry"}
CONSTANT PendingProfiles = {"no-loss"}
CONSTANT PaidAmounts = {0,1}
CONSTANT PaidMoves = {TRUE,FALSE}