Lamport TLA+ Course Lecture 2: State Machines in TLA+ (HD)
Рет қаралды 18,392
Күн бұрын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: Shows how a simple state machine is described in TLA+, giving the first glimpse of a TLA+ specification.
Original Link: lamport.azurewebsites.net/vide...
Contents
0:00 - Intro
00:04 - Prologue
00:26 - What Language Should We Use?
02:32 - Describing a State Machine with Math
08:50 - A Nicer Way to Write the Next-State Formula
12:41 - The Complete TLA+ Spec
13:59 - Decomposing Large Specs
15:08 - Epilogue
@ttong5214 5 жыл бұрын
It's my great honor to get access to these valuable lectures.
@VidhathShetty Жыл бұрын
I'm amazed as to how even experienced cs people have ignored this in their workflow. Even with my self ( a beginner). This cuts down so much of the learning curve thank you Mr.Lamport for your contribution 🙏🙏
@bwandesky Жыл бұрын
Learning TLA+ opened my mind to a different way of thinking.
@1JWL 4 жыл бұрын
After reading Merz's paper on TLA+ Logic, it's only by watching this that I now make sense of the use of definitions in writing specs. Thanks professor!
@ytdlgandalf 3 жыл бұрын
this pace is so awesome. Why wasn't my University experience like this.
@sidekick3rida Жыл бұрын
1:19 the language was SPIN. Here's the quote… "While we had an initial bias toward using SPIN [7], in the end it was decided to use TLA/TLC from Leslie Lamport. [2] Although the mathematical notation of the TLA language was first considered a hindrance versus the C-like Promela language of SPIN. In the end this has proven to be a major benefit as it forced to reason in a much more abstract way about the RTOS."
@EvgeniyDolzhenko 5 ай бұрын
haha, thank you :)
@driziiD 4 жыл бұрын
this course is VERY well made. thank you so much!
@dbzerchik 5 жыл бұрын
Thank you very much for the lecture, very interesting!
@camilo_chacon_s 4 жыл бұрын
Perfect!
@verfran 2 жыл бұрын
You got me thinking.....
@charlessmyth 2 жыл бұрын
That was good :-)
@fernandoquinonez5040 Жыл бұрын
Nice
@Vatsal-rq2sw 25 күн бұрын
why if condition is expressed as and operator and not by implies operator ?
@rafaelnunes000 6 жыл бұрын
Hi from Brazil :D
@rigille 4 жыл бұрын
another hi from brazil ^^
@VRchitecture Жыл бұрын
Hi from not Brazil :P
@Cooososoo Ай бұрын
Hi from India
@leilu5301 2 жыл бұрын
If '=' means equality in Next, then when will i' and pc' be updated?
@handsanitizer2457 2 жыл бұрын
Gangsta gangsta
@fernandoquinonez5040 Жыл бұрын
Cost me few minutes to understand why use 'and'
Turing Awardee Clips
Рет қаралды 15 М.
ZME Science
Рет қаралды 72 М.
A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness | Jeff Weiss | Code BEAM V
Code Sync
Рет қаралды 7 М.
Mathemaniac
Рет қаралды 612 М.