setup
{
  DROP TABLE IF EXISTS products;
  CREATE EXTENSION IF NOT EXISTS btree_gist;
  CREATE TABLE products (id int NOT NULL, valid_at daterange NOT NULL, price text,
      PRIMARY KEY (id, valid_at WITHOUT OVERLAPS));
  INSERT INTO products VALUES (1, '[2020-01-01,2030-01-01)', 'orig');
}

session s1
setup           { SET datestyle TO ISO, YMD; }
step s1rc       { BEGIN ISOLATION LEVEL READ COMMITTED; }
step s1c        { COMMIT; }

step s1lock2025 { SELECT * FROM products WHERE id = 1 AND valid_at && '[2025-01-01,2026-01-01)' FOR UPDATE; }
step s1lock     { SELECT * FROM products WHERE id = 1 FOR UPDATE; }

step s1upd2025  { UPDATE products FOR PORTION OF valid_at FROM '2025-01-01' TO '2026-01-01' SET price = price || '-S1' WHERE id = 1 RETURNING *; }
step s1q        { SELECT * FROM products ORDER BY id, valid_at; }

session s2
setup           { SET datestyle TO ISO, YMD; }
step s2rc       { BEGIN ISOLATION LEVEL READ COMMITTED; }
step s2c        { COMMIT; }

step s2lock2027 { SELECT * FROM products WHERE id = 1 AND valid_at && '[2027-01-01,2028-01-01)' FOR UPDATE; }
step s2lock     { SELECT * FROM products WHERE id = 1 FOR UPDATE; }
step s2upd2027  { UPDATE products FOR PORTION OF valid_at FROM '2027-01-01' TO '2028-01-01' SET price =  price || '-S2a' WHERE id = 1 RETURNING *; }

step s2lock2021 { SELECT * FROM products WHERE id = 1 AND valid_at && '[2021-01-01,2022-01-01)' FOR UPDATE; }
step s2upd2021  { UPDATE products FOR PORTION OF valid_at FROM '2021-01-01' TO '2022-01-01' SET price =  price || '-S2b' WHERE id = 1 RETURNING *; }


# Shows the problem of the s1upd2025 being "lost" (i.e. never made). The
# problem is that s1lock2025 will follow the update, but then EPQ will not
# consider the resulting row to match valid_at && '[2025-01-01,2026-01-01)'
permutation s2rc s2lock2027 s2upd2027 s1rc s1lock2025 s2c s2rc s2lock2021 s2upd2021 s1upd2025 s2c s1c s1q

# A slight reordering shows that this is indeed a concurrency
# artifact. s1lock2025 still doesn't do anything, but because s1upd2025 is
# later, it now can see the to-be-updated row.
permutation s2rc s2lock2027 s2upd2027 s1rc s1lock2025 s2c s2rc s2lock2021 s2upd2021 s2c s1upd2025 s1c s1q