tlaplus

Ce document donne un aperçu des outils et de la boîte à outils TLA⁺, un projet open source géré par la Fondation TLA⁺. Il détaille l'utilisation des outils, le processus de développement, les licences et les directives de contribution. Des versions préliminaires sont disponibles et des packages de dépendances Java sont publiés pour être intégrés dans d'autres projets. De plus amples informations sur TLA⁺ lui-même et son gestionnaire de preuves peuvent être trouvées sur les liens fournis.

Aperçu

Ce référentiel héberge les principaux outils d'interface de ligne de commande (CLI) TLA⁺ et l'environnement de développement intégré (IDE) Toolbox.

Son développement est géré par la Fondation TLA⁺.

Voir http://tlapl.us pour plus d'informations sur TLA⁺ lui-même.

Pour le gestionnaire de preuves TLA⁺, voir http://proofs.tlapl.us.

Les versions versionnées peuvent être trouvées sur la page Versions.

Actuellement, chaque commit sur la branche master est construit et téléchargé vers la pré-version 1.8.0 de Clarke.

Si vous souhaitez les derniers correctifs et fonctionnalités, vous pouvez utiliser cette version préliminaire.

Si vous souhaitez utiliser les outils TLA⁺ en tant que dépendance Java dans votre projet logiciel, les packages Maven sont périodiquement publiés sur oss.sonatype.org.

Utiliser

Les outils TLA⁺ nécessitent Java 11+ pour s'exécuter.

Le fichier tla2tools.jar contient plusieurs outils TLA⁺.

Ils peuvent être utilisés comme suit :

Si vous ajoutez tla2tools.jar à votre variable d'environnement CLASSPATH, vous pouvez ignorer le paramètre -cp tla2tools.jar.

L'exécution de java -jar tla2tools.jar est alias java -cp tla2tools.jar tlc2.TLC.

Développer et contribuer

Les outils TLA⁺ et l'IDE Toolbox sont tous deux écrits en Java.

Le code source de TLA⁺ Tools se trouve dans tlatools/org.lamport.tlatools.

L'IDE Toolbox est basé sur la plate-forme Eclipse et se trouve dans le répertoire Toolbox.

Pour obtenir des instructions sur la création et les tests de ceux-ci ainsi que sur la configuration d'un environnement de développement, voir DEVELOPING.md.

Nous apprécions vos contributions à ce projet open source !

TLA⁺ est utilisé dans les systèmes critiques pour la sécurité, nous avons donc mis en place un processus de contribution pour garantir le maintien de la qualité ; lisez CONTRIBUTING.md avant de commencer à travailler.

Licence et droit d'auteur

Droits d'auteur © 199 ? Société HP

Copyright © 2003 Microsoft Corporation

Droits d'auteur © 2023 Fondation Linux

Sous licence MIT.