Add TLA+ spec for core concurrency of spec

.gitignore

@@ -1 +1,5 @@
 deploy_key
+transaction_lifecycle.out
+.vscode/
+states/
+.tlacache/

transaction_lifecycle.cfg

@@ -0,0 +1,16 @@
+SPECIFICATION Spec
+
+CONSTANT Stores = {s1, s2}
+CONSTANT Connections = {c1, c2}
+CONSTANT Transactions = {t1, t2, t3}
+CONSTANT Versions = {0, 1, 2}
+CONSTANT MaxRequests = 3
+
+INVARIANT TypeOK
+INVARIANT UpgradeTxExcludesOtherLiveTxs
+INVARIANT ActiveUpgradeTxImpliesExclusiveConn
+INVARIANT ProcessedRequestsImpliesStarted
+INVARIANT ActiveTransactionImpliesCorrectVersion
+INVARIANT OverlappingStartedTxsAreReadOnly
+
+SYMMETRY Symmetry