project - TLA +项目的构想

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

最佳答案

带有TLA +的常规玩具项目包括:

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

模型交通信号灯 Controller :举个简单的例子，一个简单的交叉路口有很多限制，例如对面灯进行同步，并且如果一个轴具有绿色，则另一个轴具有红色。您可以添加交通状况检测和计时来优化事物。

为洗衣机建模:尤其是门锁和简单的程序。证明没有办法锁门，那就总有一种解决方案，可以在有限的时间内(即使要弄湿)也要脱衣服(即使弄湿了)，而又不会积水过多。你的地板。

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