mirror of
https://github.com/pingcap/tla-plus.git
synced 2026-08-19 10:03:30 +08:00
34 lines
511 B
INI
34 lines
511 B
INI
\* See Test2.tla.
|
|
|
|
CONSTANT
|
|
KEY <- Key
|
|
OPTIMISTIC_CLIENT <- OptimistiicClient
|
|
PESSIMISTIC_CLIENT <- PessimisticClient
|
|
CLIENT_KEY <- ClientKey
|
|
CLIENT_PRIMARY <- ClientPrimary
|
|
|
|
INIT
|
|
Init
|
|
|
|
NEXT
|
|
Next
|
|
|
|
INVARIANT
|
|
NextTsTypeOK
|
|
ClientStateTypeOK
|
|
ClientTsTypeOK
|
|
ClientKeyTypeOK
|
|
KeyDataTypeOK
|
|
KeyLockTypeOK
|
|
KeyWriteTypeOK
|
|
KeyLastReadTsTypeOK
|
|
MsgTypeOK
|
|
|
|
INVARIANT
|
|
WriteConsistency
|
|
LockConsistency
|
|
CommittedTxnConsistency
|
|
AbortedClientConsistency
|
|
RollbackConsistency
|
|
UniqueWrite
|