# Transaction rollback vs competing acquire (S8, I6).
# Bob's acquire must block on alice's uncommitted insert until her
# transaction resolves: after ROLLBACK the lease never existed; after
# COMMIT bob is denied. This demonstrates required ordering, not timing.
setup
{
  CREATE EXTENSION IF NOT EXISTS pg_lease;
}

teardown
{
  DROP EXTENSION pg_lease CASCADE;
}

session "s1"
step "begin_a"    { BEGIN; }
step "a_acq_txn"  { SELECT acquired, epoch FROM lease.acquire('k', 'alice', interval '1h'); }
step "commit_a"   { COMMIT; }
step "abort_a"    { ROLLBACK; }
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'); }

# Alice's rolled-back acquire leaves nothing: bob proceeds and wins.
permutation "begin_a" "a_acq_txn" "b_acq" "abort_a" "ins"
# Alice's committed acquire is visible: bob is denied after the wait.
permutation "begin_a" "a_acq_txn" "b_acq" "commit_a" "ins"