Ideas for a TLA+ project

Question

Please give me some suggestions regarding a project topic in the TLA+ language. I'm taking a course on the language, it's the first year I'm learning about specification and verification and I have no clue what to choose to implement in two weeks time. Any ideas?

Answer 1

Usual toy projects with TLA+ are in the line of:

• 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.