Added model for detector_chan96

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

Hide file tree

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

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

diff --git a/specifications/detector_chan96/EnvironmentController.cfg b/specifications/detector_chan96/EnvironmentController.cfg
@@ -0,0 +1,12 @@
+CONSTANTS
+  N = 3
+  T = 1
+  d0 = 2
+  SendPoint = 2
+  PredictPoint = 3
+  DELTA = 1
+  PHI = 1
+INVARIANT TypeOK
+PROPERTIES StrongCompleteness EventuallyStrongAccuracy
+SPECIFICATION Spec
+
diff --git a/specifications/detector_chan96/EnvironmentController.tla b/specifications/detector_chan96/EnvironmentController.tla
@@ -1,6 +1,6 @@
 ----------------------- MODULE EnvironmentController -----------------------
 
-(* An encoding of a parameterized and partially syncrhonous model of the eventually  
+(* An encoding of a parameterized and partially synchronous model of the eventually  
    perfect failure detectors with crash faults from:
   
    [1] Chandra, Tushar Deepak, and Sam Toueg. "Unreliable failure detectors for 
@@ -87,7 +87,7 @@
         TLC spends more than 2 hours (from 11:17 to 13:26) verifying these properties.
       
    o PROBLEMS with TLC: I believe that PHIConstraint and PHIConstraint1 are equivalent. 
-     However, whenever I check this specification with PHIConstraing1, TLC shows an 
+     However, whenever I check this specification with PHIConstraint1, TLC shows an 
      error: "Too many possible next states for the last state in the trace." I guess 
      that the reasons are from optimizations for disjunctions. *)