La lógica temporal de acciones ( TLA ) es una lógica desarrollada por Leslie Lamport , que combina la lógica temporal con una lógica de acciones . Se utiliza para describir comportamientos de sistemas concurrentes y distribuidos . Es la lógica subyacente al lenguaje de especificación TLA+ .
Las afirmaciones en la lógica temporal de acciones tienen la forma , donde A es una acción y t contiene un subconjunto de las variables que aparecen en A . Una acción es una expresión que contiene variables con y sin prima, como . El significado de las variables sin prima es el valor de la variable en este estado . El significado de las variables con prima es el valor de la variable en el siguiente estado . La expresión anterior significa que el valor de x hoy , más el valor de x mañana por el valor de y hoy , es igual al valor de y mañana .
El significado de es que A es válido ahora o las variables que aparecen en t no cambian. Esto permite pasos entrecortados, en los que ninguna de las variables del programa cambia sus valores.
Existen varios lenguajes de especificación que implementan la lógica temporal de acciones. Cada lenguaje tiene características y casos de uso únicos:
TLA+ es el lenguaje de especificación predeterminado y más utilizado para TLA. Es un lenguaje matemático diseñado para describir el comportamiento de sistemas concurrentes y distribuidos. La especificación está escrita en estilo funcional.
![estilo de visualización [A]_{t}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/03d6eaf7fc064571a2d2e88332f923d25a436f1c)
----------------------------- MÓDULO RelojHora -----------------------------EXTIENDE NaturalesVARIABLES horaInit == hora = 1Siguiente == hora' = SI hora = 12 ENTONCES 1 SI NO hora + 1Especificación == Init /\ [][Siguiente]_hora==================================================== ============================PlusCal es un lenguaje de algoritmos de alto nivel que se traduce a TLA+. Permite a los usuarios escribir algoritmos en una sintaxis similar a la de un pseudocódigo, que luego se convierten automáticamente en especificaciones TLA+. Esto hace que PlusCal sea ideal para quienes prefieren pensar en términos de algoritmos en lugar de máquinas de estados.
----------------------------- MÓDULO RelojHora ----------------------EXTIENDE Naturales(*--algoritmo HourClock { hora variable = 1; { mientras (VERDADERO) { hora := (hora % 12) + 1; } }} --*)Quint es otro lenguaje de especificación que se traduce a TLA+. Quint combina la sólida base teórica de la lógica temporal de acciones (TLA) con herramientas de desarrollo y verificación de tipos de última generación. A diferencia de PlusCal, los operadores y palabras clave de Quint tienen una traducción uno a uno a TLA+.
FizzBee [1] es un lenguaje de especificación de nivel superior que utiliza una sintaxis similar a la de Python y está diseñado para brindar métodos formales a los ingenieros de software convencionales que trabajan en sistemas distribuidos. Si bien se basa en la lógica temporal de acciones, no se traduce a TLA+ ni lo utiliza en segundo plano, a diferencia de PlusCal o Quint.
Acción Init : hora = 1 Acción atómica Tick : # El cuerpo de la acción es Starlark (un dialecto de Python) hora = ( hora % 12 ) + 1