github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2024-12-26 12:30:10 +08:00
Code Issues Packages Projects Releases Wiki Activity

all writes cannot overlap (#7)

Browse Source
This commit is contained in:
foreverbell 2018-02-01 22:37:45 +08:00 committed by siddontang
parent 393b685359
commit 013fe46836
1 changed files with 4 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Percolator/Percolator.tla
View File

@ -279,16 +279,13 @@ TypeInvariant ==
/\ KeyWriteTypeInv
--------------------------------------------------------------------------------
checkWriteOrder(w1, w2) ==
/\ w1.commit_ts < w2.commit_ts
/\ w1.start_ts < w2.start_ts
\* The committed write timestamp of the key must be in order, and for each
\* write, the commit_ts should be strictly greater than start_ts.
\* The committed write timestamp of one key must be in order, and no two writes
\* can overlap. For each write, the commit_ts should be strictly greater than
\* start_ts.
WriteConsistency ==
/\ \A k \in KEY :
\A n \in 1..Len(key_write[k]) - 1 :
checkWriteOrder(key_write[k][n], key_write[k][n + 1])
key_write[k][n].commit_ts < key_write[k][n + 1].start_ts
/\ \A k \in KEY :
\A n \in 1..Len(key_write[k]) :
key_write[k][n].start_ts < key_write[k][n].commit_ts