project - TLA+ 项目的想法

Question

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

Answer 1

带有 TLA+ 的常见玩具项目如下：

• 为电梯控制器建模：电梯有n 个门，您必须对行为和安全条件进行建模，例如，一旦到达顶部，电梯将不再向上移动，或者我们不应该打开两扇门同时，当机舱不在它前面时，没有门打开，等等。
• 模型红绿灯控制器：举个简单的例子，一个简单的交叉路口，有很多约束，比如对面的灯是同步的，如果一个轴是绿色的，那么另一个轴是红色的。您可以细化添加交通状况和时间检测的事物。
• 洗衣机模型：尤其是门储物柜，以及简单的程序。证明没有办法锁门，那就是总有办法让你的衣服在有限的时间内脱掉（即使是湿的）（你将不得不考虑除水步骤），而不会让太多的水沾上你的地板。

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