init do
    `insert into users (id, age) values (1, 10), (2, 20)`
end

process do
    transaction tx1 read_committed do
        `update users set age := 11 where id = 1`
        `update users set age := 21 where id = 2`
    end
end

process do
    transaction tx2 read_committed do
        `update users set age := 12 where id = 1`
        `update users set age := 22 where id = 2`
    end
end

property eventually(`select id, age from users` in {
    {(1, 12), (2, 22)},
    {(1, 11), (2, 21)}
})

property never(`select id, age from users` in {
    {(1, 12), (2, 21)},
    {(1, 11), (2, 22)}
})