Transform an UpdateRequest into the corresponding state transformer.

Fold a sequence of requests to transform a waiting strucutre onto the empty waiting. As we consider all exported transformations, any waiting structure can be obtained this way.

Verify that an owner with a pending request cannot make any changes to the lock structure.

Quantifier for blocked requests. Quantifies over the generic situation that there is a state, an owner, and a request that is blocked for that owner. To obtain such a situation, we use the fact that there must be a different owner having at least one lock.

Verify that an owner has a pending request after a waiting request not fullfilled immediately.

Verify that pending requests get fullfilled once all blockers release their resources.

Verify that the owner of a pending request gets notified once all blockers release their resources.

Verify that some progress is made after the direct blockers give up their locks. Note that we cannot guarantee that the original requester gets its request granted, as someone else might have a more important priority.

Verify that the notifications send out are sound, i.e., upon notification the requests actually are fulfilled. To be sure to have at least one notification we, again, use the scenario that a request is blocked and then all the blockers release their resources.

Verify that all pending requests are valid and cannot be fulfilled in the underlying lock allocation.

Verify that updateLocks is idempotent, except that in the repetition, no waiters are notified.

Verify that extRepr . fromExtRepr = id for all valid extensional representations.

Verify that any state is indistinguishable from its canonical version (i.e., the one obtained from the extensional representation) with respect to updateLocks.

Verify that any state is indistinguishable from its canonical version (i.e., the one obtained from the extensional representation) with respect to updateLocksWaiting.

Verify that if a requestor has no pending requests, safeUpdateWaiting conincides with updateLocksWaiting.

Verify that safeUpdateLocksWaiting is idempotent, that in the repetition no notifications are done.

Verify that for LockWaiting we have readJSON . showJSON is extensionally equivalent to Ok.

Verify that opportunistic union only increases the locks held.

Verify the result list of the opportunistic union: if a lock is not in the result that, than its state has not changed, and if it is, it is as requested. The latter property is tested in that liberal way, so that we really can take arbitrary requests, including those that require both, shared and exlusive state for the same lock.