Properties that cause spurious counterexamples here to illustrate the limitations of the MonotonicReduction view.

```tla
Starting... (2024-10-31 11:22:03)
Implied-temporal checking--satisfiability problem has 7 branches.
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-31 11:22:03.
Progress(3) at 2024-10-31 11:22:05: 26,895 states generated, 127 distinct states found, 0 states left on queue.
Checking 7 branches of temporal properties for the complete state space with 889 total distinct states at (2024-10-31 11:22:05)
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>)

State 2: <Extend(n3) line 45, col 5 to line 47, col 49 of module abs>
cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<3, 4>>)

State 3: <Copy(n2) line 36, col 9 to line 38, col 92 of module abs>
cLogs = (n1 :> <<>> @@ n2 :> <<3, 4>> @@ n3 :> <<3, 4>>)

State 4: <Copy(n1) line 36, col 9 to line 38, col 92 of module abs>
cLogs = (n1 :> <<3, 4>> @@ n2 :> <<3, 4>> @@ n3 :> <<3, 4>>)

Back to state 2: <Extend(n3) line 45, col 5 to line 47, col 49 of module abs>

Finished checking temporal properties in 00s at 2024-10-31 11:22:05
26895 states generated, 127 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.
Finished in 02s at (2024-10-31 11:22:05)
```

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

tla/consensus/MCabs.cfg

@@ -27,6 +27,10 @@ PROPERTIES
     \* EquivExtendProp
     \* EquivCopyMaxAndExtendProp
 
+    \* Properties that cause spurious counterexamples here to
+    \* illustrate the limitations of the MonotonicReduction view.
+    \* SpuriousPropA
+
 VIEW 
     MonotonicReduction
 

tla/consensus/MCabs.tla

@@ -2,6 +2,15 @@
 
 EXTENDS abs, TLC, SequencesExt, FiniteSetsExt, Integers
 
+\* All (temporal) formulas below are expected to hold but cause a
+\* spurious violation of liveness properties due to our MonothonicReduction
+\* view.
+
+SpuriousPropA ==
+    \* Stenghtened variant of EmptyLeadsToNonEmpty.
+    \A i \in Servers:
+        cLogs[i] = <<>> ~> [](cLogs[i] # <<>>)
+
 Symmetry ==
       Permutations(Servers)