project - TLA+ 项目的想法

Question

请给我一些关于 TLA+ 中的项目主题的建议语。我正在学习语言类(class)，这是我学习规范和验证的第一年，我不知道在两周内选择实现什么。有任何想法吗？

Answer 1

使用 TLA+ 的常见玩具项目如下:

为电梯 Controller 建模:电梯有 n 个门，您必须对行为和安全条件进行建模，例如，一旦到达顶部，电梯将不再向上移动，或者我们不应该在此时打开两扇门同时，当机舱不在它面前时，没有门打开，等等。

模型交通灯 Controller :举个简单的例子，一个简单的十字路口，有很多约束，比如面对灯是同步的，如果一个轴是绿色，另一个轴是红色。您可以细化添加交通状况和时间检测的事物。

洗衣机模型:尤其是门锁和简单的程序。证明没有办法锁门，总有办法在有限的时间内让你的衣服脱掉(即使是湿的)(你将不得不考虑一个脱水步骤)，而不会弄到太多水你的地板。

一般来说，有趣的 TLA+ 玩具项目应该结合相对简单的行为、结构和安全条件，以便您能够验证您定义的行为不会使安全条件无效。