كيف يمكنني تعيين تسلسل إلى الثوابت في قسم الثوابت في ملف تكوين TLA+؟

Question

لقد حاولت

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

لكن TLC يعطيني خطأ في بناء الجملة:

خطأ: وجدت TLC خطأ في ملف التكوين في السطر 1. كان يتوقع = أو <- ولم يجده.

لقد حاولت أيضًا تضمين Sequences الوحدة النمطية في ملف التكوين ، ولكن دون جدوى.

إذن ... ماذا علي أن أفعل لتعيين تسلسل؟

Answer 1

لا أتذكر مواجهة هذه المشكلة من أي وقت مضى و TLC الخاص بي صدئ للغاية لمحاولة إعطائك إجابة مباشرة (لقد قمت بإعادة التشغيل باستخدام TLA+ Toolbox).

من النشر المرتبط بملابس ، ومع ذلك ، أعتقد أنه لا يمكنك إنشاء مثيل للثوابت مع تسلسل من خلال ملفات تكوين TLC.

http://bbpress.tlaplus.net/topic/creating-a-equence-from-a-set

على الرغم من أن السؤال قديم ، إلا أن ترك إجابة قد يساعد في المستقبل.

Answer 2

لا يمكنك التعيين مباشرة إلى ثابت في ملف TLA+. إذا كنت تستخدم صندوق الأدوات ، فاكتب CONSTANTS seq, ، ثم في النموذج ، أضف tuple الذي تريده كمخصصات عادية.