tlaplus

このドキュメントでは、TLA⁺ Foundation が管理するオープンソース プロジェクトである TLA⁺ ツールとツールボックスの概要を説明します。ツールの使用法、開発プロセス、ライセンス、および貢献ガイドラインについて詳しく説明します。プレリリース バージョンが利用可能であり、他のプロジェクトに統合するために Java 依存関係パッケージが公開されています。 TLA⁺ 自体とその証明マネージャーの詳細については、提供されているリンクを参照してください。

概要

このリポジトリは、コア TLA⁺ コマンド ライン インターフェイス (CLI) ツールと Toolbox 統合開発環境 (IDE) をホストします。

その開発は TLA⁺ Foundation によって管理されています。

TLA⁺ 自体の詳細については、http://tlapl.us を参照してください。

TLA⁺ 証明マネージャーについては、http://proofs.tlapl.us を参照してください。

バージョン付きリリースは、「リリース」ページで見つけることができます。

現在、master ブランチへのすべてのコミットはビルドされ、1.8.0 Clarke プレリリースにアップロードされます。

最新の修正と機能が必要な場合は、そのプレリリースを使用できます。

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⁺ Tools と Toolbox IDE は両方とも Java で書かれています。

TLA⁺ ツールのソース コードは tlatools/org.lamport.tlatools にあります。

Toolbox IDE は Eclipse プラットフォームに基づいており、toolbox ディレクトリにあります。

これらの構築とテスト、および開発環境のセットアップの手順については、DEVELOPING.md を参照してください。

このオープンソース プロジェクトへの皆様の貢献を歓迎します。

TLA⁺ は安全性が重要なシステムで使用されるため、品質を維持するための貢献プロセスが用意されています。作業を始める前に CONTRIBUTING.md をお読みください。

ライセンスと著作権

著作権 © 199? HP株式会社

著作権 © 2003 Microsoft Corporation

著作権 © 2023 Linux Foundation

MITライセンスに基づいてライセンスされています。