Added model for c1cs

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

Hide file tree

Showing 3 changed files with 23 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -68,7 +68,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz)                                     | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |     ✔     |          |
 | [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  |          |             |         |           |          |
+| [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  |          |             |         |           |          |
 | [Failure Detector](specifications/detector_chan96)                                                  | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |

diff --git a/manifest.json b/manifest.json
@@ -2934,7 +2934,18 @@
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/c1cs/c1cs.cfg",
+              "runtime": "unknown",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "unknown"
+            }
+          ]
         }
       ]
     },

diff --git a/specifications/c1cs/c1cs.cfg b/specifications/c1cs/c1cs.cfg
@@ -0,0 +1,10 @@
+CONSTANTS
+  N = 4
+  T = 1
+  F = 1
+  Values = {v1, v2}
+  Bottom = Bottom
+INVARIANTS TypeOK Validity Agreement WeakAgreement IndStrengthens
+PROPERTIES Termination
+SPECIFICATION Spec
+