Geek Answers Handbook

Ideas for the TLA + Project

Please give me some suggestions regarding the topic of the project in TLA + . I take a course in the language, this is the first year when I learn about the specification and verification, and I do not know what to choose to implement in two weeks. Any ideas?

+6
specifications project verification tla +
source share
1 answer

Normal toy projects with TLA + are in the line:

  • Lift controller model: the elevator has n doors, and you have to simulate both behavior and security conditions, for example, if once at the top, the elevator will no longer move up, or that we should not have two open doors at the same time, and the door will not opens when the cabin is not in front of it, and many others.
  • Model luminous flux controller: for a simple example, a simple intersection with many restrictions, such as the front lights, is synchronized, and if one axis is green, the other is red. You can clarify what traffic and time detection adds.
  • Model of a washing machine: especially a door cabinet and simple programs. Prove that it is not possible to lock the door, that is, there is always a solution to free your clothes (even if it is wet) for a limited time (you will need to consider the step of removing water) without getting too much water on your floor.

In general, interesting toy designs for TLA + should combine relatively simple behaviors, as well as structural and safe conditions, so that you can verify what behavior you have determined will not invalidate the safety conditions.

+15
source share

More articles:


All Articles