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
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.
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
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