github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2025-01-28 04:40:12 +08:00
Code Issues Packages Projects Releases Wiki Activity

clean trailing spaces

Browse Source 
Signed-off-by: Yilin Chen <sticnarf@gmail.com>
This commit is contained in:
Yilin Chen 2019-10-21 17:36:43 +08:00
parent 5e02db1bfb
commit 977207b0fc
No known key found for this signature in database
GPG Key ID: 353E7ED34BF326E0
1 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
PessimisticTransaction/PessimisticTransaction.tla
View File

@ -71,7 +71,7 @@ Start(c) ==
/\ \E ks \in SUBSET KEY: /\ \E ks \in SUBSET KEY:
\E primary \in ks: \E primary \in ks:
client_key' = client_key' =
[client_key EXCEPT [client_key EXCEPT
![c] = [primary |-> primary, ![c] = [primary |-> primary,
secondary |-> ks \ {primary}, secondary |-> ks \ {primary},
pessimistic |-> ks, pessimistic |-> ks,
@ -96,7 +96,7 @@ Init ==
ClientOp(c) == ClientOp(c) ==
\/ Start(c) \/ Start(c)
Next == \E c \in CLIENT : ClientOp(c) Next == \E c \in CLIENT : ClientOp(c)
----------------------------------------------------------------------------- -----------------------------------------------------------------------------
@ -108,11 +108,11 @@ ClientStateTypeInv ==
CLIENT -> {"init", "working", "prewriting", CLIENT -> {"init", "working", "prewriting",
"committing", "committed", "aborted"} "committing", "committed", "aborted"}
] ]
ClientTsTypeInv == ClientTsTypeInv ==
client_ts \in client_ts \in
[CLIENT -> [start_ts : Nat, for_update_ts: Nat, commit_ts : Nat]] [CLIENT -> [start_ts : Nat, for_update_ts: Nat, commit_ts : Nat]]
ClientKeyTypeInv == ClientKeyTypeInv ==
\A c \in CLIENT: \A c \in CLIENT:
\/ client_state[c] = "init" \/ client_state[c] = "init"
@ -121,7 +121,7 @@ ClientKeyTypeInv ==
pessimistic: SUBSET KEY, pessimistic: SUBSET KEY,
pending : SUBSET KEY pending : SUBSET KEY
] ]
KeyDataTypeInv == KeyDataTypeInv ==
key_data \in [KEY -> SUBSET [ts: Pos]] key_data \in [KEY -> SUBSET [ts: Pos]]
@ -129,10 +129,10 @@ KeyLockTypeInv ==
key_lock \in [KEY -> SUBSET [ts: Pos, for_update_ts: Nat, primary: KEY]] key_lock \in [KEY -> SUBSET [ts: Pos, for_update_ts: Nat, primary: KEY]]
KeyWriteTypeInv == KeyWriteTypeInv ==
key_write \in [KEY -> key_write \in [KEY ->
SUBSET [ts: Pos, type: {"write", "rollback"}, start_ts: Pos] SUBSET [ts: Pos, type: {"write", "rollback"}, start_ts: Pos]
] ]
KeyWriteStartTsInv == KeyWriteStartTsInv ==
\A k \in DOMAIN key_write: \A k \in DOMAIN key_write:
LET LET
@ -142,18 +142,18 @@ KeyWriteStartTsInv ==
\/ IF rec.type = "write" \/ IF rec.type = "write"
THEN rec.ts > rec.start_ts THEN rec.ts > rec.start_ts
ELSE rec.type = "rollback" /\ rec.ts = rec.start_ts ELSE rec.type = "rollback" /\ rec.ts = rec.start_ts
KeyLastReadTsTypeInv == KeyLastReadTsTypeInv ==
key_last_read_ts \in [KEY -> Nat] key_last_read_ts \in [KEY -> Nat]
MsgTypeInv == MsgTypeInv ==
msg \subseteq ( msg \subseteq (
[c: CLIENT, type: {"lock", "prewrite"}, key: KEY, [c: CLIENT, type: {"lock", "prewrite"}, key: KEY,
start_ts: Pos, for_update_ts: Pos] \union start_ts: Pos, for_update_ts: Pos] \union
[c: CLIENT, type: {"commit"}, key: KEY, commit_ts: Pos] \union [c: CLIENT, type: {"commit"}, key: KEY, commit_ts: Pos] \union
[c: CLIENT, type: {"rollback"}, key: KEY] [c: CLIENT, type: {"rollback"}, key: KEY]
) )
TypeInvariant == TypeInvariant ==
/\ NextTsTypeInv /\ NextTsTypeInv
/\ ClientStateTypeInv /\ ClientStateTypeInv
@ -165,5 +165,5 @@ TypeInvariant ==
/\ KeyWriteStartTsInv /\ KeyWriteStartTsInv
/\ KeyLastReadTsTypeInv /\ KeyLastReadTsTypeInv
/\ MsgTypeInv /\ MsgTypeInv
============================================================================= =============================================================================