Skip to content

Commit 3ea60a6

Browse files
lemmyclaude
lemmy
and
claude
committed
List the new _proof.tla files in per-spec manifest.json and README.md
The `_proof.tla` files themselves were already added in the preceding commit; this commit changes nothing about TLA+ or TLAPS and contains no logic of its own. It registers the new proof modules in each spec's `manifest.json` and adds the corresponding TLAPS Proof flag (✔) to the spec table in `README.md`, keeping the two in sync (as enforced by `.github/scripts/check_markdown_table.py`). Affected per-spec manifests: - CigaretteSmokers - CoffeeCan - DieHard - KeyValueStore - MissionariesAndCannibals - MultiCarElevator - PaxosHowToWinATuringAward - ReadersWriters - SpanningTree - SpecifyingSystems - TeachingConcurrency - TwoPhase - allocator - byihive - ewd687a - ewd998 - glowingRaccoon - spanning - transaction_commit Each new module entry carries a `proof` runtime of `unknown` and an empty `models` list. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent 0ff8795 commit 3ea60a6

20 files changed

Lines changed: 319 additions & 15 deletions

File tree

‎README.md‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -35,15 +35,15 @@ Here is a list of specs included in this repository which are validated by the C
3535
| [The N-Queens Puzzle](specifications/N-Queens) | Stephan Merz | ✔ | | ✔ | ✔ | |
3636
| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill | ✔ | | ✔ | ✔ | ✔ |
3737
| [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | |
38-
| [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | ✔ |
38+
| [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | ✔ | | ✔ | ✔ |
3939
| [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | |
4040
| [The Prisoners & Switch Puzzle](specifications/Prisoners_Single_Switch) | Florian Schanda | ✔ | | | ✔ | |
41-
| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | ✔ |
41+
| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | ✔ | | ✔ | ✔ |
4242
| [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | |
43-
| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | ✔ |
43+
| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | ✔ | | ✔ | ✔ |
4444
| [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | |
45-
| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | ✔ |
46-
| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | | (✔) | ✔ | |
45+
| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | ✔ | | ✔ | ✔ |
46+
| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | ✔ | (✔) | ✔ | |
4747
| [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle) | Florian Schanda | ✔ | | | ✔ | ✔ |
4848
| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | |
4949
| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | ✔ |
@@ -61,18 +61,18 @@ Here is a list of specs included in this repository which are validated by the C
6161
| [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | |
6262
| [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | |
6363
| [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | |
64-
| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | | ✔ | ✔ | ✔ |
64+
| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | ✔ | ✔ | ✔ | ✔ |
6565
| [The Slush Protocol](specifications/SlushProtocol) | Andrew Helwer | | | ✔ | ✔ | |
6666
| [Minimal Circular Substring](specifications/LeastCircularSubstring) | Andrew Helwer | | | ✔ | ✔ | |
67-
| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | |
67+
| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | ✔ | ✔ | ✔ | |
6868
| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | ✔ | ✔ |
6969
| [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR) | Guanzhou Hu | | | ✔ | ✔ | |
7070
| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain, Giuliano Losa | | | | | ✔ |
71-
| [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | |
71+
| [Resource Allocator](specifications/allocator) | Stephan Merz | | ✔ | | ✔ | |
7272
| [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | |
7373
| [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | ✔ |
7474
| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | ✔ | |
75-
| [Span Tree Exercise](specifications/SpanningTree) | Leslie Lamport | | | | ✔ | ✔ |
75+
| [Span Tree Exercise](specifications/SpanningTree) | Leslie Lamport | | ✔ | | ✔ | ✔ |
7676
| [The Knuth-Yao Method](specifications/KnuthYao) | Ron Pressler, Markus Kuppe | | | | ✔ | |
7777
| [Huang's Algorithm](specifications/Huang) | Markus Kuppe | | | | ✔ | |
7878
| [EWD 426: Token Stabilization](specifications/ewd426) | Murat Demirbas, Markus Kuppe | | | | ✔ | ✔ |
@@ -81,9 +81,9 @@ Here is a list of specs included in this repository which are validated by the C
8181
| [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | |
8282
| [Simplified Fast Paxos](specifications/SimplifiedFastPaxos) | Lim Ngian Xin Terry, Gaurav Gandhi | | | | ✔ | |
8383
| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | |
84-
| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | |
84+
| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | ✔ | | ✔ | |
8585
| [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | |
86-
| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | ✔ |
86+
| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | ✔ | | ✔ | ✔ |
8787
| [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | |
8888
| [Folklore Reliable Broadcast](specifications/bcastFolklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | ✔ |
8989
| [The Bosco Byzantine Consensus Algorithm](specifications/bosco) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | ✔ |
@@ -92,12 +92,12 @@ Here is a list of specs included in this repository which are validated by the C
9292
| [Failure Detector](specifications/detector_chan96) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | |
9393
| [Asynchronous Non-Blocking Atomic Commit](specifications/nbacc_ray97) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | |
9494
| [Asynchronous Non-Blocking Atomic Commitment with Failure Detectors](specifications/nbacg_guer01) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | ✔ |
95-
| [Spanning Tree Broadcast Algorithm](specifications/spanning) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | ✔ |
96-
| [The Cigarette Smokers Problem](specifications/CigaretteSmokers) | Mariusz Ryndzionek | | | | ✔ | ✔ |
95+
| [Spanning Tree Broadcast Algorithm](specifications/spanning) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | | ✔ | ✔ |
96+
| [The Cigarette Smokers Problem](specifications/CigaretteSmokers) | Mariusz Ryndzionek | | ✔ | | ✔ | ✔ |
9797
| [Conway's Game of Life](specifications/GameOfLife) | Mariusz Ryndzionek | | | | ✔ | |
9898
| [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | ✔ | |
99-
| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | ✔ |
100-
| [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | |
99+
| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | ✔ | | ✔ | ✔ |
100+
| [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | ✔ | | ✔ | |
101101
| [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | |
102102
| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | ✔ | | ✔ | ✔ |
103103
| [B-trees](specifications/btree) | Lorin Hochstein | | | | ✔ | |

‎specifications/CigaretteSmokers/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,14 @@
3333
"stateDepth": 2
3434
}
3535
]
36+
},
37+
{
38+
"path": "specifications/CigaretteSmokers/CigaretteSmokers_proof.tla",
39+
"features": [],
40+
"models": [],
41+
"proof": {
42+
"runtime": "unknown"
43+
}
3644
}
3745
]
3846
}

‎specifications/CoffeeCan/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,14 @@
5050
"result": "success"
5151
}
5252
]
53+
},
54+
{
55+
"path": "specifications/CoffeeCan/CoffeeCan_proof.tla",
56+
"features": [],
57+
"models": [],
58+
"proof": {
59+
"runtime": "unknown"
60+
}
5361
}
5462
]
5563
}

‎specifications/DieHard/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,14 @@
7070
"workers": 1
7171
}
7272
]
73+
},
74+
{
75+
"path": "specifications/DieHard/DieHard_proof.tla",
76+
"features": [],
77+
"models": [],
78+
"proof": {
79+
"runtime": "unknown"
80+
}
7381
}
7482
]
7583
}

‎specifications/KeyValueStore/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,14 @@
6868
"path": "specifications/KeyValueStore/Util.tla",
6969
"features": [],
7070
"models": []
71+
},
72+
{
73+
"path": "specifications/KeyValueStore/KeyValueStore_proof.tla",
74+
"features": [],
75+
"models": [],
76+
"proof": {
77+
"runtime": "unknown"
78+
}
7179
}
7280
]
7381
}

‎specifications/MissionariesAndCannibals/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,14 @@
3030
"result": "safety failure"
3131
}
3232
]
33+
},
34+
{
35+
"path": "specifications/MissionariesAndCannibals/MissionariesAndCannibals_proof.tla",
36+
"features": [],
37+
"models": [],
38+
"proof": {
39+
"runtime": "unknown"
40+
}
3341
}
3442
]
3543
}

