TLA+ Toolbox
IDE для macOS для работы с инструментами TLA+: редактирование спецификаций, перевод PlusCal, проверка моделей TLC, исследование трасс и доказательства.
Описание
TLA+ Toolbox — интегрированная среда разработки для работы с инструментами TLA+. Она позволяет создавать и редактировать спецификации, находить ошибки разбора в исходных модулях и выполнять перевод PlusCal; ошибки перевода отмечаются в коде.
Основные возможности:
- Просмотр отформатированных версий модулей.
- Запуск средства проверки моделей TLC и исследование трасс ошибок, включая вычисление формул на шагах трассы.
- Запуск системы доказательств TLA+.
Установите приложение командой brew install --cask tla+-toolbox. Cask устанавливает приложение TLA+ Toolbox.app в /Applications. Предоставляемая загрузка для macOS — сборка x86_64, для работы cask требуется Rosetta. Чтобы начать работу, откройте приветственный экран и справочные страницы Toolbox.
pdflatex нужен только для использования команды вывода PDF с форматированными модулями; он входит в состав установки LaTeX. Toolbox — это IDE для инструментов TLA+, а не универсальный редактор.
Источники: TLA+ Toolbox · Cask Homebrew
Новая версия Что нового в 1.7.4 5 авг. 2024 г. · Редакция OpenNavo · Перевод ИИ
- TLCИсправлен пропуск нарушений свойств при многопоточной проверке живости.