# I1: simultaneous acquirers on one key — exactly one winner, in any order.
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_ins" { SELECT held, owner, epoch FROM lease.inspect('k'); }

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

session "s3"
step "c_acq" { SELECT acquired, epoch FROM lease.acquire('k', 'carol', interval '1h'); }

# Fresh-key race: first inserter wins, others denied, epoch stays 1.
permutation "a_acq" "b_acq" "c_acq" "a_ins"
permutation "b_acq" "c_acq" "a_acq" "a_ins"
permutation "c_acq" "a_acq" "b_acq" "a_ins"