tla-plus/DistributedTransaction/Test2.tla

--------------------------------- MODULE Test2 ---------------------------------
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 :> {k1, k3}
ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3
================================================================================
refine distributed transaction Signed-off-by: andylokandy <andylokandy@hotmail.com> 2020-04-08 02:36:57 +08:00			`--------------------------------- MODULE Test2 ---------------------------------`
			`EXTENDS DistributedTransaction, TLC`

			`CONSTANT k1, k2, k3`
			`CONSTANT c1, c2, c3`

add check txn status, read key, read SI check (#37) * 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> 2021-08-22 22:06:49 +08:00			`Keys == {k1, k2, k3}`
refine distributed transaction Signed-off-by: andylokandy <andylokandy@hotmail.com> 2020-04-08 02:36:57 +08:00			`OptimistiicClient == {c3}`
			`PessimisticClient == {c1, c2}`
add check txn status, read key, read SI check (#37) * 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> 2021-08-22 22:06:49 +08:00			`ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k3}`
			`ClientWriteKeys == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k1, k3}`
refine distributed transaction Signed-off-by: andylokandy <andylokandy@hotmail.com> 2020-04-08 02:36:57 +08:00			`ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3`
			`================================================================================`