TLA +视频课程

讲座可以在网上观看。但是， 慢速的网络连接可能更喜欢下载较低的分辨率 版本的视频，然后离线观看。 给出了如何做的说明 下面。 还提供了每个视频的脚本。 它包含视频中显示并说的所有内容，但镜头除外 作者的。 听觉障碍者和英语不流利的观众会发现它 在他们观看视频时阅读脚本很有帮助。 那些人也可以阅读脚本而不是观看视频 想复习讲座和讨厌视频的人。 但是，显示视频的html文件可能需要下载 材料。

TLA +简介 说明什么是TLA +，以及为什么要使用它。 它介绍了状态机的概念。 长度：21:18网页版 -- 更正 -- 离线版本： 视频文件 压缩文件 -脚本

TLA +中的状态机 显示了如何在TLA +中描述一个简单的状态机， 初步了解TLA +规范。 长度：15：40网页版 -- 离线版本： 视频文件 压缩文件 -脚本

资源和工具 描述用于学习TLA +的资源。 介绍如何下载工具箱，并说明如何 使用它来打开规格，查看漂亮的版本， 并在其上运行TLC。 该脚本在某些部分不显示正在说的内容 演示了如何使用工具箱的视频。 长度：11：13网页版 -- 更正 -- 离线版本： 视频文件 压缩文件 -脚本

死硬死硬的顽固的 我们拯救了两名好莱坞动作英雄的生命。 途中，您将开始学习写作 TLA +规范，并使用解析器和TLC进行检查。 长度：19:39网页版 -- 离线版本： 视频文件 压缩文件 -脚本

交易承诺 婚姻中的承诺 已指定数据库事务。你也是 学习 如何在规格中使用数学函数。 长度：24:39网页版 -- 更正 -- 离线版本： 视频文件 压缩文件 -脚本

两阶段提交 在婚姻和数据库中如何实现承诺 交易。您还可以了解TLA +中的记录 还有更多有关使用TLC的信息。 长度：21:22网页版 -- 更正 -- 离线版本： 视频文件 压缩文件 -脚本

Paxos提交 指定一个真正的容错算法 用于提交数据库事务。它解释了一些 用于构造和组合集合的数学运算。 长度：19:46网页版 -- 更正 -- 离线版本： 视频文件 压缩文件 -脚本

实作 分为两部分的讲座，介绍时间公式和 解释了实现一个规范意味着什么 另一个。 时长：第1部分：15：53，第2部分：12：13第1部分：初赛 网络版 -- 更正 -- 离线版本： 视频文件 压缩文件 -脚本 第2部分：工作原理 网络版 -- 离线版本： 视频文件 压缩文件 -脚本 交替比特协议 分为两部分的讲解生动活泼的讲座，介绍了什么 必须发生，并且公平。第1部分：高级规范 网络版 -- 离线版本： 视频文件 压缩文件 -脚本 长度：20:51 第2部分：协议 网络版 -- 更正 -- 离线版本： 视频文件 压缩文件 -脚本 长度：18:45 细化实施 分为两部分的讲座，解释了实现的一般含义， 其中涉及精简映射。第1部分：初步 网络版 -- 离线版本： 视频文件 压缩文件 -脚本 长度：19:53 第2部分：优化映射 网络版 -- 离线版本： 视频文件 压缩文件 -脚本 长度：21:26

离线观看任何讲座之前，请先下载 tla-video-files.zip 并将其内容提取到文件夹中。假设您命名 文件夹tla-讲座。 该文件夹应包含 文件 tlastyles.css和 tlavideo.js和文件夹 dist。 要离线观看演讲，请下载演讲视频文件并 zip文件（将具有相同的名字）放入 文件夹tla-讲座。 假设这些文件被命名为 smandtla.mp4 和smandtla.zip 将smandtla.zip的内容提取到 文件夹tla-讲座。 提取的文件之一将 被命名为smandtla.html。 （对于大多数讲座，zip文件将仅包含该文件。） 要观看视频，请在此html文件上打开Web浏览器。