¿Cómo puedo asignar a secuencias constantes en la sección de constantes de un archivo de configuración TLA +?
-
04-10-2019 - |
Pregunta
He intentado
CONSTANTS seq = <<5,6,7>>
TLC, pero me da un error de sintaxis:
Error: TLC encuentra un error en la archivo de configuración en la línea 1. Era esperando = o <-. y no lo encontró
También he intentado incluir el módulo Sequences
en el fichero de configuración, pero sin éxito.
Así que ... ¿qué tengo que hacer para asignar una secuencia?
Solución
No recuerdo alguna vez frente a este problema y mi TLC es demasiado oxidado para tratar de darle una primera respuesta parte (acabo de reiniciar los servicios con la caja de herramientas TLA +).
Desde el puesto ligada abajo, sin embargo, me figura que pueda constantes no crear una instancia con secuencias a través de los archivos de configuración de TLC.
http://bbpress.tlaplus.net/topic/ crear-a-secuencia-de-a-conjunto
A pesar de que la cuestión es de edad, dejando una respuesta puede ayudar a TLAers futuras.
Otros consejos
No se puede asignar directamente a una constante en el archivo TLA +. Si está utilizando la caja de herramientas, CONSTANTS seq
escritura, a continuación, en el modelo de añadir la tupla que desea como una ordinaria.