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