# Stale client: actions with a pre-takeover epoch are always rejected
# after any ownership transition (I2, I3).
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_release"   { SELECT status FROM lease.release('k', 'alice', 1); }
step "a_ren_stale" { SELECT status FROM lease.renew('k', 'alice', 1, interval '1h'); }
step "a_rel_stale" { SELECT status FROM lease.release('k', 'alice', 1); }
step "a_reacq"     { SELECT acquired, epoch FROM lease.acquire('k', 'alice', interval '1h'); }
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_renew"     { SELECT status FROM lease.renew('k', 'bob', 3, interval '1h'); }

# alice(1) -> release(2) -> bob(3): all of alice's epoch-1 credentials die.
permutation "a_acq" "a_release" "b_acq" "a_ren_stale" "a_rel_stale" "ins"
# Same, and bob's own epoch-3 renew works.
permutation "a_acq" "a_release" "b_acq" "a_ren_stale" "b_renew" "ins"
# Alice re-acquires after her release: fresh epoch 4, strictly greater.
permutation "a_acq" "a_release" "b_acq" "a_reacq" "ins"