TLA +项目的想法

Question

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

Answer 1

通常与TLA +的玩具项目是:

• 模拟电梯控制器:电梯有n个门,你必须模拟行为和安全条件,例如,一旦在顶部,电梯将不再向上移动,或者我们不应该打开两个门同时,当机舱不在它前面时没有门打开,还有更多.
• 模型交通灯控制器:为简单的例子,一个简单的交叉,有许多约束,如面对的灯是同步的,如果一个轴有绿色,其他有红色.您可以优化添加流量状况和时间检测的事物.
• 模拟洗衣机:特别是门锁,简单的程序.证明没有办法锁门,就是总有一个解决方案可以让你的衣服在有限的时间内自由(即使是潮湿的)(你必须考虑一个消水步骤),而不需要过多的水你的地板.

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