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