Идеи для TLA + проект

Обычные проекты игрушек с TLA+ находятся в ряду:

• Модель контроллера лифта: лифт имеет n дверей, и вам придется моделировать как поведение, так и условия безопасности, например, что, оказавшись наверху, лифт больше не будет двигаться вверх, или что у нас не должно быть двух дверей, открытых одновременно, и ни одна дверь не должна открываться, когда кабина не находится перед ней, и многое другое.
• Модель контроллера светофора: для простого примера, простой перекресток, со многими ограничениями, например, стоящие перед ним светофоры синхронизированы, и если на одной оси горит зеленый, то на другой - красный. Вы можете усовершенствовать эту вещь, добавив определение состояния трафика и времени.
• Смоделируйте стиральную машину: особенно дверной шкафчик, и простые программы. Докажите, что нет способа заблокировать дверцу, то есть всегда есть решение, как освободить одежду (даже если она мокрая) за ограниченное время (вам придется рассмотреть этап устранения воды), не набирая слишком много воды на пол.

В целом, интересные проекты игрушек для TLA+ должны сочетать в себе относительно простое поведение, а также структурные условия и условия безопасности, чтобы вы могли проверить, что определенное вами поведение не приведет к нарушению условий безопасности.