去年有個客戶請我解決一個問題：他們想把兩個大型的 TLA+ 規格組合成一個更大系統的一部分。正常來說你不應該這樣做，而是要寫一個把兩個系統都寫死在裡面的大型規格，但這些規格都非常龐大，而且各自有許多內部不變量。他們需要一種方法，能讓兩個規格獨立開發，然後以最小的成本整合起來。

這就是我想出來的解法。提醒一下：這是一個複雜的解法，目標對象是進階的 TLA+ 使用者。如果你想看溫和（非常溫和）得多的入門介紹，請參考我的網站 learntla。

範例

我們先從一個動機範例開始：一個 Worker 向 Server 發送驗證請求。如果密碼與伺服器內部的密碼相符，伺服器就回應「valid」，否則回應「invalid」。如果 Worker 收到「invalid」回應，就會進入錯誤狀態。Worker 可以從該狀態重試，並提交新的驗證請求。

Worker 和 Server 透過 request/response 共享狀態。為了增加一點複雜度，我們會再替 Server 加上內部狀態，也就是一個對 Worker 隱藏的請求紀錄（request log）。

我們可以用這個範例來說明組合時會遇到的問題，以及我的解法（不過老實說，這個範例有點太簡單，還不太值得這樣大費周章）。

組合的問題

我們想要的，是讓組合盡可能簡單、無痛。如果我們的規格是 WorkerSpec 和 ServerSpec，最簡單的組合方式就只是

CombinedSpec == WorkerSpec /\ ServerSpec

我在這裡深入談過會遇到哪些問題，但重點是，如果 ServerSpec 和 WorkerSpec 都是「一般」的規格，它們會對共享變數施加互相矛盾的限制。

舉例來說，WorkerSpec 很可能會讀取伺服器的回應，但不會去修改它。所以為了讓 WorkerSpec 能獨立於組合之外執行，我們得說回應永遠不會改變，這等同於說我們不能改變它，這又會讓 ServerSpec 無法發送回應！

常見的 workaround 是把 WorkerSpec 和 ServerSpec 拆成一堆 actions 的集合，然後再小心翼翼地以不互相矛盾的方式縫合起來。這聽起來有多複雜，做起來就有多複雜：組合兩個規格的工作量，可能跟從頭寫它們一樣多。

這就是我想找更好方法的原因。

核心想法

我們需要做的是，寫出只代表世界一部分的規格，然後再把它們整合進一個代表「整個世界」的主規格。為了做到這點，我們會用到 TLA+ 最強大的特性之一：我們可以用 x' 同時做到為 x 指派下一個值以及限制下一個值可以是什麼。假設我們有

VARIABLE x, y 

Foo == 
  /\ x' \in {0, 1}
  /\ y' \in {0, 1}

Bar == x' < y'

Next == Foo /\ Bar

當 TLC 評估 Next 時，它會把 Foo 裡的 x' 和 y' 當成指派。有四種可能的指派，所以模型檢查器會全部評估。

接著，因為 x' 和 y' 已經選定，TLC 會把 Bar 裡的陳述當成限制條件來讀。有三種可能的指派會違反這個限制，所以 TLC 會把那些可能性排除，只留下唯一一個下一個狀態。

這意味著一個規格 Q 可以拿兩個規格 X 和 Y，讓它們互相制約。X 可以有一個會遞增 x_log 的 action Inc，然後 Q 說 Inc 只有在 y_flag 為 true 時才能發生。類似地，Q 也可以讓一個指派觸發另一個：

Inc == 
  /\ x_log' = x_log + 1

Sync ==
  IF ~y_flag /\ y_flag' 
  THEN Inc 
  ELSE TRUE

Next == (X!Next \/ Y!Next) /\ Sync

現在，把 y_flag 改成 true 就會強制 x_log 遞增。Q 正在用一個規格來驅動系統中的副作用。

這其實就是狀態機！轉換上的限制條件就是 守衛條件，而轉換上的指派就是效果（effects）。這些都可以套用到狀態機本身並不知道的其他規格上。

以下是讓這個想法在實務上可行的做法：

1. 為核心元件的所有高階狀態轉換寫一個抽象狀態機
2. 把其他元件寫成「開放式」規格，不完整描述它們的下一個狀態。
3. 精煉核心元件到主規格中，並加上一個 Sync action，為狀態轉換加上守衛條件和副作用。

解法

我們會用三個獨立的規格來建模：workerSM.tla、server.tla 和 system.tla。

