使用 PlusCal 語言 [tla-0001]

比起直接寫出 Spec 等不變式，先寫 PlusCal language (https://lamport.azurewebsites.net/tla/tutorial/intro.html) 的程式再使用用它生成的 Spec 不變量會更簡單也更實用。因為 TLA+ 會嘗試生成所有可能的狀態，有可能出現所謂的 unbound model (https://learntla.com/topics/unbound-models.html)，就結果而言對它進行檢查永遠不會完成。用 PlusCal 語言寫的程式相對容易發現這種錯誤。

---- MODULE plustwo ----
EXTENDS Integers

CONSTANT Limit

(* --algorithm plustwo
variables x = 0;
begin
    while x < Limit do
        x := x + 2;
    end while;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "3f62e9ff" /\ chksum(tla) = "239a9ecd")
\* END TRANSLATION
=====

由 PlusCal 產出的不變量會被包在 BEGIN TRANSLATION 到 END TRANSLATION 裡面，可以發現它還會檢查 checksum。由於這個區塊內的程式會被機器生成的內容覆蓋，因此千萬不要把自己寫的不變量放在這個區塊中。