TLA+本、CHAPTER 3
結論から言うと、山火事問題はまだまだ荷が重い課題でした。これまでPlusCAL中心で来ていきなりTLA+の複雑な記述に挑むのは結構辛い。
なので、一旦TLA+本に戻ります。Chapter 3です。
送信機、受信機がval(値受け渡し用)、rdy(SYN用)、ack(ACK用)の3本の電線でつながってるとして、送信機はvalに値を入れると同時にrdy(0/1)の値をflipし、受信機がackの値(0/1)をflipしてrdyとackがおなじになったら、送信機は次の値を送れる、というシステムの記述です。言葉だけだとわかりにくいですが、テキストを読めば単純。
前置きとして、どのレベルまで抽象化すべきかは経験で学んでいくしか無いから頑張ってね、とランポート先生のありがたいお言葉。
3.1 The First Specification<執筆中>