形式仕様なんてどれもクソだが
クソ未満の非形式仕様が溢れかえっている喜劇

>>271
ミューテックスとセマフォの違いって排他制御の「実装」レベルの話なんじゃ
例えばデッドロックを回避する機構を入れたいなら
そういうコードを書かなきゃいけない
ミューテックスの一般的と言えるような実装がない以上
promelaでの一般的な記述もないような

余計なお世話かも知れんが
モデル検査は排他制御のあるシステムの検証には適しているといえるけど
それは排他制御を抽象化しての話
排他制御自体の検証には向いていないと思う