The properties InSync and AllSyncing are not expected to hold for Mac…

…hineClosedFairSpec. Signed-off-by: Markus Alexander Kuppe <[email protected]>
microsoft · Oct 28, 2024 · 5eff00c · 5eff00c
1 parent b545678
commit 5eff00c
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
@@ -15,9 +15,10 @@ INVARIANTS
     TypeOK
 
 PROPERTIES 
-    InSync
+    \* InSync and AllSyncing not expected to hold for MachineClosedFairSpec.
+    \* InSync
+    \* AllSyncing
     Syncing
-    AllSyncing
     AppendOnlyProp
     \* EquivExtendProp
     \* EquivCopyMaxAndExtendProp