私はもう試した
CONSTANTS seq = <<5,6,7>>
しかし、TLCは私に構文エラーを与えます：
エラー：TLCは、1行目の構成ファイルでエラーを検出しました。=または<-を予期していましたが、検出されませんでした。
Sequencesまた、モジュールを構成ファイルに含めようとしましたが、役に立ちませんでした。
だから...シーケンスを割り当てるために私は何をしなければなりませんか？
質問する
492 次
3 に答える
2
私はこの問題に直面したことを覚えていません。私のTLCは錆びすぎて、直接答えることができません（TLA +ツールボックスを使用して再起動しました）。
ただし、以下にリンクされている投稿から、TLC構成ファイルを介してシーケンスを使用して定数をインスタンス化することはできないことがわかります。
http://bbpress.tlaplus.net/topic/creating-a-sequence-from-a-set
質問は古いものですが、答えを残すことは将来のTLAerに役立つ可能性があります。
于 2011-02-17T12:03:28.530 に答える
1
TLA+ファイルの定数に直接割り当てることはできません。ツールボックスを使用している場合は、と書いてCONSTANTS seqから、モデルに通常の割り当てとして必要なタプルを追加します。
于 2018-02-01T22:59:01.330 に答える
1
.tlaしたがって、そのために別のファイルが必要であることがわかります。ソースファイルとして「Main.tla」があるとします。あなたMyConstは価値を持ちたいです<<1,2,3>>。TLA +ツールボックスMC.tlaは、定数を配置する場所を生成します。
---- MODULE MC ----
EXTENDS Main, TLC
const_uniq12345 = <<1,2,3>>
====
でMC.cfg、行があります
CONSTANT MyConst <- const_uniq12345
動作しないことに注意してください-の代わりにMyConst = const_uniq12345を使用すると、の代わりにモデル値が含まれます=<-MyConstconst_uniq12345<<1, 2, 3>>
https://github.com/hwayne/tlacliを使用してコマンドラインからTLCを実行できるようにし（TLAツールボックスにはひどいUXがあります）、.tlaこのような追加ファイルを使用してタプル定数を提供できました。const_uniq12345もちろん、私も代わりに意味のある名前を使用しました。ただし、現在は構成で処理されないためjava -cp /path/to/tla2tools.jar ...、手動で呼び出す必要がありました（の--show-scriptオプションを使用して完全なコマンドを取得しました） 。tlaclitlacli<-
于 2020-05-02T18:36:23.443 に答える