From 7d1ad5bf38da2eea743314d2c8f254c32b2705ff Mon Sep 17 00:00:00 2001
From: foreverbell <dql.foreverbell@gmail.com>
Date: Thu, 22 Mar 2018 14:56:07 +0800
Subject: [PATCH] RaftMerge: rollback and TLC models. (#11)

---
 RaftMerge/RaftMerge.tla                       | 54 ++++++++++++---
 .../RaftMerge___Test1.launch                  | 66 +++++++++++++++++++
 .../RaftMerge___Test2.launch                  | 66 +++++++++++++++++++
 .../RaftMerge___Test3.launch                  | 66 +++++++++++++++++++
 .../RaftMerge___Test4.launch                  | 66 +++++++++++++++++++
 RaftMerge/Test1.cfg                           | 31 +++++++++
 RaftMerge/Test2.cfg                           | 31 +++++++++
 RaftMerge/Test3.cfg                           | 31 +++++++++
 RaftMerge/Test4.cfg                           | 31 +++++++++
 9 files changed, 432 insertions(+), 10 deletions(-)
 create mode 100644 RaftMerge/RaftMerge.toolbox/RaftMerge___Test1.launch
 create mode 100644 RaftMerge/RaftMerge.toolbox/RaftMerge___Test2.launch
 create mode 100644 RaftMerge/RaftMerge.toolbox/RaftMerge___Test3.launch
 create mode 100644 RaftMerge/RaftMerge.toolbox/RaftMerge___Test4.launch
 create mode 100644 RaftMerge/Test1.cfg
 create mode 100644 RaftMerge/Test2.cfg
 create mode 100644 RaftMerge/Test3.cfg
 create mode 100644 RaftMerge/Test4.cfg

diff --git a/RaftMerge/RaftMerge.tla b/RaftMerge/RaftMerge.tla
index 930730a..f9240b2 100644
--- a/RaftMerge/RaftMerge.tla
+++ b/RaftMerge/RaftMerge.tla
@@ -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 ==
diff --git a/RaftMerge/RaftMerge.toolbox/RaftMerge___Test1.launch b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test1.launch
new file mode 100644
index 0000000..c3301f3
--- /dev/null
+++ b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test1.launch
@@ -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>
diff --git a/RaftMerge/RaftMerge.toolbox/RaftMerge___Test2.launch b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test2.launch
new file mode 100644
index 0000000..5b40859
--- /dev/null
+++ b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test2.launch
@@ -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>
diff --git a/RaftMerge/RaftMerge.toolbox/RaftMerge___Test3.launch b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test3.launch
new file mode 100644
index 0000000..e30642a
--- /dev/null
+++ b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test3.launch
@@ -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>
diff --git a/RaftMerge/RaftMerge.toolbox/RaftMerge___Test4.launch b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test4.launch
new file mode 100644
index 0000000..14826cc
--- /dev/null
+++ b/RaftMerge/RaftMerge.toolbox/RaftMerge___Test4.launch
@@ -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>
diff --git a/RaftMerge/Test1.cfg b/RaftMerge/Test1.cfg
new file mode 100644
index 0000000..0b1d697
--- /dev/null
+++ b/RaftMerge/Test1.cfg
@@ -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
diff --git a/RaftMerge/Test2.cfg b/RaftMerge/Test2.cfg
new file mode 100644
index 0000000..7b7637d
--- /dev/null
+++ b/RaftMerge/Test2.cfg
@@ -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
diff --git a/RaftMerge/Test3.cfg b/RaftMerge/Test3.cfg
new file mode 100644
index 0000000..8ccff88
--- /dev/null
+++ b/RaftMerge/Test3.cfg
@@ -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
diff --git a/RaftMerge/Test4.cfg b/RaftMerge/Test4.cfg
new file mode 100644
index 0000000..7bef2d6
--- /dev/null
+++ b/RaftMerge/Test4.cfg
@@ -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