Added model for spanning

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

Hide file tree

Showing 5 changed files with 31 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -73,7 +73,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [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  |          |             |         |           |          |
+| [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                   |          |             |         |           |          |

diff --git a/manifest.json b/manifest.json
@@ -3941,6 +3941,22 @@
       ],
       "tags": [],
       "modules": [
+        {
+          "path": "specifications/spanning/MC_spanning.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/spanning/MC_spanning.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "safety failure"
+            }
+          ]
+        },
         {
           "path": "specifications/spanning/spanning.tla",
           "communityDependencies": [],

diff --git a/specifications/spanning/MC_spanning.cfg b/specifications/spanning/MC_spanning.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  Proc = {1, 2, 3}
+  NoPrnt =  NoPrnt
+  root = 1
+  nbrs <- Neighbors
+INVARIANTS TypeOK SntMsg
+\*PROPERTIES Termination OneParent
+SPECIFICATION Spec
+
diff --git a/specifications/spanning/MC_spanning.tla b/specifications/spanning/MC_spanning.tla
@@ -0,0 +1,4 @@
+---- MODULE MC_spanning ----
+EXTENDS spanning
+Neighbors == {<<1, 2>>, <<1, 3>>}
+============================
diff --git a/specifications/spanning/spanning.tla b/specifications/spanning/spanning.tla
@@ -45,4 +45,4 @@ SntMsg == \A i \in Proc: (i # root /\ prnt[i] = NoPrnt => \A j \in Proc: <<i ,j>
 
 =============================================================================
 \* Modification History
-\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai
+\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai