Typed model values in consensus spec (#6229)

microsoft · Jun 6, 2024 · d554f45 · d554f45
1 parent 43ae533
commit d554f45
Show file tree

Hide file tree

Showing 6 changed files with 157 additions and 157 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -18,33 +18,33 @@ CONSTANTS
 
     Nil = Nil
 
-    Follower = Follower
-    Candidate = Candidate
-    Leader = Leader
-    None = None
+    Follower = L_Follower
+    Candidate = L_Candidate
+    Leader = L_Leader
+    None = L_None
 
-    Active = Active
-    RetirementOrdered = RetirementOrdered
-    RetirementSigned = RetirementSigned
-    RetirementCompleted = RetirementCompleted
-    RetiredCommitted = RetiredCommitted
+    Active = R_Active
+    RetirementOrdered = R_RetirementOrdered
+    RetirementSigned = R_RetirementSigned
+    RetirementCompleted = R_RetirementCompleted
+    RetiredCommitted = R_RetiredCommitted
 
-    RequestVoteRequest = RequestVoteRequest
-    RequestVoteResponse = RequestVoteResponse
-    AppendEntriesRequest = AppendEntriesRequest
-    AppendEntriesResponse = AppendEntriesResponse
-    ProposeVoteRequest = ProposeVoteRequest
+    RequestVoteRequest = M_RequestVoteRequest
+    RequestVoteResponse = M_RequestVoteResponse
+    AppendEntriesRequest = M_AppendEntriesRequest
+    AppendEntriesResponse = M_AppendEntriesResponse
+    ProposeVoteRequest = M_ProposeVoteRequest
 
-    OrderedNoDup = OrderedNoDup
-    Ordered = Ordered
-    ReorderedNoDup = ReorderedNoDup
-    Reordered = Reordered
-    Guarantee = OrderedNoDup
+    OrderedNoDup = N_OrderedNoDup
+    Ordered = N_Ordered
+    ReorderedNoDup = N_ReorderedNoDup
+    Reordered = N_Reordered
+    Guarantee = N_OrderedNoDup
 
-    TypeEntry = Entry
-    TypeSignature = Signature
-    TypeReconfiguration = Reconfiguration
-    TypeRetired = Retired
+    TypeEntry = T_Entry
+    TypeSignature = T_Signature
+    TypeReconfiguration = T_Reconfiguration
+    TypeRetired = T_Retired
 
     NodeOne = n1
     NodeTwo = n2

diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg
@@ -20,33 +20,33 @@ CONSTANTS
 
     Nil = Nil
 
-    Follower = Follower
-    Candidate = Candidate
-    Leader = Leader
-    None = None
-
-    Active = Active
-    RetirementOrdered = RetirementOrdered
-    RetirementSigned = RetirementSigned
-    RetirementCompleted = RetirementCompleted
-    RetiredCommitted = RetiredCommitted
-
-    RequestVoteRequest = RequestVoteRequest
-    RequestVoteResponse = RequestVoteResponse
-    AppendEntriesRequest = AppendEntriesRequest
-    AppendEntriesResponse = AppendEntriesResponse
-    ProposeVoteRequest = ProposeVoteRequest
-
-    OrderedNoDup = OrderedNoDup
-    Ordered = Ordered
-    ReorderedNoDup = ReorderedNoDup
-    Reordered = Reordered
-    Guarantee = OrderedNoDup
-
-    TypeEntry = Entry
-    TypeSignature = Signature
-    TypeReconfiguration = Reconfiguration
-    TypeRetired = Retired
+    Follower = L_Follower
+    Candidate = L_Candidate
+    Leader = L_Leader
+    None = L_None
+
+    Active = R_Active
+    RetirementOrdered = R_RetirementOrdered
+    RetirementSigned = R_RetirementSigned
+    RetirementCompleted = R_RetirementCompleted
+    RetiredCommitted = R_RetiredCommitted
+
+    RequestVoteRequest = M_RequestVoteRequest
+    RequestVoteResponse = M_RequestVoteResponse
+    AppendEntriesRequest = M_AppendEntriesRequest
+    AppendEntriesResponse = M_AppendEntriesResponse
+    ProposeVoteRequest = M_ProposeVoteRequest
+
+    OrderedNoDup = N_OrderedNoDup
+    Ordered = N_Ordered
+    ReorderedNoDup = N_ReorderedNoDup
+    Reordered = N_Reordered
+    Guarantee = N_OrderedNoDup
+
+    TypeEntry = T_Entry
+    TypeSignature = T_Signature
+    TypeReconfiguration = T_Reconfiguration
+    TypeRetired = T_Retired
 
     NodeOne = n1
     NodeTwo = n2

diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -19,33 +19,33 @@ CONSTANTS
 
     Nil = Nil
 
-    Follower = Follower
-    Candidate = Candidate
-    Leader = Leader
-    None = None
-
-    Active = Active
-    RetirementOrdered = RetirementOrdered
-    RetirementSigned = RetirementSigned
-    RetirementCompleted = RetirementCompleted
-    RetiredCommitted = RetiredCommitted
-
-    RequestVoteRequest = RequestVoteRequest
-    RequestVoteResponse = RequestVoteResponse
-    AppendEntriesRequest = AppendEntriesRequest
-    AppendEntriesResponse = AppendEntriesResponse
-    ProposeVoteRequest = ProposeVoteRequest
-
-    OrderedNoDup = OrderedNoDup
-    Ordered = Ordered
-    ReorderedNoDup = ReorderedNoDup
-    Reordered = Reordered
-    Guarantee = OrderedNoDup
-
-    TypeEntry = Entry
-    TypeSignature = Signature
-    TypeReconfiguration = Reconfiguration
-    TypeRetired = Retired
+    Follower = L_Follower
+    Candidate = L_Candidate
+    Leader = L_Leader
+    None = L_None
+
+    Active = R_Active
+    RetirementOrdered = R_RetirementOrdered
+    RetirementSigned = R_RetirementSigned
+    RetirementCompleted = R_RetirementCompleted
+    RetiredCommitted = R_RetiredCommitted
+
+    RequestVoteRequest = M_RequestVoteRequest
+    RequestVoteResponse = M_RequestVoteResponse
+    AppendEntriesRequest = M_AppendEntriesRequest
+    AppendEntriesResponse = M_AppendEntriesResponse
+    ProposeVoteRequest = M_ProposeVoteRequest
+
+    OrderedNoDup = N_OrderedNoDup
+    Ordered = N_Ordered
+    ReorderedNoDup = N_ReorderedNoDup
+    Reordered = N_Reordered
+    Guarantee = N_OrderedNoDup
+
+    TypeEntry = T_Entry
+    TypeSignature = T_Signature
+    TypeReconfiguration = T_Reconfiguration
+    TypeRetired = T_Retired
 
     NodeOne = n1
     NodeTwo = n2

diff --git a/tla/consensus/SIMCoverageccfraft.cfg b/tla/consensus/SIMCoverageccfraft.cfg
@@ -5,33 +5,33 @@ CONSTANTS
 
     Nil = Nil
 
-    Follower = Follower
-    Candidate = Candidate
-    Leader = Leader
-    None = None
-
-    Active = Active
-    RetirementOrdered = RetirementOrdered
-    RetirementSigned = RetirementSigned
-    RetirementCompleted = RetirementCompleted
-    RetiredCommitted = RetiredCommitted
-
-    RequestVoteRequest = RequestVoteRequest
-    RequestVoteResponse = RequestVoteResponse
-    AppendEntriesRequest = AppendEntriesRequest
-    AppendEntriesResponse = AppendEntriesResponse
-    ProposeVoteRequest = ProposeVoteRequest
-
-    OrderedNoDup = OrderedNoDup
-    Ordered = Ordered
-    ReorderedNoDup = ReorderedNoDup
-    Reordered = Reordered
-    Guarantee = OrderedNoDup
-
-    TypeEntry = Entry
-    TypeSignature = Signature
-    TypeReconfiguration = Reconfiguration
-    TypeRetired = Retired
+    Follower = L_Follower
+    Candidate = L_Candidate
+    Leader = L_Leader
+    None = L_None
+
+    Active = R_Active
+    RetirementOrdered = R_RetirementOrdered
+    RetirementSigned = R_RetirementSigned
+    RetirementCompleted = R_RetirementCompleted
+    RetiredCommitted = R_RetiredCommitted
+
+    RequestVoteRequest = M_RequestVoteRequest
+    RequestVoteResponse = M_RequestVoteResponse
+    AppendEntriesRequest = M_AppendEntriesRequest
+    AppendEntriesResponse = M_AppendEntriesResponse
+    ProposeVoteRequest = M_ProposeVoteRequest
+
+    OrderedNoDup = N_OrderedNoDup
+    Ordered = N_Ordered
+    ReorderedNoDup = N_ReorderedNoDup
+    Reordered = N_Reordered
+    Guarantee = N_OrderedNoDup
+
+    TypeEntry = T_Entry
+    TypeSignature = T_Signature
+    TypeReconfiguration = T_Reconfiguration
+    TypeRetired = T_Retired
 
     NodeOne = n1
     NodeTwo = n2

diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -5,33 +5,33 @@ CONSTANTS
 
     Nil = Nil
 
-    Follower = Follower
-    Candidate = Candidate
-    Leader = Leader
-    None = None
-
-    Active = Active
-    RetirementOrdered = RetirementOrdered
-    RetirementSigned = RetirementSigned
-    RetirementCompleted = RetirementCompleted
-    RetiredCommitted = RetiredCommitted
-
-    RequestVoteRequest = RequestVoteRequest
-    RequestVoteResponse = RequestVoteResponse
-    AppendEntriesRequest = AppendEntriesRequest
-    AppendEntriesResponse = AppendEntriesResponse
-    ProposeVoteRequest = ProposeVoteRequest
-
-    OrderedNoDup = OrderedNoDup
-    Ordered = Ordered
-    ReorderedNoDup = ReorderedNoDup
-    Reordered = Reordered
-    Guarantee = OrderedNoDup
-
-    TypeEntry = Entry
-    TypeSignature = Signature
-    TypeReconfiguration = Reconfiguration
-    TypeRetired = Retired
+    Follower = L_Follower
+    Candidate = L_Candidate
+    Leader = L_Leader
+    None = L_None
+
+    Active = R_Active
+    RetirementOrdered = R_RetirementOrdered
+    RetirementSigned = R_RetirementSigned
+    RetirementCompleted = R_RetirementCompleted
+    RetiredCommitted = R_RetiredCommitted
+
+    RequestVoteRequest = M_RequestVoteRequest
+    RequestVoteResponse = M_RequestVoteResponse
+    AppendEntriesRequest = M_AppendEntriesRequest
+    AppendEntriesResponse = M_AppendEntriesResponse
+    ProposeVoteRequest = M_ProposeVoteRequest
+
+    OrderedNoDup = N_OrderedNoDup
+    Ordered = N_Ordered
+    ReorderedNoDup = N_ReorderedNoDup
+    Reordered = N_Reordered
+    Guarantee = N_OrderedNoDup
+
+    TypeEntry = T_Entry
+    TypeSignature = T_Signature
+    TypeReconfiguration = T_Reconfiguration
+    TypeRetired = T_Retired
 
     NodeOne = n1
     NodeTwo = n2

diff --git a/tla/consensus/Traceccfraft.cfg b/tla/consensus/Traceccfraft.cfg
@@ -56,34 +56,34 @@ CONSTANTS
 
     Nil = Nil
 
-    Follower = Follower
-    Candidate = Candidate
-    Leader = Leader
-    None = None
-
-    Active = Active
-    RetirementOrdered = RetirementOrdered
-    RetirementSigned = RetirementSigned
-    RetirementCompleted = RetirementCompleted
-    RetiredCommitted = RetiredCommitted
-
-    RequestVoteRequest = RequestVoteRequest
-    RequestVoteResponse = RequestVoteResponse
-    AppendEntriesRequest = AppendEntriesRequest
-    AppendEntriesResponse = AppendEntriesResponse
-    ProposeVoteRequest = ProposeVoteRequest
-
-    OrderedNoDup = OrderedNoDup
-    Ordered = Ordered
-    ReorderedNoDup = ReorderedNoDup
-    Reordered = Reordered
+    Follower = L_Follower
+    Candidate = L_Candidate
+    Leader = L_Leader
+    None = L_None
+
+    Active = R_Active
+    RetirementOrdered = R_RetirementOrdered
+    RetirementSigned = R_RetirementSigned
+    RetirementCompleted = R_RetirementCompleted
+    RetiredCommitted = R_RetiredCommitted
+
+    RequestVoteRequest = M_RequestVoteRequest
+    RequestVoteResponse = M_RequestVoteResponse
+    AppendEntriesRequest = M_AppendEntriesRequest
+    AppendEntriesResponse = M_AppendEntriesResponse
+    ProposeVoteRequest = M_ProposeVoteRequest
+
+    OrderedNoDup = N_OrderedNoDup
+    Ordered = N_Ordered
+    ReorderedNoDup = N_ReorderedNoDup
+    Reordered = N_Reordered
     \* Ordered instead of OrderedNoDup compared to ordinary model checking.
-    Guarantee = Ordered
+    Guarantee = N_Ordered
 
-    TypeEntry = TypeEntry
-    TypeSignature = TypeSignature
-    TypeReconfiguration = TypeReconfiguration
-    TypeRetired = Retired
+    TypeEntry = T_Entry
+    TypeSignature = T_Signature
+    TypeReconfiguration = T_Reconfiguration
+    TypeRetired = T_Retired
 
     \* state.h my_node_id is a string.
     NodeOne = "0"