From 976b6d268e454ce092720e0d03d5597acbb79763 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Wed, 30 Oct 2024 10:06:42 -0700
Subject: [PATCH] Add  (temporal) formulas that are expected to result in
 counterexamples as sanity checks.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 tla/consensus/MCabs.cfg |  9 +++++++++
 tla/consensus/MCabs.tla | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+)

diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
index 642cabc109dc..ee9a7c1697df 100644
--- a/tla/consensus/MCabs.cfg
+++ b/tla/consensus/MCabs.cfg
@@ -31,6 +31,15 @@ PROPERTIES
     \* illustrate the limitations of the MonotonicReduction view.
     \* SpuriousPropA
 
+    \* NotAPropA
+    \* NotAPropB
+    \* NotAPropC
+    \* NotAPropD
+    \* NotAPropE
+    \* NotAPropF
+    \* NotAPropG
+    \* NotAPropH
+
 VIEW 
     MonotonicReduction
 
diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
index 43f60e1572d1..371e0c0e7704 100644
--- a/tla/consensus/MCabs.tla
+++ b/tla/consensus/MCabs.tla
@@ -11,6 +11,47 @@ SpuriousPropA ==
     \A i \in Servers:
         cLogs[i] = <<>> ~> [](cLogs[i] # <<>>)
 
+----
+
+\* All (temporal) formulas below are expected to result in liveness violations,
+\* as there is nothing in the behavior spec that forces all Terms to be present
+\* in any/all logs.
+
+NotAPropA ==
+    <>(\A i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropB ==
+    <>[](\A i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropC ==
+    <>(\E i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropD ==
+    <>[](\E i \in Servers: Terms = Range(cLogs[i]) )
+
+NotAPropE ==
+    \E i \in Servers:
+        cLogs[i] = <<>> ~> Terms = Range(cLogs[i])
+
+NotAPropF ==
+    \A i \in Servers:
+        \A n \in 1..10: \* 10 is arbitrary but TLC doesn't handle Nat.  LeadsTo is vacausously true if n > Len(cLogs[i]).
+            Len(cLogs[i]) = n ~> cLogs[i] = <<>>
+
+NotAPropG ==
+    \A i \in Servers:
+        \A n \in 1..10:
+            Len(cLogs[i]) = n ~> Len(cLogs[i]) = n - 1
+
+NotAPropH ==
+    \* We would expect NotAPropH to hold if we conjoin  Len(cLogs'[i]) = Len(cLogs[i]) + 1  to abs!Next.
+    \* Instead, we get a spurious violation of liveness properties, similar to SpuriousPropA.
+    \A i \in Servers:
+        \A n \in 0..1:
+            Len(cLogs[i]) = n ~> Len(cLogs[i]) = n + 1
+
+----
+
 Symmetry ==
       Permutations(Servers)