Lamport TLA+ Course Lecture 5: Transaction Commit (HD)
Рет қаралды 11,596
Күн бұрынIMPORTANT NOTE!: This is a mirror of Lamport's TLA+ lecture videos with some chapter markers in the video description from Lamport's site for ease of viewing on mobile devices, or other platforms and connection setups where KZfaq is the most optimal "format". For the original files, resources, errata, and more, please visit lamport.azurewebsites.net/vide... or the original page which is linked below.
Original Description: Commitment, in marriage and database transactions, is specified. You also learn how to use mathematical functions in specifications.
Original Link: lamport.azurewebsites.net/vide...
Corrections: lamport.azurewebsites.net/vide...
Contents
0:00 - Intro
00:02 - Prologue
00:53 - Weddings
04:14 - Transaction Commit
05:15 - The TLA+ Spec
18:14 - Checking the Spec
22:06 - A Parsing Note
22:58 - Comments
24:06 - Epilogue
@tlavideocourse8540 5 жыл бұрын
Corrections: lamport.azurewebsites.net/video/corrections.html#lecture5
@xiongxin8802 7 ай бұрын
Thank you for your course, you are one of the coolest professors I've ever seen.
@warwolt 2 жыл бұрын
I'm not sure this is 100% correct, but I think that the syntax [rmState EXCEPT ![r]="prepared"] uses the bang just as a shorthand for the name in position of rmState. You can also write [rmState EXCEPT !.r = "prepared"], so the bang just gets you out of having to write "rmState" twice.
@laozi6951 4 жыл бұрын
can i know where is the spec? in the links provided, i can not find it.
@XINClover 4 жыл бұрын
You can go to this page: lamport.azurewebsites.net/video/videos.html , and download: 5.Transaction Commit -> Offline version -> zip file. Also if you watch the video on lamport.azurewebsites.net/video/video5.html , when it comes to the "stop the video" part, the video will become small and the spec code will be shown.
@GhostixMusic 2 жыл бұрын
When you watch the Video via the WebVersion: lamport.azurewebsites.net/video/video5.html the specs will appear under the Video to the right time ;)
@evgeniakarunus9301 Жыл бұрын
@@GhostixMusic Gosh that was confusing, thanks
@user-ds1pu2vc8s 7 ай бұрын
@@evgeniakarunus9301 indeed
@nervous711 2 жыл бұрын
7:57 Was the lowercase rm in square bracket meant to be r that specified on the right side of rmState?
@atikzimmerman 2 жыл бұрын
I would say that r has a declaration scope inside it's square brackets, and rm (which is not formally declared though) is outside of it, so you have to have a different variable.
Turing Awardee Clips
Рет қаралды 15 М.
GOTO Conferences
Рет қаралды 4,9 М.