TLA+介紹
TLA+（WIKI，官網）是一門領域特定語言，主要用於數理邏輯計算和並發系統的正確性驗證。TLA+中的TLA代表的是“行為時序邏輯（Temporal Logic of Actions）”，Action 是純函數；“+”代表“Data Logic”。這是由 Dr. Lamport所提出的學說，他也因此獲得了2013年圖靈獎。Lamport在分布式計算和並發系統領域研究40多年，發布了180多篇高價值論文，是有志於此領域的必讀材料。官網提供了大量的學習資源，另外Hillel Wayne寫了一個很棒的入門教程。
TLA+利用高中或者大學學到的一些簡單的數學知識（時序邏輯和數據邏輯），就可以發現程序中的錯誤，而這些錯誤用計算機來跑很長時間也可能不會發現。
作為一門領域特定語言，TLA+語法簡單，基礎數據對象只有Set、Tuple、Function（這並不是其他語言中的函數，可以理解成Python的Dict或Java的hashmap）幾種。剩下的語法都是數學邏輯知識，不過這也是其中最困難的部分，就是用抽象的思維來思考，用數學的方式來思考。數學本身不會讓程序運行得更有效率，但能讓程序更邏輯嚴謹。TLA+已在航空航天、微軟、亞馬遜等實際系統中起到關鍵作用。
此外，為了便於使用，Lamport開發了PlusCal語言。PlusCal語言風格與C/Pascal語言類似，對傳統語言出身的軟件工程師對更加友好。在TLA+開發集成環境（TLA+ Toolbox）中，PlusCal會自動翻譯成TLA+並運行。
本文不嘗試講解TLA+和PlusCal基礎語法和設計方法，因為這方面官網提供了語言講解、教學視頻、代碼示例、cheatsheet等等豐富資源。本文主要想通過2個示例來展示TLA+的優雅和強大，讓大家感受到TLA+的魅力所在。
TLA+應用示例
看下面這題，如果用TLA+來解題，應該該如何實現？
在電影“虎膽龍威3-紐約大劫案”中，布魯斯·威利斯和傑里米·艾恩斯遇到這樣一個難題：給他們一個3加侖小壺和一個5加侖的大壺，要求在5加侖大壺里准確裝入4加侖的水。
本質上，TLA+（行為時序邏輯）描述的是一個狀態機，每一個時序（Temporal Logic）下都是一個特定狀態（action），狀態的跳變只依賴於自身（即純函數的含義）。
本題中，狀態機初始狀態為小壺和大壺都為空；此后存在6種狀態：小壺倒空、大壺倒空、小壺倒滿、大壺倒滿、小壺倒入大壺、大壺倒入小壺，狀態機的下一個狀態必為這6個狀態中的一個。把如上分析轉化為TLA+描述（如下）：
設置不變量（invariant）：big \= 4， TLA+會遍歷所有狀態可能性，並找到答案（如下）：
START（大壺水為0加侖）->{big:0,small:0} (初始狀態)-> {big:5, small:0}（倒滿大壺）-> {big:2, small:3}（大壺導入小壺）-> {big:2, small:0}（倒空小壺）-> {big:0, small:2}（大壺倒入小壺）-> {big:5, small:2}（倒滿大壺）-> {big:4, small:3}（大壺導入小壺）->END（大壺水為4加侖）
並發系統設計正確性驗證
cache = {}
def increment(id):
x = cache.get(id, None)
if x is None:
x = database.read(id)
cache[id] = x
x = x + 1
database.write(id, x)
cache[id] = x
上面一段Python代碼，increment功能為對數據庫（database）的一個字段值加一后再存入數據庫中，為了優化數據庫的讀效率，在數據庫上加了一層緩存（cache）。
在並發環境下，這段代碼實現是有問題的，你能看的出來么？如何證明或驗證此並發程序的正確性？
把上面的python代碼轉成PlusCal描述，代碼實現如下：
所謂正確性驗證，用數學的語言描述就是保證不變性。本例的一個不變性就是要保證數據庫的一致性，換句話說，如果有N個進程並發執行increment(id)，其值應該增加N。用TLA+描述如下:
DBConsistent == (\A i \in 1..N: pc[i] = "Done") => database = N
運行可見不變量DBConsistent遭違反（如下圖），也證明了此並發程序存在bug。而且在Error-Trace中給出了違例的詳細步驟和原因：如果1個進程A已執行完(Done)時，另一個進程B執行到狀態t3，此時B進程中的x為0，但實際上數據庫（database）和cache中的值已經為1了。
