mirror of
https://github.com/pingcap/tla-plus.git
synced 2025-01-14 22:00:10 +08:00
32 lines
580 B
INI
32 lines
580 B
INI
|
CONSTANT
|
||
|
AppendEntriesReply = AppendEntriesReply
|
||
|
AppendEntriesRequest = AppendEntriesRequest
|
||
|
|
||
|
LogMerge = LogMerge
|
||
|
LogNormal = LogNormal
|
||
|
LogPreMerge = LogPreMerge
|
||
|
LogRollback = LogRollback
|
||
|
|
||
|
RegionA = RegionA
|
||
|
RegionB = RegionB
|
||
|
|
||
|
RegionMerging = RegionMerging
|
||
|
RegionNormal = RegionNormal
|
||
|
RegionTombStone = RegionTombStone
|
||
|
|
||
|
Region = {RegionA, RegionB}
|
||
|
LeaderA = 1
|
||
|
LeaderB = 2
|
||
|
MaxClientRequests = 2
|
||
|
QuorumSize = 1
|
||
|
Store = {1, 2}
|
||
|
WillPerformRollback = TRUE
|
||
|
|
||
|
SPECIFICATION
|
||
|
Spec
|
||
|
|
||
|
INVARIANT
|
||
|
TypeInvariant
|
||
|
SimpliedRaftInvariant
|
||
|
RaftMergeInvariant
|