\( \def\ldef{≜} \) \( \def\globally{□} \) \( \def\eventually{◇} \) \( \def\openleftarrowplus{\overset{+}{⇾}} \) \( \def\equalv{⫤} \)

TLA+: リファレンス

Takami Torao #TLA+ #cheetsheet
  • このエントリーをはてなブックマークに追加
  1. データ型
    1. タプル: << >>
  2. 集合
    1. 演算子
  3. 参考文献

データ型

タプル: << >>

TLA+ のタプル (tuple) も一般的なプログラミング言語でのタプルと同じ。順序付けられた固定個数の値を持つことのできるデータ構造で、それぞれの値の位置に対して値の型と値の意味が決まっている。TLA+ では << >> で囲んで表現する。

集合

演算子

TLA+表記 意味
\in 包含 \(\in\) 1 \in {0, 1} \(\Rightarrow\) TRUE
\notin 包含否定 \(\notin\) 1 \notin {0, 1} \(\Rightarrow\) FALSE
\subseteq, \subset, \supseteq, \supset 部分集合 \(\subseteq, \subset, \supseteq, \supset\) {0, 2} \subseteq {0, 1, 2} \(\Rightarrow\) TRUE
= 等価 \(=\) {0, 1} = {1, 0} \(\Rightarrow\) TRUE
#, /= 非等価 \(\neq\) {0, 1} /= {0} \(\Rightarrow\) TRUE
\cap 商集合 \(\cap\) {0, 1} \cap {1, 2} \(\Rightarrow\) {1}
\cup, UNION 和集合 \(\cup\) {0, 1} \cup {1, 2} \(\Rightarrow\) {0, 1, 2}
\ 差集合 \(\setminus\) {0, 1} \ {1, 2} \(\Rightarrow\) {0}
SUBSET 全ての部分集合 SUBSET {0, 1} \(\Rightarrow\) {},{0},{1},{0,1}

参考文献

  1. Leslie Lamport (1997) The Operators of TLA+
F