tlaplus
The Xenophanes release
Este documento proporciona una descripción general de TLA⁺ Tools and Toolbox, un proyecto de código abierto administrado por la Fundación TLA⁺. Detalla el uso de las herramientas, el proceso de desarrollo, las licencias y las pautas de contribución. Hay versiones preliminares disponibles y los paquetes de dependencia de Java se publican para su integración en otros proyectos. Puede encontrar más información sobre TLA⁺ y su administrador de pruebas en los enlaces proporcionados.
Descripción general
Este repositorio alberga las herramientas principales de la interfaz de línea de comandos (CLI) de TLA⁺ y el entorno de desarrollo integrado (IDE) de Toolbox.
Su desarrollo está gestionado por la Fundación TLA⁺.
Consulte http://tlapl.us para obtener más información sobre el propio TLA⁺.
Para conocer el administrador de pruebas TLA⁺, consulte http://proofs.tlapl.us.
Las versiones versionadas se pueden encontrar en la página Lanzamientos.
Actualmente, cada confirmación a la rama maestra se crea y se carga en la versión preliminar 1.8.0 de Clarke.
Si desea las últimas correcciones y funciones, puede utilizar esa versión preliminar.
Si desea consumir las herramientas TLA⁺ como una dependencia de Java en su proyecto de software, los paquetes Maven se publican periódicamente en oss.sonatype.org.
Usar
Las herramientas TLA⁺ requieren Java 11+ para ejecutarse.
El archivo tla2tools.jar contiene varias herramientas TLA⁺.
Se pueden utilizar de la siguiente manera:
Si agrega tla2tools.jar a su variable de entorno CLASSPATH, puede omitir el parámetro -cp tla2tools.jar.
La ejecución de java -jar tla2tools.jar tiene un alias para java -cp tla2tools.jar tlc2.TLC.
Desarrollando y contribuyendo
Tanto TLA⁺ Tools como Toolbox IDE están escritos en Java.
El código fuente de TLA⁺ Tools está en tlatools/org.lamport.tlatools.
El IDE de Toolbox se basa en la plataforma Eclipse y se encuentra en el directorio de Toolbox.
Para obtener instrucciones sobre cómo crearlos y probarlos, así como configurar un entorno de desarrollo, consulte DEVELOPING.md.
¡Agradecemos sus contribuciones a este proyecto de código abierto!
TLA⁺ se utiliza en sistemas críticos para la seguridad, por lo que contamos con un proceso de contribución para garantizar que se mantenga la calidad; lea CONTRIBUTING.md antes de comenzar a trabajar.
Licencia y derechos de autor
Copyright © 199? Corporación HP
Copyright © 2003 Microsoft Corporation
Copyright © 2023 Fundación Linux
Licenciado bajo la Licencia MIT.
