結論から言うと、山火事問題はまだまだ荷が重い課題でした。これまでPlusCAL中心で来ていきなりTLA+の複雑な記述に挑むのは結構辛い。なので、一旦TLA+本に戻ります。Chapter 3です。送信機、受信機がval(値受け渡し用）、rdy(SYN用)、ack(ACK用）の３本の電…

前回２フェーズコミットを試した後、他の例として出てくるPaxosと、もう一つの問題（本件）がありました。PaxosはPlusCALで書かれていて記述自体はシンプルなものの、アルゴリズム自体が難しい点、pdf上にざっくりと載っているだけで、動くスペックにするの…