Lamport TLA+ Course Lecture 4: Die Hard (HD)

Рет қаралды 11,614

Күн бұрын

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: We save the lives of two Hollywood action heroes. On the way, you will start learning to write TLA+ specs and checking them with the parser and with TLC.
Original Link: lamport.azurewebsites.net/vide...
Corrections: lamport.azurewebsites.net/vide...
Contents
0:00 - Intro
00:02 - Prologue
00:25 - The Die Hard Problem
01:07 - Getting Started
04:04 - The Spec
05:19 - The Next-State Formula
08:22 - Pouring Between Jugs
09:33 - Saving Our Heroes
14:24 - SmallToBig and BigToSmall
16:34 - Checking Your Definitions
19:12 - Epilogue

Пікірлер: 14

@ytdlgandalf 3 жыл бұрын

Feels like I'm back in Uni. Love this.

@leiliu83 4 жыл бұрын

WOW, this is soooo nice, thanks Shifu.

@kyuantym Жыл бұрын

MR Lamport is an inspiration

@Infernal_Puppet 5 жыл бұрын

Amazing

2 жыл бұрын

Thank you for this video. I'm curious about the different solutions when the invariant big /= 4 is chosen. You showed big = 4 and small = 3 in the end. In another run I found (sadly only) one error with big = 4 and small = 0 in the end. It is always just one error found. Does it stop at the first invariant found? How can we find any errors leading to this big /= 4 at the end?

@TheWemmick 4 жыл бұрын

It looks like the spec permits a number of trivial steps that don't do anything when a jug is full or empty. Is that a problem? I think if we want to insist Next only performs steps that change the state like a person would, we could add an extra condition that (small' /= small \/ big' /= big).

@ghucc 5 жыл бұрын

Hello, I think that at 18:17 the definition of BigToSmall is false. I think we should have the line: ELSE /\ big' = big - (3 - small) Does someone else agree ?

@karanrawat3851 5 жыл бұрын

It is the same thing. big' = small + big - 3. It is just that the expression in video does not seem to be the natural way to think about it.

@karanrawat3851 5 жыл бұрын

I believe, the definition of "invariant" given at 11:54 is actually the definition of "safety property". References: Wan_Fokkin (Distributed Algorithms), Gerard_Tel (Distributed Systems)

@vapourmile 3 жыл бұрын

It says the model checker models every legal behaviour? That's great for the example systems with an easily represented complete state system but what if I'm modelling something like 32 bit addition where there is a total of 2^64 states, each state including two 32 bit integers and a 64bit integer solution, meaning you'd need 32*2^64 bytes to represent every state or 2^64 operations to iterate every state? Sounds to me you don't need a complicated system to hit Turing's halting problem.

@kardeskalap2165 3 жыл бұрын

This is a good question. As an engineer you need to choose your abstraction level wisely exactly because of this problem. Do you really need to model 32 bit addition? Is it really the best way to model it that way?

@MrArihar 2 жыл бұрын

@@kardeskalap2165 I think this problem can be designed as bit wise addition module and tested on small size of n for 2^n. Can you suggest any other better method?