SPECIFICATION ASpec
INVARIANT ASourceSafety
INVARIANT AActionPaymentSafety
INVARIANT ACheckpointSafety
INVARIANT AStepSafety
INVARIANT ACompletionSafety
INVARIANT AHistorySafety
INVARIANT AOuterSafety
PROPERTY AEventuallyReturns
CONSTANT AScenario = "empty"
CONSTANT AMutation = "none"
CONSTANT PaidAmounts = {0}
CONSTANT PaidMoves = {FALSE}