- relational specifications for weak increment - logically atomic specification for `ticket_lock.acquire`