TLA+構成ファイルの定数セクションの定数にシーケンスを割り当てるにはどうすればよいですか？

Question

私はもう試した

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

しかし、TLCは構文エラーを与えてくれます。

エラー：TLCは、1行目の構成ファイルにエラーを見つけました。=または< - が予想されていましたが、見つかりませんでした。

私も含めようとしました Sequences 構成ファイルのモジュール、役に立たない。

だから...シーケンスを割り当てるために何をしなければならないの？

Answer 1

私はこの問題に直面したことを覚えていません、そして私のTLCは錆びすぎて、あなたに直接の答えを与えようとすることができません（TLA+ Toolboxを使用して再起動しました）。

ただし、リンクされたBellowから、TLC構成ファイルを介してシーケンスを備えた定数をインスタントすることはできないと考えています。

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

質問は古いにもかかわらず、答えを残すことは将来のtlaersに役立つかもしれません。

Answer 2

TLA+ファイルで定数に直接割り当てることはできません。ツールボックスを使用している場合は、書き込みます CONSTANTS seq, 、次に、モデルでは、通常の割り当てとして必要なタプルを追加します。