Model a lift controller: the lift has n doors, and you will have to model both the behavior and safety conditions, for example that once at the top, the lift will no more move up, or that we should not have two doors opened at the same time, and no door opened when the cabin is not in front of it, and many more.
Model traffic light controller: for the easy example, a simple crossing, with many constraints, such as facing lights are synchronized, and if one axis has green, tho other has red. You can refine the thing adding detection of traffic condition, and timing.
Model a Washing machine: especially the door locker, and simple programs. Prove that there is no way to lock the door, that is there is always a solution to get your clothes free (even if wet) in a limited time (you will have to consider a water elimination step), without getting too much water on your floor.
In general, interesting toy projects for TLA+ should combine a relatively simple behavior, and structural and safety conditions, so that you will be able to verify the behavior you defined will not invalidate the safety conditions.
发布评论
评论（1）
使用 TLA+ 的常见玩具项目如下：
一般来说，有趣的 TLA+ 玩具项目应该结合相对简单的行为以及结构和安全条件，以便您能够验证您定义的行为不会使安全条件失效。
Usual toy projects with TLA+ are in the line of:
In general, interesting toy projects for TLA+ should combine a relatively simple behavior, and structural and safety conditions, so that you will be able to verify the behavior you defined will not invalidate the safety conditions.