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

Question

Пожалуйста, дайте мне несколько предложений относительно темы проекта в TLA + язык. Я беру курс на языке, это первый год, когда я узнаю о спецификации и проверке, и я понятия не имею, что выбрать для реализации в течение двух недель. Есть идеи?

Answer 1

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

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

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