Added model for cf1s_folklore

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 23, 2024 · e46331b · e46331b
1 parent dd1d486
commit e46331b
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 7 deletions.
diff --git a/README.md b/README.md
@@ -69,13 +69,13 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Folklore Reliable Broadcast](specifications/bcastFolklore)                                         | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
 | [The Bosco Byzantine Consensus Algorithm](specifications/bosco)                                     | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
 | [Consensus in One Communication Step](specifications/c1cs)                                          | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
-| [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [One-Step Consensus with Zero-Degradation](specifications/cf1s-folklore)                            | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
+| [One-Step Consensus with Zero-Degradation](specifications/cf1s-folklore)                            | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
 | [Failure Detector](specifications/detector_chan96)                                                  | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
-| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos)                                           | Leslie Lamport, Giuliano Losa              |          |             |         |           |          |
 | [Asynchronous Non-Blocking Atomic Commit](specifications/nbacc_ray97)                               | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
 | [Asynchronous Non-Blocking Atomic Commitment with Failure Detectors](specifications/nbacg_guer01)   | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
 | [Spanning Tree Broadcast Algorithm](specifications/spanning)                                        | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
+| [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
+| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos)                                           | Leslie Lamport, Giuliano Losa              |          |             |         |           |          |
 | [Transaction Commit Models](specifications/transaction_commit)                                      | Leslie Lamport, Jim Gray                   |          |             |         |           |          |
 | [Span Tree Exercise](specifications/SpanningTree)                                                   | Leslie Lamport                             |          |             |         |           |          |
 | [The Cigarette Smokers Problem](specifications/CigaretteSmokers)                                    | Mariusz Ryndzionek                         |          |             |         |           |          |

diff --git a/manifest.json b/manifest.json
@@ -2987,7 +2987,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/cf1s-folklore/cf1s_folklore.cfg",
+              "runtime": "00:01:00",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },

diff --git a/specifications/cf1s-folklore/cf1s_folklore.cfg b/specifications/cf1s-folklore/cf1s_folklore.cfg
@@ -0,0 +1,8 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+INVARIANTS TypeOK
+PROPERTIES OneStep0_Ltl OneStep1_Ltl
+SPECIFICATION Spec
+
diff --git a/specifications/cf1s-folklore/cf1s_folklore.tla b/specifications/cf1s-folklore/cf1s_folklore.tla
@@ -150,9 +150,7 @@ OneStep0_Ltl ==
 (* If all processes propose 1, then every process crashes or decides 1. *)
 OneStep1_Ltl ==  
   (\A i \in Proc : pc[i] = "V1") => <>(\A i \in Proc : pc[i] # "U0" /\ pc[i] # "U1" /\ pc[i] # "D0")
-
-
-
+
 =============================================================================
 \* Modification History
 \* Last modified Mon Jul 09 13:26:59 CEST 2018 by tthai