From 5eff00ca3c93927fda20a63c8e46322a53eacc5e Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Mon, 28 Oct 2024 11:08:14 -0700
Subject: [PATCH] The properties InSync and AllSyncing are not expected to hold
 for MachineClosedFairSpec.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 tla/consensus/MCabs.cfg | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
index 4e275454c56f..dd94f29d3008 100644
--- 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