\* The payments config (check.sh changes some constants for its other cases): gate-2
\* (Mut = {}), from any state the owner's changes can reach, two requests, and one change
\* the owner signs at any moment while they wait. Every property must hold.
CONSTANTS
    Tenants = {t1, t2}
    GoodAccounts = {good}
    BadAccounts = {bad}
    MaxAmount = 2
    ReqIds = {r1, r2}
    MaxTime = 2
    MaxLife = 1
    OpWindow = 1
    MaxOps = 1
    Owners = {o}
    FirstOwner = o
    Approver = ap
    X = x
    K = k
    KX = kx
    None = None
    Start = "any"
    Mut = {}

INIT Init
SYMMETRY Symmetry
NEXT Next
INVARIANTS
    TypeOK
    G1_PaidOnlyAsAPersonApproved
    G1_ApprovedWithAuthorityInForce
    G1_PaidOnlyToListedPayees
    G2_AtMostOnce
    G3_SetupOnce
    G3_AlwaysAnOwner
    G3_AttackerNeverGranted
PROPERTIES
    G3_AuthorityOnlyByOwners
CHECK_DEADLOCK FALSE