There are problems in how atomic actions are defined in spec.
Take for example
LockAcquire(tx, req, tuple) ==
/\ \A tx1 \in tupleOwners[tuple]:
/\ HasConflict(req,txRequest[tx1])
/\ (tx < tx1)
/\ SetAbort(tx1)
/\ UNCHANGED <<txActive, txRequest, tupleOwners, tupleWaiters>>
/\ AddWaiter(tx, tuple)
/\ PromoteWaiter(tuple)
AddWaiter and PromoteWaiter should be different actions. From initial state
it is not possible to get an execution trace which satisfies LockAcquire action.
AddWaiter says that in the next state `tx` will be added in waiters of `tuple` but
PromoteWaiter expects that `tx` is in waiters of `tuple` in current state by usage of
tx = Min(tupleWaiters[tuple]).
Correction : But there is no transaction to promote as tupleWaiters[tuple] is empty. PromoteWaiter
is evaluates to FALSE for any state transition (s, s') where s is initial state. Hence it is deadlock