狀態機

因為整個系統都是圍繞著 worker 的狀態機，我們就從 workerSM.tla 開始。這個規格不會描述當 worker 轉換狀態時發生了什麼事，只會描述有哪些轉換。

------------------- MODULE workerSM -------------------
EXTENDS Integers

VARIABLES state

Transitions == {
    [from |-> "init", to |-> "ready"]
    , [from |-> "ready", to |-> "requesting"]
    , [from |-> "requesting", to |-> "done"]
    , [from |-> "requesting", to |-> "error"]
    , [from |-> "error", to |-> "ready"]
}

Init == state = "init"

Valid(t) == state = t.from
ValidTransitions == {t \in Transitions: Valid(t)}
ValidOutcomes == {t.to : t \in ValidTransitions}

Done ==
    state = "done"

Next ==
    \E t \in ValidOutcomes:
        state' = t

Fairness == 
    /\ WF_state(Next)
    /\ SF_state(state' = "done")

Spec == Init /\ [][Next]_state /\ Fairness
Liveness == <>Done

=========================================================

Transitions 代表所有合法轉換的集合。三個 Valid- 開頭的運算子只是輔助工具。加上它們是個好習慣；大多數 TLA+ 規格的輔助工具都還不夠多。

Fairness 限制條件有點複雜，但它想說的只是，我們不能永遠都從 requesting 轉到 error。如果我們夠常到達那個狀態，最終還是會轉到 done。

除此之外，這個規格對轉換沒有加任何條件：我們不需要「做任何事」就能到 done。那是 system.tla 要做的事。

SPECIFICATION Spec

PROPERTY Liveness
CHECK_DEADLOCK FALSE

接下來，是我們要與 worker 整合的外部元件。

伺服器

------------------- MODULE server -------------------
CONSTANTS Password, NULL

VARIABLE req, resp, log

internal == <<log>>             \* (a)
external == <<req, resp>>       \* (a)
vars == <<external, internal>>  \* (a)

Init == 
    /\ req = NULL
    /\ resp = NULL
    /\ log = {}

CheckRequest ==
    /\ req # NULL
    /\ log' = log \union {req}
    /\ IF req = Password THEN
         resp' = "valid"
       ELSE
         resp' = "invalid"
    /\ req' = NULL

Next == \* (b) 
  CheckRequest

Spec == Init /\ [][Next]_internal \* (c)
====

在這個規格裡，我們做了三件不尋常的事。第一，我們把變數分成 internal 和 external 兩類 (a)。external 變數代表與組合後規格的其他部分共享的狀態，而 internal 則只跟 server 自身的性質有關。在這裡，我們用 req 代表對伺服器的請求，用 resp 代表回應。

第二，這個規格會輕易 deadlock (b)。Next 裡只有 CheckRequest 這個 action，而 CheckRequest 只有在 req 不是 null 時才會啟用，但規格裡沒有任何東西會讓 req 變成非 null。這個規格不是「自給自足」的，它需要被另一個規格使用才有意義。

第三，Spec 只對 internal 變數保持 stuttering invariant。這是透過寫成 [][Next]_internal 而非 [][Next]_vars 來達成的 (c)。這是最容易被忽略的部分，但之後會讓規格的組合與精煉都變得更容易。

現在讓我們把 server 和 worker 放在一起。

系統

這是目前為止最複雜的部分。我們先從完整的規格開始，然後再逐一拆解最重要的區段。

---- MODULE system ----
EXTENDS TLC, Integers, Sequences
CONSTANT NULL
VARIABLES ws \* worker state
 , server_req \* requests to server
 , server_resp \* server response
 , server_log \* log (internal to server)

Strings == {"a", "b", "c"}

comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>

Worker == INSTANCE workerSM WITH state <- ws

Server == INSTANCE server WITH 
  req <- server_req,
  resp <- server_resp,
  log <- server_log,
  Password <- "a"

Sync ==
    LET i == <<ws, ws'>> IN
    /\ CASE
            i = <<"ready", "requesting">> ->
            /\ \E x \in Strings:
                /\ server_req' = x
            /\ server_resp' = NULL
        []  i = <<"requesting", "error">> ->
            /\ server_resp = "invalid"
            /\ UNCHANGED comm_vars
        []  i = <<"requesting", "done">> ->
            /\ server_resp = "valid"
            /\ UNCHANGED comm_vars
        [] OTHER -> UNCHANGED comm_vars

Init ==
    /\ Worker!Init
    /\ Server!Init

Done == \* No deadlock on finish
    /\ Worker!Done
    /\ UNCHANGED vars

ServerNext ==
    /\ Server!Next
    /\ UNCHANGED ws

WorkerNext ==
    /\ Worker!Next
    /\ Sync
    /\ UNCHANGED server_log

Next == 
    \/ WorkerNext
    \/ ServerNext
    \/ Done

Fairness == 
    /\ WF_vars(Next) 

Spec == Init /\ [][Next]_vars /\ Fairness 

RefinesServer == Server!Spec
RefinesWorker == Worker!Spec

====

VARIABLES ws \* worker state
 , server_req \* requests to server
 , server_resp \* server response
 , server_log \* log (internal to server)

Strings == {"a", "b", "c"}

comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>

我喜歡依用途和規格來分組 vars。因為 server 和 worker 都會用到 server_req 和 _resp，所以我把它們另外放進 comm_vars 這個群組。

Worker == INSTANCE workerSM WITH state <- ws

Server == INSTANCE server WITH 
  req <- server_req,
  resp <- server_resp,
  log <- server_log,
  Password <- "a"

為了教學方便，我把 server 的 Password 常數寫死了。我們不需要實例化 NULL 常數，因為它在 system.tla 和 server.tla 裡名稱相同，所以會自動帶入。

Sync ==
  \* See next section

Init ==
    /\ Worker!Init
    /\ Server!Init

ServerNext ==
    /\ Server!Next
    /\ UNCHANGED ws

WorkerNext ==
    /\ Worker!Next
    /\ Sync
    /\ UNCHANGED server_log

Done == \* No deadlock on finish
    /\ Worker!Done
    /\ UNCHANGED vars

Next == 
    \/ WorkerNext
    \/ ServerNext
    \/ Done

• Init 只是分別呼叫 Worker!Init 和 Server!Init 來設定各自的變數。這裡很簡單，因為它們沒有共享任何變數。如果有兩者共用的東西，或是 system 需要額外的帳務變數，我會在這裡特別處理。

• ServerNext 只是說「server 可以自己處理自己的狀態更新」，但也考慮了 ws 的 stuttering（因為每個變數在每一步都需要被賦值）。server 在系統中是獨立運作的，它的行為不會同步依賴於 worker。在組合時，並不總是能讓元件保持分離，但在可行的情況下，這樣會更方便。

• WorkerNext 也是一樣：它的行為獨立於 ServerNext。但「system」開始發揮作用的地方，就在 Sync。

Sync

Sync 是事情變得有趣的地方。

Sync ==
    LET i == <<ws, ws'>> IN
    CASE
          i = <<"ready", "requesting">> ->
          /\ \E x \in Strings:
              server_req' = x
          /\ server_resp' = NULL
      []  i = <<"requesting", "error">> ->
          /\ server_resp = "invalid"
          /\ UNCHANGED comm_vars
      []  i = <<"requesting", "done">> ->
          /\ server_resp = "valid"
          /\ UNCHANGED comm_vars
      [] OTHER -> UNCHANGED comm_vars

回顧一下前面的說明，帶撇號的變數在被指派後，還可以在其他運算式中被使用。這表示我們可以在一個 action 中嘗試一個轉換，然後在後面的 action 中檢查這個轉換是否合法。這就是讓這一切可行的關鍵。如果沒有這一點，我們就得把守衛條件和副作用跟轉換放在同一個 action 裡。例如，在這一行：

      []  i = <<"requesting", "error">> ->
          /\ server_resp = "invalid"
          /\ UNCHANGED comm_vars

我們是把 requesting -> error 這個轉換限制為只有在伺服器回應是「invalid」時才可能發生。這只有在 Server!Next 拒絕密碼時才會成立。但我們的 worker 根本不需要知道這件事。我們可以獨立開發它們，然後靠 Sync 來正確地組合它們的行為。

我們也可以用這個來驅動系統中的效果：

      []  i = <<"ready", "requesting">> ->
          /\ \E x \in Strings:
              server_req' = x
          /\ server_resp' = NULL

這會讓 ready -> requesting 的轉換同時觸發一個請求（並清除任何尚未處理的回應）。接著這會啟用 Server!CheckRequest，進而啟用 ServerNext，讓 server 能對系統做出反應。

精煉

記得，我們一開始加上這麼多機制，就是為了把兩個複雜的規格組合在一起。我們需要確保組合的方式不會違反它們各自的性質。這就靠這幾行來處理：

RefinesServer == Server!Spec
RefinesWorker == Worker!Spec

這些是精煉性質。簡單來說，它們會檢查 system.tla 有沒有讓 Server 或 Worker 做出它們原本做不到的事。舉例來說，如果我們從 log 裡刪掉東西，這個性質就會失敗，因為在 Server!Spec 裡這是不可能發生的。¹

在 TLA+ 中，精煉是可遞的。workerSM.tla 有一個活性性質 <>Done。因為我已經在 workerSM.cfg 中驗證過它，就不需要在 system.tla 中再測試一次。如果 RefinesWorker 通過，那麼 Worker!Liveness 也保證會通過！

Spec => Worker!Spec 
(S)     (WS)

Worker!Spec => Worker!Liveness (2)
(WS)           (WL)

而目前它是失敗的：

SPECIFICATION  Spec

CONSTANTS
  NULL = NULL

PROPERTY
    RefinesServer
    RefinesWorker

問題在於 worker 可能一直選錯密碼，所以 server 一直拒絕，worker 永遠無法完成。一個修正方式是規定系統不會重試同一個密碼：

Sync ==
   \* ...
           /\ \E x \in Strings:
               /\ x \notin server_log
               /\ server_req' = x

這樣就能讓規格通過。如果你擔心把 server 的內部 log 洩漏給 system，也可以幫 worker 加上一個 log，不管是在 system.tla 裡，還是作為一個獨立元件一起放進 Sync 都可以。² 另一種修正方式是使用強公平性限制：

Sync ==
   \* ...
           /\ \E x \in Strings:
               /\ server_req' = x

Fairness == 
   /\ WF_vars(Next) 
   /\ SF_vars(WorkerNext /\ server_req' = "a")

這表示，如果「以發送正確密碼的方式執行 WorkerNext」這件事一直是終將可能發生的，那麼規格最終就會這麼做。這能在不改變系統核心邏輯的情況下讓規格通過。

封閉開放世界

還有一件事要做：讓 server.tla 能被模型檢查。我們無法直接測試它，因為它不是一個「封閉」規格：它依賴其他規格來發送請求。對於更複雜的規格，我們會希望能獨立於組合之外測試該規格的性質。

幸好，這在 TLA+ 社群中已經是個「已解決的問題」：把開放規格精煉成封閉規格。我們用一個新檔案 MCserver.tla 來做這件事：

---- MODULE MCserver ----
EXTENDS TLC, server

Strings == {"a", "b", "c"}
ASSUME Password \in Strings

MCInit == Init

WorldNext ==
    /\ \E x \in Strings:
        req' = x
    /\ UNCHANGED <<log, resp>>

MCNext ==
    \/ Next
    \/ WorldNext

MCSpec == MCInit /\ [][MCNext]_vars
====

這用一個可以發送請求的外部 World 來擴充 server。現在我們就可以透過對 MCserver.tla 做模型檢查來測試 server.tla 的行為。

SPECIFICATION MCSpec
CONSTANT 
    NULL = NULL
    Password = "b"

如果你使用的是 VSCode TLA+ 擴充套件的 nightly 版，在 server.tla 上執行「Check model with TLC」指令時，就會自動用 MCserver.tla 來跑模型檢查。它還附帶 TLA+ 除錯器。VSCode 擴充套件很棒。

優點與缺點

這要做很多事！那為什麼要這樣做，而不是直接寫一個大型規格就好？

會想組合規格，重點就是為了能獨立作業。當每個規格只有大約 30 行時，這沒什麼大不了，但當每個都超過 200 行時，你就沒辦法輕易把它們重寫成一個規格。

所以讓我們把它跟更傳統的組合方式比較一下。我會用 MongoDB Raft composition 為例，這是 Murat Demirbas 在這裡分析的案例。獨立的規格是 MongoStaticRaft 和 MongoLoglessDynamicRaft，它們在 MongoRaftReconfig 中被組合在一起。MongoStaticRaft 的 Next 長這樣：

\* MongoStaticRaft

Next == 
    \* (a)
    \/ \E s \in Server : ClientRequest(s)
    \* etc
    \* (b)
    \/ \E s \in Server : \E Q \in Quorums(config[s]) : BecomeLeader(s, Q)
    \* etc

而組合後的 Next 長這樣：

\* MongoRaftReconfig
Next == 
    \/ OSMNext /\ UNCHANGED csmVars
    \/ CSMNext /\ UNCHANGED osmVars
    \/ JointNext

OSMNext == 
    \* (a)
    \/ \E s \in Server : OSM!ClientRequest(s)
    \* etc

JointNext == 
    \* (b)
    \/ \E i \in Server : \E Q \in Quorums(config[i]) : 
        /\ OSM!BecomeLeader(i, Q)
        /\ CSM!BecomeLeader(i, Q)
    \* etc

在 (a) 底下的 actions 必須在 OSMNext 中手動重複一次，而在 (b) 底下的 actions 則必須在 JointNext 底下與另一個規格小心地交織在一起。這是組合兩個規格的標準做法，需要整合的規格越多，就會變得越困難。在這種典範下，也很難檢查精煉。

我試著用以 Sync 為基礎的方法來避開這兩個問題。每個元件本來就有自己的 Next，我們可以直接拿來用，不用改。任何會影響共享變數的部分，都由額外的 Sync 運算子來處理。

這個規格用我的方法會比較好嗎？我不知道。我設計這個方法是為了讓一個主要的「機器」與外部元件互動，而在這裡，兩個規格是平起平坐的。我有一個轉換後大概會長怎樣的草圖，但我也不確定這樣是否一定比較好。

Next == 
    \/ OSMNext
    \/ CSMNext

OSMNext ==
    /\ OSM!Next
    /\ UNCHANGED <<csmVars>>
    /\ UNCHANGED <<sharedVars>> \* new op

CSMNext ==
    /\ CSM!Next
    /\ Sync
    /\ UNCHANGED <<osmVars>>

Sync ==
    \/ \E i \in Server : \E Q \in Quorums(config[i]) : 
        /\ OSM!BecomeLeader(i, Q)
        /\ CSM!BecomeLeader(i, Q)
    \/ \* ...
    \/ UNCHANGED <<sharedVars>>

我的預測是，傳統的組合方式適用於更廣泛的情境，但在它適用的情境中，Sync 更易於維護、也更具擴充性。

兩種方法都沒辦法很好地處理「一對多」的情況。也就是你有一個單一 worker 的規格，卻想用它來加入 N 個 worker，其中 N 是一個模型參數。我在文章 Using Abstract Data Types in TLA+ 中討論過為什麼這會這麼困難。

結論

這是一個強大的技巧，但也需要經驗、會增加複雜度。如果你需要寫一個非常龐大的規格，或是需要一個可重複使用元件的函式庫，它就很適合。對於較小的規格，我會建議用標準做法，把所有元件放在同一個規格裡就好。

這個技巧是為一位顧問客戶開發的，而且效果非常好。我很興奮能跟大家分享！如果你喜歡這篇，可以在這裡閱讀其他進階的 TLA+ 技巧，例如如何讓模型檢查更快。

感謝 Murat Demirbas 和 Andrew Helwer 提供的回饋。如果你喜歡這篇文章，歡迎訂閱我的電子報！我每週都會在那裡發表新文章。

我為企業提供形式化方法培訓，讓軟體開發更快、更便宜、更安全。歡迎在此了解更多。

附錄：不使用撇號的 Sync

有些公司的風格指南禁止在後續的 action 中把帶撇號的變數當成運算式使用。在這種情況下，你可以用這種方式達到同樣的效果：

-Sync ==
-   LET i == <<ws, ws'>> IN
+Sync(t) ==
+   LET i == <<t.from, t.to>> IN

+Do(t) ==
+    /\ ws = t.from
+    /\ ws' = t.to  

WorkerNext ==
-   /\ Worker!Next
-   /\ Sync
+   /\ \E t \in Worker!ValidTransitions:
+       /\ Do(t)
+       /\ Sync(t)
    /\ UNCHANGED server_log

Do(t) 實際上只是在模擬 Worker!Next 的行為，差別在於它讓我們可以「儲存」所使用的轉換，並把它傳進 Sync。

這對於保留傳進 action 的參數也很有用，而這在組合時有時是必要的。

1. 這就是為什麼我們需要把 Server!Spec 寫成 [][Next]_internal 而不是 [][Next]_vars。Server!Next 只需要對內部變數成立，而不是對共享變數！[返回]
2. 我本來寫了一長段關於透過多層精煉來組合的內容：system.tla 精煉 worker.tla，而 worker.tla 再精煉 workerSM.tla。但最後發現要講清楚太複雜了。也許之後會寫成續集！[返回]