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

TLA+: リファレンス

2021年2月4日 #TLA+ #cheetsheet

データ型

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}`