tlaplus

無法對分散式protocol做單元測試，但可以做模型檢驗

分散式缺陷在部署後修復成本高昂。模型檢驗能讓你在寫下第一行實作程式碼之前就發現它們。以下是如何使用 TLA+ 做到這一點。

你無法對分散式protocol做單元測試。單元測試在一台機器上以單一順序執行一個程序。而你的protocol在五台機器上以十個程序、以你無法控制的順序執行。這兩種現實之間的鴻溝，正是缺陷藏身之處。…