Fixed ChangRoberts model

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 19, 2024 · 64cb2d2 · 64cb2d2
1 parent 06b7550
commit 64cb2d2
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 3 deletions.
diff --git a/README.md b/README.md
@@ -49,7 +49,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [The Slush Protocol](specifications/SlushProtocol)                                                  | Andrew Helwer                              |          |             |    ✔    |     ✔     |          |
 | [Minimal Circular Substring](specifications/LeastCircularSubstring)                                 | Andrew Helwer                              |          |             |    ✔    |     ✔     |          |
 | [Snapshot Key-Value Store](specifications/KeyValueStore)                                            | Andrew Helwer, Murat Demirbas              |          |             |    ✔    |     ✔     |          |
-| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts)               | Stephan Merz                               |          |             |    ✔    |           |          |
+| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts)               | Stephan Merz                               |          |             |    ✔    |     ✔     |          |
 | [Resource Allocator](specifications/allocator)                                                      | Stephan Merz                               |          |             |         |     ✔     |          |
 | [Transitive Closure](specifications/TransitiveClosure)                                              | Stephan Merz                               |          |             |         |     ✔     |          |
 | [Sliding Block Puzzle](specifications/SlidingPuzzles)                                               | Mariusz Ryndzionek                         |          |             |         |     ✔     |          |

diff --git a/manifest.json b/manifest.json
@@ -3093,9 +3093,10 @@
               "size": "small",
               "mode": "exhaustive search",
               "features": [
+                "ignore deadlock",
                 "liveness"
               ],
-              "result": "deadlock failure"
+              "result": "success"
             }
           ]
         }

diff --git a/specifications/chang_roberts/MCChangRoberts.cfg b/specifications/chang_roberts/MCChangRoberts.cfg
@@ -1,5 +1,6 @@
 CONSTANT N = 3
 INVARIANTS TypeOK Correctness
-PROPERTIES Termination Liveness
+PROPERTY Liveness
 SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
 
diff --git a/specifications/chang_roberts/MCChangRoberts.tla b/specifications/chang_roberts/MCChangRoberts.tla
@@ -6,3 +6,4 @@ ASSUME N \in Nat
 Id == [i \in 1 .. N |-> i]
 INSTANCE ChangRoberts
 =============================================================================
+
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,3 +6,4 @@ ASSUME N \in Nat
		Id == [i \in 1 .. N \|-> i]
		INSTANCE ChangRoberts
		=============================================================================