よく使う表現 - TLA+メモ@ウィキ

モデルを記述する際によく使う表現を記載する。

タプル(シーケンス)に含まれる特定の値の要素の数をカウントする

VARIABLES tuple
Init == tuple = <<1, 2, 3, 2, 1, 2, 3, 2, 1>>
 
Count(t,n) == LET S == {i \in DOMAIN t : t[i] = n} IN Cardinality(S)
 

この定義では、シーケンスtの各要素について、その要素がnと等しい場合にインデックスiを集合Sに追加する。
その後、Cardinality(S)を使用して集合Sの要素数（つまり、値nの出現数）を求める。
この定義を使用して、例えばCount(tuple,2)とすることで、シーケンスtuple内の2の出現数を得ることができる。

タプルを集合に変換する

VARIABLES tuple
Init == tuple = <<1, 2, 3, 2, 1, 2, 3, 2, 1>>
TupleToSet(t) == { t[i] : i \in DOMAIN t }
 

この定義では、タプルtの各要素t[i]を集合の要素として取り出している。
例えばTupleToSet(tuple)とすることで、タプルtupleを集合に変換することができる。
この場合、結果は{1, 2, 3}となる。同じ値がタプルに複数回含まれていても、集合には一度しか現れない。
これは集合が重複を許さないデータ構造であるため。

集合をタプルに変換する

VARIABLES S
Init == S = {1, 2, 3, 4, 5}
SetToTuple(set) == LET sorted == CHOOSE seq \in [1..Cardinality(set) -> set] : 
                   \A i \in 1..(Cardinality(set)-1) : seq[i] <= seq[i+1]
                   IN [i \in 1..Cardinality(set) |-> sorted[i]]
 
 

この例では、集合の要素が自然数であり、昇順に並べられると仮定している。
まずCHOOSEを使用して、集合setの要素を昇順に並べたシーケンスseqを選択し、
その後、このシーケンスを基にタプルを作成する。

この定義を使用して、例えばSetToTuple(S)とすることで、集合Sをタプルに変換することができる。
この方法は集合の要素が順序付け可能であることを前提として、また、CHOOSEは非決定的な選択を行うため、
同じ集合を複数回タプルに変換すると異なる結果が得られる可能性がある。
これはTLA+の非決定性の性質によるもので、モデル検査の際にはすべての可能な選択が考慮される。