github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2026-08-22 11:33:29 +08:00
Code Issues Packages Projects Releases Wiki Activity

fix typo

Browse Source 
Signed-off-by: andylokandy <andylokandy@hotmail.com>
This commit is contained in:
andylokandy
2020-07-10 18:53:20 +08:00
parent 92ff853acf
commit 8128e56c84
2 changed files with 598 additions and 597 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@@ -1,5 +1,6 @@
states/ states/
*.out *.out
*.tlaps
**/*.toolbox/*/ **/*.toolbox/*/
**/*.toolbox/*___*_SnapShot_*.launch **/*.toolbox/*___*_SnapShot_*.launch
**/*.toolbox/.project **/*.toolbox/.project

6
DistributedTransaction/DistributedTransaction.tla
View File

@@ -36,7 +36,7 @@ VARIABLES req_msgs
VARIABLES resp_msgs VARIABLES resp_msgs
\* key_data[k] is the set of multi-version data of the key. Since we \* key_data[k] is the set of multi-version data of the key. Since we
\* don't care about the concrete value of data, a strat_ts is sufficient \* don't care about the concrete value of data, a start_ts is sufficient
\* to represent one data version. \* to represent one data version.
VARIABLES key_data VARIABLES key_data
\* key_lock[k] is the set of lock (zero or one element). A lock is of a \* key_lock[k] is the set of lock (zero or one element). A lock is of a
@@ -570,7 +570,7 @@ MsgTsConsistency ==
\* nessesary), because SnapshotIsolation means that: \* nessesary), because SnapshotIsolation means that:
\* (1) Once a transcation is committed, all keys of the transaction should \* (1) Once a transcation is committed, all keys of the transaction should
\* be always readable or have lock on secondary keys(eventually readable). \* be always readable or have lock on secondary keys(eventually readable).
\* PROOF BY CommitConsistency, MsgConsistency \* PROOF BY CommitConsistency, MsgMonotonicity
\* (2) For a given transaction, all transaction that commits after that \* (2) For a given transaction, all transaction that commits after that
\* transaction should have greater commit_ts than the next_ts at the \* transaction should have greater commit_ts than the next_ts at the
\* time that the given transaction commits, so as to be able to \* time that the given transaction commits, so as to be able to
@@ -578,7 +578,7 @@ MsgTsConsistency ==
\* from all transactions that preserved by (1). \* from all transactions that preserved by (1).
\* PROOF BY NextTsConsistency, MsgTsConsistency \* PROOF BY NextTsConsistency, MsgTsConsistency
\* (3) All aborted transactions would be always not readable. \* (3) All aborted transactions would be always not readable.
\* PROOF BY AbortConsistency, MsgConsistency \* PROOF BY AbortConsistency, MsgMonotonicity
SnapshotIsolation == /\ CommitConsistency SnapshotIsolation == /\ CommitConsistency
/\ AbortConsistency /\ AbortConsistency
/\ NextTsMonotonicity /\ NextTsMonotonicity