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

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

process do
    transaction tx2 read_committed do
        let first_age := `select age from users where id = 1`
        latch
        let second_age := `select age from users where id = 1`
    end
end

property never(first_age in {101, 11} and second_age in {101, 11})
property eventually(`select age from users where id = 1` = 11)