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 YouTube is the most optimal "format". For the original files, resources, errata, and more, please visit [ Ссылка ] or the original page which is linked below.

Original Description: How commitment is achieved, in marriage and database transactions. You also learn about records in TLA+ and some more about using TLC.
Original Link: [ Ссылка ]
Corrections: [ Ссылка ]

Contents

0:00 - Intro
00:05 - Prologue
00:32 - Records
01:57 - Weddings
04:30 - The TLA+ Spec
12:14 - The Rest of the Spec
15:42 - Checking the Spec
16:50 - Model Values
19:27 - Correctness of Two-Phase Commit
20:48 - Correctness of Two-Phase Commit

свернуть