‎specifications/MultiCarElevator/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,14 @@
4848
"stateDepth": 37
4949
}
5050
]
51+
},
52+
{
53+
"path": "specifications/MultiCarElevator/Elevator_proof.tla",
54+
"features": [],
55+
"models": [],
56+
"proof": {
57+
"runtime": "unknown"
58+
}
5159
}
5260
]
5361
}

‎specifications/PaxosHowToWinATuringAward/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,14 @@
7878
"proof": {
7979
"runtime": "00:00:01"
8080
}
81+
},
82+
{
83+
"path": "specifications/PaxosHowToWinATuringAward/Voting_proof.tla",
84+
"features": [],
85+
"models": [],
86+
"proof": {
87+
"runtime": "unknown"
88+
}
8189
}
8290
]
8391
}

‎specifications/ReadersWriters/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,14 @@
3636
"path": "specifications/ReadersWriters/ReadersWriters.tla",
3737
"features": [],
3838
"models": []
39+
},
40+
{
41+
"path": "specifications/ReadersWriters/ReadersWriters_proof.tla",
42+
"features": [],
43+
"models": [],
44+
"proof": {
45+
"runtime": "unknown"
46+
}
3947
}
4048
]
4149
}

‎specifications/SpanningTree/manifest.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,14 @@
6464
"result": "unknown"
6565
}
6666
]
67+
},
68+
{
69+
"path": "specifications/SpanningTree/SpanTree_proof.tla",
70+
"features": [],
71+
"models": [],
72+
"proof": {
73+
"runtime": "unknown"
74+
}
6775
}
6876
]
6977
}

0 commit comments

Comments
 (0)