基础概念
TLA+是一种基于集合论和时序逻辑的形式化规范语言TLC是一个专门为 TLA+ 设计的模型检测器（Model Checker），通过穷举法遍历系统所有可能的状态，验证这些状态是否符合 TLA+ 写下的规范。
基础语法
- 不等号是
/=或# - 逻辑是TRUE和FALSE
- 元组(Tuples)：
<<"a",-3,"bc">>- 下标访问：
<<"a",-3,"bc">>[1]="a"
- 下标访问：
集合(Sets)
- 顺序无关：
{1,2,3}={3,2,1} - 元素操作：
2 \in {2,4,6}，还有\notin (-2)..1 = {-2,-1,0,1}- 集合操作
- 并集
{1,2} \cup {2,4}={1,2,4} - 交集
\cap - 差集
{1,2}\{2,4} = {1} - 子集
{"a", "c"} \subseteq {"a", "b", "c"} = TRUE
- 并集
- 无限集合：整数集合
Int，自然数集合（非负整数）Nat - TLC能处理的集合，当且仅当TLC可以比较集合中的两个元素是否相等
- 构建只包含数字的集合：
{1, 2, 3} - 构建只包含字符串的集合：
{"a", "b", "c"} - 如果结构复杂，确保层级类型一致：例如，一个“由元组组成的集合”，其中每个元组的第一个元素固定是字符串，第二个元素固定是数字的集合。
- 构建只包含数字的集合：
命题逻辑
- OR：
\/ - AND：
/\ - NOT：
~ - 蕴涵：
=>P=>Q等价于：要么P为假，要么Q为真。- 其意义在于定义安全性，比如
TypeOK => (x \in Nat)表示“只要我们认为类型是正确的，那么 x 就一定得是自然数”
- 等价：
<=>P<=>Q表示P和Q完全等价
谓词逻辑
\A：任一元素为真\E：存在元素为真- 判断质数
(n>1) /\ \A m \in 2..(n-1): ~ \E t \in 2..(n-1): n=t*m(n>1) /\ \A m \in 2..(n-1): \A t \in 2..(n-1): n/=m*t(n>1) /\ \A m,t \in 2..(n-1): n # m*t(n>1) /\ \A m \in 2..(n-1) : n % m # 0
- 哥德巴赫猜想（every even integer greater than 2 is the sum of two primes）
\A n \in Nat: (n > 2 /\ n % 2 = 0) => \E i,j \in Nat: IsPrime(i) /\ IsPrime(j) /\ n = i + j\A n \in {x \in Nat : x > 2 /\ x % 2 = 0} : \E i,j \in Nat: IsPrime(i) /\ IsPrime(j) /\ n = i + j
本文采用知识共享署名4.0国际许可协议(CC BY 4.0)进行许可