This PR adds a tla+ spec for the transaction lifecycle logic.
Background: I am involved in the efforts at Servo to implement the 3.0 spec, and I found myself struggling with how the concurrency around transaction lifecycle is specified. In particular, I found it hard to reason about how upgrade transactions interact with each other and with other types of transactions.
For example, to figure out upgrade transactions exclude any other transaction, you have to look around the spec at things like step 1 of https://w3c.github.io/IndexedDB/#dom-idbdatabase-transaction, and the fact that https://w3c.github.io/IndexedDB/#opening waits for all other connections to close before proceeding with https://w3c.github.io/IndexedDB/#upgrade-a-database.
There is also some subtlety on how the connection queue and the various "wait" interact: the "Wait until all connections in openConnections are closed" at https://w3c.github.io/IndexedDB/#opening, and the "Wait for transaction to finish" at https://w3c.github.io/IndexedDB/#upgrade-a-database.
In other words, you have to make quite an effort to understand what the spec means, which, a bit like with code, requires reading the whole things and mentally connection various parts. With TLA+ you can operate on global variables directly so the invariants pre- and post-conditions on actions are much clearer(it's all there), and off-course you can check their validity with a machine.
So this one if for your consideration. I'm not sure how you could incorporate it into the actual spec; perhaps just as a link in a note?