tlaplus
The Xenophanes release
Este documento fornece uma visão geral das ferramentas e caixa de ferramentas TLA⁺, um projeto de código aberto gerenciado pela Fundação TLA⁺. Ele detalha o uso das ferramentas, o processo de desenvolvimento, o licenciamento e as diretrizes de contribuição. Versões de pré-lançamento estão disponíveis e pacotes de dependências Java são publicados para integração em outros projetos. Mais informações sobre o próprio TLA⁺ e seu gerenciador de provas podem ser encontradas nos links fornecidos.
Visão geral
Este repositório hospeda as ferramentas principais da interface de linha de comando (CLI) do TLA⁺ e o ambiente de desenvolvimento integrado (IDE) do Toolbox.
O seu desenvolvimento é gerido pela Fundação TLA⁺.
Consulte http://tlapl.us para obter mais informações sobre o próprio TLA⁺.
Para o gerenciador de provas TLA⁺, consulte http://proofs.tlapl.us.
Versões versionadas podem ser encontradas na página Versões.
Atualmente, cada commit no branch master é compilado e carregado no pré-lançamento 1.8.0 Clarke.
Se quiser as correções e recursos mais recentes, você pode usar esse pré-lançamento.
Se você deseja consumir as ferramentas TLA⁺ como uma dependência Java em seu projeto de software, os pacotes Maven são publicados periodicamente em oss.sonatype.org.
Usar
As ferramentas TLA⁺ requerem Java 11+ para serem executadas.
O arquivo tla2tools.jar contém várias ferramentas TLA⁺.
Eles podem ser usados da seguinte forma:
Se você adicionar tla2tools.jar à variável de ambiente CLASSPATH, poderá ignorar o parâmetro -cp tla2tools.jar.
A execução de java -jar tla2tools.jar tem o alias de java -cp tla2tools.jar tlc2.TLC.
Desenvolvendo e Contribuindo
As ferramentas TLA⁺ e o IDE Toolbox são escritos em Java.
O código-fonte das ferramentas TLA⁺ está em tlatools/org.lamport.tlatools.
O Toolbox IDE é baseado na plataforma Eclipse e está no diretório do toolbox.
Para obter instruções sobre como construí-los e testá-los, bem como configurar um ambiente de desenvolvimento, consulte DEVELOPING.md.
Agradecemos suas contribuições para este projeto de código aberto!
O TLA⁺ é usado em sistemas críticos de segurança, por isso temos um processo de contribuição em vigor para garantir a manutenção da qualidade; leia CONTRIBUTING.md antes de começar a trabalhar.
Licença e Direitos Autorais
Direitos autorais © 199? Corporação HP
Direitos autorais © 2003 Microsoft Corporation
Direitos autorais © 2023 Linux Foundation
Licenciado sob a licença MIT.
