mirror of
https://github.com/pingcap/tla-plus.git
synced 2024-12-26 12:30:10 +08:00
b80ac83420
* Add CheckTxnStatus Msgs * Add CheckTxnStatus, haven't checked by the TLC revert a change DistributedTransaction: fix checkTxnStatus bugs DistributedTransaction: CheckTxnStatus: refactor change a var name Co-authored-by: Andy Lok <andylokandy@hotmail.com> DistributedTransaction: CheckTxnStatus: format spec update CheckTxnStatus comment Co-authored-by: Andy Lok <andylokandy@hotmail.com> DistributedTransaction: CheckTxnStatus: update comments * Add SI check DistributedTransactions: upd min_commit_ts DistributedTransactions: fix tla parse err DistributedTransactions: upd tests upd lock failed DistributedTransactions: upd read write keys DistributedTransactions: upd Test2 DistributedTransactions: fix many bugs * DistributedTransactions: extract unlock_key function DistributedTransactions: avoid client check txn rollback itself DistributedTransactions: add ClientCheckTxnStatus to `Next` DistributedTransactions: amend pessimistic lock DistributedTransactions: add read SI check DistributedTransactions: upd pdf version DistributedTransactions: remove ServerCleanupLock DistributedTransactions: refactor ClientReadFailed CheckTxnStatus DistributedTransactions: upd server lock key DistributedTransactions: fix ClientRetryLockKey bug DistributedTransactions: fix ReadSI def * DistributedTransactions: upd max read times DistributedTransactions: upd max read times DistributedTransactions: fix bug DistributedTransactions: upd DistributedTransactions: refactor, upd some comments DistributedTransactions: refactor, upd * DistributedTransaction: Add max client check txn times DistributedTransaction: upd lock min_commit_ts check DistributedTransaction: rename wrong name to current_ts DistributedTransaction: reformat some code * fix wrong pessimistic lock amend DistributedTransactions: fix pessimistic lock amend bug upd upd upd upd upd upd upd upd * upd read SI check upd refactor ClientRetryLockKey upd ClientRetryCommit upd max_lock_key_time upd fix bugs upd pessimistic ReadSI check, same as optimistic one * upd remove some resp msgs upd possible msg lost * apply code review suggestion upd * restucture distributed transaction spec Signed-off-by: Andy Lok <andylokandy@hotmail.com> * fix comment Signed-off-by: Andy Lok <andylokandy@hotmail.com> * update comment Signed-off-by: Andy Lok <andylokandy@hotmail.com> * update assume Signed-off-by: Andy Lok <andylokandy@hotmail.com> * update comment Signed-off-by: Andy Lok <andylokandy@hotmail.com> * enable snapshot checks Signed-off-by: Andy Lok <andylokandy@hotmail.com> * fix pessimistic si check Signed-off-by: Andy Lok <andylokandy@hotmail.com> * add comment Signed-off-by: Andy Lok <andylokandy@hotmail.com> * add comment Signed-off-by: Andy Lok <andylokandy@hotmail.com> * add comment Signed-off-by: Andy Lok <andylokandy@hotmail.com> * fix typo Signed-off-by: Andy Lok <andylokandy@hotmail.com> * fix dead end in optimistic prewrite Signed-off-by: Andy Lok <andylokandy@hotmail.com> * add test5 Signed-off-by: Andy Lok <andylokandy@hotmail.com> Co-authored-by: Andy Lok <andylokandy@hotmail.com>
14 lines
498 B
Plaintext
14 lines
498 B
Plaintext
--------------------------------- MODULE Test5 ---------------------------------
|
|
EXTENDS DistributedTransaction, TLC
|
|
|
|
CONSTANT k1, k2, k3
|
|
CONSTANT c1, c2, c3
|
|
|
|
Keys == {k1, k2, k3}
|
|
OptimistiicClient == {c3}
|
|
PessimisticClient == {c1, c2}
|
|
ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k3}
|
|
ClientWriteKeys == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k2, k3}
|
|
ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3
|
|
================================================================================
|