# Renewal/release races against acquisition and takeover.
# Every permutation must leave at most one holder (I1) and reject stale
# holders with not_owner / epoch_mismatch (I3, S7).
setup
{
  CREATE EXTENSION IF NOT EXISTS pg_lease;
}

teardown
{
  DROP EXTENSION pg_lease CASCADE;
}

session "s1"
step "a_acq"     { SELECT acquired, epoch FROM lease.acquire('k', 'alice', interval '1h'); }
step "a_renew1"  { SELECT status FROM lease.renew('k', 'alice', 1, interval '1h'); }
step "a_release" { SELECT status FROM lease.release('k', 'alice', 1); }
step "ins"       { SELECT held, owner, epoch FROM lease.inspect('k'); }

session "s2"
step "b_acq"     { SELECT acquired, epoch FROM lease.acquire('k', 'bob', interval '1h'); }
step "b_renew1"  { SELECT status FROM lease.renew('k', 'bob', 1, interval '1h'); }

# Alice holds; bob denied; alice renews fine.
permutation "a_acq" "b_acq" "a_renew1" "ins"
# Bob never held: renew is not_owner; release then works.
permutation "a_acq" "b_renew1" "a_release" "ins"
# Alice releases; bob takes over (epoch 2); alice's stale renew fails.
permutation "a_acq" "a_release" "b_acq" "a_renew1" "ins"
# Renew after release (no successor) fails: not_owner.
permutation "a_acq" "a_release" "b_renew1" "ins"
# Bob denied while held; after release his stale renew still fails.
permutation "a_acq" "b_acq" "a_release" "b_renew1" "ins"