1. 为什么前端也需要这个
先看三个你一定写过的东西。
- 提交按钮：点了以后变成“加载中”，成功后变“完成”，失败后可以再点。问题：会不会卡在“加载中”出不来？
- 请求重试：失败就自动重试。问题：会不会永远在“失败、重试、失败”里转圈，一直成功不了？
- 两个标签页同时登录：每个页面先看 localStorage 里有没有会话，没有就建一个。问题：两个页面会不会都觉得“没有”，然后各建一个？
这些 bug 的共同点：单看每一步都对，坏的是“步骤的某种先后顺序”。手动测试一般只走到你想到的那几种顺序。并发越多，顺序越多，人脑数不过来。
TLA+ 是一种写“系统怎么一步步变化”的语言。你写的这份描述叫“规格”（spec），它不是要上线的代码，只是系统行为的一个小模型。TLC 是配套的程序，叫“模型检查器”：它把规格允许的每一种步骤顺序都走一遍，找出违反你规则的那条路，并把这条路一步步打印出来。
本课进度：