tlaplus

В этом документе представлен обзор TLA⁺ Tools and Toolbox, проекта с открытым исходным кодом, управляемого TLA⁺ Foundation. В нем подробно описано использование инструментов, процесс разработки, лицензирование и рекомендации по участию. Доступны предварительные версии, а пакеты зависимостей Java публикуются для интеграции в другие проекты. Дополнительную информацию о самом TLA⁺ и его менеджере по проверке можно найти по предоставленным ссылкам.

Обзор

В этом репозитории размещены основные инструменты интерфейса командной строки (CLI) TLA⁺ и интегрированная среда разработки (IDE) Toolbox.

Его разработкой управляет Фонд TLA⁺.

Посетите http://tlapl.us для получения дополнительной информации о самом TLA⁺.

Информацию о менеджере доказательств TLA⁺ см. на http://proofs.tlapl.us.

Версии выпусков можно найти на странице «Релизы».

В настоящее время каждый коммит в основной ветке создается и загружается в предварительную версию Clarke 1.8.0.

Если вам нужны последние исправления и функции, вы можете использовать предварительную версию.

Если вы хотите использовать инструменты TLA⁺ в качестве зависимости Java в своем программном проекте, пакеты Maven периодически публикуются на oss.sonatype.org.

Использовать

Для работы инструментов TLA⁺ требуется Java 11+.

Файл tla2tools.jar содержит несколько инструментов TLA⁺.

Их можно использовать следующим образом:

Если вы добавите tla2tools.jar в переменную среды CLASSPATH, вы можете пропустить параметр -cp tla2tools.jar.

Запуск java -jar tla2tools.jar связан с java -cp tla2tools.jar tlc2.TLC.

Разработка и вклад

Инструменты TLA⁺ и Toolbox IDE написаны на Java.

Исходный код TLA⁺ Tools находится в tlatools/org.lamport.tlatools.

IDE Toolbox основана на платформе Eclipse и находится в каталоге Toolbox.

Инструкции по их созданию и тестированию, а также по настройке среды разработки см. на сайте DEVELOPING.md.

Мы приветствуем ваш вклад в этот проект с открытым исходным кодом!

TLA⁺ используется в системах, критически важных для безопасности, поэтому у нас есть процесс участия, обеспечивающий поддержание качества; прочтите CONTRIBUTING.md перед началом работы.

Лицензия и авторские права

Авторское право © 199? Корпорация HP

© Корпорация Microsoft, 2003 г.

© Linux Foundation, 2023.

Лицензировано по лицензии MIT.