Lamport TLA+ Course Lecture 8: Paxos Commit Part 1: Preliminaries (HD)
Рет қаралды 3,511
Күн бұрын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: A two-part lecture that introduces temporal formulas and explains what it means for one specification to implement another.
Original Link: lamport.azurewebsites.net/vide...
Corrections: lamport.azurewebsites.net/vide...
Contents
0:00 - Intro
00:05 - Prologue
00:37 - Implication
03:08 - Ordinary Expressions
08:48 - Temporal Formulas
13:53 - Theorems
15:31 - Epilogue
@user-ds1pu2vc8s 7 ай бұрын
It's all fun and games until this lecture..
@ytdlgandalf 3 жыл бұрын
Okay what just happened.. I could follow along pretty nicely till this lecture.
@TheWemmick 4 жыл бұрын
7:11 should be "An action expression has a value on a step" instead of a state expression. (from the errata)
TLA+ Video Course
Рет қаралды 3,3 М.
TLA+ Video Course
Рет қаралды 805
Anton Petrov
Рет қаралды 321 М.