mirror of
https://github.com/pingcap/tla-plus.git
synced 2024-12-26 12:30:10 +08:00
RaftMerge: rollback and TLC models. (#11)
This commit is contained in:
foreverbell
Ian
parent
b66286b0dd
commit
7d1ad5bf38
@ -27,6 +27,10 @@ ASSUME /\ Region = {RegionA, RegionB}
|
||||
/\ LeaderA \in Store
|
||||
/\ LeaderB \in Store
|
||||
|
||||
\* If TRUE, a rollback will be performed in place of merge.
|
||||
CONSTANTS WillPerformRollback
|
||||
ASSUME WillPerformRollback \in BOOLEAN
|
||||
|
||||
\* The minimum size of servers to be a quorum.
|
||||
\*
|
||||
\* The motivation of adding this constant is that, Raft with 1 leader and 2
|
||||
@ -57,7 +61,7 @@ VARIABLES messages
|
||||
|
||||
\* The data structures in C. MAXS = |Store|.
|
||||
\*
|
||||
\* enum Log { LogNormal, LogPreMerge, LogMerge };
|
||||
\* enum Log { LogNormal, LogPreMerge, LogMerge, LogRollback };
|
||||
\*
|
||||
\* enum RegionState { RegionNormal, RegionTombStone, RegionMerging };
|
||||
\*
|
||||
@ -89,7 +93,8 @@ VARIABLES messages
|
||||
\* Logs apart from LogNormal are admin logs.
|
||||
CONSTANTS LogNormal, \* RegionB only
|
||||
LogPreMerge,
|
||||
LogMerge
|
||||
LogMerge,
|
||||
LogRollback
|
||||
|
||||
\* Region state types.
|
||||
CONSTANTS RegionNormal,
|
||||
@ -230,6 +235,7 @@ InternalRequest(i, r, log) ==
|
||||
\* Send merge request to the leader of Region B.
|
||||
ProposeMergeRequest(i) ==
|
||||
/\ raft[i][RegionB].is_leader
|
||||
/\ region[i][RegionB] = RegionNormal
|
||||
/\ \* This request should be sent only once.
|
||||
Len(SelectSeq(raft[i][RegionB].logs, LAMBDA log : log.type = LogPreMerge)) = 0
|
||||
/\ raft' = InternalRequest(
|
||||
@ -239,6 +245,16 @@ ProposeMergeRequest(i) ==
|
||||
)
|
||||
/\ UNCHANGED <<messages, region, client_vars>>
|
||||
|
||||
\* Perform rollback by appending a rollback log on leader B.
|
||||
PerformRollbackRequest(i) ==
|
||||
/\ WillPerformRollback = TRUE
|
||||
/\ raft[i][RegionB].is_leader
|
||||
/\ region[i][RegionB] = RegionMerging
|
||||
/\ \* This log should be appended only once.
|
||||
Len(SelectSeq(raft[i][RegionB].logs, LAMBDA log : log.type = LogRollback)) = 0
|
||||
/\ raft' = InternalRequest(i, RegionB, [type |-> LogRollback])
|
||||
/\ UNCHANGED <<messages, region, client_vars>>
|
||||
|
||||
\* Return TRUE if there is a log applicable to the state machine.
|
||||
\* A log is applicable if it is committed, and the target region is not in
|
||||
\* TombStone state.
|
||||
@ -308,7 +324,11 @@ ApplyMergeLogStep2(i) ==
|
||||
/\ \* Lag logs have been applied.
|
||||
raft[i][RegionB].apply_index >= commit_index
|
||||
/\ raft' = [raft EXCEPT ![i][RegionA].apply_index = next_index]
|
||||
/\ region' = [region EXCEPT ![i][RegionB] = RegionTombStone]
|
||||
/\ IF WillPerformRollback = FALSE
|
||||
THEN
|
||||
region' = [region EXCEPT ![i][RegionB] = RegionTombStone]
|
||||
ELSE
|
||||
UNCHANGED <<region>>
|
||||
/\ UNCHANGED <<messages, client_vars>>
|
||||
|
||||
ApplyMergeLog(i) ==
|
||||
@ -320,6 +340,19 @@ ApplyMergeLog(i) ==
|
||||
/\ \/ ApplyMergeLogStep1(i)
|
||||
\/ ApplyMergeLogStep2(i)
|
||||
|
||||
\* Apply LogRollback.
|
||||
\* As we skip all logs after PreMerge log, rollback just marks the state of
|
||||
\* region as normal.
|
||||
ApplyRollbackLog(i) ==
|
||||
LET
|
||||
next_index == raft[i][RegionB].apply_index + 1
|
||||
IN
|
||||
/\ LogAppliable(i, RegionB)
|
||||
/\ raft[i][RegionB].logs[next_index].type = LogRollback
|
||||
/\ raft' = [raft EXCEPT ![i][RegionB].apply_index = next_index]
|
||||
/\ region' = [region EXCEPT ![i][RegionB] = RegionNormal]
|
||||
/\ UNCHANGED <<messages, client_vars>>
|
||||
|
||||
\* Apply LogNormal.
|
||||
\* This log simply increases apply_index.
|
||||
ApplyNormalLog(i, r) ==
|
||||
@ -345,6 +378,7 @@ ApplyLog(i) ==
|
||||
\/ \E r \in Region : ApplyNormalLog(i, r)
|
||||
\/ ApplyPreMergeLog(i)
|
||||
\/ ApplyMergeLog(i)
|
||||
\/ ApplyRollbackLog(i)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
@ -361,6 +395,7 @@ Next ==
|
||||
|
||||
\* Raft merge actions.
|
||||
\/ ProposeMergeRequest(LeaderB)
|
||||
\/ PerformRollbackRequest(LeaderB)
|
||||
\/ \E i \in Store : ApplyLog(i)
|
||||
|
||||
Init ==
|
||||
@ -397,6 +432,7 @@ LogType ==
|
||||
FlatLogType ==
|
||||
[type : {LogNormal}]
|
||||
\cup [type : {LogPreMerge}, min_index : Nat]
|
||||
\cup [type : {LogRollback}]
|
||||
IN
|
||||
FlatLogType
|
||||
\cup [type : {LogMerge},
|
||||
@ -472,14 +508,16 @@ SimpliedRaftInvariant ==
|
||||
\* Some invariants for Raft region merge.
|
||||
|
||||
\* If a region on two different stores have applied the same logs, they should
|
||||
\* also share the same region state.
|
||||
\* also share the same region state and number of applied normal logs.
|
||||
RegionApplyInvariant ==
|
||||
\A i, j \in Store :
|
||||
(
|
||||
/\ i /= j
|
||||
/\ (\A r \in Region : raft[i][r].apply_index = raft[j][r].apply_index)
|
||||
) =>
|
||||
\A r \in Region : region[i][r] = region[j][r]
|
||||
\A r \in Region :
|
||||
/\ region[i][r] = region[j][r]
|
||||
/\ raft[i][RegionB].num_applied = raft[j][RegionB].num_applied
|
||||
|
||||
\* For any two stores of region B, if both done, they should have the same
|
||||
\* number of applied logs.
|
||||
@ -490,11 +528,7 @@ MergeLogInvariant ==
|
||||
/\ region[i][RegionB] = RegionTombStone
|
||||
/\ region[j][RegionB] = RegionTombStone
|
||||
) =>
|
||||
LET
|
||||
applied_i == raft[i][RegionB].num_applied
|
||||
applied_j == raft[j][RegionB].num_applied
|
||||
IN
|
||||
applied_i = applied_j
|
||||
raft[i][RegionB].num_applied = raft[j][RegionB].num_applied
|
||||
|
||||
\* Combination of the above invariants.
|
||||
RaftMergeInvariant ==
|
||||
|
||||
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test1.launch
Normal file
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test1.launch
Normal file
@ -0,0 +1,66 @@
|
||||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
|
||||
<stringAttribute key="TLCCmdLineParameters" value="-workers 2"/>
|
||||
<stringAttribute key="configurationName" value="Test1"/>
|
||||
<booleanAttribute key="deferLiveness" value="false"/>
|
||||
<intAttribute key="dfidDepth" value="100"/>
|
||||
<booleanAttribute key="dfidMode" value="false"/>
|
||||
<intAttribute key="distributedFPSetCount" value="0"/>
|
||||
<stringAttribute key="distributedNetworkInterface" value="172.17.0.1"/>
|
||||
<intAttribute key="distributedNodesCount" value="1"/>
|
||||
<stringAttribute key="distributedTLC" value="off"/>
|
||||
<stringAttribute key="distributedTLCVMArgs" value=""/>
|
||||
<intAttribute key="fpBits" value="1"/>
|
||||
<intAttribute key="fpIndex" value="1"/>
|
||||
<intAttribute key="maxHeapSize" value="25"/>
|
||||
<intAttribute key="maxSetSize" value="1000000"/>
|
||||
<booleanAttribute key="mcMode" value="true"/>
|
||||
<stringAttribute key="modelBehaviorInit" value=""/>
|
||||
<stringAttribute key="modelBehaviorNext" value=""/>
|
||||
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
|
||||
<intAttribute key="modelBehaviorSpecType" value="1"/>
|
||||
<stringAttribute key="modelBehaviorVars" value="client_requests_index, messages, raft, region"/>
|
||||
<stringAttribute key="modelComments" value=""/>
|
||||
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
|
||||
<listAttribute key="modelCorrectnessInvariants">
|
||||
<listEntry value="1TypeInvariant"/>
|
||||
<listEntry value="1SimpliedRaftInvariant"/>
|
||||
<listEntry value="1RaftMergeInvariant"/>
|
||||
</listAttribute>
|
||||
<listAttribute key="modelCorrectnessProperties"/>
|
||||
<stringAttribute key="modelExpressionEval" value=""/>
|
||||
<stringAttribute key="modelParameterActionConstraint" value=""/>
|
||||
<listAttribute key="modelParameterConstants">
|
||||
<listEntry value="LeaderA;;1;0;0"/>
|
||||
<listEntry value="LeaderB;;2;0;0"/>
|
||||
<listEntry value="Store;;{1,2};0;0"/>
|
||||
<listEntry value="RegionA;;RegionA;1;0"/>
|
||||
<listEntry value="RegionB;;RegionB;1;0"/>
|
||||
<listEntry value="AppendEntriesReply;;AppendEntriesReply;1;0"/>
|
||||
<listEntry value="Region;;{RegionA, RegionB};0;0"/>
|
||||
<listEntry value="AppendEntriesRequest;;AppendEntriesRequest;1;0"/>
|
||||
<listEntry value="MaxClientRequests;;2;0;0"/>
|
||||
<listEntry value="QuorumSize;;1;0;0"/>
|
||||
<listEntry value="LogNormal;;LogNormal;1;0"/>
|
||||
<listEntry value="RegionNormal;;RegionNormal;1;0"/>
|
||||
<listEntry value="LogPreMerge;;LogPreMerge;1;0"/>
|
||||
<listEntry value="LogMerge;;LogMerge;1;0"/>
|
||||
<listEntry value="RegionMerging;;RegionMerging;1;0"/>
|
||||
<listEntry value="RegionTombStone;;RegionTombStone;1;0"/>
|
||||
<listEntry value="LogRollback;;LogRollback;1;0"/>
|
||||
<listEntry value="WillPerformRollback;;FALSE;0;0"/>
|
||||
</listAttribute>
|
||||
<stringAttribute key="modelParameterContraint" value=""/>
|
||||
<listAttribute key="modelParameterDefinitions"/>
|
||||
<stringAttribute key="modelParameterModelValues" value="{}"/>
|
||||
<stringAttribute key="modelParameterNewDefinitions" value=""/>
|
||||
<intAttribute key="numberOfWorkers" value="2"/>
|
||||
<booleanAttribute key="recover" value="false"/>
|
||||
<stringAttribute key="result.mail.address" value=""/>
|
||||
<intAttribute key="simuAril" value="-1"/>
|
||||
<intAttribute key="simuDepth" value="100"/>
|
||||
<intAttribute key="simuSeed" value="-1"/>
|
||||
<stringAttribute key="specName" value="RaftMerge"/>
|
||||
<stringAttribute key="view" value=""/>
|
||||
<booleanAttribute key="visualizeStateGraph" value="false"/>
|
||||
</launchConfiguration>
|
||||
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test2.launch
Normal file
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test2.launch
Normal file
@ -0,0 +1,66 @@
|
||||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
|
||||
<stringAttribute key="TLCCmdLineParameters" value="-workers 2"/>
|
||||
<stringAttribute key="configurationName" value="Test2"/>
|
||||
<booleanAttribute key="deferLiveness" value="false"/>
|
||||
<intAttribute key="dfidDepth" value="100"/>
|
||||
<booleanAttribute key="dfidMode" value="false"/>
|
||||
<intAttribute key="distributedFPSetCount" value="0"/>
|
||||
<stringAttribute key="distributedNetworkInterface" value="172.17.0.1"/>
|
||||
<intAttribute key="distributedNodesCount" value="1"/>
|
||||
<stringAttribute key="distributedTLC" value="off"/>
|
||||
<stringAttribute key="distributedTLCVMArgs" value=""/>
|
||||
<intAttribute key="fpBits" value="1"/>
|
||||
<intAttribute key="fpIndex" value="1"/>
|
||||
<intAttribute key="maxHeapSize" value="25"/>
|
||||
<intAttribute key="maxSetSize" value="1000000"/>
|
||||
<booleanAttribute key="mcMode" value="true"/>
|
||||
<stringAttribute key="modelBehaviorInit" value=""/>
|
||||
<stringAttribute key="modelBehaviorNext" value=""/>
|
||||
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
|
||||
<intAttribute key="modelBehaviorSpecType" value="1"/>
|
||||
<stringAttribute key="modelBehaviorVars" value="client_requests_index, messages, raft, region"/>
|
||||
<stringAttribute key="modelComments" value=""/>
|
||||
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
|
||||
<listAttribute key="modelCorrectnessInvariants">
|
||||
<listEntry value="1TypeInvariant"/>
|
||||
<listEntry value="1SimpliedRaftInvariant"/>
|
||||
<listEntry value="1RaftMergeInvariant"/>
|
||||
</listAttribute>
|
||||
<listAttribute key="modelCorrectnessProperties"/>
|
||||
<stringAttribute key="modelExpressionEval" value=""/>
|
||||
<stringAttribute key="modelParameterActionConstraint" value=""/>
|
||||
<listAttribute key="modelParameterConstants">
|
||||
<listEntry value="LeaderA;;1;0;0"/>
|
||||
<listEntry value="LeaderB;;1;0;0"/>
|
||||
<listEntry value="Store;;{1,2};0;0"/>
|
||||
<listEntry value="RegionA;;RegionA;1;0"/>
|
||||
<listEntry value="RegionB;;RegionB;1;0"/>
|
||||
<listEntry value="AppendEntriesReply;;AppendEntriesReply;1;0"/>
|
||||
<listEntry value="Region;;{RegionA, RegionB};0;0"/>
|
||||
<listEntry value="AppendEntriesRequest;;AppendEntriesRequest;1;0"/>
|
||||
<listEntry value="MaxClientRequests;;2;0;0"/>
|
||||
<listEntry value="QuorumSize;;1;0;0"/>
|
||||
<listEntry value="LogNormal;;LogNormal;1;0"/>
|
||||
<listEntry value="RegionNormal;;RegionNormal;1;0"/>
|
||||
<listEntry value="LogPreMerge;;LogPreMerge;1;0"/>
|
||||
<listEntry value="LogMerge;;LogMerge;1;0"/>
|
||||
<listEntry value="RegionMerging;;RegionMerging;1;0"/>
|
||||
<listEntry value="RegionTombStone;;RegionTombStone;1;0"/>
|
||||
<listEntry value="LogRollback;;LogRollback;1;0"/>
|
||||
<listEntry value="WillPerformRollback;;FALSE;0;0"/>
|
||||
</listAttribute>
|
||||
<stringAttribute key="modelParameterContraint" value=""/>
|
||||
<listAttribute key="modelParameterDefinitions"/>
|
||||
<stringAttribute key="modelParameterModelValues" value="{}"/>
|
||||
<stringAttribute key="modelParameterNewDefinitions" value=""/>
|
||||
<intAttribute key="numberOfWorkers" value="2"/>
|
||||
<booleanAttribute key="recover" value="false"/>
|
||||
<stringAttribute key="result.mail.address" value=""/>
|
||||
<intAttribute key="simuAril" value="-1"/>
|
||||
<intAttribute key="simuDepth" value="100"/>
|
||||
<intAttribute key="simuSeed" value="-1"/>
|
||||
<stringAttribute key="specName" value="RaftMerge"/>
|
||||
<stringAttribute key="view" value=""/>
|
||||
<booleanAttribute key="visualizeStateGraph" value="false"/>
|
||||
</launchConfiguration>
|
||||
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test3.launch
Normal file
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test3.launch
Normal file
@ -0,0 +1,66 @@
|
||||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
|
||||
<stringAttribute key="TLCCmdLineParameters" value="-workers 2"/>
|
||||
<stringAttribute key="configurationName" value="Test3"/>
|
||||
<booleanAttribute key="deferLiveness" value="false"/>
|
||||
<intAttribute key="dfidDepth" value="100"/>
|
||||
<booleanAttribute key="dfidMode" value="false"/>
|
||||
<intAttribute key="distributedFPSetCount" value="0"/>
|
||||
<stringAttribute key="distributedNetworkInterface" value="172.17.0.1"/>
|
||||
<intAttribute key="distributedNodesCount" value="1"/>
|
||||
<stringAttribute key="distributedTLC" value="off"/>
|
||||
<stringAttribute key="distributedTLCVMArgs" value=""/>
|
||||
<intAttribute key="fpBits" value="1"/>
|
||||
<intAttribute key="fpIndex" value="1"/>
|
||||
<intAttribute key="maxHeapSize" value="25"/>
|
||||
<intAttribute key="maxSetSize" value="1000000"/>
|
||||
<booleanAttribute key="mcMode" value="true"/>
|
||||
<stringAttribute key="modelBehaviorInit" value=""/>
|
||||
<stringAttribute key="modelBehaviorNext" value=""/>
|
||||
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
|
||||
<intAttribute key="modelBehaviorSpecType" value="1"/>
|
||||
<stringAttribute key="modelBehaviorVars" value="client_requests_index, messages, raft, region"/>
|
||||
<stringAttribute key="modelComments" value=""/>
|
||||
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
|
||||
<listAttribute key="modelCorrectnessInvariants">
|
||||
<listEntry value="1TypeInvariant"/>
|
||||
<listEntry value="1SimpliedRaftInvariant"/>
|
||||
<listEntry value="1RaftMergeInvariant"/>
|
||||
</listAttribute>
|
||||
<listAttribute key="modelCorrectnessProperties"/>
|
||||
<stringAttribute key="modelExpressionEval" value=""/>
|
||||
<stringAttribute key="modelParameterActionConstraint" value=""/>
|
||||
<listAttribute key="modelParameterConstants">
|
||||
<listEntry value="LeaderA;;1;0;0"/>
|
||||
<listEntry value="LeaderB;;2;0;0"/>
|
||||
<listEntry value="Store;;{1,2};0;0"/>
|
||||
<listEntry value="RegionA;;RegionA;1;0"/>
|
||||
<listEntry value="RegionB;;RegionB;1;0"/>
|
||||
<listEntry value="AppendEntriesReply;;AppendEntriesReply;1;0"/>
|
||||
<listEntry value="Region;;{RegionA, RegionB};0;0"/>
|
||||
<listEntry value="AppendEntriesRequest;;AppendEntriesRequest;1;0"/>
|
||||
<listEntry value="MaxClientRequests;;2;0;0"/>
|
||||
<listEntry value="QuorumSize;;1;0;0"/>
|
||||
<listEntry value="LogNormal;;LogNormal;1;0"/>
|
||||
<listEntry value="RegionNormal;;RegionNormal;1;0"/>
|
||||
<listEntry value="LogPreMerge;;LogPreMerge;1;0"/>
|
||||
<listEntry value="LogMerge;;LogMerge;1;0"/>
|
||||
<listEntry value="RegionMerging;;RegionMerging;1;0"/>
|
||||
<listEntry value="RegionTombStone;;RegionTombStone;1;0"/>
|
||||
<listEntry value="LogRollback;;LogRollback;1;0"/>
|
||||
<listEntry value="WillPerformRollback;;TRUE;0;0"/>
|
||||
</listAttribute>
|
||||
<stringAttribute key="modelParameterContraint" value=""/>
|
||||
<listAttribute key="modelParameterDefinitions"/>
|
||||
<stringAttribute key="modelParameterModelValues" value="{}"/>
|
||||
<stringAttribute key="modelParameterNewDefinitions" value=""/>
|
||||
<intAttribute key="numberOfWorkers" value="2"/>
|
||||
<booleanAttribute key="recover" value="false"/>
|
||||
<stringAttribute key="result.mail.address" value=""/>
|
||||
<intAttribute key="simuAril" value="-1"/>
|
||||
<intAttribute key="simuDepth" value="100"/>
|
||||
<intAttribute key="simuSeed" value="-1"/>
|
||||
<stringAttribute key="specName" value="RaftMerge"/>
|
||||
<stringAttribute key="view" value=""/>
|
||||
<booleanAttribute key="visualizeStateGraph" value="false"/>
|
||||
</launchConfiguration>
|
||||
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test4.launch
Normal file
66
RaftMerge/RaftMerge.toolbox/RaftMerge___Test4.launch
Normal file
@ -0,0 +1,66 @@
|
||||
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
|
||||
<stringAttribute key="TLCCmdLineParameters" value="-workers 2"/>
|
||||
<stringAttribute key="configurationName" value="Test4"/>
|
||||
<booleanAttribute key="deferLiveness" value="false"/>
|
||||
<intAttribute key="dfidDepth" value="100"/>
|
||||
<booleanAttribute key="dfidMode" value="false"/>
|
||||
<intAttribute key="distributedFPSetCount" value="0"/>
|
||||
<stringAttribute key="distributedNetworkInterface" value="172.17.0.1"/>
|
||||
<intAttribute key="distributedNodesCount" value="1"/>
|
||||
<stringAttribute key="distributedTLC" value="off"/>
|
||||
<stringAttribute key="distributedTLCVMArgs" value=""/>
|
||||
<intAttribute key="fpBits" value="1"/>
|
||||
<intAttribute key="fpIndex" value="1"/>
|
||||
<intAttribute key="maxHeapSize" value="25"/>
|
||||
<intAttribute key="maxSetSize" value="1000000"/>
|
||||
<booleanAttribute key="mcMode" value="true"/>
|
||||
<stringAttribute key="modelBehaviorInit" value=""/>
|
||||
<stringAttribute key="modelBehaviorNext" value=""/>
|
||||
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
|
||||
<intAttribute key="modelBehaviorSpecType" value="1"/>
|
||||
<stringAttribute key="modelBehaviorVars" value="client_requests_index, messages, raft, region"/>
|
||||
<stringAttribute key="modelComments" value=""/>
|
||||
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
|
||||
<listAttribute key="modelCorrectnessInvariants">
|
||||
<listEntry value="1TypeInvariant"/>
|
||||
<listEntry value="1SimpliedRaftInvariant"/>
|
||||
<listEntry value="1RaftMergeInvariant"/>
|
||||
</listAttribute>
|
||||
<listAttribute key="modelCorrectnessProperties"/>
|
||||
<stringAttribute key="modelExpressionEval" value=""/>
|
||||
<stringAttribute key="modelParameterActionConstraint" value=""/>
|
||||
<listAttribute key="modelParameterConstants">
|
||||
<listEntry value="LeaderA;;1;0;0"/>
|
||||
<listEntry value="LeaderB;;1;0;0"/>
|
||||
<listEntry value="Store;;{1,2};0;0"/>
|
||||
<listEntry value="RegionA;;RegionA;1;0"/>
|
||||
<listEntry value="RegionB;;RegionB;1;0"/>
|
||||
<listEntry value="AppendEntriesReply;;AppendEntriesReply;1;0"/>
|
||||
<listEntry value="Region;;{RegionA, RegionB};0;0"/>
|
||||
<listEntry value="AppendEntriesRequest;;AppendEntriesRequest;1;0"/>
|
||||
<listEntry value="MaxClientRequests;;2;0;0"/>
|
||||
<listEntry value="QuorumSize;;1;0;0"/>
|
||||
<listEntry value="LogNormal;;LogNormal;1;0"/>
|
||||
<listEntry value="RegionNormal;;RegionNormal;1;0"/>
|
||||
<listEntry value="LogPreMerge;;LogPreMerge;1;0"/>
|
||||
<listEntry value="LogMerge;;LogMerge;1;0"/>
|
||||
<listEntry value="RegionMerging;;RegionMerging;1;0"/>
|
||||
<listEntry value="RegionTombStone;;RegionTombStone;1;0"/>
|
||||
<listEntry value="LogRollback;;LogRollback;1;0"/>
|
||||
<listEntry value="WillPerformRollback;;TRUE;0;0"/>
|
||||
</listAttribute>
|
||||
<stringAttribute key="modelParameterContraint" value=""/>
|
||||
<listAttribute key="modelParameterDefinitions"/>
|
||||
<stringAttribute key="modelParameterModelValues" value="{}"/>
|
||||
<stringAttribute key="modelParameterNewDefinitions" value=""/>
|
||||
<intAttribute key="numberOfWorkers" value="2"/>
|
||||
<booleanAttribute key="recover" value="false"/>
|
||||
<stringAttribute key="result.mail.address" value=""/>
|
||||
<intAttribute key="simuAril" value="-1"/>
|
||||
<intAttribute key="simuDepth" value="100"/>
|
||||
<intAttribute key="simuSeed" value="-1"/>
|
||||
<stringAttribute key="specName" value="RaftMerge"/>
|
||||
<stringAttribute key="view" value=""/>
|
||||
<booleanAttribute key="visualizeStateGraph" value="false"/>
|
||||
</launchConfiguration>
|
||||
31
RaftMerge/Test1.cfg
Normal file
31
RaftMerge/Test1.cfg
Normal file
@ -0,0 +1,31 @@
|
||||
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 = FALSE
|
||||
|
||||
SPECIFICATION
|
||||
Spec
|
||||
|
||||
INVARIANT
|
||||
TypeInvariant
|
||||
SimpliedRaftInvariant
|
||||
RaftMergeInvariant
|
||||
31
RaftMerge/Test2.cfg
Normal file
31
RaftMerge/Test2.cfg
Normal file
@ -0,0 +1,31 @@
|
||||
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 = 1
|
||||
MaxClientRequests = 2
|
||||
QuorumSize = 1
|
||||
Store = {1, 2}
|
||||
WillPerformRollback = FALSE
|
||||
|
||||
SPECIFICATION
|
||||
Spec
|
||||
|
||||
INVARIANT
|
||||
TypeInvariant
|
||||
SimpliedRaftInvariant
|
||||
RaftMergeInvariant
|
||||
31
RaftMerge/Test3.cfg
Normal file
31
RaftMerge/Test3.cfg
Normal file
@ -0,0 +1,31 @@
|
||||
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
|
||||
31
RaftMerge/Test4.cfg
Normal file
31
RaftMerge/Test4.cfg
Normal file
@ -0,0 +1,31 @@
|
||||
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 = 1
|
||||
MaxClientRequests = 2
|
||||
QuorumSize = 1
|
||||
Store = {1, 2}
|
||||
WillPerformRollback = TRUE
|
||||
|
||||
SPECIFICATION
|
||||
Spec
|
||||
|
||||
INVARIANT
|
||||
TypeInvariant
|
||||
SimpliedRaftInvariant
|
||||
RaftMergeInvariant
|
||||
Loading…
Reference in New Issue
Block a user