Add a leads-to property LogsLeadToSubset to the properties we check u…

…nder the MonotonicReduction view. Signed-off-by: Markus Alexander Kuppe <[email protected]>
microsoft · Oct 30, 2024 · 6abbb50 · 6abbb50
1 parent a8cd795
commit 6abbb50
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
@@ -22,6 +22,7 @@ PROPERTIES
     SynchingLockStep
     AllExtending
     \* AllExtendingLockStep
+    LogsLeadToSubset
     AppendOnlyProp
     \* EquivExtendProp
     \* EquivCopyMaxAndExtendProp

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
@@ -140,6 +140,10 @@ AllExtendingLockStep ==
 
 LEMMA AllExtendingLockStep => AllExtending
 
+LogsLeadToSubset ==
+    \A i \in Servers:
+        cLogs[i] = <<>> ~> [](Range(cLogs[i]) \in SUBSET Terms)
+
 FairSpecLockStep ==
     /\ Spec
     \* There repeatedly exists a state where the logs of all servers are synced.
@@ -155,13 +159,13 @@ WeakFairnessSpec ==
     /\ WF_cLogs(Next)
 
 THEOREM FairSpecLockStep => 
-    (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ InSyncLockStep)
+    (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ InSyncLockStep /\ LogsLeadToSubset)
 
 THEOREM FairSpec =>
-    (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync)
+    (Syncing /\ SynchingLockStep /\ AllExtending /\ InSync /\ LogsLeadToSubset)
 
 THEOREM WeakFairnessSpec => 
-    (Syncing /\ SynchingLockStep /\ AllExtending)
+    (Syncing /\ SynchingLockStep /\ AllExtending /\ LogsLeadToSubset)
 
 ----