TLA+ 并不是一門很容易掌握的語言，在學(xué)習(xí)之前，我們需要了解一些簡單的數(shù)學(xué)知識。這里需要注意，為了打字方便，很多數(shù)學(xué)符號我直接使用了 ASCII 來表示，具體符號與 ASCII 的對應(yīng)，大家可以參考 TLA+ cheat-sheet

算數(shù)

最基本的整數(shù)算數(shù)運算包含在 TLA+ 的 Integers module 里面，主要就是常用的 +，-，*，^ ，% 這些，還包括 >，<，>=，<= 等。

Integers module 同時定義了：

• Int：所有整數(shù)
• Nat：所有自然數(shù)
• ..：m..n 表示了從 m 到 n 之間的所有整數(shù)集合

對于 /，則是在 Real module 里面定義了。Real module 也同時定義了 Real 用來表示所有的實數(shù)。

邏輯

在 TLA+ 里面，TRUE 表示真，而 FALSE 則是假。譬如 1 + 1 = 2 的值是 TRUE，而 1 + 1 = 3 的值是 FALSE。

命題邏輯

跟整數(shù)有加減乘除運算符一樣，布爾也有相關(guān)的命題邏輯運算符，我們需要知道如下 5 個：

• /\：and，當(dāng)且只有 F 和 G 都等于 TRUE，F /\ G 等于 TRUE
• \/：or，當(dāng)且只有 F 或者 G 一個等于 TRUE（或者都為 TRUE），F \/ G 等于 TRUE
• ~：negation，當(dāng)且只有 F 等于 FALSE，~F 等于 TRUE
• =>：implication，當(dāng)且只有 F 等于 FALSE 或者 G 等于 TRUE（或者 F 和 G 都為 TRUE 或者 FALSE），F => G 等于 TRUE
• <=>：equivalence，當(dāng)且只有 F 和 G 都為 TRUE 或者都為 FALSE，F <=> G 等于 TRUE

這里我們可能對 => 的定義感到困惑，為什么只有 F 為 TRUE 并且 G 為 FALSE 的時候 F => G 才為 FALSE，我們可以通過 (n > 5) => (n > 3) 來說明，對于整數(shù) n 來說，如果 n 為 6，n > 5 就是 TRUE，自然 n > 3 也是 TRUE，也就是 (n > 5) 蘊(yùn)含著 (n > 3)，我們可以將 n 設(shè)置為 1，4 這些值在自行推導(dǎo)。

謂語邏輯

在命題邏輯基礎(chǔ)上，謂語邏輯擴(kuò)展了兩個運算符，我們叫做量詞。一個是全稱量詞 \A，另一個則是存在量詞 \E。對于公式 \A x \in S: P(x) 來說，在集合 S 里面所有的 x，P(x) 都必須等于 TRUE，那么該公式值才是 TRUE。而對于 \E x \in S: P(x) 來說，只要 S 里面一個 x 存在 P(x) 等于 TRUE，那么該公式的值就是 TRUE。

CHOOSE

CHOOSE 操作符類似于上面說的 \E。對于公式 \E x \in S : P(x) 來說，如果在集合 S 里面存在一個值 x，滿足 P(x) 為 TRUE，那么 CHOOSE x \in S : P(x) 就等于這個值。

當(dāng)使用 CHOOSE 在集合里面選擇了一個值之后，每次執(zhí)行都會使用這個值，譬如對于 v' = CHOOSE n \in 1..10 : TRUE 來說，我們并不知道 CHOOSE 選擇了哪一個值，沒準(zhǔn)是 1，也沒準(zhǔn)是 10，但我們能夠確定，每次執(zhí)行都會是這個值。如果我們需要每次使用不同的值，可以通過 \E n \in 1..10 : v' = n 來設(shè)置。

集合

集合應(yīng)該是 TLA+ 的理論基石，一個集合可能含有有限或者無限個數(shù)的元素。譬如所有自然數(shù)集合就是是一個無窮集合。集合主要有以下操作：

• \intersect 或者 \cap：兩個集合的交集，譬如 {1, 2} \intersect {2, 3} = {2}
• \union 或者 \cup：兩個集合的并集，譬如 {1, 2} \union {2, 3} = {1, 2, 3}
• \subseteq：一個集合是否是另一個集合的子集，譬如 {1, 3} \subseteq {1, 2, 3} 等于 TRUE
• \：兩個集合的差集，譬如 {1, 2, 3} \ {1, 4} = {2, 3}
• SUBSET：集合的子集，譬如 {1, 2} 的子集就是 {{}, {1}, {2}, {1, 2}}
• UNION：集合的并集，譬如 {{1, 2}, {2, 3}, {3, 4}} 的并集就是 {1, 2, 3, 4}
• Cardinality(S)：有限集合 S 中元素的個數(shù)
• IsFiniteSet(S)：驗證集合 S 是否是有限的還是無限的

這里我們在重點關(guān)注兩個集合的構(gòu)造操作符：

• {x \in S : P(x)}：集合由在 S 中滿足 P(x) 為 TRUE 的元素構(gòu)造，譬如 {n \in Nat : n % 2 = 1} 就返回了一個偶數(shù)集合
• {e(x) : x \in S}：集合由在 S 中元素通過 e(x) 得到新值構(gòu)造，譬如 {2 * n + 1 : n \in Nat} 就返回了一個奇數(shù)集合

函數(shù)

TLA+ 里面的函數(shù)跟我們程序里面的函數(shù)意義是不一樣的，反倒有點類似于數(shù)組，這點一定要注意。

對于函數(shù)，首先我們需要了解的是值域，我們可以認(rèn)為就是程序語言里面數(shù)組的索引集合，譬如對于 tuple（一種特殊的函數(shù)來說），DOMAIN <<"a", "b", "c">> 就是一個 1..3 的集合。

如果 f 是一個函數(shù)，而 x 是 f 值域里面的一個元素，f[x] 就表示的將 f 應(yīng)用到 x 上面。對于上面的 tuple，<<"a", "b", "c">>[2] 就會得到 "b"，而 <<"a", "b", "c">>[4] 則會報錯。

我們可以通過 [x \in S |-> e]構(gòu)造任意值域的函數(shù)，這里仍然先以 tuple 為例， tuple，一種特殊的函數(shù)，它的值域就是集合 1..n，n 為 tuple 的個數(shù)。譬如 tuple 可以寫成 [ i \in 1..3 |-> i - 7]，這個就會得到 tuple <<-6, -5, -4>>，然后我們可以使用 <<-6, -5, -4>>[1] 得到 -6 了。

我們再來看一個更通用的例子，[i \in {2, 4, 6, 8} |-> i - 42][4] ，這里我們得到的值是 4 - 42，也就是 38。

當(dāng)一個函數(shù) f 的值域在 S，并且 f[x] 在集合 T 里面，我們就可以用 [S -> T] 來表示所有這樣函數(shù)的集合。

我們也可以使用 EXCEPT 來構(gòu)造另一個函數(shù)，對于公式 [f EXCEPT ![e1] = e2] 表示新的函數(shù) f’ 等于 f 除了 f'[e1] = e2。我們也可以使用 @ 來表示 f[e1]，譬如 f' = [f EXCEPT ![e1] = f[e1] + 1 中，我們就可以寫成 f' = [f EXCEPT ![e1] = @ + 1

小結(jié)

可以看到，TLA+ 需要的數(shù)學(xué)知識其實就是最基本的四則運算，布爾代數(shù)，集合論相關(guān)的。當(dāng)然，還有很多運算符這里沒有提到，后面實際例子的時候我們繼續(xù)詳細(xì)說明。