Wie kann ich assign Sequenzen Konstanten im KONSTANTEN Abschnitt einer TLA + Konfigurationsdatei?

Question

Ich habe versucht,

CONSTANTS seq = <<5,6,7>>

aber TLC gibt mir einen Syntaxfehler:

Fehler: TLC fand einen Fehler in der Konfigurationsdatei in Zeile 1. Es war erwartet = oder <-. und fand es nicht

Ich habe auch gehören das Sequences Modul in der Konfigurationsdatei, ohne Erfolg versucht.

Also ... was muss ich tun, um eine Sequenz zuweisen?

Answer 1

Ich erinnere mich nicht, jemals mit diesem Problem konfrontiert und meine TLC ist zu rostig, um zu versuchen und gibt Ihnen eine erste Hand Antwort (ich die TLA + Toolbox nur neu gestartet verwenden).

Von der Post verbunden unten aber ich Figur, dass man nicht instantiate Konstanten mit Sequenzen durch die TLC-Konfigurationsdateien.

http://bbpress.tlaplus.net/topic/ Erstellen-a-Sequenz-von-einem-Satz

Auch wenn die Frage alt ist, kann eine Antwort zu verlassen Zukunft TLAers helfen.

Answer 2

Sie können nicht direkt auf eine Konstante in der TLA + Datei zuweisen. Wenn Sie die Toolbox verwenden, Schreib CONSTANTS seq, dann im Modell fügen Sie den Tupel Sie als gewöhnliche Zuordnung mögen.