tlaplus

Dieses Dokument bietet einen Überblick über die TLA⁺ Tools and Toolbox, ein Open-Source-Projekt, das von der TLA⁺ Foundation verwaltet wird. Darin werden die Nutzung, der Entwicklungsprozess, die Lizenzierung und die Beitragsrichtlinien der Tools detailliert beschrieben. Vorabversionen sind verfügbar und Java-Abhängigkeitspakete werden zur Integration in andere Projekte veröffentlicht. Weitere Informationen zu TLA⁺ selbst und seinem Proof-Manager finden Sie unter den bereitgestellten Links.

Überblick

Dieses Repository hostet die Kerntools der TLA⁺-Befehlszeilenschnittstelle (CLI) und die integrierte Entwicklungsumgebung (IDE) Toolbox.

Seine Entwicklung wird von der TLA⁺ Foundation verwaltet.

Weitere Informationen zu TLA⁺ selbst finden Sie unter http://tlapl.us.

Informationen zum TLA⁺-Proof-Manager finden Sie unter http://proofs.tlapl.us.

Versionierte Veröffentlichungen finden Sie auf der Seite Veröffentlichungen.

Derzeit wird jeder Commit für den Master-Zweig erstellt und in die Clarke-Vorabversion 1.8.0 hochgeladen.

Wenn Sie die neuesten Fixes und Funktionen benötigen, können Sie diese Vorabversion verwenden.

Wenn Sie die TLA⁺-Tools als Java-Abhängigkeit in Ihrem Softwareprojekt nutzen möchten, werden Maven-Pakete regelmäßig auf oss.sonatype.org veröffentlicht.

Verwenden

Für die Ausführung der TLA⁺-Tools ist Java 11+ erforderlich.

Die Datei tla2tools.jar enthält mehrere TLA⁺-Tools.

Sie können wie folgt verwendet werden:

Wenn Sie tla2tools.jar zu Ihrer Umgebungsvariablen CLASSPATH hinzufügen, können Sie den Parameter -cp tla2tools.jar überspringen.

Das Ausführen von java -jar tla2tools.jar hat einen Alias ​​für java -cp tla2tools.jar tlc2.TLC.

Entwickeln und Mitwirken

Die TLA⁺ Tools und die Toolbox-IDE sind beide in Java geschrieben.

Der Quellcode der TLA⁺ Tools befindet sich in tlatools/org.lamport.tlatools.

Die Toolbox-IDE basiert auf der Eclipse-Plattform und befindet sich im Toolbox-Verzeichnis.

Anweisungen zum Erstellen und Testen dieser sowie zum Einrichten einer Entwicklungsumgebung finden Sie unter DEVELOPING.md.

Wir freuen uns über Ihre Beiträge zu diesem Open-Source-Projekt!

TLA⁺ wird in sicherheitskritischen Systemen verwendet, daher verfügen wir über einen Beitragsprozess, um die Aufrechterhaltung der Qualität sicherzustellen; Lesen Sie CONTRIBUTING.md, bevor Sie mit der Arbeit beginnen.

Lizenz & Urheberrecht

Urheberrecht © 199? HP Corporation

Copyright © 2003 Microsoft Corporation

Copyright © 2023 Linux Foundation

Lizenziert unter der MIT-Lizenz.