TLA+项目的想法

Question

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

Answer 1

带有TLA+的通常玩具项目处于以下方式：

• A型电梯控制器：电梯有 n 门，您必须同时建模行为和安全条件，例如，一旦顶部处于顶部，升降机就不会再上升了，或者我们不应同时开着两扇门机舱不在它的前面，还有更多。
• 模型交通信号灯控制器：就一个简单的示例而言，一个简单的交叉口，具有许多约束，例如面向灯的同步，如果一个轴有绿色，则另一个轴具有红色。您可以完善添加交通状况和时机检测的东西。
• 模型洗衣机：尤其是门储物柜和简单的程序。证明没有办法锁定门，那总是有一个解决方案，可以在有限的时间内获得免费衣服（即使湿润）（您将不得不考虑消水步骤）你的地板。

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