Lógica temporal de ações
Lógica temporal de ações (LTA) é uma lógica desenvolvida por Leslie Lamport, que combina a Lógica temporal com a lógica de ações. É usada para descrever comportamentos de sistemas concorrentes.
Detalhes[editar | editar código-fonte]
Declarações na lógica temporal são da forma , onde A é a ação e t contem um subconjunto de variáveis ocorrendo em A. Uma ação é uma expressão contendo variáveis primas e não primas, assim como . O significado de variável não-prima é o valor da variável neste estado. O significado de variável prima é o valor da variável no próximo estado. A expressão acima significa o valor de x agora, mais o valor de x depois vezes o valor de y agora, igual ao valor de y depois.
![{\displaystyle [A]_{t}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/03d6eaf7fc064571a2d2e88332f923d25a436f1c)
O significado de é que ou A é válida agora, ou as variáveis que ocorrem em t não mudam. Isto possibilita para os passos, no qual nenhuma das variáveis de programa mudam o seus valores.
Editores[editar | editar código-fonte]
Alguns editores TLA+ incluem:
- TLA+ Toolbox (Uma IDE Eclipse para ferramentas TLA+, incluindo o tradutor PlusCal, Modelo TLC de verificação e Sistema de prova TLA+)
- Eclipse TLA+ Plugin
- VisualTLA
- TLA Editor
- TLA# Plugin para Microsoft Visual Studio 2005
Ver também[editar | editar código-fonte]
Referências
- Lamport, Leslie (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. [S.l.]: Addison-Wesley. ISBN 0-321-14306-X. Consultado em 2 de fevereiro de 2007
- Leslie Lamport (16 de dezembro de 1994), Introduction to TLA (PDF), consultado em 17 de setembro de 2010
